1 \documentclass[times, 10pt,twocolumn, draft]{article}
4 \usepackage{amssymb,amsmath,mathrsfs,stmaryrd,amsthm}
13 \newcommand{\semT}[1]{\ensuremath{\llbracket #1 \rrbracket}}
14 \newcommand{\sem}[1]{\llbracket \ensuremath{#1} \rrbracket}
15 \newcommand{\pair}[2]{<\!#1,#2\!>}
16 \newcommand{\canonical}{\bot}
17 \newcommand{\R}{~\mathscr{R}~}
18 \newcommand{\N}{\,\mathbb{N}\,}
19 \newcommand{\B}{\,\mathbb{B}\,}
20 \newcommand{\NT}{\,\mathbb{N}\,}
21 \newcommand{\NH}{\,\mathbb{N}\,}
22 \renewcommand{\star}{\ast}
23 \renewcommand{\vec}{\overrightarrow}
24 \newcommand{\one}{{\bf 1}}
25 \newcommand{\mult}{\cdot}
26 \newcommand{\ind}{Ind(X)}
27 \newcommand{\indP}{Ind(\vec{P}~|~X)}
28 \newcommand{\Xind}{\ensuremath{X_{ind}}}
29 \newcommand{\XindP}{\ensuremath{X_{ind}}}
30 \renewcommand{\|}{\ensuremath{\quad | \quad}}
31 \newcommand{\triUP}{\ensuremath{\Delta}}
32 \newcommand{\triDOWN}{\ensuremath{\nabla}}
33 \newcommand{\Rx}{\ensuremath{R_X}}
35 \newtheorem{thm}{Theorem}[subsection]
37 \title{Modified Realizability and Inductive Types}
49 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
50 \Section{Introduction}
51 The characterization of the provable recursive functions of
52 Peano Arithmetic as the terms of system T is a well known
53 result of G\"odel \cite{Godel58,Godel90}. Although several authors acknowledge
54 that the functional interpretation of the Dialectica paper
55 is not among the major achievements of the author (see e.g. \cite{Girard87}),
56 the result has been extensively investigated and there is a wide
58 topic (see e.g. \cite{Troelstra,HS86,Girard87}, just to mention textbooks,
59 and the bibliography therein).
61 A different, more neglected, but for many respects much more
62 direct relation between Peano (or Heyting) Arithmetics and
63 G\"odel System T is provided
64 by the so called {\em modified realizability}. Modified realizability
65 was first introduced by Kreisel in \cite{Kreisel59} - although it will take you
66 a bit of effort to recognize it in the few lines of paragraph 3.52 -
67 and later in \cite{Kreisel62} under the name of generalized realizability.
68 The name of modified realizability seems to be due to Troelstra
70 - who contested Kreisel's name but unfortunately failed in proposing
71 a valid alternative; we shall reluctantly adopt this latter name
72 to avoid further confusion. Modified realizability is a typed variant of
73 realizability, essentially providing interpretations
74 of $HA^{\omega}$ into itself: each theorem is realized by a typed function
75 of system T, that also gives the actual computational content extracted
77 In spite of the simplicity and the elegance of the proof, it is extremely
78 difficult to find a modern discussion of this result; the most recent
79 exposition we are aware of is in the encyclopedic work by
80 Troelstra \cite{Troelstra} (pp.213-229) going back to thirty years ago.
81 Even modern introductory books
82 to Type Theory and Proof Theory devoting much space to system T
83 such as \cite{GLT} and \cite{TS} surprisingly leave out this simple and
84 illuminating result. Both the previous textbooks
85 prefer to focus on higher order arithmetics and its relation with
86 Girard's System $F$ \cite{Girard86}, but the technical complexity and
87 the didactical value of the two proofs is not comparable: when you
88 prove that the Induction Principle is realized by the recursor $R$
89 of system $T$ you catch a sudden gleam of understanding in the
90 students eyes; usually, the same does not happen when you show, say,
91 that the ``forgetful'' interpretation of the higher order predicate defining
92 the natural numbers is the system $F$ encoding
93 $\forall X.(X\to X) \to X \to X$ of $\N$.
94 Moreover, after a first period of enthusiasm, the impredicative
95 encoding of inductive types in Logical Frameworks has shown several
96 problems and limitations (see e.g. \cite{Werner} pp.24-25) mostly
97 solved by assuming inductive types as a primitive logical notion
98 (leading e.g. form the Calculus of Constructions to the Calculus
99 of Inductive Constructions - CIC). Even the extraction algorithm of
100 CIC, strictly based on realizability principles, and in a first time
101 still oriented towards System F \cite{Paulin87,Paulin89} has been
102 recently rewritten \cite{Letouzey04}
103 to take advantage of concrete types and pattern matching of ML-like
104 languages. Unfortunately, systems like the Calculus of Inductive
105 Constructions are so complex, from the logical point of view, to
106 substantially prevent a really neat theoretical exposition (at present,
108 even exists a truly complete consistency proofs covering all aspects
109 of such systems); moreover, not everybody may be interested in all the features
110 offered by these frameworks, from polymorphism to types depending on
111 proofs. Our program is to restart the analysis of logical systems with
112 primitive inductive types in a smooth way, starting form first order
113 logic and adding little by little small bits of logical power.
114 This paper is the first step in this direction.
116 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
117 \Section{G\"odel system T}
118 We shall use a variant of system T with three atomic types $\N$ (natural
119 numbers), $\B$ (booleans) and $\one$ (a terminal object), and two binary
120 type constructors $\times$ (product) and $\to$ (arrow type).
122 The terms of the language comprise the usual simply typed lambda terms
123 with explicit pairs, plus the following additional constants:
126 \item $true: \B$, $false:\B$, $D:A\to A \to \B \to A$
127 \item $O:\N$, $S:\N \to \N$, $R:A \to (A \to \N \to A) \to \N \to A$,
129 Redexes comprise $\beta$-reduction, projections,
130 and type specific reductions as reported in table \ref{tab:tredex}
134 \begin{tabular}{p{0.34\textwidth}r}
135 $\lambda x:U.M ~ N \leadsto M[N/x]$ & $(\beta)$ \\
136 $fst \pair{M}{N} \leadsto M$ & $(\pi_1)$ \\
137 $snd \pair{M}{N} \leadsto N$ & $(\pi_2)$ \\
138 $D~M~N~ true \leadsto M$ & $(D_{true})$ \\
139 $D~M~N~false \leadsto N$ & $(D_{false})$ \\
140 $R~M~F~ 0 \leadsto M$ & $(R_0)$ \\
141 $R~M~F~(S~n) \leadsto F~n~(R~M~F~n)$ & $(R_S)$ \\
142 $M \leadsto * ~~~~ $ for any M of type $\one$ & $(*)$
143 \end{tabular}\vspace{0.1cm}
145 \caption{\label{tab:tredex}Reduction rules for System T}
148 Note that using the well known isomorpshims
149 $\one \to A \cong A$, $A \to \one \cong \one$
150 and $A \times \one \cong A \cong \one\times A$ (see \cite{AL91}, pp.231-239)
151 we may always get rid of $\one$ (apart the trivial case).
152 The terminal object does not play a major role in our treatment, but
153 it allows to extract better algorithms. In particular we use it
154 to realize atomic proposition, and stripping out the terminal object using
155 the above isomorphisms gives a simple way of just keeping the truly
156 informative part of the algorithms.
158 \Section{Heyting's arithmetics}
163 \item $nat\_ind: P(0) \to (\forall x.P(x) \to P(S(x))) \to \forall x.P(x)$
164 \item $ex\_ind: (\forall x.P(x) \to Q) \to \exists x.P(x) \to Q$
165 \item $ex\_intro: \forall x.(P \to \exists x.P)$
166 \item $fst: P \land Q \to P$
167 \item $snd: P \land Q \to Q$
168 \item $conj: P \to Q \to P \land Q$
169 \item $false\_ind: \bot \to Q$
170 \item $discriminate:\forall x.0 = S(x) \to \bot$
171 \item $injS: \forall x,y.S(x) = S(y) \to x=y$
172 \item $plus\_O:\forall x.x+0=x$
173 \item $plus\_S:\forall x,y.x+S(y)=S(x+y)$
174 \item $times\_O:\forall x.x\mult0=0$
175 \item $times\_S:\forall x,y.x\mult S(y)=x+(x\mult y)$
179 {\bf Inference Rules}
181 say that ax:AX refers to the previous Axioms list...
183 %\hrule\vspace{0.1cm}
184 %\begin{tabular}{p{0.34\textwidth}r}
186 $$\Gamma, x:A, \Delta \vdash x:A ~~~ (Proj)$$
187 $$ \Gamma \vdash ax : AX~~~ (Const)$$
188 $$\frac{\Gamma,x:A \vdash M:Q}{\Gamma \vdash \lambda x:A.M: A \to Q} ~~~ (\to_i)$$
189 $$\frac{\Gamma \vdash M: A \to Q \hspace{0.5cm}\Gamma \vdash N: A}
190 {\Gamma \vdash M N: Q} ~~~ (\to_e)$$
191 $$\frac{\Gamma \vdash M:P}{\Gamma \vdash \lambda x:\N.M: \forall x.P}(*) ~~~
193 $$\frac{\Gamma \vdash M :\forall x.P}{\Gamma \vdash M t: P[t/x]}
196 %\end{tabular}\vspace{0.1cm}
198 %\caption{\label{tab:HArules}Inference rules}
202 % (\land_i)\frac{\Gamma \vdash M:A \hspace{1cm}\Gamma \vdash N:B}
203 % {\Gamma \vdash \pair{M}{N} : A \land B}
205 % (\land_{el})\frac{\Gamma \vdash A \land B}{\Gamma \vdash A}
207 % (\land_{er})\frac{\Gamma \vdash A \land B}{\Gamma \vdash B}
212 % (\exists_i)\frac{\Gamma \vdash P[t/x]}{\Gamma \vdash \exists x.P}\hspace{2cm}
213 % (\exists_e)\frac{\Gamma \vdash \exists x.P\hspace{1cm}\Gamma \vdash \forall x.P \to Q}
219 The formulae to types translation function $\sem{\cdot}$, see table
220 \ref{tab:formulae2types}, takes in input formulae in HA and returns
221 types in T. In table \ref{tab:structproof} we the proofs to terms
222 function for structured proofs. Axiom translation is reported in table
223 \ref{tab:axioms}. In table \ref{tab:canonical} we define how the
224 canoniac element is formed.
228 \begin{tabular}{p{0.21\textwidth}p{0.21\textwidth}}
229 $\sem{A} = \one$ if A is atomic &
230 $\sem{A \land B} = \sem{A}\times \sem{B}$ \\
231 $\sem{A \to B} = \sem{A}\to \sem{B}$ &
232 $\sem{\forall x:\N.P} = \N \to \sem{P}$ \\
233 $\sem{\exists x:\N.P} = \N \times \sem{P}$ &
234 \end{tabular}\vspace{0.1cm}
236 \caption{\label{tab:formulae2types}Formulae to types translation}
241 \begin{tabular}{p{0.20\textwidth}p{0.20\textwidth}}
242 $\semT{M N} = \semT{M} \semT{N}$ &
243 $\semT{M t} = \semT{M} \semT{t}$ \\
244 \multicolumn{2}{l}{$\semT{\lambda x:A.M} = \lambda x:\sem{A}.\semT{M}$} \\
245 \multicolumn{2}{l}{$\semT{\lambda x:\N.M} = \lambda x:\N.\semT{M}$}
246 \end{tabular}\vspace{0.1cm}
248 \caption{\label{tab:structproof}Structured proofs}
253 \begin{tabular}{l}%{0.47\textwidth}p{0.47\textwidth}}
254 $\sem{fst} = \pi_1$\\
255 $\sem{snd} = \pi_2$\\
256 $\sem{conj} = \lambda x:\sem{P}.\lambda y:\sem{Q}.\pair{x}{y}$\\
257 $\sem{false\_ind} = \canonical_{\sem{Q}}$\\
258 $\sem{discriminate} = \lambda \_:\N.\lambda \_:\one.\star$\\
259 $\sem{injS}= \lambda \_:\N. \lambda \_:\N.\lambda \_:\one.\star$\\
260 $\sem{plus\_O} = \sem{times\_O} = \lambda \_:\N.\star$\\
261 $\sem{nat\_ind} = R$ \\
262 $\sem{plus\_S} = \sem{times\_S} = \lambda \_:\N. \lambda \_:\N.\star$ \\
263 $\sem{ex\_intro} = \lambda x:\N.\lambda f:\sem{P}.\pair{x}{f}$ \\
264 $\sem{ex\_ind} = \lambda f:(\N \to \sem{P} \to \sem{Q}).$\\
265 $\qquad\lambda p:\N\times \sem{P}.f~(fst~p)~(snd~p)$
266 \end{tabular}\vspace{0.1cm}
268 \caption{\label{tab:axioms}Axioms translation}
273 \begin{tabular}{l}%p{0.23\textwidth}p{0.23\textwidth}}
274 $\canonical_\one = \lambda x:\one.x$ \\
275 $\canonical_N = \lambda x:\one.0$ \\
276 $\canonical_{U\times V} = \lambda x:\one.\pair{\canonical_{U}
277 x}{\canonical_{V} x}$ \\
278 $\canonical_{U\to V} = \lambda x:\one.\lambda \_:U. \canonical_{V} x$
279 \end{tabular}\vspace{0.1cm}
281 \caption{\label{tab:canonical}Canonical element}
285 \Section{Realizability}
286 The realizability relation is a relation $f \R P$ where $f: \sem{P}$, and
287 $P$ is a closed formula.
290 \item $\neg (\star \R \bot)$
291 \item $* \R (t_1=t_2)$ iff $t_1=t_2$ is true ...
292 \item $\pair{f}{g} \R (P\land Q)$ iff $f \R P$ and $g \R Q$
293 \item $f \R (P\to Q)$ iff for any $m$ such that $m \R P$, $(f \,m) \R Q$
294 \item $f \R (\forall x.P)$ iff for any natural number $n$ $(f n) \R P[\underline{n}/x]$
295 \item $\pair{n}{g}\R (\exists x.P)$ iff $g \R P[\underline{n}/x]$
297 %We need to generalize the notion of realizability to sequents.
298 %Given a sequent $B_1, \ldots, B_n \vdash A$ with free variables in
299 %$\vec{x} = x_1,\ldots, x_m$, we say that $f \R B1, \ldots, B_n \vdash A$ iff
300 %forall natural numbers $n_1, \ldots, n_m$,
301 %if forall $i \in {1,\ldots,n}$
302 %$m_i \R B_i[\vec{\underline{n}}/\vec{x}]$ then
303 %$$f <m_1, \ldots, m_n> \R A[\vec{\underline{n}}/\vec{x}]$$.
306 We need to generalize the notion of realizability to sequents.\\
307 Let $\vec{x} = FV_{\N}( B_1, \ldots, B_n, P)$ a vector of variables of type
308 $\N$ that occur free in $B_1, \ldots, B_n, P$. Let $\vec{b:B}$ the vector
309 $b_1:B_1, \ldots, b_n:B_n$.\\
310 We say that $f \R B_1, \ldots, B_n \vdash A:P$ iff
311 $$\lambda \vec{x:\N}. \lambda \vec{b:B}.f \R
312 \forall \vec{x}. B_1 \to \ldots \to B_n \to P$$
313 Note that $\forall \vec{x}. B_1 \to \ldots \to B_n \to P$ is a closed formula,
314 so we can use the previous definition of realizability on it.
317 We proceed to prove that all axioms $ax:Ax$ are realized by $\sem{ax}$.
321 We must prove that the recursion schema $R$ realizes the induction principle.
322 To this aim we must prove that for any $a$ and $f$ such that $a \R P(0)$ and
323 $f \R \forall x.(P(x) \to P(S(x)))$, and any natural number $n$, $(R \,a \,f
324 \,n) \R P(\underline{n})$.\\
325 We proceed by induction on n.\\
326 If $n=O$, $(R \,a \,f \,O) = a$ and by hypothesis $a \R P(0)$.\\
327 Suppose by induction that
328 $(R \,a \,f \,n) \R P(\underline{n})$, and let us prove that the relation
329 still holds for $n+1$. By definition
330 $(R \,a \,f \,(n+1)) = f \,n \,(R \,a \,f \,n)$,
331 and since $f \R \forall x.(P(x) \to P(S(x)))$,
332 $(f n (R a f n)) \R P(S(\underline{n}))=P(\underline{n+1})$.
335 We must prove that $$\underline{ex\_ind} \R (\forall x:(P x)
336 \to Q) \to (\exists x:(P x)) \to Q$$ Following the definition of $\R$ we have
337 to prove that given\\ $f~\R~\forall~x:((P~x)~\to~Q)$ and
338 $p~\R~\exists~x:(P~x)$, then $\underline{ex\_ind}~f~p \R Q$.\\
339 $p$ is a couple $\pair{n_p}{g_p}$ such that $g_p \R P[\underline{n_p}/x]$, while
340 $f$ is a function such that forall $n$ and for all $m \R P[\underline{n}/x]$
341 then $f~n~m \R Q$ (note that $x$ is not free in $Q$ so $[\underline{n}/x]$
343 Expanding the definition of $\underline{ex\_ind}$, $fst$
344 and $snd$ we obtain $f~n_p~g_p$ that we know is in relation $\R$ with $Q$
345 since $g_p \R P[\underline{n_p}/x]$.
349 $$\lambda x:\N.\lambda f:\sem{P}.\pair{x}{f} \R \forall x.(P\to\exists x.P(x)$$
350 that leads to prove that for each n
351 $\underline{ex\_into}~n \R (P\to\exists x.P(x))[\underline{n}/x]$.\\
352 Evaluating the substitution we have
353 $\underline{ex\_into}~n \R (P[\underline{n}/x]\to\exists x.P(x))$.\\
354 Again by definition of $\R$ we have to prove that given a
355 $m \R P[\underline{n}/x]$ then $\underline{ex\_into}~n~m \R \exists x.P(x)$.
356 Expanding the definition of $\underline{ex\_intro}$ we have
357 $\pair{n}{m} \R \exists x.P(x)$ that is true since $m \R P[\underline{n}/x]$.
360 We have to prove that $\pi_1 \R P \land Q \to P$, that is equal to proving
361 that for each $m \R P \land Q$ then $\pi_1~m \R P$ .
362 $m$ must be a couple $\pair{f_m}{g_m}$ such that $f_m \R P$ and $g_m \R Q$.
363 So we conclude that $\pi_1~m$ reduces to $f_m$ that is in relation $\R$
366 \item $snd$. The same for $fst$.
369 We have to prove that
370 $$\lambda x:\sem{P}. \lambda y:\sem{Q}.\pair{x}{y}\R P \to Q \to P \land Q$$
371 Following the definition of $\R$ we have to show that
372 for each $m \R P$ and for each $n \R Q$ then
373 $(\lambda x:\sem{P}. \lambda y:\sem{Q}.\pair{x}{y})~m~n \R P \land Q$.\\
374 This is the same of $\pair{m}{n} \R P \land Q$ that is verified since
375 $m \R P$ and $n \R Q$.
379 We have to prove that $\bot_{\sem{Q}} \R \bot \to Q$.
380 Trivial, since there is no $m \R \bot$.
382 \item $discriminate$.
383 Since there is no $n$ such that $0 = S n$ is true... \\
384 $\underline{discriminate}~n \R 0 = S~\underline{n} \to \bot$ for each n.
387 We have to prove that for each $n_1$ and $n_2$\\
388 $\lambda \_:\N. \lambda \_:\N.\lambda \_:\one.*~n_1~n_2 \R
389 (S(x)=S(y)\to x=y)[n_1/x][n_2/y]$.\\
390 We assume that $m \R S(n_1)=S(n_2)$ and we have to show that
391 $\lambda \_:\N. \lambda \_:\N.\lambda \_:\one.*~n_1~n_2~m$ that reduces to
392 $*$ is in relation $\R$ with $n_1=n_2$. Since in the standard model of
393 natural numbers $S(n_1)=S(n_2)$ implies $n_1=n_2$ we have that
397 Since in the standard model for natural numbers $0$ is the neutral element
398 for addition $\lambda \_:\N.\star \R \forall x.x + 0 = x$.
401 In the standard model of natural numbers the addition of two numbers is the
402 operation of counting the second starting from the first. So
403 $$\lambda \_:\N. \lambda \_:\N. \star \R \forall x,y.x+S(y)=S(x+y)$$.
406 Since in the standard model for natural numbers $0$ is the absorbing element
407 for multiplication $\lambda \_:\N.\star \R \forall x.x \mult 0 = 0$.
410 In the standard model of natural numbers the multiplications of two
411 numbers is the operation of adding the first to himself a number of times
412 equal to the second number. So
413 $$\lambda \_:\N. \lambda \_:\N. \star \R \forall x,y.x+S(y)=S(x+y)$$.
420 Let us prove the following principle of well founded induction:
421 \[(\forall m.(\forall p. p < m \to P~p) \to P~m) \to \forall n.P~n\]
422 In the following proof we shall make use of proof-terms, since we finally
423 wish to extract the computational content; we leave to reader the easy
424 check that the proof object describes the usual and natural proof
427 We assume to have already proved the following lemmas (having trivial
429 \[L : \forall p, q.p < q \to q \le 0 \to \bot\]
430 \[M : \forall p,q,n.p < q \to q \le (S n) \to p \le n \]
431 Let us assume $h : \forall m.(\forall p. p < m \to P~p) \to P~m$.
432 We prove by induction on $n$ that $\forall q. q \le n \to P~q$.
433 For $n=0$, we get a proof of $P ~q$ by
435 B & \equiv & \lambda q.\lambda h_0:q \le 0. h ~q~ \nonumber\\
436 & & \quad (\lambda p.\lambda k:p < q. false\_ind ~(L~p~q~k~h_0)) \nonumber
438 In the inductive case, we must prove that, for any $n$,
439 \[(\forall q. q \le n \to P~q) \to (\forall q. q \le S n \to P~q)\]
440 Assume $h_1: \forall q. q \le n \to P q$ and
441 $h_2: q \le S ~n$. Let us prove $\forall p. p < q \to P~p$.
442 If $h_3: p < q$ then $(M~ p~ q~ n~ h_3~ h_2): p \le n$, hence
443 $h_1 ~p ~ (M~ p~ q~ n~ h_3~ h_2): P~p$.\\
444 In conclusion, the proof of the
447 I & \equiv & \lambda n.\lambda h_1:\forall q. q \le n \to P~ q.\lambda q.\lambda h_2:q \le S n. \nonumber\\
448 & & \quad h ~ q ~ (\lambda p.\lambda h_3:p < q.h_1 ~p~ (M~ p~ q~ n~ h_3~ h_2))
451 (where $h$ is free in I).
454 & \lambda h:\forall m.(\forall p. p < m\to P~p)\to P~m.\lambda m. &\nonumber\\
455 & \quad nat\_ind ~B ~ I ~m~m~ (le\_n ~ m) & \nonumber
458 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$.\\
459 Form the previous proof,after stripping terminal objects,
460 and a bit of eta-contraction to make
461 the term more readable, we extract the following term (types are omitted):
463 \[R' \equiv \lambda f.\lambda m.
464 R~ (\lambda n.f ~n~ (\lambda q.*))~
465 (\lambda n\lambda g\lambda q.f ~q~g)~m ~m\]
467 The intuition of this operator is the following: supose to
468 have a recursive definition $h q = F[h]$ where $q:\N$ and
469 $F[h]: A$. This defines a functional
470 $f: \lambda q.\lambda g.F[g]: N\to(N\to A) \to A$, such that
471 (morally) $h$ is the fixpoint of $f$. For instance,
472 in the case of the fibonacci function, $f$ is
474 fibo & \equiv & \lambda q. \lambda g. if~ q = 0~then~ 1~ else \nonumber\\
475 & & \quad if~ q = 1~ then~ 1~ else ~ g (q-1)+g (q-2) \nonumber
479 approximation of $h$ from the previous approximation $h$ taken
480 as input. $R'$ precisely computes the mth-approximation starting
481 from a dummy function $(\lambda q.*_A)$. Alternatively,
482 you may look at $g$ as the ``history'' (curse of values) of $h$
483 for all values less or equal to $q$; then $f$ extend $g$ to
486 Let's compute for example
488 R'~fibo~2 & \leadsto &
489 R~ (\lambda n.fibo ~n~ (\lambda q.*))~
490 (\lambda n\lambda g\lambda q.fibo ~q~g)~2 ~2\nonumber\\
492 (\lambda n\lambda g\lambda q.fibo ~q~g)~1~
494 (\lambda n.fibo ~n~ (\lambda q.*))~
495 (\lambda n\lambda g\lambda q.fibo ~q~g)~1)~
500 (\lambda n.fibo ~n~ (\lambda q.*))~
501 (\lambda n\lambda g\lambda q.fibo ~q~g)~1)~
505 ((\lambda n\lambda g\lambda q.fibo ~q~g)~0~
507 (\lambda n.fibo ~n~ (\lambda q.*))~
508 (\lambda n\lambda g\lambda q.fibo ~q~g)~0))~
514 (\lambda n.fibo ~n~ (\lambda q.*))~
515 (\lambda n\lambda g\lambda q.fibo ~q~g)~0)
520 (\lambda n.fibo ~n~ (\lambda q.*)))2
523 fibo~2~(\lambda q.fibo ~q~ (\lambda n.fibo ~n~ (\lambda q.*))) \nonumber\\
525 (\lambda q.fibo ~q~ (\lambda n.fibo ~n~ (\lambda q.*))) 1 +
526 (\lambda q.fibo ~q~ (\lambda n.fibo ~n~ (\lambda q.*))) 0 \nonumber\\
528 fibo ~1~ (\lambda n.fibo ~n~ (\lambda q.*)) +
529 fibo ~0~ (\lambda n.fibo ~n~ (\lambda q.*)) \nonumber\\
533 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...
536 n non serve perche' c'e' una relazione logica di n con q,
537 in particolare $q <= Sn$ ... quindi $q < n$ (lemma M)...
538 e quindi posso usare come history $< n$ una history $< q$.
539 il $\lambda h2$ essendo $[[q <= Sn]]$ = 1 viene scartata.
541 se si spiega come array viene decente... forse. lunedi' provo a scrivere
544 \Section{Inductive types}
545 The notation we will use is similar to the one used in
546 \cite{Werner} and \cite{Paulin89} but we prefer
547 giving a label to each constructor and use that label instead of the
548 longer $Constr(n,\ind\{\ldots\})$ to indicate the $n^{th}$ constructor.
549 We adopt the vector notation to make things more readable.
550 $\vec{m}$ has to be intended as $m_1~\ldots~m_n$ where $n$ may
551 be equal to 0 (we use $m_1~\vec{m}$ when we want to give a
552 name to the first $m$ and assert $n>0$). If the vector notation is
553 used inside an arrow type it has a slightly different meaning,
554 $A \to \vec{B} \to C$ is a shortcut for
555 $A \to B_1 \to \ldots \to B_n \to C$.
557 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
558 \SubSection{Extensions to the logic framework}
559 To talk about arbitrary inductive types (and not hard coded natural numbers) we
560 have to extend a bit our framework.
562 First we admit quantification over inductive types $T$, thus $\forall x:T.A$
563 and $\exists x:T.A$ are allowed. Then rules 4 and 5 of the $\sem{\cdot}$
564 definition are replaced by $\sem{\forall x:T.P} = T \to \sem{P}$ and
565 $\sem{\exists x:T.P} = T \times \sem{P}$.
567 For each inductive type we will describe the formation rules and the
568 corresponding induction principle schema.
570 Symmetrically we have to extend System T with arbitrary inductive types and
571 we will see how theyr recursors are defined in the following sections.
573 The definition of $\R$ is modified substituting each occurrence of $\N$ with
574 a generic inductive type $T$.
576 %%%%%%%%%%%%%%%%%%%%%%%%%%%%
577 \SubSection{Type definition}
578 $$\ind\{c_1:C(X); \ldots ; c_n:C(X)\}$$
579 $$C(X) ::= X \| T \to C(X) \| X \to C(X)$$
580 In the second case we mean $T \neq X$.
582 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
583 \SubSection{Induction principle}
584 The induction principle for an inductive type $X$ and a predicate $Q$
585 is a constant with the following type
586 $$\Xind:\vec{\triUP\{C(X), c\}} \to \forall t:X.Q(t)$$
587 $\triUP$ takes a constructor type $C(X)$ and a term $c$ (initially $c$ is a
588 constructor of X, and $c:C(X)$) and is defined by recursion as follows:
590 \triUP\{X, c\} & = & Q(c) \nonumber\\
591 \triUP\{T \to C(X), c\} & = &
592 \forall m:T.\triUP\{C(X),c~m\} \nonumber\\
593 \triUP\{X \to C(X), c\} & = &
594 \forall t:X.Q(t) \to \triUP\{C(X), c~t\} \nonumber
597 %%%%%%%%%%%%%%%%%%%%%
598 \SubSection{Recursor}
599 %\SubSubSection{Type}
600 The type of the recursor $\Rx$ on an inductive type $X$ is
601 $$\Rx : \vec{\square\{C(X)\}} \to X \to \alpha$$
602 $\square$ is defined by recursion on the constructor type $C(X)$.
604 \square\{X\} & = & \alpha \nonumber \\
605 \square\{T \to C(X)\} & = & T \to \square\{C(X)\}\nonumber \\
606 \square\{X \to C(X)\} & = & X \to \alpha \to \square\{C(X)\}\nonumber
608 %\SubSubSection{Reduction rules}
610 $$\Rx~\vec{f}~(c_i~\vec{m}) \leadsto
611 \triDOWN\{C(X)_i, f_i, \vec{m}\}$$
612 $\triDOWN$ takes a constructor type $C(X)$, a term $f$
613 (of type $\square\{C(X)\}$) and is defined by recursion as follows:
615 \triDOWN\{X, f, \} & = & f\nonumber \\
616 \triDOWN\{T \to C(X), f, m_1~\vec{m}\} & = &
617 \triDOWN\{C(X), f~m_1, \vec{m}\}\nonumber \\
618 \triDOWN\{X \to C(X), f, m_1~\vec{m}\} & = &
619 \triDOWN\{C(X), f~m_1~(\Rx~\vec{f}~m_1),
622 We assume $\Rx~\vec{f}~(c_i~\vec{m})$ is well typed, so in the first case we
623 can omit $\vec{m}$ since it is an empty sequence.
625 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
626 \SubSection{Realizability of the induction principle}
627 Once we have inductive types and their induction principle we want to show that
628 the recursor $\Rx$ realizes $\Xind$, that is that $\Rx$ has type
629 $\sem{\Xind}$ and is in relation $\R$ with $\Xind$.
631 \begin{thm}$\Rx : \sem{\Xind}$\end{thm}
633 We have to compare the definition of $\square$ and $\triUP$
634 since they play the same role in constructing respectively the types of
636 $\Xind$. If we assume $\alpha = \sem{Q}$ and we apply the $\sem{\cdot}$
637 function to each right side of the $\triUP$ definition we obtain
638 exactly $\square$. The last two elements of the arrows $\Rx$ and
639 $\Xind$ are again the same up to $\sem{\cdot}$.
642 \begin{thm}$\Rx\R \Xind$\end{thm}
644 To prove that $\Rx\R \Xind$ we must assume that for each $i$ index
645 of a constructor of $X$, $f_i \R \triUP\{C(X)_i, c_i\}$ and we
646 have to prove that for each $t:X$
647 $$\Rx~\vec{f}~t \R Q(t)$$
649 We proceed by induction on the structure of $t$.
651 The base case is when the
652 type of the head constructor of $t$ has no recursive arguments (i.e. the type
653 is generated using only the first two rules $C(X)$), so
654 $(\Rx~\vec{f}~(c_i~\vec{m}))$ reduces in one step to $(f_i~\vec{m})$. $f_i$
655 realizes $\triUP\{C(X)_i, c_i\}$ by assumption and since we are in the base
656 case $\triUP\{C(X)_i, c_i\}$ is of the form $\vec{\forall t:T}.Q(c_i~\vec{t})$.
657 Thus $f_i~\vec{m} \R Q(c_i~\vec{m})$.
659 In the induction step we have as induction hypothesis that for each recursive
660 argument $t_i$ of the head constructor $c_i$, $r_i\equiv
661 \Rx~\vec{f}~t_i \R Q(t_i)$. By the third rule of $\triDOWN$ we obtain the reduct
662 $f_i~\vec{m}~\vec{t~r}$ (here we write first all the non recursive arguments,
663 then all the recursive one. In general they can be mixed and the proof is
664 exactly the same but the notation is really heavier). We know by hypothesis
665 that $f_i \R \triUP\{C(X)_i, c_i\} \equiv \vec{\forall m:T}.\vec{\forall
666 t:X.Q(t)} \to Q(c_i~\vec{m}~\vec{t})$, thus $f_i~\vec{m}~\vec{t~r} \R
667 Q(c_i~\vec{m}~\vec{t})$.
669 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
670 \Section{Strong normalization of extended system T}
671 Strong normalization for system T is a well know result\cite{GLT}
672 that can be easily extended to System T with this kind of inductive
673 types. The first thing we have to do is to extend the definition of
674 neutral term to the terms not of the form $<u,v>$, $\lambda x.u$,
677 In conformity with the demonstration we are extending we call $\nu(t)$
678 the length of the longest reduction path from $t$ and $\ell(t)$ the
679 number of symbols in the normal form of $t$.
681 For an inductive type $\ind\{c_1:C(X); \ldots ; c_n:C(X)\}$
682 we have to prove that for each $i$,
683 given a proper sequence of reducible arguments $\vec{m}$ and $\vec{f}$,
684 $(c_i~\vec{m})$ and $\Rx~\vec{f}~(c_i~\vec{m})$ are reducible.
686 First the simple case of constructors. If the constructor $c_i$ takes
687 no arguments then it is already in normal form. If it takes
688 $m_1,\ldots,m_n$ reducible arguments, then $\nu(c_i~\vec{m}) = max \{m_1,
689 \ldots,m_n\}$ and so $c_i~\vec{m}$ is strongly nomalizable thus
690 reducible for the definition of reducibility for base types.
692 To show that $\Rx~\vec{f}~(c_i~\vec{m})$ is reducible we can use
693 (\textbf{CR 3}) that states that if $t$ is neutral and every $t'$ obtained by
694 executing one redex of $t$ is reducible, then $t$ is reducible.
696 Now we have to show that each term that can be obtained by a
697 reduction step is reducible. We can procede induction on
698 $\Sigma\nu(f_i) + \nu(c_i~\vec{m}) +
699 \ell(c_i~\vec{m})$ since we know by hypothesis that $\vec{f}$ and
700 $(c_i~\vec{m})$ are reducible and consequently strongly normalizing.
702 The base case is when $c_i$ takes no arguments and $\vec{f}$ are
703 normal. In this case the only redex we can compute is
704 $$\Rx~\vec{f}~c_i~\leadsto~f_i$$ that is reducible by hypothesis.
706 The interesting inductive case is when $\vec{m}$ and $\vec{f}$ are
707 normal, so the only reduction step we can execute is
708 $$\Rx~\vec{f}~(c_i~\vec{m})~\leadsto~f_i~\vec{m}~\vec{(\Rx~\vec{f}~n)}$$
709 where $\vec{n}$ are the recursive arguments of $c_i$ (here we wrote
710 the recursive calls as the last parameters of $f_i$ just to lighten
711 notation). Since $\ell(n_j)$ is less than $\ell(c_i~\vec{m})$ for
712 every $j$ we can apply the inductive hypothesis and state that
713 $\Rx~\vec{f}~n_j$ is reducible. Then by definition of reducibility of
714 the arrow types and by the hypothesis that $f_i$ and $\vec{m}$ are
715 reducible, we obtain that $$f_i~\vec{m}~\vec{(\Rx~\vec{f}~n)}$$ is
718 All other cases, when we execute a redex in $\vec{m}$ or $\vec{f}$,
719 are straightforward applications of the induction hypothesis.
722 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
723 \Section{Improving inductive types}
724 It is possible to parametrise inductive types over other inductive types
725 without much difficulties since the type $T$ in $C(X)$ is free. Both the
726 recursor and the induction principle are schemas, parametric over $T$.
728 Possiamo anche definire $X_{\vec{P}}\equiv Ind(P|X)={c_i : C(P|X)}$ e poi
729 fare variare $T$ su $\vec{P}$, ma non ottengo niente di meglio.
731 Credo anche che quantificare su eventuali variabili di tipo non cambi niente
732 visto che non abbiamo funzioni.
734 Se ammettiamo che i tipi dipendano da termini di tipo induttivo
737 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
738 \bibliographystyle{latex8}
739 %\bibliography{latex8}
741 \begin{thebibliography}{}
742 \bibitem{AL91}A.Asperti, G.Longo. Categories, Types and Structures.
743 Foundations of Computing, Cambrdidge University press, 1991.
744 \bibitem{Girard86}G.Y.Girard. The system F of variable types, fifteen
745 years later. Theoretical Computer Science 45, 1986.
746 \bibitem{Girard87}G.Y.Girard. Proof Theory and Logical Complexity.
747 Bibliopolis, Napoli, 1987.
748 \bibitem{GLT}G.Y.Girard, Y.Lafont, P.Tailor. Proofs and Types.
749 Cambridge Tracts in Theoretical Computer Science 7.Cambridge University
751 \bibitem{Godel58}K.G\"odel. \"Uber eine bisher noch nicht ben\"utzte Erweiterung
752 des finiten Standpunktes. Dialectica, 12, pp.34-38, 1958.
753 \bibitem{Godel90}K.G\"odel. Collected Works. Vol.II, Oxford University Press,
755 \bibitem{HS86}J.R.Hindley, J. P. Seldin. Introduction to Combinators and
756 Lambda-calculus, Cambridge University Press, 1986.
757 \bibitem{Howard68}W.A.Howard. Functional interpretation of bar induction
758 by bar recursion. Compositio Mathematica 20, pp.107-124. 1958
759 \bibitem{Howard80}W.A.Howard. The formulae-as-types notion of constructions.
760 in J.P.Seldin and j.R.Hindley editors, to H.B.Curry: Essays on Combinatory
761 Logic, Lambda calculus and Formalism. Acedemic Press, 1980.
762 \bibitem{Kleene45}S.C.Kleene. On the interpretation of intuitionistic
763 number theory. Journal of Symbolic Logic, n.10, pp.109-124, 1945.
764 \bibitem{Kreisel59} G.Kreisel. Interpretation of analysis by means of
765 constructive functionals of finite type. In. A.Heyting ed.
766 {\em Constructivity in mathematics}. North Holland, Amsterdam,1959.
767 \bibitem{Kreisel62} G.Kreisel. On weak completeness of intuitionistic
768 predicatelogic. Journal of Symbolic Logic 27, pp. 139-158. 1962.
769 \bibitem{Letouzey04}P.Letouzey. Programmation fonctionnelle
770 certifi\'ee; l'extraction
771 de programmes dans l'assistant Coq. Ph.D. Thesis, Universit\'e de
772 Paris XI-Orsay, 2004.
773 \bibitem{Loef}P.Martin-L\"of. Intuitionistic Type Theory.
774 Bibliopolis, Napoli, 1984.
775 \bibitem{Paulin87}C.Paulin-Mohring. Extraction de programme dans le Calcul de
776 Constructions. Ph.D. Thesis, Universit\'e de
778 \bibitem{Paulin89}C.Paulin-Mohring. Extracting $F_{\omega}$ programs
779 from proofs in the Calculus of Constructions. In proc. of the Sixteenth Annual
781 Principles of Programming Languages, Austin, January, ACML Press 1989.
782 \bibitem{Sch}K.Sch\"utte. Proof Theory. Grundlehren der mathematischen
783 Wissenschaften 225, Springer Verlag, Berlin, 1977.
784 \bibitem{Troelstra}A.S.Troelstra. Metamathemtical Investigation of
786 Arithmetic and Analysis. Lecture Notes in Mathematics 344, Springer Verlag,
788 \bibitem{TS}A.S.Troelstra, H.Schwichtenberg. Basic Proof Theory.
789 Cambridge Tracts in Theoretical Computer Science 43.Cambridge University
791 \bibitem{Werner}B.Werner. Une Th\'eorie des Constructions Inductives.
792 Ph.D.Thesis, Universit\'e de Paris 7, 1994.
795 \end{thebibliography}