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{\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{\indP}{Ind(\vec{P}~|~X)}
23 \newcommand{\Xind}{\ensuremath{X_{ind}}}
24 \newcommand{\XindP}{\ensuremath{X_{ind}}}
25 \renewcommand{\|}{\ensuremath{\quad | \quad}}
26 \newcommand{\triUP}{\ensuremath{\Delta}}
27 \newcommand{\triDOWN}{\ensuremath{\nabla}}
28 \newcommand{\Rx}{\ensuremath{R_X}}
30 \newtheorem{thm}{Theorem}[subsection]
32 \title{Modified Realizability and Inductive Types}
43 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
44 \section{Introduction}
45 The characterization of the provable recursive functions of
46 Peano Arithmetic as the terms of system T is a well known
47 result of G\"odel \cite{Godel58,Godel90}. Although several authors acknowledge
48 that the functional interpretation of the Dialectica paper
49 is not among the major achievements of the author (see e.g. \cite{Girard87}),
50 the result has been extensively investigated and there is a wide
52 topic (see e.g. \cite{Troelstra,HS86,Girard87}, just to mention textbooks,
53 and the bibliography therein).
55 A different, more neglected, but for many respects much more
56 direct relation between Peano (or Heyting) Arithmetics and
57 G\"odel System T is provided
58 by the so called {\em modified realizability}. Modified realizability
59 was first introduced by Kreisel in \cite{Kreisel59} - although it will take you
60 a bit of effort to recognize it in the few lines of paragraph 3.52 -
61 and later in \cite{Kreisel62} under the name of generalized realizability.
62 The name of modified realizability seems to be due to Troelstra
64 - who contested Kreisel's name but unfortunately failed in proposing
65 a valid alternative; we shall reluctantly adopt this latter name
66 to avoid further confusion. Modified realizability is a typed variant of
67 realizability, essentially providing interpretations
68 of $HA^{\omega}$ into itself: each theorem is realized by a typed function
69 of system T, that also gives the actual computational content extracted
71 In spite of the simplicity and the elegance of the proof, it is extremely
72 difficult to find a modern discussion of this result; the most recent
73 exposition we are aware of is in the encyclopedic work by
74 Troelstra \cite{Troelstra} (pp.213-229) going back to thirty years ago.
75 Even modern introductory books
76 to Type Theory and Proof Theory devoting much space to system T
77 such as \cite{GLT} and \cite{TS} surprisingly leave out this simple and
78 illuminating result. Both the previous textbooks
79 prefer to focus on higher order arithmetics and its relation with
80 Girard's System $F$ \cite{Girard86}, but the technical complexity and
81 the didactical value of the two proofs is not comparable: when you
82 prove that the Induction Principle is realized by the recursor $R$
83 of system $T$ you catch a sudden gleam of understanding in the
84 students eyes; usually, the same does not happen when you show, say,
85 that the ``forgetful'' interpretation of the higher order predicate defining
86 the natural numbers is the system $F$ encoding
87 $\forall X.(X\to X) \to X \to X$ of $\N$.
88 Moreover, after a first period of enthusiasm, the impredicative
89 encoding of inductive types in Logical Frameworks has shown several
90 problems and limitations (see e.g. \cite{Werner} pp.24-25) mostly
91 solved by assuming inductive types as a primitive logical notion
92 (leading e.g. form the Calculus of Constructions to the Calculus
93 of Inductive Constructions - CIC). Even the extraction algorithm of
94 CIC, strictly based on realizability principles, and in a first time
95 still oriented towards System F \cite{Paulin87,Paulin89} has been
96 recently rewritten \cite{Letouzey04}
97 to take advantage of concrete types and pattern matching of ML-like
98 languages. Unfortunately, systems like the Calculus of Inductive
99 Constructions are so complex, from the logical point of view, to
100 substantially prevent a really neat theoretical exposition (at present,
102 even exists a truly complete consistency proofs covering all aspects
103 of such systems); moreover, not everybody may be interested in all the features
104 offered by these frameworks, from polymorphism to types depending on
105 proofs. Our program is to restart the analysis of logical systems with
106 primitive inductive types in a smooth way, starting form first order
107 logic and adding little by little small bits of logical power.
108 This paper is the first step in this direction.
110 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
111 \section{G\"odel system T}
112 We shall use a variant of system T with three atomic types $\N$ (natural
113 numbers), $\B$ (booleans) and $\one$ (a terminal object), and two binary
114 type constructors $\times$ (product) and $\to$ (arrow type).
116 The terms of the language comprise the usual simply typed lambda terms
117 with explicit pairs, plus the following additional constants:
120 \item $true: \B$, $false:\B$, $D:A\to A \to \B \to A$
121 \item $O:\N$, $S:\N \to \N$, $R:A \to (A \to \N \to A) \to \N \to A$,
123 Redexes comprise $\beta$-reduction
124 \[(\beta)~~ \lambda x:U.M ~ N \leadsto M[N/x]\]
127 \[(\pi_1)~~fst \pair{M}{N} \leadsto M\\ \hspace{.6cm} (\pi_2)~~ snd \pair{M}{N}
129 and the following type specific reductions:
130 \[(D_{true})~~\\D~M~N~ true \leadsto M \hspace{.6cm}
131 (D_{false})~~ D~M~N~false \leadsto N \]
132 \[(R_0)~~\\R~M~F~ 0 \leadsto M \hspace{.6cm}
133 (R_S)~~ R~M~F~(S~n) \leadsto F~n~(R~M~F~n) \]
134 \[(*)~~ M \leadsto * \]
135 where (*) holds for any $M$ of type $\one$.
137 Note that using the well known isomorpshims
138 $\one \to A \cong A$, $A \to \one \cong \one$
139 and $A \times \one \cong A \cong \one\times A$ (see \cite{AL91}, pp.231-239)
140 we may always get rid of $\one$ (apart the trivial case).
141 The terminal object does not play a major role in our treatment, but
142 it allows to extract better algorithms. In particular we use it
143 to realize atomic proposition, and stripping out the terminal object using
144 the above isomorphisms gives a simple way of just keeping the truly
145 informative part of the algorithms.
149 \section{Heyting's arithmetics}
154 \item $nat\_ind: P(0) \to (\forall x.P(x) \to P(S(x))) \to \forall x.P(x)$
155 \item $ex\_ind: (\forall x.P(x) \to Q) \to \exists x.P(x) \to Q$
156 \item $ex\_intro: \forall x.(P \to \exists x.P)$
157 \item $fst: P \land Q \to P$
158 \item $snd: P \land Q \to Q$
159 \item $conj: P \to Q \to P \land Q$
160 \item $false\_ind: \bot \to Q$
161 \item $discriminate:\forall x.0 = S(x) \to \bot$
162 \item $injS: \forall x,y.S(x) = S(y) \to x=y$
163 \item $plus\_O:\forall x.x+0=x$
164 \item $plus\_S:\forall x,y.x+S(y)=S(x+y)$
165 \item $times\_O:\forall x.x\mult0=0$
166 \item $times\_S:\forall x,y.x\mult S(y)=x+(x\mult y)$
170 {\bf Inference Rules}
172 say that ax:AX refers to the previous Axioms list...
175 (Proj)\hspace{0.2cm} \Gamma, x:A, \Delta \vdash x:A
177 (Const)\hspace{0.2cm} \Gamma \vdash ax : AX
181 (\to_i)\hspace{0.2cm}\frac{\Gamma,x:A \vdash M:Q}{\Gamma \vdash \lambda x:A.M: A \to Q} \hspace{2cm}
182 (\to_e)\hspace{0.2cm}\frac{\Gamma \vdash M: A \to Q \hspace{1cm}\Gamma \vdash N: A}
183 {\Gamma \vdash M N: Q}
187 % (\land_i)\frac{\Gamma \vdash M:A \hspace{1cm}\Gamma \vdash N:B}
188 % {\Gamma \vdash \pair{M}{N} : A \land B}
190 % (\land_{el})\frac{\Gamma \vdash A \land B}{\Gamma \vdash A}
192 % (\land_{er})\frac{\Gamma \vdash A \land B}{\Gamma \vdash B}
196 (\forall_i)\hspace{0.2cm}\frac{\Gamma \vdash M:P}{\Gamma \vdash
197 \lambda x:\N.M: \forall x.P}(*) \hspace{2cm}
198 (\forall_e)\hspace{0.2cm}\frac{\Gamma \vdash M :\forall x.P}{\Gamma \vdash M t: P[t/x]}
203 % (\exists_i)\frac{\Gamma \vdash P[t/x]}{\Gamma \vdash \exists x.P}\hspace{2cm}
204 % (\exists_e)\frac{\Gamma \vdash \exists x.P\hspace{1cm}\Gamma \vdash \forall x.P \to Q}
210 The formulae to types translation function
211 $\sem{\cdot}$ takes in input formulae in HA and returns types in T.
214 \item $\sem{A} = \one$ if A is atomic
215 \item $\sem{A \land B} = \sem{A}\times \sem{B}$
216 \item $\sem{A \to B} = \sem{A}\to \sem{B}$
217 \item $\sem{\forall x:\N.P} = \N \to \sem{P}$
218 \item $\sem{\exists x:\N.P} = \N \times \sem{P}$
222 For any type T of system T $\canonical_T: \one \to T$ is inductively defined as follows:
224 \item $\canonical_\one = \lambda x:\one.x$
225 \item $\canonical_N = \lambda x:\one.0$
226 \item $\canonical_{U\times V} = \lambda x:\one.\pair{\canonical_{U} x}{\canonical_{V} x}$
227 \item $\canonical_{U\to V} = \lambda x:\one.\lambda \_:U. \canonical_{V} x$
231 \item $\sem{nat\_ind} = R$
232 \item $\sem{ex\_ind} = (\lambda f:(\N \to \sem{P} \to \sem{Q}).
233 \lambda p:\N\times \sem{P}.f (fst \,p) (snd \,p)$.
234 \item $\sem{ex\_intro} = \lambda x:\N.\lambda f:\sem{P}.\pair{x}{f}$
235 \item $\sem{fst} = \pi_1$
236 \item $\sem{snd} = \pi_2$
237 \item $\sem{conj} = \lambda x:\sem{P}.\lambda y:\sem{Q}.\pair{x}{y}$
238 \item $\sem{false\_ind} = \canonical_{\sem{Q}}$
239 \item $\sem{discriminate} = \lambda \_:\N.\lambda \_:\one.\star$
240 \item $\sem{injS}= \lambda \_:\N. \lambda \_:\N.\lambda \_:\one.\star$
241 \item $\sem{plus\_O} = \sem{times\_O} = \lambda \_:\N.\star$
242 \item $\sem{plus\_S} = \sem{times_S} = \lambda \_:\N. \lambda \_:\N.\star$
245 In the case of structured proofs:
247 \item $\semT{M N} = \semT{M} \semT{N}$
248 \item $\semT{\lambda x:A.M} = \lambda x:\sem{A}.\semT{M}$
249 \item $\semT{\lambda x:\N.M} = \lambda x:\N.\semT{M}$
250 \item $\semT{M t} = \semT{M} \semT{t}$
253 \section{Realizability}
254 The realizability relation is a relation $f \R P$ where $f: \sem{P}$, and
255 $P$ is a closed formula.
258 \item $\neg (\star \R \bot)$
259 \item $* \R (t_1=t_2)$ iff $t_1=t_2$ is true ...
260 \item $\pair{f}{g} \R (P\land Q)$ iff $f \R P$ and $g \R Q$
261 \item $f \R (P\to Q)$ iff for any $m$ such that $m \R P$, $(f \,m) \R Q$
262 \item $f \R (\forall x.P)$ iff for any natural number $n$ $(f n) \R P[\underline{n}/x]$
263 \item $\pair{n}{g}\R (\exists x.P)$ iff $g \R P[\underline{n}/x]$
265 %We need to generalize the notion of realizability to sequents.
266 %Given a sequent $B_1, \ldots, B_n \vdash A$ with free variables in
267 %$\vec{x} = x_1,\ldots, x_m$, we say that $f \R B1, \ldots, B_n \vdash A$ iff
268 %forall natural numbers $n_1, \ldots, n_m$,
269 %if forall $i \in {1,\ldots,n}$
270 %$m_i \R B_i[\vec{\underline{n}}/\vec{x}]$ then
271 %$$f <m_1, \ldots, m_n> \R A[\vec{\underline{n}}/\vec{x}]$$.
274 We need to generalize the notion of realizability to sequents.\\
275 Let $\vec{x} = FV_{\N}( B_1, \ldots, B_n, P)$ a vector of variables of type
276 $\N$ that occur free in $B_1, \ldots, B_n, P$. Let $\vec{b:B}$ the vector
277 $b_1:B_1, \ldots, b_n:B_n$.\\
278 We say that $f \R B_1, \ldots, B_n \vdash A:P$ iff
279 $$\lambda \vec{x:\N}. \lambda \vec{b:B}.f \R
280 \forall \vec{x}. B_1 \to \ldots \to B_n \to P$$
281 Note that $\forall \vec{x}. B_1 \to \ldots \to B_n \to P$ is a closed formula,
282 so we can use the previous definition of realizability on it.
285 We proceed to prove that all axioms $ax:Ax$ are realized by $\sem{ax}$.
289 We must prove that the recursion schema $R$ realizes the induction principle.
290 To this aim we must prove that for any $a$ and $f$ such that $a \R P(0)$ and
291 $f \R \forall x.(P(x) \to P(S(x)))$, and any natural number $n$, $(R \,a \,f
292 \,n) \R P(\underline{n})$.\\
293 We proceed by induction on n.\\
294 If $n=O$, $(R \,a \,f \,O) = a$ and by hypothesis $a \R P(0)$.\\
295 Suppose by induction that
296 $(R \,a \,f \,n) \R P(\underline{n})$, and let us prove that the relation
297 still holds for $n+1$. By definition
298 $(R \,a \,f \,(n+1)) = f \,n \,(R \,a \,f \,n)$,
299 and since $f \R \forall x.(P(x) \to P(S(x)))$,
300 $(f n (R a f n)) \R P(S(\underline{n}))=P(\underline{n+1})$.
303 We must prove that $$\underline{ex\_ind} \R (\forall x:(P x)
304 \to Q) \to (\exists x:(P x)) \to Q$$ Following the definition of $\R$ we have
305 to prove that given\\ $f~\R~\forall~x:((P~x)~\to~Q)$ and
306 $p~\R~\exists~x:(P~x)$, then $\underline{ex\_ind}~f~p \R Q$.\\
307 $p$ is a couple $\pair{n_p}{g_p}$ such that $g_p \R P[\underline{n_p}/x]$, while
308 $f$ is a function such that forall $n$ and for all $m \R P[\underline{n}/x]$
309 then $f~n~m \R Q$ (note that $x$ is not free in $Q$ so $[\underline{n}/x]$
311 Expanding the definition of $\underline{ex\_ind}$, $fst$
312 and $snd$ we obtain $f~n_p~g_p$ that we know is in relation $\R$ with $Q$
313 since $g_p \R P[\underline{n_p}/x]$.
317 $$\lambda x:\N.\lambda f:\sem{P}.\pair{x}{f} \R \forall x.(P\to\exists x.P(x)$$
318 that leads to prove that for each n
319 $\underline{ex\_into}~n \R (P\to\exists x.P(x))[\underline{n}/x]$.\\
320 Evaluating the substitution we have
321 $\underline{ex\_into}~n \R (P[\underline{n}/x]\to\exists x.P(x))$.\\
322 Again by definition of $\R$ we have to prove that given a
323 $m \R P[\underline{n}/x]$ then $\underline{ex\_into}~n~m \R \exists x.P(x)$.
324 Expanding the definition of $\underline{ex\_intro}$ we have
325 $\pair{n}{m} \R \exists x.P(x)$ that is true since $m \R P[\underline{n}/x]$.
328 We have to prove that $\pi_1 \R P \land Q \to P$, that is equal to proving
329 that for each $m \R P \land Q$ then $\pi_1~m \R P$ .
330 $m$ must be a couple $\pair{f_m}{g_m}$ such that $f_m \R P$ and $g_m \R Q$.
331 So we conclude that $\pi_1~m$ reduces to $f_m$ that is in relation $\R$
334 \item $snd$. The same for $fst$.
337 We have to prove that
338 $$\lambda x:\sem{P}. \lambda y:\sem{Q}.\pair{x}{y}\R P \to Q \to P \land Q$$
339 Following the definition of $\R$ we have to show that
340 for each $m \R P$ and for each $n \R Q$ then
341 $(\lambda x:\sem{P}. \lambda y:\sem{Q}.\pair{x}{y})~m~n \R P \land Q$.\\
342 This is the same of $\pair{m}{n} \R P \land Q$ that is verified since
343 $m \R P$ and $n \R Q$.
347 We have to prove that $\bot_{\sem{Q}} \R \bot \to Q$.
348 Trivial, since there is no $m \R \bot$.
350 \item $discriminate$.
351 Since there is no $n$ such that $0 = S n$ is true... \\
352 $\underline{discriminate}~n \R 0 = S~\underline{n} \to \bot$ for each n.
355 We have to prove that for each $n_1$ and $n_2$\\
356 $\lambda \_:\N. \lambda \_:\N.\lambda \_:\one.*~n_1~n_2 \R
357 (S(x)=S(y)\to x=y)[n_1/x][n_2/y]$.\\
358 We assume that $m \R S(n_1)=S(n_2)$ and we have to show that
359 $\lambda \_:\N. \lambda \_:\N.\lambda \_:\one.*~n_1~n_2~m$ that reduces to
360 $*$ is in relation $\R$ with $n_1=n_2$. Since in the standard model of
361 natural numbers $S(n_1)=S(n_2)$ implies $n_1=n_2$ we have that
365 Since in the standard model for natural numbers $0$ is the neutral element
366 for addition $\lambda \_:\N.\star \R \forall x.x + 0 = x$.
369 In the standard model of natural numbers the addition of two numbers is the
370 operation of counting the second starting from the first. So
371 $$\lambda \_:\N. \lambda \_:\N. \star \R \forall x,y.x+S(y)=S(x+y)$$.
374 Since in the standard model for natural numbers $0$ is the absorbing element
375 for multiplication $\lambda \_:\N.\star \R \forall x.x \mult 0 = 0$.
378 In the standard model of natural numbers the multiplications of two
379 numbers is the operation of adding the first to himself a number of times
380 equal to the second number. So
381 $$\lambda \_:\N. \lambda \_:\N. \star \R \forall x,y.x+S(y)=S(x+y)$$.
388 Let us prove the following principle of well founded induction:
389 \[(\forall m.(\forall p. p < m \to P~p) \to P~m) \to \forall n.P~n\]
390 In the following proof we shall make use of proof-terms, since we finally
391 wish to extract the computational content; we leave to reader the easy
392 check that the proof object describes the usual and natural proof
395 We assume to have already proved the following lemmas (having trivial
397 \[L : \forall p, q.p < q \to q \le 0 \to \bot\]
398 \[M : \forall p,q,n.p < q \to q \le (S n) \to p \le n \]
399 Let us assume $h : \forall m.(\forall p. p < m \to P~p) \to P~m$.
400 We prove by induction on $n$ that $\forall q. q \le n \to P~q$.
401 For $n=0$, we get a proof of $P ~q$ by
402 \[ B \equiv \lambda q.\lambda h_0:q \le 0. h ~q~
403 (\lambda p.\lambda k:p < q. false\_ind ~(L~p~q~k~h_0)) \]
404 In the inductive case, we must prove that, for any $n$,
405 \[(\forall q. q \le n \to P~q) \to (\forall q. q \le S n \to P~q)\]
406 Assume $h_1: \forall q. q \le n \to P q$ and
407 $h_2: q \le S ~n$. Let us prove $\forall p. p < q \to P~p$.
408 If $h_3: p < q$ then $(M~ p~ q~ n~ h_3~ h_2): p \le n$, hence
409 $h_1 ~p ~ (M~ p~ q~ n~ h_3~ h_2): P~p$.\\
410 In conclusion, the proof of the
412 \[I \equiv \lambda n.\lambda h_1:\forall q. q \le n \to P~ q.\lambda q.\lambda h_2:q \le S n.
413 h ~ q ~ (\lambda p.\lambda h_3:p < q.h_1 ~p~ (M~ p~ q~ n~ h_3~ h_2)) \]
414 (where $h$ is free in I).
416 \[ \lambda h: \forall m.(\forall p. p < m \to P~p) \to P~m.\lambda m.
417 nat\_ind ~B ~ I ~m~m~ (le\_n ~ m) \]
418 where $le\_n$ is a proof that $\forall n. n \le n$, and the free $P$ in the definition of $nat_{ind}$ is instantiated with $\forall m.m \le m \to P~m$.\\
419 Form the previous proof,after stripping terminal objects,
420 and a bit of eta-contraction to make
421 the term more readable, we extract the following term (types are omitted):
423 \[R' \equiv \lambda f.\lambda m.
424 R~ (\lambda n.f ~n~ (\lambda q.*))~
425 (\lambda n\lambda g\lambda q.f ~q~g)~m ~m\]
427 The intuition of this operator is the following: supose to
428 have a recursive definition $h q = F[h]$ where $q:\N$ and
429 $F[h]: A$. This defines a functional
430 $f: \lambda q.\lambda g.F[g]: N\to(N\to A) \to A$, such that
431 (morally) $h$ is the fixpoint of $f$. For instance,
432 in the case of the fibonacci function, $f$ is
433 \[fibo \equiv \lambda q. \lambda g.
434 if~ q = 0~then~ 1~ else~ if~ q = 1~ then~ 1~ else~ g (q-1)+g (q-2)\]
437 approximation of $h$ from the previous approximation $h$ taken
438 as input. $R'$ precisely computes the mth-approximation starting
439 from a dummy function $(\lambda q.*_A)$. Alternatively,
440 you may look at $g$ as the ``history'' (curse of values) of $h$
441 for all values less or equal to $q$; then $f$ extend $g$ to
444 Let's compute for example
446 R'~fibo~2 & \leadsto &
447 R~ (\lambda n.fibo ~n~ (\lambda q.*))~
448 (\lambda n\lambda g\lambda q.fibo ~q~g)~2 ~2\nonumber\\
450 (\lambda n\lambda g\lambda q.fibo ~q~g)~1~
452 (\lambda n.fibo ~n~ (\lambda q.*))~
453 (\lambda n\lambda g\lambda q.fibo ~q~g)~1)~
458 (\lambda n.fibo ~n~ (\lambda q.*))~
459 (\lambda n\lambda g\lambda q.fibo ~q~g)~1)~
463 ((\lambda n\lambda g\lambda q.fibo ~q~g)~0~
465 (\lambda n.fibo ~n~ (\lambda q.*))~
466 (\lambda n\lambda g\lambda q.fibo ~q~g)~0))~
472 (\lambda n.fibo ~n~ (\lambda q.*))~
473 (\lambda n\lambda g\lambda q.fibo ~q~g)~0)
478 (\lambda n.fibo ~n~ (\lambda q.*)))2
481 fibo~2~(\lambda q.fibo ~q~ (\lambda n.fibo ~n~ (\lambda q.*))) \nonumber\\
483 (\lambda q.fibo ~q~ (\lambda n.fibo ~n~ (\lambda q.*))) 1 +
484 (\lambda q.fibo ~q~ (\lambda n.fibo ~n~ (\lambda q.*))) 0 \nonumber\\
486 fibo ~1~ (\lambda n.fibo ~n~ (\lambda q.*)) +
487 fibo ~0~ (\lambda n.fibo ~n~ (\lambda q.*)) \nonumber\\
491 Note that the second argument of $fibo$ is always a method to calculate all the prvious values of $fibo$. DA CAPIRE (per me) come mai $\lambda n$ non viene usata...
494 n non serve perche' c'e' una relazione logica di n con q,
495 in particolare $q <= Sn$ ... quindi $q < n$ (lemma M)...
496 e quindi posso usare come history $< n$ una history $< q$.
497 il $\lambda h2$ essendo $[[q <= Sn]]$ = 1 viene scartata.
499 se si spiega come array viene decente... forse. lunedi' provo a scrivere
502 \section{Inductive types}
503 The notation we will use is similar to the one used in
504 \cite{Werner} and \cite{Paulin89} but we prefer
505 giving a label to each constructor and use that label instead of the
506 longer $Constr(n,\ind\{\ldots\})$ to indicate the $n^{th}$ constructor.
507 We adopt the vector notation to make things more readable.
508 $\vec{m}$ has to be intended as $m_1~\ldots~m_n$ where $n$ may
509 be equal to 0 (we use $m_1~\vec{m}$ when we want to give a
510 name to the first $m$ and assert $n>0$). If the vector notation is
511 used inside an arrow type it has a slightly different meaning,
512 $A \to \vec{B} \to C$ is a shortcut for
513 $A \to B_1 \to \ldots \to B_n \to C$.
515 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
516 \subsection{Extensions to the logic framework}
517 To talk about arbitrary inductive types (and not hard coded natural numbers) we
518 have to extend a bit our framework.
520 First we admit quantification over inductive types $T$, thus $\forall x:T.A$
521 and $\exists x:T.A$ are allowed. Then rules 4 and 5 of the $\sem{\cdot}$
522 definition are replaced by $\sem{\forall x:T.P} = T \to \sem{P}$ and
523 $\sem{\exists x:T.P} = T \times \sem{P}$.
525 For each inductive type we will describe the formation rules and the
526 corresponding induction principle schema.
528 Symmetrically we have to extend System T with arbitrary inductive types and
529 we will see how theyr recursors are defined in the following sections.
531 The definition of $\R$ is modified substituting each occurrence of $\N$ with
532 a generic inductive type $T$.
534 %%%%%%%%%%%%%%%%%%%%%%%%%%%%
535 \subsection{Type definition}
536 $$\ind\{c_1:C(X); \ldots ; c_n:C(X)\}$$
537 $$C(X) ::= X \| T \to C(X) \| X \to C(X)$$
538 In the second case we mean $T \neq X$.
540 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
541 \subsection{Induction principle}
542 The induction principle for an inductive type $X$ and a predicate $Q$
543 is a constant with the following type
544 $$\Xind:\vec{\triUP\{C(X), c\}} \to \forall t:X.Q(t)$$
545 $\triUP$ takes a constructor type $C(X)$ and a term $c$ (initially $c$ is a
546 constructor of X, and $c:C(X)$) and is defined by recursion as follows:
548 \triUP\{X, c\} & = & Q(c) \nonumber\\
549 \triUP\{T \to C(X), c\} & = &
550 \forall m:T.\triUP\{C(X),c~m\} \nonumber\\
551 \triUP\{X \to C(X), c\} & = &
552 \forall t:X.Q(t) \to \triUP\{C(X), c~t\} \nonumber
555 %%%%%%%%%%%%%%%%%%%%%
556 \subsection{Recursor}
558 The type of the recursor $\Rx$ on an inductive type $X$ is
559 $$\Rx : \vec{\square\{C(X)\}} \to X \to \alpha$$
560 $\square$ is defined by recursion on the constructor type $C(X)$.
562 \square\{X\} & = & \alpha \nonumber \\
563 \square\{T \to C(X)\} & = & T \to \square\{C(X)\}\nonumber \\
564 \square\{X \to C(X)\} & = & X \to \alpha \to \square\{C(X)\}\nonumber
566 \subsubsection{Reduction rules}
568 $$\Rx~\vec{f}~(c_i~\vec{m}) \leadsto
569 \triDOWN\{C(X)_i, f_i, \vec{m}\}$$
570 $\triDOWN$ takes a constructor type $C(X)$, a term $f$
571 (of type $\square\{C(X)\}$) and is defined by recursion as follows:
573 \triDOWN\{X, f, \} & = & f\nonumber \\
574 \triDOWN\{T \to C(X), f, m_1~\vec{m}\} & = &
575 \triDOWN\{C(X), f~m_1, \vec{m}\}\nonumber \\
576 \triDOWN\{X \to C(X), f, m_1~\vec{m}\} & = &
577 \triDOWN\{C(X), f~m_1~(\Rx~\vec{f}~m_1),
580 We assume $\Rx~\vec{f}~(c_i~\vec{m})$ is well typed, so in the first case we
581 can omit $\vec{m}$ since it is an empty sequence.
583 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
584 \subsection{Realizability of the induction principle}
585 Once we have inductive types and their induction principle we want to show that
586 the recursor $\Rx$ realizes $\Xind$, that is that $\Rx$ has type
587 $\sem{\Xind}$ and is in relation $\R$ with $\Xind$.
589 \begin{thm}$\Rx : \sem{\Xind}$\end{thm}
591 We have to compare the definition of $\square$ and $\triUP$
592 since they play the same role in constructing respectively the types of
594 $\Xind$. If we assume $\alpha = \sem{Q}$ and we apply the $\sem{\cdot}$
595 function to each right side of the $\triUP$ definition we obtain
596 exactly $\square$. The last two elements of the arrows $\Rx$ and
597 $\Xind$ are again the same up to $\sem{\cdot}$.
600 \begin{thm}$\Rx\R \Xind$\end{thm}
602 To prove that $\Rx\R \Xind$ we must assume that for each $i$ index
603 of a constructor of $X$, $f_i \R \triUP\{C(X)_i, c_i\}$ and we
604 have to prove that for each $t:X$
605 $$\Rx~\vec{f}~t \R Q(t)$$
607 We proceed by induction on the structure of $t$.
609 The base case is when the
610 type of the head constructor of $t$ has no recursive arguments (i.e. the type
611 is generated using only the first two rules $C(X)$), so
612 $(\Rx~\vec{f}~(c_i~\vec{m}))$ reduces in one step to $(f_i~\vec{m})$. $f_i$
613 realizes $\triUP\{C(X)_i, c_i\}$ by assumption and since we are in the base
614 case $\triUP\{C(X)_i, c_i\}$ is of the form $\vec{\forall t:T}.Q(c_i~\vec{t})$.
615 Thus $f_i~\vec{m} \R Q(c_i~\vec{m})$.
617 In the induction step we have as induction hypothesis that for each recursive
618 argument $t_i$ of the head constructor $c_i$, $r_i\equiv
619 \Rx~\vec{f}~t_i \R Q(t_i)$. By the third rule of $\triDOWN$ we obtain the reduct
620 $f_i~\vec{m}~\vec{t~r}$ (here we write first all the non recursive arguments,
621 then all the recursive one. In general they can be mixed and the proof is
622 exactly the same but the notation is really heavier). We know by hypothesis
623 that $f_i \R \triUP\{C(X)_i, c_i\} \equiv \vec{\forall m:T}.\vec{\forall
624 t:X.Q(t)} \to Q(c_i~\vec{m}~\vec{t})$, thus $f_i~\vec{m}~\vec{t~r} \R
625 Q(c_i~\vec{m}~\vec{t})$.
628 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
629 \section{Improoving inductive types}
630 It is possible to parametrize inductive types over other inductive types
631 without much difficulties since the type $T$ in $C(X)$ is free. Both the
632 recursor and the induction principle are schemas, parametric over $T$.
634 Possiamo anche definire $X_{\vec{P}}\equiv Ind(P|X)={c_i : C(P|X)}$ e poi
635 fare variare $T$ su $\vec{P}$, ma non ottengo niente di meglio.
637 Credo anche che quantificare su eventuali variabili di tipo non cambi niente
638 visto che non abbiamo funzioni.
640 Se ammettiamo che i tipi dipendano da termini di tipo induttivo
643 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
644 \begin{thebibliography}{}
645 \bibitem{AL91}A.Asperti, G.Longo. Categories, Types and Structures.
646 Foundations of Computing, Cambrdidge University press, 1991.
647 \bibitem{Girard86}G.Y.Girard. The system F of variable types, fifteen
648 years later. Theoretical Computer Science 45, 1986.
649 \bibitem{Girard87}G.Y.Girard. Proof Theory and Logical Complexity.
650 Bibliopolis, Napoli, 1987.
651 \bibitem{GLT}G.Y.Girard, Y.Lafont, P.Tailor. Proofs and Types.
652 Cambridge Tracts in Theoretical Computer Science 7.Cambridge University
654 \bibitem{Godel58}K.G\"odel. \"Uber eine bisher noch nicht ben\"utzte Erweiterung
655 des finiten Standpunktes. Dialectica, 12, pp.34-38, 1958.
656 \bibitem{Godel90}K.G\"odel. Collected Works. Vol.II, Oxford University Press,
658 \bibitem{HS86}J.R.Hindley, J. P. Seldin. Introduction to Combinators and
659 Lambda-calculus, Cambridge University Press, 1986.
660 \bibitem{Howard68}W.A.Howard. Functional interpretation of bar induction
661 by bar recursion. Compositio Mathematica 20, pp.107-124. 1958
662 \bibitem{Howard80}W.A.Howard. The formulae-as-types notion of constructions.
663 in J.P.Seldin and j.R.Hindley editors, to H.B.Curry: Essays on Combinatory
664 Logic, Lambda calculus and Formalism. Acedemic Press, 1980.
665 \bibitem{Kleene45}S.C.Kleene. On the interpretation of intuitionistic
666 number theory. Journal of Symbolic Logic, n.10, pp.109-124, 1945.
667 \bibitem{Kreisel59} G.Kreisel. Interpretation of analysis by means of
668 constructive functionals of finite type. In. A.Heyting ed.
669 {\em Constructivity in mathematics}. North Holland, Amsterdam,1959.
670 \bibitem{Kreisel62} G.Kreisel. On weak completeness of intuitionistic
671 predicatelogic. Journal of Symbolic Logic 27, pp. 139-158. 1962.
672 \bibitem{Letouzey04}P.Letouzey. Programmation fonctionnelle
673 certifi\'ee; l'extraction
674 de programmes dans l'assistant Coq. Ph.D. Thesis, Universit\'e de
675 Paris XI-Orsay, 2004.
676 \bibitem{Loef}P.Martin-L\"of. Intuitionistic Type Theory.
677 Bibliopolis, Napoli, 1984.
678 \bibitem{Paulin87}C.Paulin-Mohring. Extraction de programme dans le Calcul de
679 Constructions. Ph.D. Thesis, Universit\'e de
681 \bibitem{Paulin89}C.Paulin-Mohring. Extracting $F_{\omega}$ programs
682 from proofs in the Calculus of Constructions. In proc. of the Sixteenth Annual
684 Principles of Programming Languages, Austin, January, ACML Press 1989.
685 \bibitem{Sch}K.Sch\"utte. Proof Theory. Grundlehren der mathematischen
686 Wissenschaften 225, Springer Verlag, Berlin, 1977.
687 \bibitem{Troelstra}A.S.Troelstra. Metamathemtical Investigation of
689 Arithmetic and Analysis. Lecture Notes in Mathematics 344, Springer Verlag,
691 \bibitem{TS}A.S.Troelstra, H.Schwichtenberg. Basic Proof Theory.
692 Cambridge Tracts in Theoretical Computer Science 43.Cambridge University
694 \bibitem{Werner}B.Werner. Une Th\'eorie des Constructions Inductives.
695 Ph.D.Thesis, Universit\'e de Paris 7, 1994.
698 \end{thebibliography}