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
case $\triUP\{C(X)_i, c_i\}$ is of the form $\vec{\forall t:T}.Q(c_i~\vec{t})$.
Thus $f_i~\vec{m} \R Q(c_i~\vec{m})$.
\\
-In the induction step we have as induction hypothesis that each recursive
-argument $t_i$ of the head constructor $c_i$ is realized by $r_i\equiv
-\Rx~\vec{f}~t_i$. By the third rule of $\triDOWN$ we obtain the reduct
+In the induction step we have as induction hypothesis that for each recursive
+argument $t_i$ of the head constructor $c_i$, $r_i\equiv
+\Rx~\vec{f}~t_i \R Q(t_i)$. By the third rule of $\triDOWN$ we obtain the reduct
$f_i~\vec{m}~\vec{t~r}$ (here we write first all the non recursive arguments,
then all the recursive one. In general they can be mixed and the proof is
exactly the same but the notation is really heavier). We know by hypothesis
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.
projects / helm.git / blobdiff