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.1cm} \Gamma, x:A, \Delta \vdash x:A
177 (Const)\hspace{0.1cm} \Gamma \vdash ax : AX
181 (\to_i)\hspace{0.1cm}\frac{\Gamma,x:A \vdash M:Q}{\Gamma \vdash \lambda x:A.M: A \to Q} \hspace{2cm}
182 (\to_e)\hspace{0.1cm}\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.1cm}\frac{\Gamma \vdash M:P}{\Gamma \vdash
197 \lambda x:\N.M: \forall x.P}(*) \hspace{2cm}
198 (\forall_e)\hspace{0.1cm}\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 $\sem{\cdot}$, see table
211 \ref{tab:formulae2types}, takes in input formulae in HA and returns
212 types in T. In table \ref{tab:structproof} we the proofs to terms
213 function for structured proofs. Axiom translation is reported in table
214 \ref{tab:axioms}. In table \ref{tab:canonical} we define how the
215 canoniac element is formed.
219 \begin{tabular}{p{0.47\textwidth}p{0.47\textwidth}}
220 $\sem{A} = \one$ if A is atomic &
221 $\sem{A \land B} = \sem{A}\times \sem{B}$ \\
222 $\sem{A \to B} = \sem{A}\to \sem{B}$ &
223 $\sem{\forall x:\N.P} = \N \to \sem{P}$ \\
224 $\sem{\exists x:\N.P} = \N \times \sem{P}$ &
225 \end{tabular}\vspace{0.1cm}
227 \caption{\label{tab:formulae2types}Formulae to types translation}
232 \begin{tabular}{p{0.47\textwidth}p{0.47\textwidth}}
233 $\semT{M N} = \semT{M} \semT{N}$ &
234 $\semT{\lambda x:A.M} = \lambda x:\sem{A}.\semT{M}$ \\
235 $\semT{\lambda x:\N.M} = \lambda x:\N.\semT{M}$ &
236 $\semT{M t} = \semT{M} \semT{t}$
237 \end{tabular}\vspace{0.1cm}
239 \caption{\label{tab:structproof}Structured proofs}
244 \begin{tabular}{p{0.47\textwidth}p{0.47\textwidth}}
246 $\sem{snd} = \pi_2$\\
247 $\sem{conj} = \lambda x:\sem{P}.\lambda y:\sem{Q}.\pair{x}{y}$&
248 $\sem{false\_ind} = \canonical_{\sem{Q}}$\\
249 $\sem{discriminate} = \lambda \_:\N.\lambda \_:\one.\star$&
250 $\sem{injS}= \lambda \_:\N. \lambda \_:\N.\lambda \_:\one.\star$\\
251 $\sem{plus\_O} = \sem{times\_O} = \lambda \_:\N.\star$&
252 $\sem{nat\_ind} = R$ \\
254 $\sem{plus\_S} = \sem{times\_S} = \lambda \_:\N. \lambda \_:\N.\star$
257 $\sem{ex\_intro} = \lambda x:\N.\lambda f:\sem{P}.\pair{x}{f}$
261 \lambda f:(\N \to \sem{P} \to \sem{Q}).
262 \lambda p:\N\times \sem{P}.f~(fst~p)~(snd~p)$.
264 \end{tabular}\vspace{0.1cm}
266 \caption{\label{tab:axioms}Axioms translation}
271 \begin{tabular}{p{0.47\textwidth}p{0.47\textwidth}}
272 $\canonical_\one = \lambda x:\one.x$ &
273 $\canonical_N = \lambda x:\one.0$ \\
274 $\canonical_{U\times V} = \lambda x:\one.\pair{\canonical_{U}
275 x}{\canonical_{V} x}$ &
276 $\canonical_{U\to V} = \lambda x:\one.\lambda \_:U. \canonical_{V} x$
277 \end{tabular}\vspace{0.1cm}
279 \caption{\label{tab:canonical}Canonical element}
283 \section{Realizability}
284 The realizability relation is a relation $f \R P$ where $f: \sem{P}$, and
285 $P$ is a closed formula.
288 \item $\neg (\star \R \bot)$
289 \item $* \R (t_1=t_2)$ iff $t_1=t_2$ is true ...
290 \item $\pair{f}{g} \R (P\land Q)$ iff $f \R P$ and $g \R Q$
291 \item $f \R (P\to Q)$ iff for any $m$ such that $m \R P$, $(f \,m) \R Q$
292 \item $f \R (\forall x.P)$ iff for any natural number $n$ $(f n) \R P[\underline{n}/x]$
293 \item $\pair{n}{g}\R (\exists x.P)$ iff $g \R P[\underline{n}/x]$
295 %We need to generalize the notion of realizability to sequents.
296 %Given a sequent $B_1, \ldots, B_n \vdash A$ with free variables in
297 %$\vec{x} = x_1,\ldots, x_m$, we say that $f \R B1, \ldots, B_n \vdash A$ iff
298 %forall natural numbers $n_1, \ldots, n_m$,
299 %if forall $i \in {1,\ldots,n}$
300 %$m_i \R B_i[\vec{\underline{n}}/\vec{x}]$ then
301 %$$f <m_1, \ldots, m_n> \R A[\vec{\underline{n}}/\vec{x}]$$.
304 We need to generalize the notion of realizability to sequents.\\
305 Let $\vec{x} = FV_{\N}( B_1, \ldots, B_n, P)$ a vector of variables of type
306 $\N$ that occur free in $B_1, \ldots, B_n, P$. Let $\vec{b:B}$ the vector
307 $b_1:B_1, \ldots, b_n:B_n$.\\
308 We say that $f \R B_1, \ldots, B_n \vdash A:P$ iff
309 $$\lambda \vec{x:\N}. \lambda \vec{b:B}.f \R
310 \forall \vec{x}. B_1 \to \ldots \to B_n \to P$$
311 Note that $\forall \vec{x}. B_1 \to \ldots \to B_n \to P$ is a closed formula,
312 so we can use the previous definition of realizability on it.
315 We proceed to prove that all axioms $ax:Ax$ are realized by $\sem{ax}$.
319 We must prove that the recursion schema $R$ realizes the induction principle.
320 To this aim we must prove that for any $a$ and $f$ such that $a \R P(0)$ and
321 $f \R \forall x.(P(x) \to P(S(x)))$, and any natural number $n$, $(R \,a \,f
322 \,n) \R P(\underline{n})$.\\
323 We proceed by induction on n.\\
324 If $n=O$, $(R \,a \,f \,O) = a$ and by hypothesis $a \R P(0)$.\\
325 Suppose by induction that
326 $(R \,a \,f \,n) \R P(\underline{n})$, and let us prove that the relation
327 still holds for $n+1$. By definition
328 $(R \,a \,f \,(n+1)) = f \,n \,(R \,a \,f \,n)$,
329 and since $f \R \forall x.(P(x) \to P(S(x)))$,
330 $(f n (R a f n)) \R P(S(\underline{n}))=P(\underline{n+1})$.
333 We must prove that $$\underline{ex\_ind} \R (\forall x:(P x)
334 \to Q) \to (\exists x:(P x)) \to Q$$ Following the definition of $\R$ we have
335 to prove that given\\ $f~\R~\forall~x:((P~x)~\to~Q)$ and
336 $p~\R~\exists~x:(P~x)$, then $\underline{ex\_ind}~f~p \R Q$.\\
337 $p$ is a couple $\pair{n_p}{g_p}$ such that $g_p \R P[\underline{n_p}/x]$, while
338 $f$ is a function such that forall $n$ and for all $m \R P[\underline{n}/x]$
339 then $f~n~m \R Q$ (note that $x$ is not free in $Q$ so $[\underline{n}/x]$
341 Expanding the definition of $\underline{ex\_ind}$, $fst$
342 and $snd$ we obtain $f~n_p~g_p$ that we know is in relation $\R$ with $Q$
343 since $g_p \R P[\underline{n_p}/x]$.
347 $$\lambda x:\N.\lambda f:\sem{P}.\pair{x}{f} \R \forall x.(P\to\exists x.P(x)$$
348 that leads to prove that for each n
349 $\underline{ex\_into}~n \R (P\to\exists x.P(x))[\underline{n}/x]$.\\
350 Evaluating the substitution we have
351 $\underline{ex\_into}~n \R (P[\underline{n}/x]\to\exists x.P(x))$.\\
352 Again by definition of $\R$ we have to prove that given a
353 $m \R P[\underline{n}/x]$ then $\underline{ex\_into}~n~m \R \exists x.P(x)$.
354 Expanding the definition of $\underline{ex\_intro}$ we have
355 $\pair{n}{m} \R \exists x.P(x)$ that is true since $m \R P[\underline{n}/x]$.
358 We have to prove that $\pi_1 \R P \land Q \to P$, that is equal to proving
359 that for each $m \R P \land Q$ then $\pi_1~m \R P$ .
360 $m$ must be a couple $\pair{f_m}{g_m}$ such that $f_m \R P$ and $g_m \R Q$.
361 So we conclude that $\pi_1~m$ reduces to $f_m$ that is in relation $\R$
364 \item $snd$. The same for $fst$.
367 We have to prove that
368 $$\lambda x:\sem{P}. \lambda y:\sem{Q}.\pair{x}{y}\R P \to Q \to P \land Q$$
369 Following the definition of $\R$ we have to show that
370 for each $m \R P$ and for each $n \R Q$ then
371 $(\lambda x:\sem{P}. \lambda y:\sem{Q}.\pair{x}{y})~m~n \R P \land Q$.\\
372 This is the same of $\pair{m}{n} \R P \land Q$ that is verified since
373 $m \R P$ and $n \R Q$.
377 We have to prove that $\bot_{\sem{Q}} \R \bot \to Q$.
378 Trivial, since there is no $m \R \bot$.
380 \item $discriminate$.
381 Since there is no $n$ such that $0 = S n$ is true... \\
382 $\underline{discriminate}~n \R 0 = S~\underline{n} \to \bot$ for each n.
385 We have to prove that for each $n_1$ and $n_2$\\
386 $\lambda \_:\N. \lambda \_:\N.\lambda \_:\one.*~n_1~n_2 \R
387 (S(x)=S(y)\to x=y)[n_1/x][n_2/y]$.\\
388 We assume that $m \R S(n_1)=S(n_2)$ and we have to show that
389 $\lambda \_:\N. \lambda \_:\N.\lambda \_:\one.*~n_1~n_2~m$ that reduces to
390 $*$ is in relation $\R$ with $n_1=n_2$. Since in the standard model of
391 natural numbers $S(n_1)=S(n_2)$ implies $n_1=n_2$ we have that
395 Since in the standard model for natural numbers $0$ is the neutral element
396 for addition $\lambda \_:\N.\star \R \forall x.x + 0 = x$.
399 In the standard model of natural numbers the addition of two numbers is the
400 operation of counting the second starting from the first. So
401 $$\lambda \_:\N. \lambda \_:\N. \star \R \forall x,y.x+S(y)=S(x+y)$$.
404 Since in the standard model for natural numbers $0$ is the absorbing element
405 for multiplication $\lambda \_:\N.\star \R \forall x.x \mult 0 = 0$.
408 In the standard model of natural numbers the multiplications of two
409 numbers is the operation of adding the first to himself a number of times
410 equal to the second number. So
411 $$\lambda \_:\N. \lambda \_:\N. \star \R \forall x,y.x+S(y)=S(x+y)$$.
418 Let us prove the following principle of well founded induction:
419 \[(\forall m.(\forall p. p < m \to P~p) \to P~m) \to \forall n.P~n\]
420 In the following proof we shall make use of proof-terms, since we finally
421 wish to extract the computational content; we leave to reader the easy
422 check that the proof object describes the usual and natural proof
425 We assume to have already proved the following lemmas (having trivial
427 \[L : \forall p, q.p < q \to q \le 0 \to \bot\]
428 \[M : \forall p,q,n.p < q \to q \le (S n) \to p \le n \]
429 Let us assume $h : \forall m.(\forall p. p < m \to P~p) \to P~m$.
430 We prove by induction on $n$ that $\forall q. q \le n \to P~q$.
431 For $n=0$, we get a proof of $P ~q$ by
432 \[ B \equiv \lambda q.\lambda h_0:q \le 0. h ~q~
433 (\lambda p.\lambda k:p < q. false\_ind ~(L~p~q~k~h_0)) \]
434 In the inductive case, we must prove that, for any $n$,
435 \[(\forall q. q \le n \to P~q) \to (\forall q. q \le S n \to P~q)\]
436 Assume $h_1: \forall q. q \le n \to P q$ and
437 $h_2: q \le S ~n$. Let us prove $\forall p. p < q \to P~p$.
438 If $h_3: p < q$ then $(M~ p~ q~ n~ h_3~ h_2): p \le n$, hence
439 $h_1 ~p ~ (M~ p~ q~ n~ h_3~ h_2): P~p$.\\
440 In conclusion, the proof of the
442 \[I \equiv \lambda n.\lambda h_1:\forall q. q \le n \to P~ q.\lambda q.\lambda h_2:q \le S n.
443 h ~ q ~ (\lambda p.\lambda h_3:p < q.h_1 ~p~ (M~ p~ q~ n~ h_3~ h_2)) \]
444 (where $h$ is free in I).
446 \[ \lambda h: \forall m.(\forall p. p < m \to P~p) \to P~m.\lambda m.
447 nat\_ind ~B ~ I ~m~m~ (le\_n ~ m) \]
448 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$.\\
449 Form the previous proof,after stripping terminal objects,
450 and a bit of eta-contraction to make
451 the term more readable, we extract the following term (types are omitted):
453 \[R' \equiv \lambda f.\lambda m.
454 R~ (\lambda n.f ~n~ (\lambda q.*))~
455 (\lambda n\lambda g\lambda q.f ~q~g)~m ~m\]
457 The intuition of this operator is the following: supose to
458 have a recursive definition $h q = F[h]$ where $q:\N$ and
459 $F[h]: A$. This defines a functional
460 $f: \lambda q.\lambda g.F[g]: N\to(N\to A) \to A$, such that
461 (morally) $h$ is the fixpoint of $f$. For instance,
462 in the case of the fibonacci function, $f$ is
463 \[fibo \equiv \lambda q. \lambda g.
464 if~ q = 0~then~ 1~ else~ if~ q = 1~ then~ 1~ else~ g (q-1)+g (q-2)\]
467 approximation of $h$ from the previous approximation $h$ taken
468 as input. $R'$ precisely computes the mth-approximation starting
469 from a dummy function $(\lambda q.*_A)$. Alternatively,
470 you may look at $g$ as the ``history'' (curse of values) of $h$
471 for all values less or equal to $q$; then $f$ extend $g$ to
474 Let's compute for example
476 R'~fibo~2 & \leadsto &
477 R~ (\lambda n.fibo ~n~ (\lambda q.*))~
478 (\lambda n\lambda g\lambda q.fibo ~q~g)~2 ~2\nonumber\\
480 (\lambda n\lambda g\lambda q.fibo ~q~g)~1~
482 (\lambda n.fibo ~n~ (\lambda q.*))~
483 (\lambda n\lambda g\lambda q.fibo ~q~g)~1)~
488 (\lambda n.fibo ~n~ (\lambda q.*))~
489 (\lambda n\lambda g\lambda q.fibo ~q~g)~1)~
493 ((\lambda n\lambda g\lambda q.fibo ~q~g)~0~
495 (\lambda n.fibo ~n~ (\lambda q.*))~
496 (\lambda n\lambda g\lambda q.fibo ~q~g)~0))~
502 (\lambda n.fibo ~n~ (\lambda q.*))~
503 (\lambda n\lambda g\lambda q.fibo ~q~g)~0)
508 (\lambda n.fibo ~n~ (\lambda q.*)))2
511 fibo~2~(\lambda q.fibo ~q~ (\lambda n.fibo ~n~ (\lambda q.*))) \nonumber\\
513 (\lambda q.fibo ~q~ (\lambda n.fibo ~n~ (\lambda q.*))) 1 +
514 (\lambda q.fibo ~q~ (\lambda n.fibo ~n~ (\lambda q.*))) 0 \nonumber\\
516 fibo ~1~ (\lambda n.fibo ~n~ (\lambda q.*)) +
517 fibo ~0~ (\lambda n.fibo ~n~ (\lambda q.*)) \nonumber\\
521 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...
524 n non serve perche' c'e' una relazione logica di n con q,
525 in particolare $q <= Sn$ ... quindi $q < n$ (lemma M)...
526 e quindi posso usare come history $< n$ una history $< q$.
527 il $\lambda h2$ essendo $[[q <= Sn]]$ = 1 viene scartata.
529 se si spiega come array viene decente... forse. lunedi' provo a scrivere
532 \section{Inductive types}
533 The notation we will use is similar to the one used in
534 \cite{Werner} and \cite{Paulin89} but we prefer
535 giving a label to each constructor and use that label instead of the
536 longer $Constr(n,\ind\{\ldots\})$ to indicate the $n^{th}$ constructor.
537 We adopt the vector notation to make things more readable.
538 $\vec{m}$ has to be intended as $m_1~\ldots~m_n$ where $n$ may
539 be equal to 0 (we use $m_1~\vec{m}$ when we want to give a
540 name to the first $m$ and assert $n>0$). If the vector notation is
541 used inside an arrow type it has a slightly different meaning,
542 $A \to \vec{B} \to C$ is a shortcut for
543 $A \to B_1 \to \ldots \to B_n \to C$.
545 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
546 \subsection{Extensions to the logic framework}
547 To talk about arbitrary inductive types (and not hard coded natural numbers) we
548 have to extend a bit our framework.
550 First we admit quantification over inductive types $T$, thus $\forall x:T.A$
551 and $\exists x:T.A$ are allowed. Then rules 4 and 5 of the $\sem{\cdot}$
552 definition are replaced by $\sem{\forall x:T.P} = T \to \sem{P}$ and
553 $\sem{\exists x:T.P} = T \times \sem{P}$.
555 For each inductive type we will describe the formation rules and the
556 corresponding induction principle schema.
558 Symmetrically we have to extend System T with arbitrary inductive types and
559 we will see how theyr recursors are defined in the following sections.
561 The definition of $\R$ is modified substituting each occurrence of $\N$ with
562 a generic inductive type $T$.
564 %%%%%%%%%%%%%%%%%%%%%%%%%%%%
565 \subsection{Type definition}
566 $$\ind\{c_1:C(X); \ldots ; c_n:C(X)\}$$
567 $$C(X) ::= X \| T \to C(X) \| X \to C(X)$$
568 In the second case we mean $T \neq X$.
570 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
571 \subsection{Induction principle}
572 The induction principle for an inductive type $X$ and a predicate $Q$
573 is a constant with the following type
574 $$\Xind:\vec{\triUP\{C(X), c\}} \to \forall t:X.Q(t)$$
575 $\triUP$ takes a constructor type $C(X)$ and a term $c$ (initially $c$ is a
576 constructor of X, and $c:C(X)$) and is defined by recursion as follows:
578 \triUP\{X, c\} & = & Q(c) \nonumber\\
579 \triUP\{T \to C(X), c\} & = &
580 \forall m:T.\triUP\{C(X),c~m\} \nonumber\\
581 \triUP\{X \to C(X), c\} & = &
582 \forall t:X.Q(t) \to \triUP\{C(X), c~t\} \nonumber
585 %%%%%%%%%%%%%%%%%%%%%
586 \subsection{Recursor}
588 The type of the recursor $\Rx$ on an inductive type $X$ is
589 $$\Rx : \vec{\square\{C(X)\}} \to X \to \alpha$$
590 $\square$ is defined by recursion on the constructor type $C(X)$.
592 \square\{X\} & = & \alpha \nonumber \\
593 \square\{T \to C(X)\} & = & T \to \square\{C(X)\}\nonumber \\
594 \square\{X \to C(X)\} & = & X \to \alpha \to \square\{C(X)\}\nonumber
596 \subsubsection{Reduction rules}
598 $$\Rx~\vec{f}~(c_i~\vec{m}) \leadsto
599 \triDOWN\{C(X)_i, f_i, \vec{m}\}$$
600 $\triDOWN$ takes a constructor type $C(X)$, a term $f$
601 (of type $\square\{C(X)\}$) and is defined by recursion as follows:
603 \triDOWN\{X, f, \} & = & f\nonumber \\
604 \triDOWN\{T \to C(X), f, m_1~\vec{m}\} & = &
605 \triDOWN\{C(X), f~m_1, \vec{m}\}\nonumber \\
606 \triDOWN\{X \to C(X), f, m_1~\vec{m}\} & = &
607 \triDOWN\{C(X), f~m_1~(\Rx~\vec{f}~m_1),
610 We assume $\Rx~\vec{f}~(c_i~\vec{m})$ is well typed, so in the first case we
611 can omit $\vec{m}$ since it is an empty sequence.
613 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
614 \subsection{Realizability of the induction principle}
615 Once we have inductive types and their induction principle we want to show that
616 the recursor $\Rx$ realizes $\Xind$, that is that $\Rx$ has type
617 $\sem{\Xind}$ and is in relation $\R$ with $\Xind$.
619 \begin{thm}$\Rx : \sem{\Xind}$\end{thm}
621 We have to compare the definition of $\square$ and $\triUP$
622 since they play the same role in constructing respectively the types of
624 $\Xind$. If we assume $\alpha = \sem{Q}$ and we apply the $\sem{\cdot}$
625 function to each right side of the $\triUP$ definition we obtain
626 exactly $\square$. The last two elements of the arrows $\Rx$ and
627 $\Xind$ are again the same up to $\sem{\cdot}$.
630 \begin{thm}$\Rx\R \Xind$\end{thm}
632 To prove that $\Rx\R \Xind$ we must assume that for each $i$ index
633 of a constructor of $X$, $f_i \R \triUP\{C(X)_i, c_i\}$ and we
634 have to prove that for each $t:X$
635 $$\Rx~\vec{f}~t \R Q(t)$$
637 We proceed by induction on the structure of $t$.
639 The base case is when the
640 type of the head constructor of $t$ has no recursive arguments (i.e. the type
641 is generated using only the first two rules $C(X)$), so
642 $(\Rx~\vec{f}~(c_i~\vec{m}))$ reduces in one step to $(f_i~\vec{m})$. $f_i$
643 realizes $\triUP\{C(X)_i, c_i\}$ by assumption and since we are in the base
644 case $\triUP\{C(X)_i, c_i\}$ is of the form $\vec{\forall t:T}.Q(c_i~\vec{t})$.
645 Thus $f_i~\vec{m} \R Q(c_i~\vec{m})$.
647 In the induction step we have as induction hypothesis that for each recursive
648 argument $t_i$ of the head constructor $c_i$, $r_i\equiv
649 \Rx~\vec{f}~t_i \R Q(t_i)$. By the third rule of $\triDOWN$ we obtain the reduct
650 $f_i~\vec{m}~\vec{t~r}$ (here we write first all the non recursive arguments,
651 then all the recursive one. In general they can be mixed and the proof is
652 exactly the same but the notation is really heavier). We know by hypothesis
653 that $f_i \R \triUP\{C(X)_i, c_i\} \equiv \vec{\forall m:T}.\vec{\forall
654 t:X.Q(t)} \to Q(c_i~\vec{m}~\vec{t})$, thus $f_i~\vec{m}~\vec{t~r} \R
655 Q(c_i~\vec{m}~\vec{t})$.
657 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
658 \section{Strong normalization of extended system T}
659 Strong normalization for system T is a well know result\cite{GLT}
660 that can be easily extended to System T with this kind of inductive
661 types. The first thing we have to do is to extend the definition of
662 neutral term to the terms not of the form $<u,v>$, $\lambda x.u$,
665 In conformity with the demonstration we are extending we call $\nu(t)$
666 the length of the longest reduction path from $t$ and $\ell(t)$ the
667 number of symbols in the normal form of $t$.
669 For an inductive type $\ind\{c_1:C(X); \ldots ; c_n:C(X)\}$
670 we have to prove that for each $i$,
671 given a proper sequence of reducible arguments $\vec{m}$ and $\vec{f}$,
672 $(c_i~\vec{m})$ and $\Rx~\vec{f}~(c_i~\vec{m})$ are reducible.
674 First the simple case of constructors. If the constructor $c_i$ takes
675 no arguments then it is already in normal form. If it takes
676 $m_1,\ldots,m_n$ reducible arguments, then $\nu(c_i~\vec{m}) = max \{m_1,
677 \ldots,m_n\}$ and so $c_i~\vec{m}$ is strongly nomalizable thus
678 reducible for the definition of reducibility for base types.
680 To show that $\Rx~\vec{f}~(c_i~\vec{m})$ is reducible we can use
681 (\textbf{CR 3}) that states that if $t$ is neutral and every $t'$ obtained by
682 executing one redex of $t$ is reducible, then $t$ is reducible.
684 Now we have to show that each term that can be obtained by a
685 reduction step is reducible. We can procede induction on
686 $\Sigma\nu(f_i) + \nu(c_i~\vec{m}) +
687 \ell(c_i~\vec{m})$ since we know by hypothesis that $\vec{f}$ and
688 $(c_i~\vec{m})$ are reducible and consequently strongly normalizing.
690 The base case is when $c_i$ takes no arguments and $\vec{f}$ are
691 normal. In this case the only redex we can compute is
692 $$\Rx~\vec{f}~c_i~\leadsto~f_i$$ that is reducible by hypothesis.
694 The interesting inductive case is when $\vec{m}$ and $\vec{f}$ are
695 normal, so the only reduction step we can execute is
696 $$\Rx~\vec{f}~(c_i~\vec{m})~\leadsto~f_i~\vec{m}~\vec{(\Rx~\vec{f}~n)}$$
697 where $\vec{n}$ are the recursive arguments of $c_i$ (here we wrote
698 the recursive calls as the last parameters of $f_i$ just to lighten
699 notation). Since $\ell(n_j)$ is less than $\ell(c_i~\vec{m})$ for
700 every $j$ we can apply the inductive hypothesis and state that
701 $\Rx~\vec{f}~n_j$ is reducible. Then by definition of reducibility of
702 the arrow types and by the hypothesis that $f_i$ and $\vec{m}$ are
703 reducible, we obtain that $$f_i~\vec{m}~\vec{(\Rx~\vec{f}~n)}$$ is
706 All other cases, when we execute a redex in $\vec{m}$ or $\vec{f}$,
707 are straightforward applications of the induction hypothesis.
710 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
711 \section{Improving inductive types}
712 It is possible to parametrise inductive types over other inductive types
713 without much difficulties since the type $T$ in $C(X)$ is free. Both the
714 recursor and the induction principle are schemas, parametric over $T$.
716 Possiamo anche definire $X_{\vec{P}}\equiv Ind(P|X)={c_i : C(P|X)}$ e poi
717 fare variare $T$ su $\vec{P}$, ma non ottengo niente di meglio.
719 Credo anche che quantificare su eventuali variabili di tipo non cambi niente
720 visto che non abbiamo funzioni.
722 Se ammettiamo che i tipi dipendano da termini di tipo induttivo
725 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
726 \begin{thebibliography}{}
727 \bibitem{AL91}A.Asperti, G.Longo. Categories, Types and Structures.
728 Foundations of Computing, Cambrdidge University press, 1991.
729 \bibitem{Girard86}G.Y.Girard. The system F of variable types, fifteen
730 years later. Theoretical Computer Science 45, 1986.
731 \bibitem{Girard87}G.Y.Girard. Proof Theory and Logical Complexity.
732 Bibliopolis, Napoli, 1987.
733 \bibitem{GLT}G.Y.Girard, Y.Lafont, P.Tailor. Proofs and Types.
734 Cambridge Tracts in Theoretical Computer Science 7.Cambridge University
736 \bibitem{Godel58}K.G\"odel. \"Uber eine bisher noch nicht ben\"utzte Erweiterung
737 des finiten Standpunktes. Dialectica, 12, pp.34-38, 1958.
738 \bibitem{Godel90}K.G\"odel. Collected Works. Vol.II, Oxford University Press,
740 \bibitem{HS86}J.R.Hindley, J. P. Seldin. Introduction to Combinators and
741 Lambda-calculus, Cambridge University Press, 1986.
742 \bibitem{Howard68}W.A.Howard. Functional interpretation of bar induction
743 by bar recursion. Compositio Mathematica 20, pp.107-124. 1958
744 \bibitem{Howard80}W.A.Howard. The formulae-as-types notion of constructions.
745 in J.P.Seldin and j.R.Hindley editors, to H.B.Curry: Essays on Combinatory
746 Logic, Lambda calculus and Formalism. Acedemic Press, 1980.
747 \bibitem{Kleene45}S.C.Kleene. On the interpretation of intuitionistic
748 number theory. Journal of Symbolic Logic, n.10, pp.109-124, 1945.
749 \bibitem{Kreisel59} G.Kreisel. Interpretation of analysis by means of
750 constructive functionals of finite type. In. A.Heyting ed.
751 {\em Constructivity in mathematics}. North Holland, Amsterdam,1959.
752 \bibitem{Kreisel62} G.Kreisel. On weak completeness of intuitionistic
753 predicatelogic. Journal of Symbolic Logic 27, pp. 139-158. 1962.
754 \bibitem{Letouzey04}P.Letouzey. Programmation fonctionnelle
755 certifi\'ee; l'extraction
756 de programmes dans l'assistant Coq. Ph.D. Thesis, Universit\'e de
757 Paris XI-Orsay, 2004.
758 \bibitem{Loef}P.Martin-L\"of. Intuitionistic Type Theory.
759 Bibliopolis, Napoli, 1984.
760 \bibitem{Paulin87}C.Paulin-Mohring. Extraction de programme dans le Calcul de
761 Constructions. Ph.D. Thesis, Universit\'e de
763 \bibitem{Paulin89}C.Paulin-Mohring. Extracting $F_{\omega}$ programs
764 from proofs in the Calculus of Constructions. In proc. of the Sixteenth Annual
766 Principles of Programming Languages, Austin, January, ACML Press 1989.
767 \bibitem{Sch}K.Sch\"utte. Proof Theory. Grundlehren der mathematischen
768 Wissenschaften 225, Springer Verlag, Berlin, 1977.
769 \bibitem{Troelstra}A.S.Troelstra. Metamathemtical Investigation of
771 Arithmetic and Analysis. Lecture Notes in Mathematics 344, Springer Verlag,
773 \bibitem{TS}A.S.Troelstra, H.Schwichtenberg. Basic Proof Theory.
774 Cambridge Tracts in Theoretical Computer Science 43.Cambridge University
776 \bibitem{Werner}B.Werner. Une Th\'eorie des Constructions Inductives.
777 Ph.D.Thesis, Universit\'e de Paris 7, 1994.
780 \end{thebibliography}