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