\documentclass[a4paper]{article}
\pagestyle{headings}
%\usepackage{graphicx}
-\usepackage{amssymb,amsmath,mathrsfs}
+\usepackage{amssymb,amsmath,mathrsfs,stmaryrd,amsthm}
%\usepackage{hyperref}
%\usepackage{picins}
-\newcommand{\sem}[1]{[\![ #1 ]\!]}
-\newcommand{\R}{\;\mathscr{R}\;}
+\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}
-\newcommand{\one}{\mathbb{1}}
-\renewcommand{\times}{\cdot}
+\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{...}
...
\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
+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{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
prove that the Induction Principle is realized by the recursor $R$
-of system $T$ you catch a sudden gleam of intelligence in the
+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'' intrepretation of the higher order predicate defining
+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
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
+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
+\[(\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}
\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 $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)$
+\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...
+
+\[
+ (Proj)\hspace{0.2cm} \Gamma, x:A, \Delta \vdash x:A
+ \hspace{2cm}
+ (Const)\hspace{0.2cm} \Gamma \vdash ax : AX
+\]
+
\[
- (\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}
+ (\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}
\]
%\[
% (\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)\frac{\Gamma \vdash M:P}{\Gamma \vdash
+ (\forall_i)\hspace{0.2cm}\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]}
+ (\forall_e)\hspace{0.2cm}\frac{\Gamma \vdash M :\forall x.P}{\Gamma \vdash M t: P[t/x]}
\]
\section{Extraction}
-We have to extend systeem T with inductive types (and they recursors).
-\begin{itemize}
-\item $\sem{A} = 1$ if A is atomic
+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:T.P} = T \to \sem{P}$
-\item $\sem{\exists x:T.P} = T \times \sem{P}$
-\end{itemize}
+\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: 1 \to T$ is inuctively defined as follows:
+For any type T of system T $\canonical_T: \one \to T$ is inductively 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$
+\item $\canonical_\one = \lambda x:\one.x$
+\item $\canonical_N = \lambda x:\one.0$
+\item $\canonical_{U\times V} = \lambda x:\one.\pair{\canonical_{U} x}{\canonical_{V} x}$
+\item $\canonical_{U\to V} = \lambda x:\one.\lambda \_:U. \canonical_{V} x$
\end{enumerate}
\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{ex\_intro} = \lambda x:\N.\lambda f:\sem{P}.\pair{x}{f}$
\item $\sem{fst} = \pi_1$
\item $\sem{snd} = \pi_2$
-\item $\sem{conj} = \lambda x:\sem{P}.\lambda y:\sem{Q}.<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{conj} = \lambda x:\sem{P}.\lambda y:\sem{Q}.\pair{x}{y}$
+\item $\sem{false\_ind} = \canonical_{\sem{Q}}$
+\item $\sem{discriminate} = \lambda \_:\N.\lambda \_:\one.\star$
+\item $\sem{injS}= \lambda \_:\N. \lambda \_:\N.\lambda \_:\one.\star$
\item $\sem{plus\_O} = \sem{times\_O} = \lambda \_:\N.\star$
\item $\sem{plus\_S} = \sem{times_S} = \lambda \_:\N. \lambda \_:\N.\star$
\end{itemize}
In the case of structured proofs:
\begin{itemize}
-\item $\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}$
+\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}$.
+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
+%$\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}$.
\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$).\\
- Exapanding the definition of $\underline{ex\_ind}$, $fst$
+ 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}.<x,f> \R \forall x.(P\to\exists x.P(x)$$
- that leads to prove that foreach n
+ $$\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
- $<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$.
- Wehave to prove that $\pi_1 \R P \land Q \to P$, that is equal to proving
+ 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
- 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
+ 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 $injS$.
We have to prove that for each $n_1$ and $n_2$\\
- $\lambda \_:\N. \lambda \_:\N.\lambda \_:1.*~n_1~n_2 \R
+ $\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 \_:1.*~n_1~n_2~m$ that reduces to
+ $\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 $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$.
+ 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
\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
+\[ 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 \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 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' \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
+\[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
+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 wwill use is similar to the one used in
+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 contructor and use that label instead of the
+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.
-$\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
+$\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 \overrightarrow{B} \to C$ is a shortcut for
-$A \to B_1 \to \ldots \to B_n \to C$
+$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 \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...).
-
+$$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
-$$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)$.
+$$\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}
-\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
+\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 $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)$.
+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\{\forall m:T.C(X)\} & = & T \to \square\{C(X)\}\nonumber \\
-\square\{t \to C(X)\} & = & X \to \alpha \to \square\{C(X)\}\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
-$$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)$.
+$$\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}
-\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
+\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}
-
-\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{...}$
-
-
-
-
-
-
+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{Improoving inductive types}
+It is possible to parametrize 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
+
+
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\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