-\documentclass[a4paper]{article}
+\documentclass[times, 10pt,twocolumn, draft]{article}
\pagestyle{headings}
%\usepackage{graphicx}
\usepackage{amssymb,amsmath,mathrsfs,stmaryrd,amsthm}
%\usepackage{hyperref}
%\usepackage{picins}
+\usepackage{latex8}
+\usepackage{times}
+
+\pagestyle{empty}
+
\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}}
\begin{document}
\maketitle
+\thispagestyle{empty}
\begin{abstract}
...
\end{abstract}
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
-\section{Introduction}
+\Section{Introduction}
The characterization of the provable recursive functions of
Peano Arithmetic as the terms of system T is a well known
result of G\"odel \cite{Godel58,Godel90}. Although several authors acknowledge
is not among the major achievements of the author (see e.g. \cite{Girard87}),
the result has been extensively investigated and there is a wide
literature on the
-topic (see e.g. \cite{Howard68,Troelstra,Girard87}.
+topic (see e.g. \cite{Troelstra,HS86,Girard87}, just to mention textbooks,
+and the bibliography therein).
A different, more neglected, but for many respects much more
direct relation between Peano (or Heyting) Arithmetics and
from the proof.
In spite of the simplicity and the elegance of the proof, it is extremely
difficult to find a modern discussion of this result; the most recent
-exposition we are aware of is in the encyclopedic (typewritten!) work by
-Troelstra \cite{Troelstra} (pp.213-229). Even modern introductory books
+exposition we are aware of is in the encyclopedic work by
+Troelstra \cite{Troelstra} (pp.213-229) going back to thirty years ago.
+Even modern introductory books
to Type Theory and Proof Theory devoting much space to system T
such as \cite{GLT} and \cite{TS} surprisingly leave out this simple and
-illuminating result. Both \cite{GLT} and \cite{TS}
+illuminating result. Both the previous textbooks
prefer to focus on higher order arithmetics and its relation with
Girard's System $F$ \cite{Girard86}, but the technical complexity and
the didactical value of the two proofs is not comparable: when you
This paper is the first step in this direction.
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
-\section{Heyting's arithmetics}
+\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, projections,
+and type specific reductions as reported in table \ref{tab:tredex}
+
+\begin{table}[!h]
+\hrule\vspace{0.1cm}
+\begin{tabular}{p{0.34\textwidth}r}
+ $\lambda x:U.M ~ N \leadsto M[N/x]$ & $(\beta)$ \\
+ $fst \pair{M}{N} \leadsto M$ & $(\pi_1)$ \\
+ $snd \pair{M}{N} \leadsto N$ & $(\pi_2)$ \\
+ $D~M~N~ true \leadsto M$ & $(D_{true})$ \\
+ $D~M~N~false \leadsto N$ & $(D_{false})$ \\
+ $R~M~F~ 0 \leadsto M$ & $(R_0)$ \\
+ $R~M~F~(S~n) \leadsto F~n~(R~M~F~n)$ & $(R_S)$ \\
+ $M \leadsto * ~~~~ $ for any M of type $\one$ & $(*)$
+\end{tabular}\vspace{0.1cm}
+\hrule
+\caption{\label{tab:tredex}Reduction rules for System T}
+\end{table}
+
+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}
{\bf Inference Rules}
say that ax:AX refers to the previous Axioms list...
-
-\[
- (Proj)\hspace{0.2cm} \Gamma, x:A, \Delta \vdash x:A
- \hspace{2cm}
- (Const)\hspace{0.2cm} \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}
- {\Gamma \vdash M N: Q}
-\]
+%\begin{table}[!h]
+%\hrule\vspace{0.1cm}
+%\begin{tabular}{p{0.34\textwidth}r}
+
+ $$\Gamma, x:A, \Delta \vdash x:A ~~~ (Proj)$$
+ $$ \Gamma \vdash ax : AX~~~ (Const)$$
+ $$\frac{\Gamma,x:A \vdash M:Q}{\Gamma \vdash \lambda x:A.M: A \to Q} ~~~ (\to_i)$$
+ $$\frac{\Gamma \vdash M: A \to Q \hspace{0.5cm}\Gamma \vdash N: A}
+ {\Gamma \vdash M N: Q} ~~~ (\to_e)$$
+ $$\frac{\Gamma \vdash M:P}{\Gamma \vdash \lambda x:\N.M: \forall x.P}(*) ~~~
+ (\forall_i)$$
+ $$\frac{\Gamma \vdash M :\forall x.P}{\Gamma \vdash M t: P[t/x]}
+ ~~~ (\forall_e)$$
+
+%\end{tabular}\vspace{0.1cm}
+%\hrule
+%\caption{\label{tab:HArules}Inference rules}
+%\end{table}{lr}
%\[
% (\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}
% (\land_{er})\frac{\Gamma \vdash A \land B}{\Gamma \vdash B}
%\]
-\[
- (\forall_i)\hspace{0.2cm}\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]}
-\]
-
%\[
% (\exists_i)\frac{\Gamma \vdash P[t/x]}{\Gamma \vdash \exists x.P}\hspace{2cm}
%{\Gamma \vdash Q}
%\]
-\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}
-
-\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}
+\Section{Extraction}
+
+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.21\textwidth}p{0.21\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.20\textwidth}p{0.20\textwidth}}
+ $\semT{M N} = \semT{M} \semT{N}$ &
+ $\semT{M t} = \semT{M} \semT{t}$ \\
+ \multicolumn{2}{l}{$\semT{\lambda x:A.M} = \lambda x:\sem{A}.\semT{M}$} \\
+ \multicolumn{2}{l}{$\semT{\lambda x:\N.M} = \lambda x:\N.\semT{M}$}
+\end{tabular}\vspace{0.1cm}
+\hrule
+\caption{\label{tab:structproof}Structured proofs}
+\end{table}
+
+\begin{table}[!h]
+\hrule\vspace{0.1cm}
+\begin{tabular}{l}%{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$ \\
+ $\sem{plus\_S} = \sem{times\_S} = \lambda \_:\N. \lambda \_:\N.\star$ \\
+ $\sem{ex\_intro} = \lambda x:\N.\lambda f:\sem{P}.\pair{x}{f}$ \\
+ $\sem{ex\_ind} = \lambda f:(\N \to \sem{P} \to \sem{Q}).$\\
+ $\qquad\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}{l}%p{0.23\textwidth}p{0.23\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}
+
+
+\Section{Realizability}
The realizability relation is a relation $f \R P$ where $f: \sem{P}$, and
$P$ is a closed formula.
In particular:
\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$.
\end{itemize}
-%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
-\section{Inductive types}
+
+\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
+\begin{eqnarray}
+B & \equiv & \lambda q.\lambda h_0:q \le 0. h ~q~ \nonumber\\
+& & \quad (\lambda p.\lambda k:p < q. false\_ind ~(L~p~q~k~h_0)) \nonumber
+\end{eqnarray}
+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
+\begin{eqnarray}
+I & \equiv & \lambda n.\lambda h_1:\forall q. q \le n \to P~ q.\lambda q.\lambda h_2:q \le S n. \nonumber\\
+ & & \quad h ~ q ~ (\lambda p.\lambda h_3:p < q.h_1 ~p~ (M~ p~ q~ n~ h_3~ h_2))
+ \nonumber
+\end{eqnarray}
+(where $h$ is free in I).
+The full proof is
+\begin{eqnarray}
+& \lambda h:\forall m.(\forall p. p < m\to P~p)\to P~m.\lambda m. &\nonumber\\
+& \quad nat\_ind ~B ~ I ~m~m~ (le\_n ~ m) & \nonumber
+\end{eqnarray}
+
+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
+\begin{eqnarray}
+fibo & \equiv & \lambda q. \lambda g. if~ q = 0~then~ 1~ else \nonumber\\
+& & \quad if~ q = 1~ then~ 1~ else ~ g (q-1)+g (q-2) \nonumber
+\end{eqnarray}
+
+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
$A \to B_1 \to \ldots \to B_n \to C$.
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
-\subsection{Extensions to the logic framework}
+\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.
a generic inductive type $T$.
%%%%%%%%%%%%%%%%%%%%%%%%%%%%
-\subsection{Type definition}
+\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}
+\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}
\end{eqnarray}
%%%%%%%%%%%%%%%%%%%%%
-\subsection{Recursor}
-\subsubsection{Type}
+\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)$.
\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}
+%\SubSubSection{Reduction rules}
We say that
$$\Rx~\vec{f}~(c_i~\vec{m}) \leadsto
\triDOWN\{C(X)_i, f_i, \vec{m}\}$$
can omit $\vec{m}$ since it is an empty sequence.
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
-\subsection{Realizability of the induction principle}
+\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$.
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 each recursive
-argument $t_i$ of the head constructor $c_i$ is realized by $r_i\equiv
-\Rx~\vec{f}~t_i$. By the third rule of $\triDOWN$ we obtain the reduct
+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
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
+
+
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+\bibliographystyle{latex8}
+%\bibliography{latex8}
+
\begin{thebibliography}{}
+\bibitem{AL91}A.Asperti, G.Longo. Categories, Types and Structures.
+Foundations of Computing, Cambrdidge University press, 1991.
\bibitem{Girard86}G.Y.Girard. The system F of variable types, fifteen
years later. Theoretical Computer Science 45, 1986.
\bibitem{Girard87}G.Y.Girard. Proof Theory and Logical Complexity.
des finiten Standpunktes. Dialectica, 12, pp.34-38, 1958.
\bibitem{Godel90}K.G\"odel. Collected Works. Vol.II, Oxford University Press,
1990.
+\bibitem{HS86}J.R.Hindley, J. P. Seldin. Introduction to Combinators and
+Lambda-calculus, Cambridge University Press, 1986.
\bibitem{Howard68}W.A.Howard. Functional interpretation of bar induction
by bar recursion. Compositio Mathematica 20, pp.107-124. 1958
\bibitem{Howard80}W.A.Howard. The formulae-as-types notion of constructions.
in J.P.Seldin and j.R.Hindley editors, to H.B.Curry: Essays on Combinatory
Logic, Lambda calculus and Formalism. Acedemic Press, 1980.
+\bibitem{Kleene45}S.C.Kleene. On the interpretation of intuitionistic
+number theory. Journal of Symbolic Logic, n.10, pp.109-124, 1945.
\bibitem{Kreisel59} G.Kreisel. Interpretation of analysis by means of
constructive functionals of finite type. In. A.Heyting ed.
{\em Constructivity in mathematics}. North Holland, Amsterdam,1959.
projects / helm.git / blobdiff