\newcommand{\semT}[1]{\ensuremath{\llbracket #1 \rrbracket}}
\newcommand{\sem}[1]{\llbracket \ensuremath{#1} \rrbracket}
-\newcommand{\R}{\;\mathscr{R}\;}
+\newcommand{\pair}[2]{<\!#1,#2\!>}
+\newcommand{\canonical}{\bot}
+\newcommand{\R}{~\mathscr{R}~}
\newcommand{\N}{\,\mathbb{N}\,}
+\newcommand{\B}{\,\mathbb{B}\,}
\newcommand{\NT}{\,\mathbb{N}\,}
\newcommand{\NH}{\,\mathbb{N}\,}
\renewcommand{\star}{\ast}
\renewcommand{\vec}{\overrightarrow}
-\newcommand{\one}{\mathscr{1}}
+\newcommand{\one}{{\bf 1}}
\newcommand{\mult}{\cdot}
\newcommand{\ind}{Ind(X)}
+\newcommand{\indP}{Ind(\vec{P}~|~X)}
\newcommand{\Xind}{\ensuremath{X_{ind}}}
+\newcommand{\XindP}{\ensuremath{X_{ind}}}
\renewcommand{\|}{\ensuremath{\quad | \quad}}
\newcommand{\triUP}{\ensuremath{\Delta}}
\newcommand{\triDOWN}{\ensuremath{\nabla}}
This paper is the first step in this direction.
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+\section{G\"odel system T}
+We shall use a variant of system T with three atomic types $\N$ (natural
+numbers), $\B$ (booleans) and $\one$ (a terminal object), and two binary
+type constructors $\times$ (product) and $\to$ (arrow type).
+
+The terms of the language comprise the usual simply typed lambda terms
+with explicit pairs, plus the following additional constants:
+\begin{itemize}
+\item $*:\one$,
+\item $true: \B$, $false:\B$, $D:A\to A \to \B \to A$
+\item $O:\N$, $S:\N \to \N$, $R:A \to (A \to \N \to A) \to \N \to A$,
+\end{itemize}
+Redexes comprise $\beta$-reduction
+\[(\beta)~~ \lambda x:U.M ~ N \leadsto M[N/x]\]
+projections
+
+\[(\pi_1)~~fst \pair{M}{N} \leadsto M\\ \hspace{.6cm} (\pi_2)~~ snd \pair{M}{N}
+\leadsto N \]
+and the following type specific reductions:
+\[(D_{true})~~\\D~M~N~ true \leadsto M \hspace{.6cm}
+ (D_{false})~~ D~M~N~false \leadsto N \]
+\[(R_0)~~\\R~M~F~ 0 \leadsto M \hspace{.6cm}
+ (R_S)~~ R~M~F~(S~n) \leadsto F~n~(R~M~F~n) \]
+\[(*)~~ M \leadsto * \]
+where (*) holds for any $M$ of type $\one$.
+
+Note that using the well known isomorpshims
+$\one \to A \cong A$, $A \to \one \cong \one$
+and $A \times \one \cong A \cong \one\times A$ (see \cite{AL91}, pp.231-239)
+we may always get rid of $\one$ (apart the trivial case).
+The terminal object does not play a major role in our treatment, but
+it allows to extract better algorithms. In particular we use it
+to realize atomic proposition, and stripping out the terminal object using
+the above isomorphisms gives a simple way of just keeping the truly
+informative part of the algorithms.
+
+
+
\section{Heyting's arithmetics}
{\bf Axioms}
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}
\]
%\[
% (\land_i)\frac{\Gamma \vdash M:A \hspace{1cm}\Gamma \vdash N:B}
-% {\Gamma \vdash <M,N> : A \land B}
+% {\Gamma \vdash \pair{M}{N} : A \land B}
%\hspace{2cm}
% (\land_{el})\frac{\Gamma \vdash A \land B}{\Gamma \vdash A}
%\hspace{2cm}
%\]
\[
- (\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]}
\]
\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 $\bot_T: \one \to T$ is inductively defined as follows:
-\begin{enumerate}
-\item $\bot_\one = \lambda x:\one.x$
-\item $\bot_N = \lambda x:\one.0$
-\item $\bot_{U\times V} = \lambda x:\one.<\bot_{U} x,\bot_{V} x>$
-\item $\bot_{U\to V} = \lambda x:\one.\lambda \_:U. \bot_{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}.<x,f>$
-\item $\sem{fst} = \pi_1$
-\item $\sem{snd} = \pi_2$
-\item $\sem{conj} = \lambda x:\sem{P}.\lambda y:\sem{Q}.<x,y>$
-\item $\sem{false\_ind} = \bot_{\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
\begin{itemize}
\item $\neg (\star \R \bot)$
\item $* \R (t_1=t_2)$ iff $t_1=t_2$ is true ...
-\item $<f,g> \R (P\land Q)$ iff $f \R P$ and $g \R Q$
+\item $\pair{f}{g} \R (P\land Q)$ iff $f \R P$ and $g \R Q$
\item $f \R (P\to Q)$ iff for any $m$ such that $m \R P$, $(f \,m) \R Q$
\item $f \R (\forall x.P)$ iff for any natural number $n$ $(f n) \R P[\underline{n}/x]$
-\item $<n,g> \R (\exists x.P)$ iff $g \R P[\underline{n}/x]$
+\item $\pair{n}{g}\R (\exists x.P)$ iff $g \R P[\underline{n}/x]$
\end{itemize}
%We need to generalize the notion of realizability to sequents.
%Given a sequent $B_1, \ldots, B_n \vdash A$ with free variables in
\to Q) \to (\exists x:(P x)) \to Q$$ Following the definition of $\R$ we have
to prove that given\\ $f~\R~\forall~x:((P~x)~\to~Q)$ and
$p~\R~\exists~x:(P~x)$, then $\underline{ex\_ind}~f~p \R Q$.\\
- $p$ is a couple $<n_p,g_p>$ such that $g_p \R P[\underline{n_p}/x]$, while
+ $p$ is a couple $\pair{n_p}{g_p}$ such that $g_p \R P[\underline{n_p}/x]$, while
$f$ is a function such that forall $n$ and for all $m \R P[\underline{n}/x]$
then $f~n~m \R Q$ (note that $x$ is not free in $Q$ so $[\underline{n}/x]$
affects only $P$).\\
\item $ex\_intro$.
We must prove that
- $$\lambda x:\N.\lambda f:\sem{P}.<x,f> \R \forall x.(P\to\exists x.P(x)$$
+ $$\lambda x:\N.\lambda f:\sem{P}.\pair{x}{f} \R \forall x.(P\to\exists x.P(x)$$
that leads to prove that for each n
$\underline{ex\_into}~n \R (P\to\exists x.P(x))[\underline{n}/x]$.\\
Evaluating the substitution we have
Again by definition of $\R$ we have to prove that given a
$m \R P[\underline{n}/x]$ then $\underline{ex\_into}~n~m \R \exists x.P(x)$.
Expanding the definition of $\underline{ex\_intro}$ we have
- $<n,m> \R \exists x.P(x)$ that is true since $m \R P[\underline{n}/x]$.
+ $\pair{n}{m} \R \exists x.P(x)$ that is true since $m \R P[\underline{n}/x]$.
\item $fst$.
We have to prove that $\pi_1 \R P \land Q \to P$, that is equal to proving
that for each $m \R P \land Q$ then $\pi_1~m \R P$ .
- $m$ must be a couple $<f_m,g_m>$ such that $f_m \R P$ and $g_m \R Q$.
+ $m$ must be a couple $\pair{f_m}{g_m}$ such that $f_m \R P$ and $g_m \R Q$.
So we conclude that $\pi_1~m$ reduces to $f_m$ that is in relation $\R$
with $P$.
\item $conj$.
We have to prove that
- $$\lambda x:\sem{P}. \lambda y:\sem{Q}.<x,y> \R P \to Q \to P \land Q$$
+ $$\lambda x:\sem{P}. \lambda y:\sem{Q}.\pair{x}{y}\R P \to Q \to P \land Q$$
Following the definition of $\R$ we have to show that
for each $m \R P$ and for each $n \R Q$ then
- $(\lambda x:\sem{P}. \lambda y:\sem{Q}.<x,y>)~m~n \R P \land Q$.\\
- This is the same of $<m,n> \R P \land Q$ that is verified since
+ $(\lambda x:\sem{P}. \lambda y:\sem{Q}.\pair{x}{y})~m~n \R P \land Q$.\\
+ This is the same of $\pair{m}{n} \R P \land Q$ that is verified since
$m \R P$ and $n \R Q$.
\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\]
+\[(\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
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$.\\
+\[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: \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)) \]
+\[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 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$.\\
+\[ \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' = \lambda m.\lambda f.
-R\; (f \; O\; (\lambda q.*_A))\;
-(\lambda n\lambda g\lambda q.f \;q\;g)\;m \;m\]
+\[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: \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)\]
+\[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
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
\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(x)$$
+$$\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}
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
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
projects / helm.git / blobdiff