From 8a4dae57d41a2000778341240c823287eb15bb35 Mon Sep 17 00:00:00 2001
From: Andrea Asperti <andrea.asperti@unibo.it>
Date: Wed, 9 Nov 2005 11:06:26 +0000
Subject: [PATCH] Added an example (well founded recursion).

---
 helm/papers/system_T/t.tex | 60 +++++++++++++++++++++++++++++++++++++-
 1 file changed, 59 insertions(+), 1 deletion(-)

diff --git a/helm/papers/system_T/t.tex b/helm/papers/system_T/t.tex
index 14ead6b91..642c8c35d 100644
--- a/helm/papers/system_T/t.tex
+++ b/helm/papers/system_T/t.tex
@@ -337,7 +337,65 @@ We proceed to prove that all axioms $ax:Ax$ are realized by $\sem{ax}$.
   
 \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
-- 
2.39.2