is not among the major achievements of the author (see e.g. \cite{Girard87}),
the result has been extensively investigated and there is a wide
literature on the
-topic (see e.g. \cite{Howard68,Troelstra,Girard87}.
+topic (see e.g. \cite{Troelstra,HS86,Girard87}, just to mention textbooks,
+and the bibliography therein).
A different, more neglected, but for many respects much more
direct relation between Peano (or Heyting) Arithmetics and
from the proof.
In spite of the simplicity and the elegance of the proof, it is extremely
difficult to find a modern discussion of this result; the most recent
-exposition we are aware of is in the encyclopedic (typewritten!) work by
-Troelstra \cite{Troelstra} (pp.213-229). Even modern introductory books
+exposition we are aware of is in the encyclopedic work by
+Troelstra \cite{Troelstra} (pp.213-229) going back to thirty years ago.
+Even modern introductory books
to Type Theory and Proof Theory devoting much space to system T
such as \cite{GLT} and \cite{TS} surprisingly leave out this simple and
-illuminating result. Both \cite{GLT} and \cite{TS}
+illuminating result. Both the previous textbooks
prefer to focus on higher order arithmetics and its relation with
Girard's System $F$ \cite{Girard86}, but the technical complexity and
the didactical value of the two proofs is not comparable: when you
\end{itemize}
-%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+
+\noindent
+{\bf example}\\
+Let us prove the following principle of well founded induction:
+\[(\forall m.(\forall p. p < m \to P p) \to P m) \to \forall n.P n\]
+In the following proof we shall make use of proof-terms, since we finally
+wish to extract the computational content; we leave to reader the easy
+check that the proof object describes the usual and natural proof
+of the statement.
+
+We assume to have already proved the following lemmas (having trivial
+realizers):\\
+\[L: \lambda b.p < 0 \to \bot\]
+\[M: \lambda p,q,n.p < q \to q \le (S n) \to p \le n \]
+Let us assume $h: \forall m.(\forall p. p < m \to P p) \to P m$.
+We prove by induction on n that $\forall q. q \le n \to P q$.
+For $n=0$, we get a proof of $P \;0$ by
+\[ B: \lambda q.\lambda \_:q \le n. h \;0\;
+(\lambda p.\lambda k:p < 0. false\_ind \;(L\;p\; k)) \]
+In the inductive case, we must prove that, for any n,
+\[(\forall q. q \le n \to P q) \to (\forall q. q \le S n \to P q)\]
+Assume $h1: \forall q. q \le n \to P q$ and
+$h2: q \le S \;n$. Let us prove $\forall p. p < q \to P p$.
+If $h3: p < q$ then $(M\; p\; q\; n\; h3\; h2): p \le n$, hence
+$h1 \;p \; (M\; p\; q\; n\; h3\; h2): P p$.\\
+In conclusion, the proof of the
+inductive case is
+\[I: \lambda h1:\forall q. q \le n \to P\; q.\lambda q.\lambda h2:q \le S n.
+h \; q \; (\lambda p.\lambda h3:p < q.h1 \;p\; (M\; p\; q\; n\; h3\; h2)) \]
+(where $h$ is free in I).
+The full proof is
+\[ \lambda m.\lambda h: \forall m.(\forall p. p < m \to P p) \to P m.
+nat\_ind \;B \; I \;m\; (le\_n \; m) \]
+where $le\_n$ is a proof that $\forall n. n \le n$.\\
+Form the previous proof,after stripping terminal objects,
+and a bit of eta-contraction to make
+the term more readable, we extract the following term (types are omitted):
+
+\[R' = \lambda m.\lambda f.
+R\; (f \; O\; (\lambda q.*_A))\;
+(\lambda n\lambda g\lambda q.f \;q\;g)\;m \;m\]
+
+The intuition of this operator is the following: supose to
+have a recursive definition $h q = F[h]$ where $q:\N$ and
+$F[h]: A$. This defines a functional
+$f: \lambda q.\lambda g.F[g]: N\to(N\to A) \to A$, such that
+(morally) $h$ is the fixpoint of $f$. For instance,
+in the case of the fibonacci function, $f$ is
+\[\lambda q. \lambda g.
+if\; q = 0\;then\; 1\; else\; if\; q = 1\; then\; 1\; else\; g (q-1)+g (q-2)\]
+
+So $f$ build a new
+approximation of $h$ from the previous approximation $h$ taken
+as input. $R'$ precisely computes the mth-approximation starting
+from a dummy function $(\lambda q.*_A)$. Alternatively,
+you may look at $g$ as the ``history'' (curse of values) of $h$
+for all values less or equal to $q$; then $f$ extend $g$ to
+$q+1$.
+
\section{Inductive types}
The notation we will use is similar to the one used in
\cite{Werner} and \cite{Paulin89} but we prefer
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\begin{thebibliography}{}
+\bibitem{AL91}A.Asperti, G.Longo. Categories, Types and Structures.
+Foundations of Computing, Cambrdidge University press, 1991.
\bibitem{Girard86}G.Y.Girard. The system F of variable types, fifteen
years later. Theoretical Computer Science 45, 1986.
\bibitem{Girard87}G.Y.Girard. Proof Theory and Logical Complexity.
des finiten Standpunktes. Dialectica, 12, pp.34-38, 1958.
\bibitem{Godel90}K.G\"odel. Collected Works. Vol.II, Oxford University Press,
1990.
+\bibitem{HS86}J.R.Hindley, J. P. Seldin. Introduction to Combinators and
+Lambda-calculus, Cambridge University Press, 1986.
\bibitem{Howard68}W.A.Howard. Functional interpretation of bar induction
by bar recursion. Compositio Mathematica 20, pp.107-124. 1958
\bibitem{Howard80}W.A.Howard. The formulae-as-types notion of constructions.
in J.P.Seldin and j.R.Hindley editors, to H.B.Curry: Essays on Combinatory
Logic, Lambda calculus and Formalism. Acedemic Press, 1980.
+\bibitem{Kleene45}S.C.Kleene. On the interpretation of intuitionistic
+number theory. Journal of Symbolic Logic, n.10, pp.109-124, 1945.
\bibitem{Kreisel59} G.Kreisel. Interpretation of analysis by means of
constructive functionals of finite type. In. A.Heyting ed.
{\em Constructivity in mathematics}. North Holland, Amsterdam,1959.
projects / helm.git / blobdiff