]> matita.cs.unibo.it Git - helm.git/blob - helm/papers/system_T/t.tex
Definition of system T.
[helm.git] / helm / papers / system_T / t.tex
1 \documentclass[a4paper]{article}
2 \pagestyle{headings}
3 %\usepackage{graphicx}
4 \usepackage{amssymb,amsmath,mathrsfs,stmaryrd,amsthm}
5 %\usepackage{hyperref}
6 %\usepackage{picins}
7
8 \newcommand{\semT}[1]{\ensuremath{\llbracket #1 \rrbracket}}
9 \newcommand{\sem}[1]{\llbracket \ensuremath{#1} \rrbracket}
10 \newcommand{\pair}[2]{<\!#1,#2\!>}
11 \newcommand{\canonical}{\bot}
12 \newcommand{\R}{\;\mathscr{R}\;}
13 \newcommand{\N}{\,\mathbb{N}\,}
14 \newcommand{\B}{\,\mathbb{B}\,}
15 \newcommand{\NT}{\,\mathbb{N}\,}
16 \newcommand{\NH}{\,\mathbb{N}\,}
17 \renewcommand{\star}{\ast}
18 \renewcommand{\vec}{\overrightarrow}
19 \newcommand{\one}{{\bf 1}}
20 \newcommand{\mult}{\cdot}
21 \newcommand{\ind}{Ind(X)}
22 \newcommand{\Xind}{\ensuremath{X_{ind}}}
23 \renewcommand{\|}{\ensuremath{\quad | \quad}}
24 \newcommand{\triUP}{\ensuremath{\Delta}}
25 \newcommand{\triDOWN}{\ensuremath{\nabla}}
26 \newcommand{\Rx}{\ensuremath{R_X}}
27
28 \newtheorem{thm}{Theorem}[subsection]
29
30 \title{Modified Realizability and Inductive Types}
31 \author{...}
32
33
34 \begin{document}
35 \maketitle
36
37 \begin{abstract}
38 ...
39 \end{abstract}
40
41 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
42 \section{Introduction}
43 The characterization of the provable recursive functions of 
44 Peano Arithmetic as the terms of system T is a well known
45 result of G\"odel \cite{Godel58,Godel90}. Although several authors acknowledge 
46 that the functional interpretation of the Dialectica paper
47 is not among the major achievements of the author (see e.g. \cite{Girard87}), 
48 the result has been extensively investigated and there is a wide 
49 literature on the 
50 topic (see e.g. \cite{Troelstra,HS86,Girard87}, just to mention textbooks,
51 and the bibliography therein). 
52
53 A different, more neglected, but for many respects much more 
54 direct relation between Peano (or Heyting) Arithmetics and 
55 G\"odel System T is provided
56 by the so called {\em modified realizability}. Modified realizability
57 was first introduced by Kreisel in \cite{Kreisel59} - although it will take you
58 a bit of effort to recognize it in the few lines of paragraph 3.52 -
59 and later in \cite{Kreisel62} under the name of generalized realizability.
60 The name of modified realizability seems to be due to Troelstra 
61 \cite{Troelstra}
62 - who contested Kreisel's name but unfortunately failed in proposing 
63 a valid alternative; we shall reluctantly adopt this latter name 
64 to avoid further confusion. Modified realizability is a typed variant of 
65 realizability, essentially providing interpretations 
66 of $HA^{\omega}$ into itself: each theorem is realized by a typed function
67 of system T, that also gives the actual computational content extracted 
68 from the proof. 
69 In spite of the simplicity and the elegance of the proof, it is extremely
70 difficult to find a modern discussion of this result; the most recent
71 exposition we are aware of is in the encyclopedic work by
72 Troelstra \cite{Troelstra} (pp.213-229) going back to thirty years ago. 
73 Even modern introductory books
74 to Type Theory and Proof Theory devoting much space to system T
75 such as \cite{GLT} and \cite{TS} surprisingly leave out this simple and 
76 illuminating result. Both the previous textbooks
77 prefer to focus on higher order arithmetics and its relation with 
78 Girard's System $F$ \cite{Girard86}, but the technical complexity and
79 the didactical value of the two proofs is not comparable: when you 
80 prove that the Induction Principle is realized by the recursor $R$ 
81 of system $T$ you catch a sudden gleam of understanding in the 
82 students eyes; usually, the same does not happen when you show, say, 
83 that the ``forgetful'' interpretation of the higher order predicate defining
84 the natural numbers is the system $F$ encoding 
85 $\forall X.(X\to X) \to X \to X$ of $\N$. 
86 Moreover, after a first period of enthusiasm, the impredicative 
87 encoding of inductive types in Logical Frameworks has shown several 
88 problems and limitations (see e.g. \cite{Werner} pp.24-25) mostly
89 solved by assuming inductive types as a primitive logical notion
90 (leading e.g. form the Calculus of Constructions to the Calculus
91 of Inductive Constructions - CIC). Even the extraction algorithm of
92 CIC, strictly based on realizability principles, and in a first time
93 still oriented towards System F \cite{Paulin87,Paulin89} has been 
94 recently rewritten \cite{Letouzey04}
95 to take advantage of concrete types and pattern matching of ML-like
96 languages. Unfortunately, systems like the Calculus of Inductive 
97 Constructions are so complex, from the logical point of view, to 
98 substantially prevent a really neat theoretical exposition (at present, 
99 it does not
100 even exists a truly complete consistency proofs covering all aspects
101 of such systems); moreover, not everybody may be interested in all the features
102 offered by these frameworks, from polymorphism to types depending on 
103 proofs. Our program is to restart the analysis of logical systems with
104 primitive inductive types in a smooth way, starting form first order
105 logic and adding little by little small bits of logical power.
106 This paper is the first step in this direction.
107
108 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
109 \section{G\"odel system T}
110 We shall use a variant of system T with three atomic types $\N$ (natural 
111 numbers), $\B$ (booleans) and $\one$ (a terminal object), and two binary
112 type constructors $\times$ (product) and $\to$ (arrow type).
113
114 The terms of the language comprise the usual simply typed lambda terms 
115 with explicit pairs, plus the following additional constants:
116 \begin{itemize}
117 \item $*:\one$, 
118 \item $true: \B$, $false:\B$, $D:A\to A \to \B \to A$ 
119 \item $O:\N$, $S:\N \to \N$, $R:A \to (A \to \N \to A) \to \N \to A$,
120 \end{itemize}
121 Redexes comprise $\beta$-reduction
122 \[(\beta)\;\; \lambda x:U.M \; N \leadsto M[N/x]\]
123 projections
124
125 \[(\pi_1)\;\;fst \pair{M}{N} \leadsto M\\ \hspace{.6cm} (\pi_2)\;\; snd \pair{M}{N} 
126 \leadsto N \] 
127 and the following type specific reductions:
128 \[(D_{true})\;\;\\D\;M\;N\; true \leadsto M  \hspace{.6cm} 
129   (D_{false})\;\;  D\;M\;N\;false \leadsto N \] 
130 \[(R_0)\;\;\\R\;M\;F\; 0 \leadsto M  \hspace{.6cm} 
131   (R_S)\;\;  R\;M\;F\;(S\;n) \leadsto F\;n\;(R\;M\;F\;n) \] 
132 \[(*)\;\; M \leadsto * \]
133 where (*) holds for any $M$ of type $\one$.
134
135 Note that using the well known isomorpshims 
136 $\one \to A \cong A$, $A \to \one \cong \one$
137 and $A \times \one \cong A \cong \one\times A$ (see \cite{AL91}, pp.231-239)
138 we may always get rid of $\one$ (apart the trivial case).
139 The terminal object does not play a major role in our treatment, but 
140 it allows to extract better algorithms. In particular we use it 
141 to realize atomic proposition, and stripping out the terminal object using 
142 the above isomorphisms gives a simple way of just keeping the truly 
143 informative part of the algorithms.
144
145
146
147 \section{Heyting's arithmetics}
148
149 {\bf Axioms}
150
151 \begin{itemize}
152 \item $nat\_ind: P(0) \to (\forall x.P(x) \to P(S(x))) \to \forall x.P(x)$ 
153 \item $ex\_ind: (\forall x.P(x) \to Q) \to \exists x.P(x) \to Q$
154 \item $ex\_intro: \forall x.(P \to \exists x.P)$
155 \item $fst: P \land Q \to P$
156 \item $snd: P \land Q \to Q$
157 \item $conj: P \to Q \to P \land Q$
158 \item $false\_ind: \bot \to Q$
159 \item $discriminate:\forall x.0 = S(x) \to \bot$
160 \item $injS: \forall x,y.S(x) = S(y) \to x=y$
161 \item $plus\_O:\forall x.x+0=x$
162 \item $plus\_S:\forall x,y.x+S(y)=S(x+y)$ 
163 \item $times\_O:\forall x.x\mult0=0$
164 \item $times\_S:\forall x,y.x\mult S(y)=x+(x\mult y)$ 
165 \end{itemize}
166
167 \noindent
168 {\bf Inference Rules}
169
170 say that ax:AX refers to the previous Axioms list...
171
172 \[
173   (Proj)\hspace{0.2cm} \Gamma, x:A, \Delta \vdash x:A
174   \hspace{2cm}
175   (Const)\hspace{0.2cm} \Gamma \vdash ax : AX
176 \]
177
178 \[ 
179    (\to_i)\hspace{0.2cm}\frac{\Gamma,x:A \vdash M:Q}{\Gamma \vdash \lambda x:A.M: A \to Q} \hspace{2cm}
180    (\to_e)\hspace{0.2cm}\frac{\Gamma \vdash M: A \to Q \hspace{1cm}\Gamma \vdash N: A}
181     {\Gamma \vdash M N: Q} 
182 \]
183
184 %\[ 
185 %   (\land_i)\frac{\Gamma \vdash M:A \hspace{1cm}\Gamma \vdash N:B}
186 %   {\Gamma \vdash \pair{M}{N} : A \land B} 
187 %\hspace{2cm}
188 %   (\land_{el})\frac{\Gamma \vdash A \land B}{\Gamma \vdash A}
189 %\hspace{2cm}
190 %   (\land_{er})\frac{\Gamma \vdash A \land B}{\Gamma \vdash B}  
191 %\]
192
193 \[ 
194    (\forall_i)\hspace{0.2cm}\frac{\Gamma \vdash M:P}{\Gamma \vdash 
195    \lambda x:\N.M: \forall x.P}(*) \hspace{2cm}
196    (\forall_e)\hspace{0.2cm}\frac{\Gamma \vdash M :\forall x.P}{\Gamma \vdash M t: P[t/x]} 
197 \]
198
199
200 %\[ 
201 %   (\exists_i)\frac{\Gamma \vdash P[t/x]}{\Gamma \vdash \exists x.P}\hspace{2cm}
202 %   (\exists_e)\frac{\Gamma \vdash \exists x.P\hspace{1cm}\Gamma \vdash \forall x.P \to Q}
203 %{\Gamma \vdash Q} 
204 %\]
205
206 \section{Extraction}
207
208 The formulae to types translation function 
209 $\sem{\cdot}$ takes in input formulae in HA and returns types in T.
210
211 \begin{enumerate}
212 \item $\sem{A} = \one$ if A is atomic
213 \item $\sem{A \land B} = \sem{A}\times \sem{B}$
214 \item $\sem{A \to B} = \sem{A}\to \sem{B}$
215 \item $\sem{\forall x:\N.P} = \N \to \sem{P}$
216 \item $\sem{\exists x:\N.P} = \N \times \sem{P}$
217 \end{enumerate}
218
219 definition.
220 For any type T of system T $\canonical_T: \one \to T$  is inductively defined as follows:
221 \begin{enumerate}
222 \item $\canonical_\one = \lambda x:\one.x$
223 \item $\canonical_N = \lambda x:\one.0$
224 \item $\canonical_{U\times V} = \lambda x:\one.\pair{\canonical_{U} x}{\canonical_{V} x}$
225 \item $\canonical_{U\to V} = \lambda x:\one.\lambda \_:U. \canonical_{V} x$
226 \end{enumerate}
227
228 \begin{itemize}
229 \item $\sem{nat\_ind} = R$
230 \item $\sem{ex\_ind} = (\lambda f:(\N \to \sem{P} \to \sem{Q}).
231 \lambda p:\N\times \sem{P}.f (fst \,p) (snd \,p)$. 
232 \item $\sem{ex\_intro} = \lambda x:\N.\lambda f:\sem{P}.\pair{x}{f}$
233 \item $\sem{fst} = \pi_1$
234 \item $\sem{snd} = \pi_2$
235 \item $\sem{conj} = \lambda x:\sem{P}.\lambda y:\sem{Q}.\pair{x}{y}$
236 \item $\sem{false\_ind} = \canonical_{\sem{Q}}$
237 \item $\sem{discriminate} = \lambda \_:\N.\lambda \_:\one.\star$
238 \item $\sem{injS}= \lambda \_:\N. \lambda \_:\N.\lambda \_:\one.\star$
239 \item $\sem{plus\_O} = \sem{times\_O} = \lambda \_:\N.\star$
240 \item $\sem{plus\_S} = \sem{times_S} = \lambda \_:\N. \lambda \_:\N.\star$
241 \end{itemize}
242
243 In the case of structured proofs:
244 \begin{itemize}
245 \item $\semT{M N} = \semT{M} \semT{N}$
246 \item $\semT{\lambda x:A.M} = \lambda x:\sem{A}.\semT{M}$
247 \item $\semT{\lambda x:\N.M} = \lambda x:\N.\semT{M}$
248 \item $\semT{M t} = \semT{M} \semT{t}$
249 \end{itemize}
250
251 \section{Realizability}
252 The realizability relation is a relation $f \R P$ where $f: \sem{P}$, and
253 $P$ is a closed formula.
254 In particular:
255 \begin{itemize}
256 \item $\neg (\star \R \bot)$
257 \item $* \R (t_1=t_2)$ iff $t_1=t_2$ is true ...
258 \item $\pair{f}{g} \R (P\land Q)$ iff $f \R P$ and $g \R Q$
259 \item $f \R (P\to Q)$ iff for any $m$ such that $m \R P$, $(f \,m) \R Q$
260 \item $f \R (\forall x.P)$ iff for any natural number $n$ $(f n) \R P[\underline{n}/x]$
261 \item $\pair{n}{g}\R (\exists x.P)$ iff $g \R P[\underline{n}/x]$
262 \end{itemize}
263 %We need to generalize the notion of realizability to sequents.
264 %Given a sequent $B_1, \ldots, B_n \vdash A$ with free variables in 
265 %$\vec{x} = x_1,\ldots, x_m$, we say that $f \R B1, \ldots, B_n \vdash A$ iff 
266 %forall natural numbers $n_1, \ldots, n_m$, 
267 %if forall $i \in {1,\ldots,n}$ 
268 %$m_i \R B_i[\vec{\underline{n}}/\vec{x}]$ then
269 %$$f <m_1, \ldots, m_n> \R A[\vec{\underline{n}}/\vec{x}]$$.
270 %
271 \noindent
272 We need to generalize the notion of realizability to sequents.\\
273 Let $\vec{x} = FV_{\N}( B_1, \ldots, B_n, P)$ a vector of variables of type
274 $\N$ that occur free in $B_1, \ldots, B_n, P$. Let $\vec{b:B}$ the vector
275 $b_1:B_1, \ldots, b_n:B_n$.\\ 
276 We say that $f \R B_1, \ldots, B_n \vdash A:P$ iff
277 $$\lambda \vec{x:\N}. \lambda \vec{b:B}.f \R 
278 \forall \vec{x}. B_1 \to \ldots \to B_n \to P$$
279 Note that $\forall \vec{x}. B_1 \to \ldots \to B_n \to P$ is a closed formula,
280 so we can use the previous definition of realizability on it.
281
282 \noindent
283 We proceed to prove that all axioms $ax:Ax$ are realized by $\sem{ax}$.
284
285 \begin{itemize}
286 \item $nat\_ind$. 
287   We must prove that the recursion schema $R$ realizes the induction principle.
288   To this aim we must prove that for any $a$ and $f$ such that $a \R P(0)$ and
289   $f \R \forall x.(P(x) \to P(S(x)))$, and any natural number $n$, $(R \,a \,f
290   \,n) \R P(\underline{n})$.\\ 
291   We proceed by induction on n.\\ 
292   If $n=O$, $(R \,a \,f \,O) = a$ and by hypothesis $a \R P(0)$.\\ 
293   Suppose by induction that
294   $(R \,a \,f \,n) \R P(\underline{n})$, and let us prove that the relation
295   still holds for $n+1$.  By definition 
296   $(R \,a \,f \,(n+1)) = f \,n \,(R \,a \,f \,n)$, 
297   and since $f \R \forall x.(P(x) \to P(S(x)))$,  
298   $(f n (R a f n)) \R P(S(\underline{n}))=P(\underline{n+1})$.
299
300 \item $ex\_ind$. 
301   We must prove that $$\underline{ex\_ind} \R (\forall x:(P x)
302   \to Q) \to (\exists x:(P x)) \to Q$$ Following the definition of $\R$ we have
303   to prove that given\\ $f~\R~\forall~x:((P~x)~\to~Q)$ and
304   $p~\R~\exists~x:(P~x)$, then $\underline{ex\_ind}~f~p \R Q$.\\ 
305   $p$ is a couple $\pair{n_p}{g_p}$ such that $g_p \R P[\underline{n_p}/x]$, while
306   $f$ is a function such that forall $n$ and for all $m \R P[\underline{n}/x]$
307   then $f~n~m \R Q$ (note that $x$ is not free in $Q$ so $[\underline{n}/x]$
308   affects only $P$).\\
309   Expanding the definition of $\underline{ex\_ind}$, $fst$
310   and $snd$ we obtain $f~n_p~g_p$ that we know is in relation $\R$ with $Q$
311   since $g_p \R P[\underline{n_p}/x]$.
312
313 \item $ex\_intro$.
314   We must prove that 
315   $$\lambda x:\N.\lambda f:\sem{P}.\pair{x}{f} \R \forall x.(P\to\exists x.P(x)$$
316   that leads to prove that for each n
317   $\underline{ex\_into}~n \R (P\to\exists x.P(x))[\underline{n}/x]$.\\
318   Evaluating the substitution we have 
319   $\underline{ex\_into}~n \R (P[\underline{n}/x]\to\exists x.P(x))$.\\
320   Again by definition of $\R$ we have to prove that given a 
321   $m \R P[\underline{n}/x]$ then $\underline{ex\_into}~n~m \R \exists x.P(x)$.
322   Expanding the definition of $\underline{ex\_intro}$ we have
323   $\pair{n}{m} \R \exists x.P(x)$ that is true since $m \R P[\underline{n}/x]$.
324
325 \item $fst$.
326   We have to prove that $\pi_1 \R P \land Q \to P$, that is equal to proving
327   that for each $m \R P \land Q$ then $\pi_1~m \R P$ .
328   $m$ must be a couple $\pair{f_m}{g_m}$ such that $f_m \R P$ and $g_m \R Q$.
329   So we conclude that $\pi_1~m$ reduces to $f_m$ that is in relation $\R$
330   with $P$.
331
332 \item $snd$. The same for $fst$.
333
334 \item $conj$. 
335   We have to prove that 
336   $$\lambda x:\sem{P}. \lambda y:\sem{Q}.\pair{x}{y}\R P \to Q \to P \land Q$$
337   Following the definition of $\R$ we have to show that 
338   for each $m \R P$ and for each $n \R Q$ then 
339   $(\lambda x:\sem{P}. \lambda y:\sem{Q}.\pair{x}{y})~m~n \R P \land Q$.\\
340   This is the same of $\pair{m}{n} \R P \land Q$ that is verified since 
341   $m \R P$ and $n \R Q$.
342
343
344 \item $false\_ind$. 
345   We have to prove that $\bot_{\sem{Q}} \R \bot \to Q$. 
346   Trivial, since there is no $m \R \bot$.
347
348 \item $discriminate$. 
349   Since there is no $n$ such that $0 = S n$ is true... \\
350   $\underline{discriminate}~n \R 0 = S~\underline{n} \to \bot$ for each n.
351
352 \item $injS$.
353   We have to prove that for each $n_1$ and $n_2$\\
354   $\lambda \_:\N. \lambda \_:\N.\lambda \_:\one.*~n_1~n_2 \R 
355   (S(x)=S(y)\to x=y)[n_1/x][n_2/y]$.\\
356   We assume that $m \R S(n_1)=S(n_2)$ and we have to show that 
357   $\lambda \_:\N. \lambda \_:\N.\lambda \_:\one.*~n_1~n_2~m$ that reduces to
358   $*$ is in relation $\R$ with $n_1=n_2$. Since in the standard model of 
359   natural numbers  $S(n_1)=S(n_2)$ implies $n_1=n_2$ we have that 
360   $* \R n_1=n_2$.
361
362 \item $plus\_O$. 
363   Since in the standard model for natural numbers $0$ is the neutral element
364   for addition $\lambda \_:\N.\star \R \forall x.x + 0 = x$.
365
366 \item $plus\_S$.
367   In the standard model of natural numbers the addition of two numbers is the 
368   operation of counting the second starting from the first. So
369   $$\lambda \_:\N. \lambda \_:\N. \star \R \forall x,y.x+S(y)=S(x+y)$$.
370
371 \item $times\_O$.
372   Since in the standard model for natural numbers $0$ is the absorbing element
373   for multiplication $\lambda \_:\N.\star \R \forall x.x \mult 0 = 0$.
374   
375 \item $times\_S$.
376   In the standard model of natural numbers the multiplications of two 
377   numbers is the operation of adding the first to himself a number of times
378   equal to the second number. So
379   $$\lambda \_:\N. \lambda \_:\N. \star \R \forall x,y.x+S(y)=S(x+y)$$.
380   
381 \end{itemize}
382
383
384 \noindent
385 {\bf example}\\
386 Let us prove the following principle of well founded induction:
387 \[(\forall m.(\forall p. p < m \to P p) \to P m) \to \forall n.P n\]
388 In the following proof we shall make use of proof-terms, since we finally
389 wish to extract the computational content; we leave to reader the easy
390 check that the proof object describes the usual and natural proof
391 of the statement.
392
393 We assume to have already proved the following lemmas (having trivial
394 realizers):\\
395 \[L: \lambda b.p < 0 \to \bot\]
396 \[M: \lambda p,q,n.p < q \to q \le (S n) \to p \le n \]
397 Let us assume $h: \forall m.(\forall p. p < m \to P p) \to P m$.
398 We prove by induction on n that $\forall q. q \le n \to P q$.
399 For $n=0$, we get a proof of $P \;0$ by 
400 \[ B: \lambda q.\lambda \_:q \le n. h \;0\; 
401 (\lambda p.\lambda k:p < 0. false\_ind \;(L\;p\; k)) \]
402 In the inductive case, we must prove that, for any n, 
403 \[(\forall q. q \le n \to P q) \to (\forall q. q \le S n \to P q)\]
404 Assume $h1: \forall q. q \le n \to P q$ and
405 $h2: q \le S \;n$. Let us prove $\forall p. p < q \to P p$.
406 If $h3: p < q$ then $(M\; p\; q\; n\; h3\; h2): p \le n$, hence 
407 $h1 \;p \; (M\; p\; q\; n\; h3\; h2): P p$.\\ 
408 In conclusion, the proof of the 
409 inductive case is
410 \[I: \lambda h1:\forall q. q \le n \to P\; q.\lambda q.\lambda h2:q \le S n.
411 h \; q \; (\lambda p.\lambda h3:p < q.h1 \;p\; (M\; p\; q\; n\; h3\; h2)) \]
412 (where $h$ is free in I).
413 The full proof is
414 \[ \lambda m.\lambda h: \forall m.(\forall p. p < m \to P p) \to P m.
415 nat\_ind \;B \; I \;m\; (le\_n \; m) \]
416 where $le\_n$ is a proof that $\forall n. n \le n$.\\
417 Form the previous proof,after stripping terminal objects, 
418 and a bit of eta-contraction to make
419 the term more readable, we extract the following term (types are omitted):
420
421 \[R' = \lambda m.\lambda f.
422 R\; (f \; O\; (\lambda q.*_A))\; 
423 (\lambda n\lambda g\lambda q.f \;q\;g)\;m \;m\]
424
425 The intuition of this operator is the following: supose to
426 have a recursive definition $h q = F[h]$ where $q:\N$ and 
427 $F[h]: A$. This defines a functional 
428 $f: \lambda q.\lambda g.F[g]: N\to(N\to A) \to A$, such that
429 (morally) $h$ is the fixpoint of $f$. For instance, 
430 in the case of the fibonacci function, $f$ is 
431 \[\lambda q. \lambda g.
432 if\; q = 0\;then\; 1\; else\; if\; q = 1\; then\; 1\; else\; g (q-1)+g (q-2)\]
433
434 So $f$ build a new 
435 approximation of $h$ from the previous approximation $h$ taken
436 as input. $R'$ precisely computes the mth-approximation starting
437 from a dummy function $(\lambda q.*_A)$. Alternatively, 
438 you may look at $g$ as the ``history'' (curse of values) of $h$ 
439 for all values less or equal to $q$; then $f$ extend $g$ to
440 $q+1$.
441
442 \section{Inductive types}
443 The notation we will use is similar to the one used in 
444 \cite{Werner} and \cite{Paulin89} but we prefer
445 giving a label to each constructor and use that label instead of the
446 longer $Constr(n,\ind\{\ldots\})$ to indicate the $n^{th}$ constructor.
447 We adopt the vector notation to make things more readable.
448 $\vec{m}$ has to be intended as $m_1~\ldots~m_n$ where $n$ may
449 be equal to 0 (we use $m_1~\vec{m}$ when we want to give a
450 name to the first $m$ and assert $n>0$). If the vector notation is
451 used inside an arrow type it has a slightly different meaning, 
452 $A \to \vec{B} \to C$ is a shortcut for 
453 $A \to B_1 \to \ldots \to B_n \to C$.
454
455 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
456 \subsection{Extensions to the logic framework}
457 To talk about arbitrary inductive types (and not hard coded natural numbers) we
458 have to extend a bit our framework.
459
460 First we admit quantification over inductive types $T$, thus $\forall x:T.A$
461 and $\exists x:T.A$ are allowed. Then rules 4 and 5 of the $\sem{\cdot}$
462 definition are replaced by $\sem{\forall x:T.P} = T \to \sem{P}$ and
463 $\sem{\exists x:T.P} = T \times \sem{P}$.
464
465 For each inductive type we will describe the formation rules and the
466 corresponding induction principle schema.
467
468 Symmetrically we have to extend System T with arbitrary inductive types and 
469 we will see how theyr recursors are defined in the following sections. 
470
471 The definition of $\R$ is modified substituting each occurrence of $\N$ with 
472 a generic inductive type $T$.
473
474 %%%%%%%%%%%%%%%%%%%%%%%%%%%%
475 \subsection{Type definition}
476 $$\ind\{c_1:C(X); \ldots ; c_n:C(X)\}$$
477 $$C(X) ::= X \| T \to C(X) \| X \to C(X)$$
478 In the second case we mean $T \neq X$.
479
480 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
481 \subsection{Induction principle}
482 The induction principle for an inductive type $X$ and a predicate $Q$ 
483 is a constant with the following type
484 $$\Xind:\vec{\triUP\{C(X), c\}} \to \forall t:X.Q(x)$$
485 $\triUP$ takes a constructor type $C(X)$ and a term $c$ (initially $c$ is a
486 constructor of X, and $c:C(X)$) and is defined by recursion as follows:
487 \begin{eqnarray}
488 \triUP\{X, c\} & = & Q(c) \nonumber\\
489 \triUP\{T \to C(X), c\} & = & 
490         \forall m:T.\triUP\{C(X),c~m\} \nonumber\\
491 \triUP\{X \to C(X), c\} & = & 
492         \forall t:X.Q(t) \to \triUP\{C(X), c~t\} \nonumber
493 \end{eqnarray}
494
495 %%%%%%%%%%%%%%%%%%%%%
496 \subsection{Recursor}
497 \subsubsection{Type}
498 The type of the recursor $\Rx$ on an inductive type $X$ is
499 $$\Rx : \vec{\square\{C(X)\}} \to X \to \alpha$$
500 $\square$ is defined by recursion on the constructor type $C(X)$.
501 \begin{eqnarray}
502 \square\{X\} & = & \alpha \nonumber \\
503 \square\{T \to C(X)\} & = & T \to \square\{C(X)\}\nonumber \\
504 \square\{X \to C(X)\} & = & X \to \alpha \to \square\{C(X)\}\nonumber 
505 \end{eqnarray}
506 \subsubsection{Reduction rules}
507 We say that 
508 $$\Rx~\vec{f}~(c_i~\vec{m}) \leadsto
509 \triDOWN\{C(X)_i, f_i, \vec{m}\}$$
510 $\triDOWN$ takes a constructor type $C(X)$, a term $f$ 
511 (of type $\square\{C(X)\}$) and is defined by recursion as follows:
512 \begin{eqnarray}
513 \triDOWN\{X, f, \} & = & f\nonumber \\
514 \triDOWN\{T \to C(X), f, m_1~\vec{m}\} & = &
515         \triDOWN\{C(X), f~m_1, \vec{m}\}\nonumber \\
516 \triDOWN\{X \to C(X), f, m_1~\vec{m}\} & = & 
517         \triDOWN\{C(X), f~m_1~(\Rx~\vec{f}~m_1),
518         \vec{m}\}\nonumber
519 \end{eqnarray}
520 We assume $\Rx~\vec{f}~(c_i~\vec{m})$ is well typed, so in the first case we
521 can omit $\vec{m}$ since it is an empty sequence.
522
523 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
524 \subsection{Realizability of the induction principle}
525 Once we have inductive types and their induction principle we want to show that
526 the recursor $\Rx$ realizes $\Xind$, that is that $\Rx$ has type 
527 $\sem{\Xind}$ and is in relation $\R$ with $\Xind$. 
528
529 \begin{thm}$\Rx : \sem{\Xind}$\end{thm}
530 \begin{proof}
531 We have to compare the definition of $\square$ and $\triUP$
532 since they play the same role in constructing respectively the types of 
533 $\Rx$ and
534 $\Xind$. If we assume $\alpha = \sem{Q}$ and we apply the $\sem{\cdot}$
535 function to each right side of the $\triUP$ definition we obtain
536 exactly $\square$. The last two elements of the arrows $\Rx$ and
537 $\Xind$ are again the same up to $\sem{\cdot}$.
538 \end{proof}
539
540 \begin{thm}$\Rx\R \Xind$\end{thm}
541 \begin{proof}
542 To prove that $\Rx\R \Xind$ we must assume that for each $i$ index
543 of a constructor of $X$, $f_i \R \triUP\{C(X)_i, c_i\}$ and we
544 have to prove that for each $t:X$
545 $$\Rx~\vec{f}~t \R Q(t)$$
546 \noindent
547 We proceed by induction on the structure of $t$.
548 \\
549 The base case is when the
550 type of the head constructor of $t$ has no recursive arguments (i.e. the type
551 is generated using only the first two rules $C(X)$), so
552 $(\Rx~\vec{f}~(c_i~\vec{m}))$ reduces in one step to $(f_i~\vec{m})$.  $f_i$
553 realizes $\triUP\{C(X)_i, c_i\}$ by assumption and since we are in the base
554 case $\triUP\{C(X)_i, c_i\}$ is of the form $\vec{\forall t:T}.Q(c_i~\vec{t})$.
555 Thus $f_i~\vec{m} \R Q(c_i~\vec{m})$.
556 \\ 
557 In the induction step we have as induction hypothesis that for each recursive
558 argument $t_i$ of the head constructor $c_i$, $r_i\equiv
559 \Rx~\vec{f}~t_i \R Q(t_i)$. By the third rule of $\triDOWN$ we obtain the reduct
560 $f_i~\vec{m}~\vec{t~r}$ (here we write first all the non recursive arguments,
561 then all the recursive one. In general they can be mixed and the proof is
562 exactly the same but the notation is really heavier). We know by hypothesis
563 that $f_i \R \triUP\{C(X)_i, c_i\} \equiv \vec{\forall m:T}.\vec{\forall
564 t:X.Q(t)} \to Q(c_i~\vec{m}~\vec{t})$, thus $f_i~\vec{m}~\vec{t~r} \R
565 Q(c_i~\vec{m}~\vec{t})$.
566 \end{proof}
567
568
569 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
570 \begin{thebibliography}{}
571 \bibitem{AL91}A.Asperti, G.Longo. Categories, Types and Structures. 
572 Foundations of Computing, Cambrdidge University press, 1991.
573 \bibitem{Girard86}G.Y.Girard. The system F of variable types, fifteen
574 years later. Theoretical Computer Science 45, 1986.
575 \bibitem{Girard87}G.Y.Girard. Proof Theory and Logical Complexity. 
576 Bibliopolis, Napoli, 1987.
577 \bibitem{GLT}G.Y.Girard, Y.Lafont, P.Tailor. Proofs and Types.
578 Cambridge Tracts in Theoretical Computer Science 7.Cambridge University
579 Press, 1989.
580 \bibitem{Godel58}K.G\"odel. \"Uber eine bisher noch nicht ben\"utzte Erweiterung
581 des finiten Standpunktes. Dialectica, 12, pp.34-38, 1958.
582 \bibitem{Godel90}K.G\"odel. Collected Works. Vol.II, Oxford University Press,
583 1990.
584 \bibitem{HS86}J.R.Hindley, J. P. Seldin. Introduction to Combinators and 
585 Lambda-calculus, Cambridge University Press, 1986.
586 \bibitem{Howard68}W.A.Howard. Functional interpretation of bar induction
587 by bar recursion. Compositio Mathematica 20, pp.107-124. 1958
588 \bibitem{Howard80}W.A.Howard. The formulae-as-types notion of constructions.
589 in J.P.Seldin and j.R.Hindley editors, to H.B.Curry: Essays on Combinatory 
590 Logic, Lambda calculus and Formalism. Acedemic Press, 1980.
591 \bibitem{Kleene45}S.C.Kleene. On the interpretation of intuitionistic 
592 number theory. Journal of Symbolic Logic, n.10, pp.109-124, 1945.
593 \bibitem{Kreisel59} G.Kreisel. Interpretation of analysis by means of
594 constructive functionals of finite type. In. A.Heyting ed. 
595 {\em Constructivity in mathematics}. North Holland, Amsterdam,1959.
596  \bibitem{Kreisel62} G.Kreisel. On weak completeness of intuitionistic 
597 predicatelogic. Journal of Symbolic Logic 27, pp. 139-158. 1962.
598 \bibitem{Letouzey04}P.Letouzey. Programmation fonctionnelle 
599 certifi\'ee; l'extraction
600 de programmes dans l'assistant Coq. Ph.D. Thesis, Universit\'e de 
601 Paris XI-Orsay, 2004.
602 \bibitem{Loef}P.Martin-L\"of. Intuitionistic Type Theory.
603 Bibliopolis, Napoli, 1984.
604 \bibitem{Paulin87}C.Paulin-Mohring. Extraction de programme dans le Calcul de
605 Constructions. Ph.D. Thesis, Universit\'e de 
606 Paris 7, 1987.
607 \bibitem{Paulin89}C.Paulin-Mohring. Extracting $F_{\omega}$ programs 
608 from proofs in the Calculus of Constructions. In proc. of the Sixteenth Annual 
609 ACM Symposium on 
610 Principles of Programming Languages, Austin, January, ACML Press 1989.
611 \bibitem{Sch}K.Sch\"utte. Proof Theory. Grundlehren der mathematischen 
612 Wissenschaften 225, Springer Verlag, Berlin, 1977.
613 \bibitem{Troelstra}A.S.Troelstra. Metamathemtical Investigation of 
614 Intuitionistic
615 Arithmetic and Analysis. Lecture Notes in Mathematics 344, Springer Verlag,
616 Berlin, 1973.
617 \bibitem{TS}A.S.Troelstra, H.Schwichtenberg. Basic Proof Theory.
618 Cambridge Tracts in Theoretical Computer Science 43.Cambridge University
619 Press, 1996.
620 \bibitem{Werner}B.Werner. Une Th\'eorie des Constructions Inductives.
621 Ph.D.Thesis, Universit\'e de Paris 7, 1994.
622
623
624 \end{thebibliography}
625
626 \end{document}
627