- uniformed command line handling of matitamake with that of other matita tools

[helm.git] / helm / papers / system_T / t.tex

\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{\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}{{\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}}
\newcommand{\Rx}{\ensuremath{R_X}}

\newtheorem{thm}{Theorem}[subsection]

\title{Modified Realizability and Inductive Types}
\author{...}


\begin{document}
\maketitle
\thispagestyle{empty}

\begin{abstract}
In 1959, Kreisel introduced a notion of ``modified'' realizability to
provide an alternative technique to G\"odel functional (dialectica)
interpretation for establishing the connection between Peano Arihtmetic
and System T. While the dialectica interpretation has been widely
studied in the literature, Kreisel's technique, although remarkably 
simpler,has apparently been almost neglected (with the only exception
of Troelstra). In this paper we give a modern presentation of the technique, 
and generalize it to arbitrary inductive types in a first order setting.
This is part of a larger program, advocating the study 
of logical systems with primitive inductive types starting form
weak, predicative logical frameworks and adding little by little small 
bits of logical power.

\end{abstract}

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\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 
that the functional interpretation of the Dialectica paper
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{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 
G\"odel System T is provided
by the so called {\em modified realizability}. Modified realizability
was first introduced by Kreisel in \cite{Kreisel59} - although it will take you
a bit of effort to recognize it in the few lines of paragraph 3.52 -
and later in \cite{Kreisel62} under the name of generalized realizability.
The name of modified realizability seems to be due to Troelstra 
\cite{Troelstra}
- who contested Kreisel's name but unfortunately failed in proposing 
a valid alternative; we shall reluctantly adopt this latter name 
to avoid further confusion. Modified realizability is a typed variant of 
realizability, essentially providing interpretations 
of $HA^{\omega}$ into itself: each theorem is realized by a typed function
of system T, that also gives the actual computational content extracted 
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 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 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 
prove that the Induction Principle is realized by the recursor $R$ 
of system $T$ you catch a sudden gleam of understanding in the 
students eyes; usually, the same does not happen when you show, say, 
that the ``forgetful'' interpretation of the higher order predicate defining
the natural numbers is the system $F$ encoding 
$\forall X.(X\to X) \to X \to X$ of $\N$. 
Moreover, after a first period of enthusiasm, the impredicative 
encoding of inductive types in Logical Frameworks has shown several 
problems and limitations (see e.g. \cite{Werner} pp.24-25) mostly
solved by assuming inductive types as a primitive logical notion
(leading e.g. form the Calculus of Constructions to the Calculus
of Inductive Constructions - CIC). Even the extraction algorithm of
CIC, strictly based on realizability principles, and in a first time
still oriented towards System F \cite{Paulin87,Paulin89} has been 
recently rewritten \cite{Letouzey04}
to take advantage of concrete types and pattern matching of ML-like
languages. Unfortunately, systems like the Calculus of Inductive 
Constructions are so complex, from the logical point of view, to 
substantially prevent a really neat theoretical exposition (at present, 
it does not
even exists a truly complete consistency proofs covering all aspects
of such systems); moreover, not everybody may be interested in all the features
offered by these frameworks, from polymorphism to types depending on 
proofs. Our program is to restart the analysis of logical systems with
primitive inductive types in a smooth way, starting form first order
logic and adding little by little small bits of logical power.
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, 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}

\begin{itemize}
\item $nat\_ind: P(0) \to (\forall x.P(x) \to P(S(x))) \to \forall x.P(x)$ 
\item $ex\_ind: (\forall x.P(x) \to Q) \to \exists x.P(x) \to Q$
\item $ex\_intro: \forall x.(P \to \exists x.P)$
\item $fst: P \land Q \to P$
\item $snd: P \land Q \to Q$
\item $conj: P \to Q \to P \land Q$
\item $false\_ind: \bot \to Q$
\item $discriminate:\forall x.0 = S(x) \to \bot$
\item $injS: \forall x,y.S(x) = S(y) \to x=y$
\item $plus\_O:\forall x.x+0=x$
\item $plus\_S:\forall x,y.x+S(y)=S(x+y)$ 
\item $times\_O:\forall x.x\mult0=0$
\item $times\_S:\forall x,y.x\mult S(y)=x+(x\mult y)$ 
\end{itemize}

\noindent
{\bf Inference Rules}

say that ax:AX refers to the previous Axioms list...
%\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 \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}  
%\]


%\[ 
%   (\exists_i)\frac{\Gamma \vdash P[t/x]}{\Gamma \vdash \exists x.P}\hspace{2cm}
%   (\exists_e)\frac{\Gamma \vdash \exists x.P\hspace{1cm}\Gamma \vdash \forall x.P \to Q}
%{\Gamma \vdash Q} 
%\]

\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 $\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 $\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 
%$\vec{x} = x_1,\ldots, x_m$, we say that $f \R B1, \ldots, B_n \vdash A$ iff 
%forall natural numbers $n_1, \ldots, n_m$, 
%if forall $i \in {1,\ldots,n}$ 
%$m_i \R B_i[\vec{\underline{n}}/\vec{x}]$ then
%$$f <m_1, \ldots, m_n> \R A[\vec{\underline{n}}/\vec{x}]$$.
%
\noindent
We need to generalize the notion of realizability to sequents.\\
Let $\vec{x} = FV_{\N}( B_1, \ldots, B_n, P)$ a vector of variables of type
$\N$ that occur free in $B_1, \ldots, B_n, P$. Let $\vec{b:B}$ the vector
$b_1:B_1, \ldots, b_n:B_n$.\\ 
We say that $f \R B_1, \ldots, B_n \vdash A:P$ iff
$$\lambda \vec{x:\N}. \lambda \vec{b:B}.f \R 
\forall \vec{x}. B_1 \to \ldots \to B_n \to P$$
Note that $\forall \vec{x}. B_1 \to \ldots \to B_n \to P$ is a closed formula,
so we can use the previous definition of realizability on it.

\noindent
We proceed to prove that all axioms $ax:Ax$ are realized by $\sem{ax}$.

\begin{itemize}
\item $nat\_ind$. 
  We must prove that the recursion schema $R$ realizes the induction principle.
  To this aim we must prove that for any $a$ and $f$ such that $a \R P(0)$ and
  $f \R \forall x.(P(x) \to P(S(x)))$, and any natural number $n$, $(R \,a \,f
  \,n) \R P(\underline{n})$.\\ 
  We proceed by induction on n.\\ 
  If $n=O$, $(R \,a \,f \,O) = a$ and by hypothesis $a \R P(0)$.\\ 
  Suppose by induction that
  $(R \,a \,f \,n) \R P(\underline{n})$, and let us prove that the relation
  still holds for $n+1$.  By definition 
  $(R \,a \,f \,(n+1)) = f \,n \,(R \,a \,f \,n)$, 
  and since $f \R \forall x.(P(x) \to P(S(x)))$,  
  $(f n (R a f n)) \R P(S(\underline{n}))=P(\underline{n+1})$.

\item $ex\_ind$. 
  We must prove that $$\underline{ex\_ind} \R (\forall x:(P x)
  \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 $\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$).\\
  Expanding the definition of $\underline{ex\_ind}$, $fst$
  and $snd$ we obtain $f~n_p~g_p$ that we know is in relation $\R$ with $Q$
  since $g_p \R P[\underline{n_p}/x]$.

\item $ex\_intro$.
  We must prove that 
  $$\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 
  $\underline{ex\_into}~n \R (P[\underline{n}/x]\to\exists x.P(x))$.\\
  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
  $\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 $\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 $snd$. The same for $fst$.

\item $conj$. 
  We have to prove that 
  $$\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}.\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$.


\item $false\_ind$. 
  We have to prove that $\bot_{\sem{Q}} \R \bot \to Q$. 
  Trivial, since there is no $m \R \bot$.

\item $discriminate$. 
  Since there is no $n$ such that $0 = S n$ is true... \\
  $\underline{discriminate}~n \R 0 = S~\underline{n} \to \bot$ for each n.

\item $injS$.
  We have to prove that for each $n_1$ and $n_2$\\
  $\lambda \_:\N. \lambda \_:\N.\lambda \_:\one.*~n_1~n_2 \R 
  (S(x)=S(y)\to x=y)[n_1/x][n_2/y]$.\\
  We assume that $m \R S(n_1)=S(n_2)$ and we have to show that 
  $\lambda \_:\N. \lambda \_:\N.\lambda \_:\one.*~n_1~n_2~m$ that reduces to
  $*$ is in relation $\R$ with $n_1=n_2$. Since in the standard model of 
  natural numbers  $S(n_1)=S(n_2)$ implies $n_1=n_2$ we have that 
  $* \R n_1=n_2$.

\item $plus\_O$. 
  Since in the standard model for natural numbers $0$ is the neutral element
  for addition $\lambda \_:\N.\star \R \forall x.x + 0 = x$.

\item $plus\_S$.
  In the standard model of natural numbers the addition of two numbers is the 
  operation of counting the second starting from the first. So
  $$\lambda \_:\N. \lambda \_:\N. \star \R \forall x,y.x+S(y)=S(x+y)$$.

\item $times\_O$.
  Since in the standard model for natural numbers $0$ is the absorbing element
  for multiplication $\lambda \_:\N.\star \R \forall x.x \mult 0 = 0$.
  
\item $times\_S$.
  In the standard model of natural numbers the multiplications of two 
  numbers is the operation of adding the first to himself a number of times
  equal to the second number. So
  $$\lambda \_:\N. \lambda \_:\N. \star \R \forall x,y.x+S(y)=S(x+y)$$.
  
\end{itemize}


\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
longer $Constr(n,\ind\{\ldots\})$ to indicate the $n^{th}$ constructor.
We adopt the vector notation to make things more readable.
$\vec{m}$ has to be intended as $m_1~\ldots~m_n$ where $n$ may
be equal to 0 (we use $m_1~\vec{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 \vec{B} \to C$ is a shortcut for 
$A \to B_1 \to \ldots \to B_n \to C$.

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\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.

First we admit quantification over inductive types $T$, thus $\forall x:T.A$
and $\exists x:T.A$ are allowed. Then rules 4 and 5 of the $\sem{\cdot}$
definition are replaced by $\sem{\forall x:T.P} = T \to \sem{P}$ and
$\sem{\exists x:T.P} = T \times \sem{P}$.

For each inductive type we will describe the formation rules and the
corresponding induction principle schema.

Symmetrically we have to extend System T with arbitrary inductive types and 
we will see how theyr recursors are defined in the following sections. 

The definition of $\R$ is modified substituting each occurrence of $\N$ with 
a generic inductive type $T$.

%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\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}
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(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}
\triUP\{X, c\} & = & Q(c) \nonumber\\
\triUP\{T \to C(X), c\} & = & 
        \forall m:T.\triUP\{C(X),c~m\} \nonumber\\
\triUP\{X \to C(X), c\} & = & 
        \forall t:X.Q(t) \to \triUP\{C(X), c~t\} \nonumber
\end{eqnarray}

%%%%%%%%%%%%%%%%%%%%%
\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)$.
\begin{eqnarray}
\square\{X\} & = & \alpha \nonumber \\
\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}
We say that 
$$\Rx~\vec{f}~(c_i~\vec{m}) \leadsto
\triDOWN\{C(X)_i, f_i, \vec{m}\}$$
$\triDOWN$ takes a constructor type $C(X)$, a term $f$ 
(of type $\square\{C(X)\}$) and is defined by recursion as follows:
\begin{eqnarray}
\triDOWN\{X, f, \} & = & f\nonumber \\
\triDOWN\{T \to C(X), f, m_1~\vec{m}\} & = &
        \triDOWN\{C(X), f~m_1, \vec{m}\}\nonumber \\
\triDOWN\{X \to C(X), f, m_1~\vec{m}\} & = & 
        \triDOWN\{C(X), f~m_1~(\Rx~\vec{f}~m_1),
        \vec{m}\}\nonumber
\end{eqnarray}
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


%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\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. 
Bibliopolis, Napoli, 1987.
\bibitem{GLT}G.Y.Girard, Y.Lafont, P.Tailor. Proofs and Types.
Cambridge Tracts in Theoretical Computer Science 7.Cambridge University
Press, 1989.
\bibitem{Godel58}K.G\"odel. \"Uber eine bisher noch nicht ben\"utzte Erweiterung
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.
 \bibitem{Kreisel62} G.Kreisel. On weak completeness of intuitionistic 
predicatelogic. Journal of Symbolic Logic 27, pp. 139-158. 1962.
\bibitem{Letouzey04}P.Letouzey. Programmation fonctionnelle 
certifi\'ee; l'extraction
de programmes dans l'assistant Coq. Ph.D. Thesis, Universit\'e de 
Paris XI-Orsay, 2004.
\bibitem{Loef}P.Martin-L\"of. Intuitionistic Type Theory.
Bibliopolis, Napoli, 1984.
\bibitem{Paulin87}C.Paulin-Mohring. Extraction de programme dans le Calcul de
Constructions. Ph.D. Thesis, Universit\'e de 
Paris 7, 1987.
\bibitem{Paulin89}C.Paulin-Mohring. Extracting $F_{\omega}$ programs 
from proofs in the Calculus of Constructions. In proc. of the Sixteenth Annual 
ACM Symposium on 
Principles of Programming Languages, Austin, January, ACML Press 1989.
\bibitem{Sch}K.Sch\"utte. Proof Theory. Grundlehren der mathematischen 
Wissenschaften 225, Springer Verlag, Berlin, 1977.
\bibitem{Troelstra}A.S.Troelstra. Metamathemtical Investigation of 
Intuitionistic
Arithmetic and Analysis. Lecture Notes in Mathematics 344, Springer Verlag,
Berlin, 1973.
\bibitem{TS}A.S.Troelstra, H.Schwichtenberg. Basic Proof Theory.
Cambridge Tracts in Theoretical Computer Science 43.Cambridge University
Press, 1996.
\bibitem{Werner}B.Werner. Une Th\'eorie des Constructions Inductives.
Ph.D.Thesis, Universit\'e de Paris 7, 1994.


\end{thebibliography}

\end{document}