added some stuff on inductive types

diff --git a/helm/papers/system_T/t.tex b/helm/papers/system_T/t.tex
index 2766e16ff5eb305546d4fa5717de0a69fbd5df2f..9a1f4ec25f442d05dc5d707b14f80db3bbe44572 100644 (file)
--- a/helm/papers/system_T/t.tex
+++ b/helm/papers/system_T/t.tex
@@ -13,6 +13,7 @@
 \renewcommand{\star}{\ast}
 \newcommand{\one}{\mathbb{1}}
 \renewcommand{\times}{\cdot}
+\newcommand{\ind}{Ind(X)}
 \title{Modified Realizability and Inductive Types}
 \author{...}
 
@@ -149,12 +150,13 @@ This paper is the first step in this direction.
 
 \section{Extraction}
 
+We have to extend systeem T with inductive types (and they recursors).
 \begin{itemize}
 \item $\sem{A} = 1$ if A is atomic
 \item $\sem{A \land B} = \sem{A}\times \sem{B}$
 \item $\sem{A \to B} = \sem{A}\to \sem{B}$
-\item $\sem{\forall x.P} = \N \to \sem{P}$
-\item $\sem{\exists x.P} = \N \times \sem{P}$
+\item $\sem{\forall x:T.P} = T \to \sem{P}$
+\item $\sem{\exists x:T.P} = T \times \sem{P}$
 \end{itemize}
 
 definition.
@@ -300,9 +302,105 @@ We proceed to prove that all axioms $ax:Ax$ are realized by $\sem{ax}$.
   equal to the second number. So
   $$\lambda \_:\N. \lambda \_:\N. \star \R \forall x,y.x+S(y)=S(x+y)$$.
   
-
 \end{itemize}
 
+\section{Inductive types}
+The notation we wwill use is similar to the one used in 
+\cite{Werner} and \cite{Paulin89} but we prefer
+giving a label to each contructor 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.
+$\overrightarrow{m}$ has to be intended as $m_1~\ldots~m_n$ where $n$ may
+be equal to 0 (we use $m_1~\overrightarrow{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 \overrightarrow{B} \to C$ is a shortcut for 
+$A \to B_1 \to \ldots \to B_n \to C$
+
+\subsection{Type definition}
+$$\ind\{c_1:C(X); \ldots ; c_n:C(X)\}$$
+$$C(X) ::= 
+X \quad | \quad 
+\forall m:T.C(X) \quad | \quad 
+t \to C(X)$$
+In the second case we need $(X \notin FV(T))$, while in the third we
+need that POS(X,t) holds.
+POS(X,t) is true iff t = X (POS has a meaning only for Higher Order...).
+
+
+\subsection{Induction principle}
+The induction principle for an inductive type $X$ and a predicate $Q$ 
+is a constant with the following type
+$$X_{ind}:\overrightarrow{\vartriangle\{C(X), c\}} \to \forall t:X.Q(x)$$
+$\vartriangle$ takes a constructor type and the is defined by recursion on $C(X)$.
+\begin{eqnarray}
+\vartriangle\{C(X), c\} & = & Q(c) \nonumber\\
+\vartriangle\{\forall t:T.C(X), c\} & = & 
+       \forall m:T.\vartriangle\{C(X),c~m\} \nonumber\\
+\vartriangle\{t \to C(X), c\} & = & 
+       \forall t:X.Q(t) \to \vartriangle\{C(X), c~t\} \nonumber
+\end{eqnarray}
+
+
+\subsection{Recursor}
+\subsubsection{Type}
+The type of the recursor $R_X$ on an inductive type $X$ is
+$$R_X : \overrightarrow{\square\{C(X)\}} \to X \to \alpha$$
+$\square$ is defined by recursion on the contructor type $C(X)$.
+\begin{eqnarray}
+\square\{X\} & = & \alpha \nonumber \\
+\square\{\forall m:T.C(X)\} & = & T \to \square\{C(X)\}\nonumber \\
+\square\{t \to C(X)\} & = & X \to \alpha \to \square\{C(X)\}\nonumber 
+\end{eqnarray}
+\subsubsection{Reduction rules}
+We say that 
+$$R_X~\overrightarrow{f}~(c_i~\overrightarrow{m}) \leadsto
+\triangledown\{C(X)_i, f_i, \overrightarrow{m}\}$$
+$\triangledown$ is defined by recursion on the constructor type $C(X)$.
+\begin{eqnarray}
+\triangledown\{X, f, \overrightarrow{m}\} & = & f\nonumber \\
+\triangledown\{\forall m:T.C(X), f, m_1~\overrightarrow{m}\} & = &
+       \triangledown\{C(X), f~m_1, \overrightarrow{m}\}\nonumber \\
+\triangledown\{t \to C(X), f, m_1~\overrightarrow{m}\} & = & 
+       \triangledown\{C(X), f~m_1~(R_X~\overrightarrow{f}~m_1),
+       \overrightarrow{m}\}\nonumber
+\end{eqnarray}
+
+\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{...}$
+
+
+
+
+
+
 \begin{thebibliography}{}
 \bibitem{Girard86}G.Y.Girard. The system F of variable types, fifteen
 years later. Theoretical Computer Science 45, 1986.