\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}}
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{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}
%\[
% (\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}
\end{enumerate}
definition.
-For any type T of system T $\bot_T: \one \to T$ is inductively defined as follows:
+For any type T of system T $\canonical_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$
+\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{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$
\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}
-%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+
+\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 will use is similar to the one used in
\cite{Werner} and \cite{Paulin89} but we prefer
\subsection{Induction principle}
The induction principle for an inductive type $X$ and a predicate $Q$
is a constant with the following type
-$$\Xind:\vec{\triUP\{C(X), c\}} \to \forall t:X.Q(x)$$
+$$\Xind:\vec{\triUP\{C(X), c\}} \to \forall t:X.Q(t)$$
$\triUP$ takes a constructor type $C(X)$ and a term $c$ (initially $c$ is a
constructor of X, and $c:C(X)$) and is defined by recursion as follows:
\begin{eqnarray}
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