added some stuff on inductive types

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

\documentclass[a4paper]{article}
\pagestyle{headings}
%\usepackage{graphicx}
\usepackage{amssymb,amsmath,mathrsfs}
%\usepackage{hyperref}
%\usepackage{picins}

\newcommand{\sem}[1]{[\![ #1 ]\!]}
\newcommand{\R}{\;\mathscr{R}\;}
\newcommand{\N}{\,\mathbb{N}\,}
\newcommand{\NT}{\,\mathbb{N}\,}
\newcommand{\NH}{\,\mathbb{N}\,}
\renewcommand{\star}{\ast}
\newcommand{\one}{\mathbb{1}}
\renewcommand{\times}{\cdot}
\newcommand{\ind}{Ind(X)}
\title{Modified Realizability and Inductive Types}
\author{...}


\begin{document}
\maketitle

\begin{abstract}
...
\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 many 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{Howard68,Troelstra,Girard87}. 

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 (typewritten!) work by
Troelstra \cite{Troelstra} (pp.213-229). 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}
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 intelligence in the 
students eyes; usually, the same does not happen when you show, say, 
that the ``forgetful'' intrepretation 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 eveybody 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{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\times0=0$
\item $times\_S:\forall x,y.x\times S(y)=x+(x\times y)$ 
\end{itemize}

\noindent
{\bf Inference Rules}

\[ 
   (\to_i)\frac{\Gamma,x:A \vdash M:Q}{\Gamma \vdash \lambda x:A.M: A \to Q} \hspace{2cm}
   (\to_e)\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} 
%\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)\frac{\Gamma \vdash M:P}{\Gamma \vdash 
   \lambda x:\N.M: \forall x.P}(*) \hspace{2cm}
   (\forall_e)\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}
%   (\exists_e)\frac{\Gamma \vdash \exists x.P\hspace{1cm}\Gamma \vdash \forall x.P \to Q}
%{\Gamma \vdash Q} 
%\]

\section{Extraction}

We have to extend systeem T with inductive types (and they recursors).
\begin{itemize}
\item $\sem{A} = 1$ if A is atomic
\item $\sem{A \land B} = \sem{A}\times \sem{B}$
\item $\sem{A \to B} = \sem{A}\to \sem{B}$
\item $\sem{\forall x:T.P} = T \to \sem{P}$
\item $\sem{\exists x:T.P} = T \times \sem{P}$
\end{itemize}

definition.
For any type T of system T $\bot_T: 1 \to T$  is inuctively defined as follows:
\begin{enumerate}
\item $\bot_1 = \lambda x:1.x$
\item $\bot_N = \lambda x:1.0$
\item $\bot_{U\times V} = \lambda x:1.<\bot_{U} x,\bot_{V} x>$
\item $\bot_{U\to V} = \lambda x:1.\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 \_:1.\star$
\item $\sem{injS}= \lambda \_:\N. \lambda \_:\N.\lambda \_:1.\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 $\sem{M N} = \sem{M} \sem{N}$
\item $\sem{\lambda x:A.M} = \lambda x:\sem{A}.\sem{M}$
\item $\sem{\lambda x:\N.M} = \lambda x:\N.\sem{M}$
\item $\sem{M t} = \sem{M} \sem{t}$
\end{itemize}

\section{Realizability}
The realizability relation is a relation $f \R P$ where $f: \sem{P}$.
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 $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]$
\end{itemize}

\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 $<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$).\\
  Exapanding 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}.<x,f> \R \forall x.(P\to\exists x.P(x)$$
  that leads to prove that foreach 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
  $<n,m> \R \exists x.P(x)$ that is true since $m \R P[\underline{n}/x]$.

\item $fst$.
  Wehave 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$.
  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}.<x,y> \R P \to Q \to P \land Q$$
  Following the definition of $\R$ we have to show that 
  foreach $m \R P$ and foreach $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 
  $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 \_:1.*~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 \_:1.*~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 \times 0 = x$.
  
\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}

\section{Inductive types}
The notation we wwill use is similar to the one used in 
\cite{Werner} and \cite{Paulin89} but we prefer
giving a label to each contructor and use that label instead of the
longer $Constr(n,\ind\{\ldots\})$ to indicate the $n^{th}$ constructor.
We adopt the vector notation to make things more readable.
$\overrightarrow{m}$ has to be intended as $m_1~\ldots~m_n$ where $n$ may
be equal to 0 (we use $m_1~\overrightarrow{m}$ when we want to give a
name to the first $m$ and assert $n>0$). If the vector notation is
used inside an arrow type it has a slightly different meaning, 
$A \to \overrightarrow{B} \to C$ is a shortcut for 
$A \to B_1 \to \ldots \to B_n \to C$

\subsection{Type definition}
$$\ind\{c_1:C(X); \ldots ; c_n:C(X)\}$$
$$C(X) ::= 
X \quad | \quad 
\forall m:T.C(X) \quad | \quad 
t \to C(X)$$
In the second case we need $(X \notin FV(T))$, while in the third we
need that POS(X,t) holds.
POS(X,t) is true iff t = X (POS has a meaning only for Higher Order...).


\subsection{Induction principle}
The induction principle for an inductive type $X$ and a predicate $Q$ 
is a constant with the following type
$$X_{ind}:\overrightarrow{\vartriangle\{C(X), c\}} \to \forall t:X.Q(x)$$
$\vartriangle$ takes a constructor type and the is defined by recursion on $C(X)$.
\begin{eqnarray}
\vartriangle\{C(X), c\} & = & Q(c) \nonumber\\
\vartriangle\{\forall t:T.C(X), c\} & = & 
        \forall m:T.\vartriangle\{C(X),c~m\} \nonumber\\
\vartriangle\{t \to C(X), c\} & = & 
        \forall t:X.Q(t) \to \vartriangle\{C(X), c~t\} \nonumber
\end{eqnarray}


\subsection{Recursor}
\subsubsection{Type}
The type of the recursor $R_X$ on an inductive type $X$ is
$$R_X : \overrightarrow{\square\{C(X)\}} \to X \to \alpha$$
$\square$ is defined by recursion on the contructor type $C(X)$.
\begin{eqnarray}
\square\{X\} & = & \alpha \nonumber \\
\square\{\forall m:T.C(X)\} & = & T \to \square\{C(X)\}\nonumber \\
\square\{t \to C(X)\} & = & X \to \alpha \to \square\{C(X)\}\nonumber 
\end{eqnarray}
\subsubsection{Reduction rules}
We say that 
$$R_X~\overrightarrow{f}~(c_i~\overrightarrow{m}) \leadsto
\triangledown\{C(X)_i, f_i, \overrightarrow{m}\}$$
$\triangledown$ is defined by recursion on the constructor type $C(X)$.
\begin{eqnarray}
\triangledown\{X, f, \overrightarrow{m}\} & = & f\nonumber \\
\triangledown\{\forall m:T.C(X), f, m_1~\overrightarrow{m}\} & = &
        \triangledown\{C(X), f~m_1, \overrightarrow{m}\}\nonumber \\
\triangledown\{t \to C(X), f, m_1~\overrightarrow{m}\} & = & 
        \triangledown\{C(X), f~m_1~(R_X~\overrightarrow{f}~m_1),
        \overrightarrow{m}\}\nonumber
\end{eqnarray}

\subsection{$R_X : \sem{X_{ind}}$ and $R_X\R X_{ind}$}
We have to compare the definition of $\square$ and $\vartriangle$
since thay play the same role in constructing respectively $R_X$ and
$X_{ind}$. If we assume $\alpha = \sem{Q}$ and we apply the $\sem$
function to each righ side of the $\vartriangle$ definition we obtain
exactly $\square$. The last two elements of the arrows $R_X$ and
$X_{ind}$ are again the same up to $\sem$.

questa non va bene, il caso base e' se il tipo del costruttore usa
solo le prime 2 regole di delta, quello induttivo se usa ANCHE la
terza...

To prove that $R_X\R X_{ind}$ we must assume that for each $i$ index
of a constructor of $X$, $f_i \R \vartriangle\{C(X)_i, c_i\}$ and we
have to proove that for each $t:X$
$$R_X~\overrightarrow{f}~t \R Q(t)$$.
We proceede by induction on the type of the head constructor $c_i$ in $t$.
The first base case is $c_i=X$ that, according to $\triangledown$, 
reduces in one 
step to $f_i$ and by hypothesis we have $f_i \R \vartriangle\{X,
c_i\}$. Unfolding $\vartriangle$ we have $f_i \R Q(c_i)$. The second
base case is $c_i=\overrightarrow{\forall t:T}.X$ and is analoug to
the first case.\\
The inductive step is when we have one or more recursive aruments in
$c_i$ and the induction hypothesis is that for each recursve argument
$m$, $R_X~\overrightarrow{f}~m \R X \to Q$. Since $f_i \R
\vartriangle\{C(X)_i, c_i\}$ and
$R_X~\overrightarrow{f}~(c_i~\overrightarrow{m})$ reduces to 
$f_i~\overrightarrow{...}$






\begin{thebibliography}{}
\bibitem{Girard86}G.Y.Girard. The system F of variable types, fifteen
years later. Theoretical Computer Science 45, 1986.
\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{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{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}