1: %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
2: %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
3: %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
4:
5: % strong normalization
6:
7: %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
8: %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
9: %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
10:
11: \section{Strong normalization}
12: \label{sec-sn}
13:
14: Typed $\la$-calculi are generally proved strongly normalizing by using
15: Tait and Girard's technique of {\em reducibility candidates}
16: \cite{girard88book}. The idea of Tait, later extended by Girard to the
17: polymorphic $\la$-calculus, is to strengthen the induction
18: hypothesis. Instead of proving that every term is strongly
19: normalizable (set $\SN$), one associates to every type $T$ a set
20: $\I{T}\sle\SN$, the {\em interpretation} of $T$, and proves that every
21: term $t$ of type $T$ is {\em computable}, {\em i.e.} belongs to
22: $\I{T}$. Hereafter, we follow the proof given in \cite{blanqui03short}
23: which greatly simplifies the one given in \cite{blanqui01thesis}.
24:
25: %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
26: % reducibility candidates
27: %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
28:
29: \begin{dfn}[Reducibility candidates]
30: A term $t$ is {\em neutral} if it is not an abstraction, not of the
31: form $c\vt$ with $c:(\vy:\vU)C\vv$ and $C$ constant, nor of the form
32: $f\vt$ with $f$ defined and $|\vt|<\at_f$. We inductively define the
33: complete lattice $\cR_t$ of the interpretations for the terms of type
34: $t$, the ordering $\le_t$ on $\cR_t$, and the greatest element
35: $\top_t\in\cR_t$ as follows.
36:
37: \begin{lst}{--}
38: \item $\cR_t=\{\vide\}$, $\le_t=\sle$ and $\top_t=\vide$ if $t\neq\B$
39: and $\G\not\th t:\B$.
40:
41: \item $\cR_s$ is the set of subsets $R\sle\cT$ such that:
42: \begin{bfenumii}{R}
43: \item $R\sle\SN$ (strong normalization).
44: \item If $t\in R$ then $\a\!\!(t)=\{t'~|~t\a t'\}\sle R$ (stability by
45: reduction).
46: \item If $t$ is neutral and $\a\!\!(t)\sle R$ then $t\in R$ (neutral terms).
47: \end{bfenumii}
48: Furthermore, $\le_s=\sle$ and $\top_s=\SN$.
49:
50: \item $\cR_{(x:U)K}$ is the set of functions $R$ from $\cT\times\cR_U$
51: to $\cR_K$ such that $R(u,S)=R(u',S)$ whenever $u\a u'$,
52: $R\le_{(x:U)K} R'$ iff, for all $(u,S)\in\cT\times\cR_U$, $R(u,S)\le_K
53: R'(u,S)$, and $\top_{(x:U)K}(u,S)=\top_K$.
54: \end{lst}
55: \end{dfn}
56:
57: Note that $\cR_t=\cR_{t'}$ whenever $t\a t'$ and that, for all
58: $R\in\cR_s$, $\cX\sle R$.
59:
60: %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
61: % interpretation schema
62: %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
63:
64: \begin{dfn}[Interpretation schema]
65: \label{def-schema-int}
66:
67: A {\em candidate assignment} is a function $\xi$ from $\cX$ to
68: $\bigcup \,\{\cR_t ~|~ t\in\cT\}$. An assignment $\xi$ {\em validates}
69: an environment $\G$, written $\xi\models\G$, if, for all
70: $x\in\dom(\G)$, $x\xi\in \cR_{x\G}$. An {\em interpretation} for a
71: symbol $f$ is an element of $\cR_\tf$. An {\em interpretation} for a
72: set $\cG$ of symbols is a function which, to each symbol $g\in\cG$,
73: associates an interpretation for $g$.
74:
75: The {\em interpretation} of $t$ w.r.t. a candidate assignment $\xi$,
76: an interpretation $I$ for $\cF$ and a substitution $\t$, is defined by
77: induction on $t$ as follows.
78:
79: \begin{lst}{\bu}
80: \item $\I{t}^I_{\xi,\t}= \top_t$ if $t$ is an object or a sort,
81: \item $\I{x}^I_{\xi,\t}= x\xi$,
82: \item $\I{f}^I_{\xi,\t}= I_f$,
83: \item $\I{(x:U)V}^I_{\xi,\t}= \{t\in\cT~|~ \all u\in\I{U}^I_{\xi,\t},
84: \all S\in\cR_U, tu\in\I{V}^I_{\xi_x^S,\t_x^u}\}$,
85: \item $\I{[x:U]v}^I_{\xi,\t}(u,S)= \I{v}^I_{\xi_x^S,\t_x^u}$,
86: \item $\I{tu}^I_{\xi,\t}= \I{t}^I_{\xi,\t}(u\t,\I{u}^I_{\xi,\t})$,
87: \end{lst}
88:
89: \noindent
90: where $\xi_x^S=\xi\cup\xS$ and $\t_x^u=\t\cup\xu$. A substitution $\t$
91: is {\em adapted} to a $\G$-assignment $\xi$ if $\dom(\t)\sle\dom(\G)$
92: and, for all $x\in\dom(\t)$, $x\t\in \I{x\G}^I_{\xi,\t}$. A pair
93: $(\xi,\t)$ is {\em $\G$-valid}, written $\xi,\t\models\G$, if
94: $\xi\models\G$ and $\t$ is adapted to $\xi$.
95: \end{dfn}
96:
97: %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
98: % conditions
99: %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
100:
101: Note that $\I{t}_{\xi,\t}^I= \I{t}_{\xi',\t'}^{I'}$ whenever $\xi$ and
102: $\xi'$ agree on the predicate variables free in $t$, $\t$ and $\t'$
103: agree on the variables free in $t$, and $I$ and $I'$ agree on the
104: symbols occurring in $t$. The difficult point is then to define an
105: interpretation for predicate symbols and to prove that every symbol
106: $f$ is computable ({\em i.e.} $f\in\I{\tf}$).
107:
108: %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
109: % interpretation of constant predicate symbols
110: %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
111:
112: Following previous works on inductive types
113: \cite{mendler87thesis,werner94thesis}, the interpretation of a
114: constant predicate symbol $C$ is defined as the least fixpoint of a
115: monotone function $I\mapsto\vphi_C^I$ on the complete lattice
116: $\cR_\tC$. Following Matthes \cite{matthes98thesis}, there is
117: essentially two possible definitions that we illustrate by the case of
118: $nat$. The {\em introduction-based} definition:
119:
120: \begin{center}
121: $\vphi_{nat}^I= \{t\in\SN~|~ t\a^* su\A u\in I\}$
122: \end{center}
123:
124: \noindent
125: and the {\em elimination-based} definition:
126:
127: \begin{center}
128: $\vphi_{nat}^I= \{t\in\cT~|~ \all (\xi,\t)\, \G\mbox{-valid},\,
129: rec~P\t~u\t~v\t~t\in\I{Pn}^I_{\xi,\t_n^t}\}$
130: \end{center}
131:
132: \noindent
133: where $\G=P:nat\A\st,u:P0,v:(n:nat)Pn\A P(sn)$. In both cases, the
134: monotonicity of $\vphi_{nat}$ is ensured by the fact that $nat$ occurs
135: only positively\footnote{$X$ occurs positively in $Y\A X$ and
136: negatively in $X\A Y$. In Section \ref{sec-indrec}, we give an
137: extended definition of positivity for dealing with inductive-recursive
138: types \cite{dybjer00jsl}.} in the types of the arguments of its
139: constructors, a common condition for inductive types.\footnote{Mendler
140: proved that recursors for negative types are not normalizing
141: \cite{mendler87thesis}. Take for instance an inductive type $C$ with a
142: constructor $c:(C\a nat)\a C$. Assume now that we have $p:C\a (C\a
143: nat)$ defined by the rule $p(cx)\a x$ (case analysis). Then, by taking
144: $\w= [x:C](px)x$, we get $\w(c\w)\ab p(c\w)(c\w)\a \w(c\w)\ab
145: \ldots$}.
146:
147: In \cite{blanqui01thesis}, we used the introduction-based approach
148: since this allows us to have non-free constructors and
149: pattern-matching on defined symbols, which is forbidden in CIC and
150: does not seem possible with the elimination-based approach. Indeed, in
151: CAC, it is possible to formalize the type $int$ of integers by taking
152: the symbols $0:int$, $s:int\A int$ and $p:int\A int$, together with
153: the rules:
154:
155: \begin{rewc}
156: s~(p~x) & x\\
157: p~(s~x) & x\\
158: \end{rewc}
159:
160: It is also possible to have the following rule on natural numbers:
161:
162: \begin{rewc}
163: x\times(y+z) & (x\times y)+(x\times z)\\
164: \end{rewc}
165:
166: \newcommand{\acc}{\mr{Acc}}
167:
168: To this end, we extended the notion of constructor by considering as
169: {\em constructor} any symbol $c$ whose output type is a constant
170: predicate symbol $C$ (perhaps applied to some arguments). Then, the
171: arguments of $c$ that can be used to define the result of a function
172: are restricted to the arguments, called {\em accessible}, in the type
173: of which $C$ occurs only positively. We denote by $\acc(c)$ the set of
174: accessible arguments of $c$. For instance, $x$ is accessible in $sx$
175: since $nat$ occurs only positively in the type of $x$. But, we also
176: have $x$ and $y$ accessible in $x+y$ since $nat$ occurs only
177: positively in the types of $x$ and $y$. So, $+$ can be seen as a
178: constructor too.
179:
180: With this approach, we can safely take:
181:
182: \begin{center}
183: $\vphi_{nat}^I= \{t\in\SN~|~ \all f, t\a^* f\vu\A \all j\in \acc(f),
184: u_j\in \I{U_j}^I_{\xi,\t}\}$
185: \end{center}
186:
187: \noindent
188: where $f:(\vy:\vU)C\vv$ and $\t=\vyu$, whenever an appropriate
189: assignment $\xi$ for the predicate variables of $U_j$ can be defined,
190: which is possible only if the condition (I6) is satisfied (see the
191: type $\fin$ in Section \ref{sec-intro}).
192: