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