X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fpapers%2Fsystem_T%2Ft.tex;h=7804118ab5a00d8284195acd07f3dc8460dba1be;hb=4167cea65ca58897d1a3dbb81ff95de5074700cc;hp=df00823e88061ee5f08fd0491ee09126571cffc8;hpb=24a1ba93b3894d03eeb212fdd077b0712a8e1947;p=helm.git diff --git a/helm/papers/system_T/t.tex b/helm/papers/system_T/t.tex index df00823e8..7804118ab 100644 --- a/helm/papers/system_T/t.tex +++ b/helm/papers/system_T/t.tex @@ -1,19 +1,35 @@ \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} -\title{A gentle approach to\\program extraction and realizability} +\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{...} @@ -24,12 +40,117 @@ ... \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 +\[(\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)$ @@ -41,22 +162,30 @@ \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 : 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} @@ -64,9 +193,9 @@ %\] \[ - (\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]} \] @@ -78,57 +207,79 @@ \section{Extraction} -\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.P} = \N \to \sem{P}$ -\item $\sem{\exists x.P} = \N \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}.$ +\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}.$ -\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 $ \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 $ \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 \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}$. @@ -153,30 +304,30 @@ 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 $$ 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}. \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 - $ \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 $$ 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$. @@ -184,11 +335,11 @@ We proceed to prove that all axioms $ax:Ax$ are realized by $\sem{ax}$. \item $conj$. We have to prove that - $$\lambda x:\sem{P}. \lambda y:\sem{Q}. \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}.)~m~n \R P \land Q$.\\ - This is the same of $ \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$. @@ -202,10 +353,10 @@ We proceed to prove that all axioms $ax:Ax$ are realized by $\sem{ax}$. \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$. @@ -221,7 +372,7 @@ We proceed to prove that all axioms $ax:Ax$ are realized by $\sem{ax}$. \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 @@ -229,42 +380,319 @@ We proceed to prove that all axioms $ax:Ax$ are realized by $\sem{ax}$. 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 +\[ 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 +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{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{GLT}G.Y.Girard. Proof Theory and Logical Complexity. +\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{God}K.G\"odel. \"Uber eine bisher noch nicht ben\"utzte Erweiterung +\bibitem{Godel58}K.G\"odel. \"Uber eine bisher noch nicht ben\"utzte Erweiterung des finiten Standpunktes. Dialectica, 12, pp.34-38, 1958. -\bibitem{God}K.G\"odel. Collected Works. Vol.II, Oxford University Press, +\bibitem{Godel90}K.G\"odel. Collected Works. Vol.II, Oxford University Press, 1990. -\bibitem{How}W.A.Howard. The formulae-as-types notion of constructions. +\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{Let}P.Letouzey. Programmation fonctionnelle certifi\'ee; l'extraction +\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{Pau87}C.Paulin-Mohring. Extraction de programme dans le Calcul de +\bibitem{Paulin87}C.Paulin-Mohring. Extraction de programme dans le Calcul de Constructions. Ph.D. Thesis, Universit\'e de Paris 7, 1987. -\bibitem{Pau89}C.Paulin-Mohring. Extracting $F_{\omega}$ programs from proofs -in the Calculus of Constructions. In proc. of the Sixteenth Annual +\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{Tro}A.S.Troelstra. Metamathemtical Investigation of Intuitionistic +\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}