X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;ds=inline;f=helm%2Fpapers%2Fsystem_T%2Ft.tex;h=9d5622d2bb13bf799f66723d8f28450b57a0ffd9;hb=a7063fc0997a9d9eae6c329443e67ab92c4b6a0f;hp=7804118ab5a00d8284195acd07f3dc8460dba1be;hpb=82b5d7944ba0d238f696207cf4bb4c3549dabddd;p=helm.git

diff --git a/helm/papers/system_T/t.tex b/helm/papers/system_T/t.tex
index 7804118ab..9d5622d2b 100644
--- a/helm/papers/system_T/t.tex
+++ b/helm/papers/system_T/t.tex
@@ -172,14 +172,14 @@ informative part of the algorithms.
 say that ax:AX refers to the previous Axioms list...
 
 \[
-  (Proj)\hspace{0.2cm} \Gamma, x:A, \Delta \vdash x:A
+  (Proj)\hspace{0.1cm} \Gamma, x:A, \Delta \vdash x:A
   \hspace{2cm}
-  (Const)\hspace{0.2cm} \Gamma \vdash ax : AX
+  (Const)\hspace{0.1cm} \Gamma \vdash ax : AX
 \]
 
 \[ 
-   (\to_i)\hspace{0.2cm}\frac{\Gamma,x:A \vdash M:Q}{\Gamma \vdash \lambda x:A.M: A \to Q} \hspace{2cm}
-   (\to_e)\hspace{0.2cm}\frac{\Gamma \vdash M: A \to Q \hspace{1cm}\Gamma \vdash N: A}
+   (\to_i)\hspace{0.1cm}\frac{\Gamma,x:A \vdash M:Q}{\Gamma \vdash \lambda x:A.M: A \to Q} \hspace{2cm}
+   (\to_e)\hspace{0.1cm}\frac{\Gamma \vdash M: A \to Q \hspace{1cm}\Gamma \vdash N: A}
     {\Gamma \vdash M N: Q} 
 \]
 
@@ -193,9 +193,9 @@ say that ax:AX refers to the previous Axioms list...
 %\]
 
 \[ 
-   (\forall_i)\hspace{0.2cm}\frac{\Gamma \vdash M:P}{\Gamma \vdash 
+   (\forall_i)\hspace{0.1cm}\frac{\Gamma \vdash M:P}{\Gamma \vdash 
    \lambda x:\N.M: \forall x.P}(*) \hspace{2cm}
-   (\forall_e)\hspace{0.2cm}\frac{\Gamma \vdash M :\forall x.P}{\Gamma \vdash M t: P[t/x]} 
+   (\forall_e)\hspace{0.1cm}\frac{\Gamma \vdash M :\forall x.P}{\Gamma \vdash M t: P[t/x]} 
 \]
 
 
@@ -207,48 +207,78 @@ say that ax:AX refers to the previous Axioms list...
 
 \section{Extraction}
 
-The formulae to types translation function 
-$\sem{\cdot}$ takes in input formulae in HA and returns types in T.
-
-\begin{enumerate}
-\item $\sem{A} = \one$ 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:\N.P} = \N \to \sem{P}$
-\item $\sem{\exists x:\N.P} = \N \times \sem{P}$
-\end{enumerate}
-
-definition.
-For any type T of system T $\canonical_T: \one \to T$  is inductively defined as follows:
-\begin{enumerate}
-\item $\canonical_\one = \lambda x:\one.x$
-\item $\canonical_N = \lambda x:\one.0$
-\item $\canonical_{U\times V} = \lambda x:\one.\pair{\canonical_{U} x}{\canonical_{V} x}$
-\item $\canonical_{U\to V} = \lambda x:\one.\lambda \_:U. \canonical_{V} x$
-\end{enumerate}
+The formulae to types translation function $\sem{\cdot}$, see table
+\ref{tab:formulae2types}, takes in input formulae in HA and returns 
+types in T. In table \ref{tab:structproof} we the proofs to terms
+function for structured proofs. Axiom translation is reported in table 
+\ref{tab:axioms}. In table \ref{tab:canonical} we define how the
+canoniac element is formed.
+
+\begin{table}[!h]
+\hrule\vspace{0.1cm}
+\begin{tabular}{p{0.47\textwidth}p{0.47\textwidth}}
+ $\sem{A} = \one$ if A is atomic &
+ $\sem{A \land B} = \sem{A}\times \sem{B}$ \\
+ $\sem{A \to B} = \sem{A}\to \sem{B}$ &
+ $\sem{\forall x:\N.P} = \N \to \sem{P}$ \\
+ $\sem{\exists x:\N.P} = \N \times \sem{P}$ &
+\end{tabular}\vspace{0.1cm}
+\hrule
+\caption{\label{tab:formulae2types}Formulae to types translation}
+\end{table}
+
+\begin{table}[!h]
+\hrule\vspace{0.1cm}
+\begin{tabular}{p{0.47\textwidth}p{0.47\textwidth}}
+ $\semT{M N} = \semT{M} \semT{N}$ &
+ $\semT{\lambda x:A.M} = \lambda x:\sem{A}.\semT{M}$ \\
+ $\semT{\lambda x:\N.M} = \lambda x:\N.\semT{M}$ & 
+ $\semT{M t} = \semT{M} \semT{t}$
+\end{tabular}\vspace{0.1cm}
+\hrule
+\caption{\label{tab:structproof}Structured proofs}
+\end{table}
+
+\begin{table}[!h]
+\hrule\vspace{0.1cm}
+\begin{tabular}{p{0.47\textwidth}p{0.47\textwidth}}
+ $\sem{fst} = \pi_1$&
+ $\sem{snd} = \pi_2$\\
+ $\sem{conj} = \lambda x:\sem{P}.\lambda y:\sem{Q}.\pair{x}{y}$&
+ $\sem{false\_ind} = \canonical_{\sem{Q}}$\\
+ $\sem{discriminate} = \lambda \_:\N.\lambda \_:\one.\star$&
+ $\sem{injS}= \lambda \_:\N. \lambda \_:\N.\lambda \_:\one.\star$\\
+ $\sem{plus\_O} = \sem{times\_O} = \lambda \_:\N.\star$&
+ $\sem{nat\_ind} = R$ \\
+ \multicolumn{2}{l}{
+   $\sem{plus\_S} = \sem{times\_S} = \lambda \_:\N. \lambda \_:\N.\star$
+ }\\
+ \multicolumn{2}{l}{
+   $\sem{ex\_intro} = \lambda x:\N.\lambda f:\sem{P}.\pair{x}{f}$
+ }\\
+ \multicolumn{2}{l}{
+   $\sem{ex\_ind} = 
+   \lambda f:(\N \to \sem{P} \to \sem{Q}).
+   \lambda p:\N\times \sem{P}.f~(fst~p)~(snd~p)$. 
+ }
+\end{tabular}\vspace{0.1cm}
+\hrule
+\caption{\label{tab:axioms}Axioms translation}
+\end{table}
+
+\begin{table}[!h]
+\hrule\vspace{0.1cm}
+\begin{tabular}{p{0.47\textwidth}p{0.47\textwidth}}
+ $\canonical_\one = \lambda x:\one.x$ &
+ $\canonical_N = \lambda x:\one.0$ \\
+ $\canonical_{U\times V} = \lambda x:\one.\pair{\canonical_{U}
+ x}{\canonical_{V} x}$ &
+ $\canonical_{U\to V} = \lambda x:\one.\lambda \_:U. \canonical_{V} x$
+\end{tabular}\vspace{0.1cm}
+\hrule
+\caption{\label{tab:canonical}Canonical element}
+\end{table}
 
-\begin{itemize}
-\item $\sem{nat\_ind} = R$
-\item $\sem{ex\_ind} = (\lambda f:(\N \to \sem{P} \to \sem{Q}).
-\lambda p:\N\times \sem{P}.f (fst \,p) (snd \,p)$. 
-\item $\sem{ex\_intro} = \lambda x:\N.\lambda f:\sem{P}.\pair{x}{f}$
-\item $\sem{fst} = \pi_1$
-\item $\sem{snd} = \pi_2$
-\item $\sem{conj} = \lambda x:\sem{P}.\lambda y:\sem{Q}.\pair{x}{y}$
-\item $\sem{false\_ind} = \canonical_{\sem{Q}}$
-\item $\sem{discriminate} = \lambda \_:\N.\lambda \_:\one.\star$
-\item $\sem{injS}= \lambda \_:\N. \lambda \_:\N.\lambda \_:\one.\star$
-\item $\sem{plus\_O} = \sem{times\_O} = \lambda \_:\N.\star$
-\item $\sem{plus\_S} = \sem{times_S} = \lambda \_:\N. \lambda \_:\N.\star$
-\end{itemize}
-
-In the case of structured proofs:
-\begin{itemize}
-\item $\semT{M N} = \semT{M} \semT{N}$
-\item $\semT{\lambda x:A.M} = \lambda x:\sem{A}.\semT{M}$
-\item $\semT{\lambda x:\N.M} = \lambda x:\N.\semT{M}$
-\item $\semT{M t} = \semT{M} \semT{t}$
-\end{itemize}
 
 \section{Realizability}
 The realizability relation is a relation $f \R P$ where $f: \sem{P}$, and
@@ -624,10 +654,62 @@ 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{Improoving inductive types}
-It is possible to parametrize inductive types over other inductive types
+\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$.