+
+\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 : \forall p, q.p < q \to q \le 0 \to \bot\]
+\[M : \forall 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 ~q$ by
+\[ B \equiv \lambda q.\lambda h_0:q \le 0. h ~q~
+(\lambda p.\lambda k:p < q. false\_ind ~(L~p~q~k~h_0)) \]
+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 $h_1: \forall q. q \le n \to P q$ and
+$h_2: q \le S ~n$. Let us prove $\forall p. p < q \to P~p$.
+If $h_3: p < q$ then $(M~ p~ q~ n~ h_3~ h_2): p \le n$, hence
+$h_1 ~p ~ (M~ p~ q~ n~ h_3~ h_2): P~p$.\\
+In conclusion, the proof of the
+inductive case is
+\[I \equiv \lambda n.\lambda h_1:\forall q. q \le n \to P~ q.\lambda q.\lambda h_2:q \le S n.
+h ~ q ~ (\lambda p.\lambda h_3:p < q.h_1 ~p~ (M~ p~ q~ n~ h_3~ h_2)) \]
+(where $h$ is free in I).
+The full proof is
+\[ \lambda h: \forall m.(\forall p. p < m \to P~p) \to P~m.\lambda m.
+nat\_ind ~B ~ I ~m~m~ (le\_n ~ m) \]
+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$.\\
+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' \equiv \lambda f.\lambda m.
+R~ (\lambda n.f ~n~ (\lambda q.*))~
+(\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
+\[fibo \equiv \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$.
+
+Let's compute for example
+\begin{eqnarray}
+R'~fibo~2 & \leadsto &
+ R~ (\lambda n.fibo ~n~ (\lambda q.*))~
+ (\lambda n\lambda g\lambda q.fibo ~q~g)~2 ~2\nonumber\\
+& \leadsto &
+ (\lambda n\lambda g\lambda q.fibo ~q~g)~1~
+ (R~
+ (\lambda n.fibo ~n~ (\lambda q.*))~
+ (\lambda n\lambda g\lambda q.fibo ~q~g)~1)~
+ 2 \nonumber\\
+& \leadsto &
+ \lambda q.fibo ~q~
+ (R~
+ (\lambda n.fibo ~n~ (\lambda q.*))~
+ (\lambda n\lambda g\lambda q.fibo ~q~g)~1)~
+ 2 \nonumber\\
+& \leadsto &
+ \lambda q.fibo ~q~
+ ((\lambda n\lambda g\lambda q.fibo ~q~g)~0~
+ (R~
+ (\lambda n.fibo ~n~ (\lambda q.*))~
+ (\lambda n\lambda g\lambda q.fibo ~q~g)~0))~
+ 2 \nonumber\\
+& \leadsto &
+ \lambda q.fibo ~q~
+ (\lambda q.fibo ~q~
+ (R~
+ (\lambda n.fibo ~n~ (\lambda q.*))~
+ (\lambda n\lambda g\lambda q.fibo ~q~g)~0)
+ )2 \nonumber\\
+& \leadsto &
+ \lambda q.fibo ~q~
+ (\lambda q.fibo ~q~
+ (\lambda n.fibo ~n~ (\lambda q.*)))2
+ \nonumber\\
+& \leadsto &
+ fibo~2~(\lambda q.fibo ~q~ (\lambda n.fibo ~n~ (\lambda q.*))) \nonumber\\
+& \leadsto &
+ (\lambda q.fibo ~q~ (\lambda n.fibo ~n~ (\lambda q.*))) 1 +
+ (\lambda q.fibo ~q~ (\lambda n.fibo ~n~ (\lambda q.*))) 0 \nonumber\\
+& \leadsto &
+ fibo ~1~ (\lambda n.fibo ~n~ (\lambda q.*)) +
+ fibo ~0~ (\lambda n.fibo ~n~ (\lambda q.*)) \nonumber\\
+& \leadsto &
+ 1 + 1 \nonumber
+\end{eqnarray}
+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...
+CAPITA CON csc:
+
+n non serve perche' c'e' una relazione logica di n con q,
+in particolare $q <= Sn$ ... quindi $q < n$ (lemma M)...
+e quindi posso usare come history $< n$ una history $< q$.
+il $\lambda h2$ essendo $[[q <= Sn]]$ = 1 viene scartata.
+
+se si spiega come array viene decente... forse. lunedi' provo a scrivere
+meglio.
+
+\section{Inductive types}
+The notation we will use is similar to the one used in
+\cite{Werner} and \cite{Paulin89} but we prefer
+giving a label to each constructor and use that label instead of the
+longer $Constr(n,\ind\{\ldots\})$ to indicate the $n^{th}$ constructor.
+We adopt the vector notation to make things more readable.
+$\vec{m}$ has to be intended as $m_1~\ldots~m_n$ where $n$ may
+be equal to 0 (we use $m_1~\vec{m}$ when we want to give a
+name to the first $m$ and assert $n>0$). If the vector notation is
+used inside an arrow type it has a slightly different meaning,
+$A \to \vec{B} \to C$ is a shortcut for
+$A \to B_1 \to \ldots \to B_n \to C$.
+
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+\subsection{Extensions to the logic framework}
+To talk about arbitrary inductive types (and not hard coded natural numbers) we
+have to extend a bit our framework.
+
+First we admit quantification over inductive types $T$, thus $\forall x:T.A$
+and $\exists x:T.A$ are allowed. Then rules 4 and 5 of the $\sem{\cdot}$
+definition are replaced by $\sem{\forall x:T.P} = T \to \sem{P}$ and
+$\sem{\exists x:T.P} = T \times \sem{P}$.
+
+For each inductive type we will describe the formation rules and the
+corresponding induction principle schema.
+
+Symmetrically we have to extend System T with arbitrary inductive types and
+we will see how theyr recursors are defined in the following sections.
+
+The definition of $\R$ is modified substituting each occurrence of $\N$ with
+a generic inductive type $T$.
+
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+\subsection{Type definition}
+$$\ind\{c_1:C(X); \ldots ; c_n:C(X)\}$$
+$$C(X) ::= X \| T \to C(X) \| X \to C(X)$$
+In the second case we mean $T \neq X$.
+
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+\subsection{Induction principle}
+The induction principle for an inductive type $X$ and a predicate $Q$
+is a constant with the following type
+$$\Xind:\vec{\triUP\{C(X), c\}} \to \forall t:X.Q(t)$$
+$\triUP$ takes a constructor type $C(X)$ and a term $c$ (initially $c$ is a
+constructor of X, and $c:C(X)$) and is defined by recursion as follows:
+\begin{eqnarray}
+\triUP\{X, c\} & = & Q(c) \nonumber\\
+\triUP\{T \to C(X), c\} & = &
+ \forall m:T.\triUP\{C(X),c~m\} \nonumber\\
+\triUP\{X \to C(X), c\} & = &
+ \forall t:X.Q(t) \to \triUP\{C(X), c~t\} \nonumber
+\end{eqnarray}
+
+%%%%%%%%%%%%%%%%%%%%%
+\subsection{Recursor}
+\subsubsection{Type}
+The type of the recursor $\Rx$ on an inductive type $X$ is
+$$\Rx : \vec{\square\{C(X)\}} \to X \to \alpha$$
+$\square$ is defined by recursion on the constructor type $C(X)$.
+\begin{eqnarray}
+\square\{X\} & = & \alpha \nonumber \\
+\square\{T \to C(X)\} & = & T \to \square\{C(X)\}\nonumber \\
+\square\{X \to C(X)\} & = & X \to \alpha \to \square\{C(X)\}\nonumber
+\end{eqnarray}
+\subsubsection{Reduction rules}
+We say that
+$$\Rx~\vec{f}~(c_i~\vec{m}) \leadsto
+\triDOWN\{C(X)_i, f_i, \vec{m}\}$$
+$\triDOWN$ takes a constructor type $C(X)$, a term $f$
+(of type $\square\{C(X)\}$) and is defined by recursion as follows:
+\begin{eqnarray}
+\triDOWN\{X, f, \} & = & f\nonumber \\
+\triDOWN\{T \to C(X), f, m_1~\vec{m}\} & = &
+ \triDOWN\{C(X), f~m_1, \vec{m}\}\nonumber \\
+\triDOWN\{X \to C(X), f, m_1~\vec{m}\} & = &
+ \triDOWN\{C(X), f~m_1~(\Rx~\vec{f}~m_1),
+ \vec{m}\}\nonumber
+\end{eqnarray}
+We assume $\Rx~\vec{f}~(c_i~\vec{m})$ is well typed, so in the first case we
+can omit $\vec{m}$ since it is an empty sequence.
+
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+\subsection{Realizability of the induction principle}
+Once we have inductive types and their induction principle we want to show that
+the recursor $\Rx$ realizes $\Xind$, that is that $\Rx$ has type
+$\sem{\Xind}$ and is in relation $\R$ with $\Xind$.
+
+\begin{thm}$\Rx : \sem{\Xind}$\end{thm}
+\begin{proof}
+We have to compare the definition of $\square$ and $\triUP$
+since they play the same role in constructing respectively the types of
+$\Rx$ and
+$\Xind$. If we assume $\alpha = \sem{Q}$ and we apply the $\sem{\cdot}$
+function to each right side of the $\triUP$ definition we obtain
+exactly $\square$. The last two elements of the arrows $\Rx$ and
+$\Xind$ are again the same up to $\sem{\cdot}$.
+\end{proof}
+
+\begin{thm}$\Rx\R \Xind$\end{thm}
+\begin{proof}
+To prove that $\Rx\R \Xind$ we must assume that for each $i$ index
+of a constructor of $X$, $f_i \R \triUP\{C(X)_i, c_i\}$ and we
+have to prove that for each $t:X$
+$$\Rx~\vec{f}~t \R Q(t)$$
+\noindent
+We proceed by induction on the structure of $t$.
+\\
+The base case is when the
+type of the head constructor of $t$ has no recursive arguments (i.e. the type
+is generated using only the first two rules $C(X)$), so
+$(\Rx~\vec{f}~(c_i~\vec{m}))$ reduces in one step to $(f_i~\vec{m})$. $f_i$
+realizes $\triUP\{C(X)_i, c_i\}$ by assumption and since we are in the base
+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 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
+that $f_i \R \triUP\{C(X)_i, c_i\} \equiv \vec{\forall m:T}.\vec{\forall
+t:X.Q(t)} \to Q(c_i~\vec{m}~\vec{t})$, thus $f_i~\vec{m}~\vec{t~r} \R
+Q(c_i~\vec{m}~\vec{t})$.
+\end{proof}
+
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+\section{Improoving inductive types}
+It is possible to parametrize inductive types over other inductive types
+without much difficulties since the type $T$ in $C(X)$ is free. Both the
+recursor and the induction principle are schemas, parametric over $T$.
+
+Possiamo anche definire $X_{\vec{P}}\equiv Ind(P|X)={c_i : C(P|X)}$ e poi
+fare variare $T$ su $\vec{P}$, ma non ottengo niente di meglio.
+
+Credo anche che quantificare su eventuali variabili di tipo non cambi niente
+visto che non abbiamo funzioni.
+
+Se ammettiamo che i tipi dipendano da termini di tipo induttivo
+
+
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%