-
-\subsection{$R_X : \sem{X_{ind}}$ and $R_X\R X_{ind}$}
-We have to compare the definition of $\square$ and $\vartriangle$
-since thay play the same role in constructing respectively $R_X$ and
-$X_{ind}$. If we assume $\alpha = \sem{Q}$ and we apply the $\sem$
-function to each righ side of the $\vartriangle$ definition we obtain
-exactly $\square$. The last two elements of the arrows $R_X$ and
-$X_{ind}$ are again the same up to $\sem$.
-
-questa non va bene, il caso base e' se il tipo del costruttore usa
-solo le prime 2 regole di delta, quello induttivo se usa ANCHE la
-terza...
-
-To prove that $R_X\R X_{ind}$ we must assume that for each $i$ index
-of a constructor of $X$, $f_i \R \vartriangle\{C(X)_i, c_i\}$ and we
-have to proove that for each $t:X$
-$$R_X~\overrightarrow{f}~t \R Q(t)$$.
-We proceede by induction on the type of the head constructor $c_i$ in $t$.
-The first base case is $c_i=X$ that, according to $\triangledown$,
-reduces in one
-step to $f_i$ and by hypothesis we have $f_i \R \vartriangle\{X,
-c_i\}$. Unfolding $\vartriangle$ we have $f_i \R Q(c_i)$. The second
-base case is $c_i=\overrightarrow{\forall t:T}.X$ and is analoug to
-the first case.\\
-The inductive step is when we have one or more recursive aruments in
-$c_i$ and the induction hypothesis is that for each recursve argument
-$m$, $R_X~\overrightarrow{f}~m \R X \to Q$. Since $f_i \R
-\vartriangle\{C(X)_i, c_i\}$ and
-$R_X~\overrightarrow{f}~(c_i~\overrightarrow{m})$ reduces to
-$f_i~\overrightarrow{...}$
-
-
-
-
-
-
+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{Strong normalization of extended system T}
+Strong normalization for system T is a well know result\cite{GLT}
+that can be easily extended to System T with this kind of inductive
+types. The first thing we have to do is to extend the definition of
+neutral term to the terms not of the form $<u,v>$, $\lambda x.u$,
+$c_i~\vec{m}$.
+
+In conformity with the demonstration we are extending we call $\nu(t)$
+the length of the longest reduction path from $t$ and $\ell(t)$ the
+number of symbols in the normal form of $t$.
+
+For an inductive type $\ind\{c_1:C(X); \ldots ; c_n:C(X)\}$
+we have to prove that for each $i$,
+given a proper sequence of reducible arguments $\vec{m}$ and $\vec{f}$,
+$(c_i~\vec{m})$ and $\Rx~\vec{f}~(c_i~\vec{m})$ are reducible.
+
+First the simple case of constructors. If the constructor $c_i$ takes
+no arguments then it is already in normal form. If it takes
+$m_1,\ldots,m_n$ reducible arguments, then $\nu(c_i~\vec{m}) = max \{m_1,
+\ldots,m_n\}$ and so $c_i~\vec{m}$ is strongly nomalizable thus
+reducible for the definition of reducibility for base types.
+
+To show that $\Rx~\vec{f}~(c_i~\vec{m})$ is reducible we can use
+(\textbf{CR 3}) that states that if $t$ is neutral and every $t'$ obtained by
+executing one redex of $t$ is reducible, then $t$ is reducible.
+
+Now we have to show that each term that can be obtained by a
+reduction step is reducible. We can procede induction on
+$\Sigma\nu(f_i) + \nu(c_i~\vec{m}) +
+\ell(c_i~\vec{m})$ since we know by hypothesis that $\vec{f}$ and
+$(c_i~\vec{m})$ are reducible and consequently strongly normalizing.
+\\
+The base case is when $c_i$ takes no arguments and $\vec{f}$ are
+normal. In this case the only redex we can compute is
+$$\Rx~\vec{f}~c_i~\leadsto~f_i$$ that is reducible by hypothesis.
+\\
+The interesting inductive case is when $\vec{m}$ and $\vec{f}$ are
+normal, so the only reduction step we can execute is
+$$\Rx~\vec{f}~(c_i~\vec{m})~\leadsto~f_i~\vec{m}~\vec{(\Rx~\vec{f}~n)}$$
+where $\vec{n}$ are the recursive arguments of $c_i$ (here we wrote
+the recursive calls as the last parameters of $f_i$ just to lighten
+notation). Since $\ell(n_j)$ is less than $\ell(c_i~\vec{m})$ for
+every $j$ we can apply the inductive hypothesis and state that
+$\Rx~\vec{f}~n_j$ is reducible. Then by definition of reducibility of
+the arrow types and by the hypothesis that $f_i$ and $\vec{m}$ are
+reducible, we obtain that $$f_i~\vec{m}~\vec{(\Rx~\vec{f}~n)}$$ is
+reducible.
+\\
+All other cases, when we execute a redex in $\vec{m}$ or $\vec{f}$,
+are straightforward applications of the induction hypothesis.
+
+
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+\section{Improving inductive types}
+It is possible to parametrise 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
+
+
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%