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