+++ /dev/null
-\documentclass[times, 10pt,twocolumn, draft]{article}
-\pagestyle{headings}
-%\usepackage{graphicx}
-\usepackage{amssymb,amsmath,mathrsfs,stmaryrd,amsthm}
-%\usepackage{hyperref}
-%\usepackage{picins}
-\usepackage{latex8}
-\usepackage{times}
-
-\pagestyle{empty}
-
-
-\newcommand{\semT}[1]{\ensuremath{\llbracket #1 \rrbracket}}
-\newcommand{\sem}[1]{\llbracket \ensuremath{#1} \rrbracket}
-\newcommand{\pair}[2]{<\!#1,#2\!>}
-\newcommand{\canonical}{\bot}
-\newcommand{\R}{~\mathscr{R}~}
-\newcommand{\N}{\,\mathbb{N}\,}
-\newcommand{\B}{\,\mathbb{B}\,}
-\newcommand{\NT}{\,\mathbb{N}\,}
-\newcommand{\NH}{\,\mathbb{N}\,}
-\renewcommand{\star}{\ast}
-\renewcommand{\vec}{\overrightarrow}
-\newcommand{\one}{{\bf 1}}
-\newcommand{\mult}{\cdot}
-\newcommand{\ind}{Ind(X)}
-\newcommand{\indP}{Ind(\vec{P}~|~X)}
-\newcommand{\Xind}{\ensuremath{X_{ind}}}
-\newcommand{\XindP}{\ensuremath{X_{ind}}}
-\renewcommand{\|}{\ensuremath{\quad | \quad}}
-\newcommand{\triUP}{\ensuremath{\Delta}}
-\newcommand{\triDOWN}{\ensuremath{\nabla}}
-\newcommand{\Rx}{\ensuremath{R_X}}
-
-\newtheorem{thm}{Theorem}[subsection]
-
-\title{Modified Realizability and Inductive Types}
-\author{...}
-
-
-\begin{document}
-\maketitle
-\thispagestyle{empty}
-
-\begin{abstract}
-In 1959, Kreisel introduced a notion of ``modified'' realizability to
-provide an alternative technique to G\"odel functional (dialectica)
-interpretation for establishing the connection between Peano Arihtmetic
-and System T. While the dialectica interpretation has been widely
-studied in the literature, Kreisel's technique, although remarkably
-simpler,has apparently been almost neglected (with the only exception
-of Troelstra). In this paper we give a modern presentation of the technique,
-and generalize it to arbitrary inductive types in a first order setting.
-This is part of a larger program, advocating the study
-of logical systems with primitive inductive types starting form
-weak, predicative logical frameworks and adding little by little small
-bits of logical power.
-
-\end{abstract}
-
-%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
-\Section{Introduction}
-The characterization of the provable recursive functions of
-Peano Arithmetic as the terms of system T is a well known
-result of G\"odel \cite{Godel58,Godel90}. Although several authors acknowledge
-that the functional interpretation of the Dialectica paper
-is not among the major achievements of the author (see e.g. \cite{Girard87}),
-the result has been extensively investigated and there is a wide
-literature on the
-topic (see e.g. \cite{Troelstra,HS86,Girard87}, just to mention textbooks,
-and the bibliography therein).
-
-A different, more neglected, but for many respects much more
-direct relation between Peano (or Heyting) Arithmetics and
-G\"odel System T is provided
-by the so called {\em modified realizability}. Modified realizability
-was first introduced by Kreisel in \cite{Kreisel59} - although it will take you
-a bit of effort to recognize it in the few lines of paragraph 3.52 -
-and later in \cite{Kreisel62} under the name of generalized realizability.
-The name of modified realizability seems to be due to Troelstra
-\cite{Troelstra}
-- who contested Kreisel's name but unfortunately failed in proposing
-a valid alternative; we shall reluctantly adopt this latter name
-to avoid further confusion. Modified realizability is a typed variant of
-realizability, essentially providing interpretations
-of $HA^{\omega}$ into itself: each theorem is realized by a typed function
-of system T, that also gives the actual computational content extracted
-from the proof.
-In spite of the simplicity and the elegance of the proof, it is extremely
-difficult to find a modern discussion of this result; the most recent
-exposition we are aware of is in the encyclopedic work by
-Troelstra \cite{Troelstra} (pp.213-229) going back to thirty years ago.
-Even modern introductory books
-to Type Theory and Proof Theory devoting much space to system T
-such as \cite{GLT} and \cite{TS} surprisingly leave out this simple and
-illuminating result. Both the previous textbooks
-prefer to focus on higher order arithmetics and its relation with
-Girard's System $F$ \cite{Girard86}, but the technical complexity and
-the didactical value of the two proofs is not comparable: when you
-prove that the Induction Principle is realized by the recursor $R$
-of system $T$ you catch a sudden gleam of understanding in the
-students eyes; usually, the same does not happen when you show, say,
-that the ``forgetful'' interpretation of the higher order predicate defining
-the natural numbers is the system $F$ encoding
-$\forall X.(X\to X) \to X \to X$ of $\N$.
-Moreover, after a first period of enthusiasm, the impredicative
-encoding of inductive types in Logical Frameworks has shown several
-problems and limitations (see e.g. \cite{Werner} pp.24-25) mostly
-solved by assuming inductive types as a primitive logical notion
-(leading e.g. form the Calculus of Constructions to the Calculus
-of Inductive Constructions - CIC). Even the extraction algorithm of
-CIC, strictly based on realizability principles, and in a first time
-still oriented towards System F \cite{Paulin87,Paulin89} has been
-recently rewritten \cite{Letouzey04}
-to take advantage of concrete types and pattern matching of ML-like
-languages. Unfortunately, systems like the Calculus of Inductive
-Constructions are so complex, from the logical point of view, to
-substantially prevent a really neat theoretical exposition (at present,
-it does not
-even exists a truly complete consistency proofs covering all aspects
-of such systems); moreover, not everybody may be interested in all the features
-offered by these frameworks, from polymorphism to types depending on
-proofs. Our program is to restart the analysis of logical systems with
-primitive inductive types in a smooth way, starting form first order
-logic and adding little by little small bits of logical power.
-This paper is the first step in this direction.
-
-%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
-\Section{G\"odel system T}
-We shall use a variant of system T with three atomic types $\N$ (natural
-numbers), $\B$ (booleans) and $\one$ (a terminal object), and two binary
-type constructors $\times$ (product) and $\to$ (arrow type).
-
-The terms of the language comprise the usual simply typed lambda terms
-with explicit pairs, plus the following additional constants:
-\begin{itemize}
-\item $*:\one$,
-\item $true: \B$, $false:\B$, $D:A\to A \to \B \to A$
-\item $O:\N$, $S:\N \to \N$, $R:A \to (A \to \N \to A) \to \N \to A$,
-\end{itemize}
-Redexes comprise $\beta$-reduction, projections,
-and type specific reductions as reported in table \ref{tab:tredex}
-
-\begin{table}[!h]
-\hrule\vspace{0.1cm}
-\begin{tabular}{p{0.34\textwidth}r}
- $\lambda x:U.M ~ N \leadsto M[N/x]$ & $(\beta)$ \\
- $fst \pair{M}{N} \leadsto M$ & $(\pi_1)$ \\
- $snd \pair{M}{N} \leadsto N$ & $(\pi_2)$ \\
- $D~M~N~ true \leadsto M$ & $(D_{true})$ \\
- $D~M~N~false \leadsto N$ & $(D_{false})$ \\
- $R~M~F~ 0 \leadsto M$ & $(R_0)$ \\
- $R~M~F~(S~n) \leadsto F~n~(R~M~F~n)$ & $(R_S)$ \\
- $M \leadsto * ~~~~ $ for any M of type $\one$ & $(*)$
-\end{tabular}\vspace{0.1cm}
-\hrule
-\caption{\label{tab:tredex}Reduction rules for System T}
-\end{table}
-
-Note that using the well known isomorpshims
-$\one \to A \cong A$, $A \to \one \cong \one$
-and $A \times \one \cong A \cong \one\times A$ (see \cite{AL91}, pp.231-239)
-we may always get rid of $\one$ (apart the trivial case).
-The terminal object does not play a major role in our treatment, but
-it allows to extract better algorithms. In particular we use it
-to realize atomic proposition, and stripping out the terminal object using
-the above isomorphisms gives a simple way of just keeping the truly
-informative part of the algorithms.
-
-\Section{Heyting's arithmetics}
-
-{\bf Axioms}
-
-\begin{itemize}
-\item $nat\_ind: P(0) \to (\forall x.P(x) \to P(S(x))) \to \forall x.P(x)$
-\item $ex\_ind: (\forall x.P(x) \to Q) \to \exists x.P(x) \to Q$
-\item $ex\_intro: \forall x.(P \to \exists x.P)$
-\item $fst: P \land Q \to P$
-\item $snd: P \land Q \to Q$
-\item $conj: P \to Q \to P \land Q$
-\item $false\_ind: \bot \to Q$
-\item $discriminate:\forall x.0 = S(x) \to \bot$
-\item $injS: \forall x,y.S(x) = S(y) \to x=y$
-\item $plus\_O:\forall x.x+0=x$
-\item $plus\_S:\forall x,y.x+S(y)=S(x+y)$
-\item $times\_O:\forall x.x\mult0=0$
-\item $times\_S:\forall x,y.x\mult S(y)=x+(x\mult y)$
-\end{itemize}
-
-\noindent
-{\bf Inference Rules}
-
-say that ax:AX refers to the previous Axioms list...
-%\begin{table}[!h]
-%\hrule\vspace{0.1cm}
-%\begin{tabular}{p{0.34\textwidth}r}
-
- $$\Gamma, x:A, \Delta \vdash x:A ~~~ (Proj)$$
- $$ \Gamma \vdash ax : AX~~~ (Const)$$
- $$\frac{\Gamma,x:A \vdash M:Q}{\Gamma \vdash \lambda x:A.M: A \to Q} ~~~ (\to_i)$$
- $$\frac{\Gamma \vdash M: A \to Q \hspace{0.5cm}\Gamma \vdash N: A}
- {\Gamma \vdash M N: Q} ~~~ (\to_e)$$
- $$\frac{\Gamma \vdash M:P}{\Gamma \vdash \lambda x:\N.M: \forall x.P}(*) ~~~
- (\forall_i)$$
- $$\frac{\Gamma \vdash M :\forall x.P}{\Gamma \vdash M t: P[t/x]}
- ~~~ (\forall_e)$$
-
-%\end{tabular}\vspace{0.1cm}
-%\hrule
-%\caption{\label{tab:HArules}Inference rules}
-%\end{table}{lr}
-
-%\[
-% (\land_i)\frac{\Gamma \vdash M:A \hspace{1cm}\Gamma \vdash N:B}
-% {\Gamma \vdash \pair{M}{N} : A \land B}
-%\hspace{2cm}
-% (\land_{el})\frac{\Gamma \vdash A \land B}{\Gamma \vdash A}
-%\hspace{2cm}
-% (\land_{er})\frac{\Gamma \vdash A \land B}{\Gamma \vdash B}
-%\]
-
-
-%\[
-% (\exists_i)\frac{\Gamma \vdash P[t/x]}{\Gamma \vdash \exists x.P}\hspace{2cm}
-% (\exists_e)\frac{\Gamma \vdash \exists x.P\hspace{1cm}\Gamma \vdash \forall x.P \to Q}
-%{\Gamma \vdash Q}
-%\]
-
-\Section{Extraction}
-
-The formulae to types translation function $\sem{\cdot}$, see table
-\ref{tab:formulae2types}, takes in input formulae in HA and returns
-types in T. In table \ref{tab:structproof} we the proofs to terms
-function for structured proofs. Axiom translation is reported in table
-\ref{tab:axioms}. In table \ref{tab:canonical} we define how the
-canoniac element is formed.
-
-\begin{table}[!h]
-\hrule\vspace{0.1cm}
-\begin{tabular}{p{0.21\textwidth}p{0.21\textwidth}}
- $\sem{A} = \one$ if A is atomic &
- $\sem{A \land B} = \sem{A}\times \sem{B}$ \\
- $\sem{A \to B} = \sem{A}\to \sem{B}$ &
- $\sem{\forall x:\N.P} = \N \to \sem{P}$ \\
- $\sem{\exists x:\N.P} = \N \times \sem{P}$ &
-\end{tabular}\vspace{0.1cm}
-\hrule
-\caption{\label{tab:formulae2types}Formulae to types translation}
-\end{table}
-
-\begin{table}[!h]
-\hrule\vspace{0.1cm}
-\begin{tabular}{p{0.20\textwidth}p{0.20\textwidth}}
- $\semT{M N} = \semT{M} \semT{N}$ &
- $\semT{M t} = \semT{M} \semT{t}$ \\
- \multicolumn{2}{l}{$\semT{\lambda x:A.M} = \lambda x:\sem{A}.\semT{M}$} \\
- \multicolumn{2}{l}{$\semT{\lambda x:\N.M} = \lambda x:\N.\semT{M}$}
-\end{tabular}\vspace{0.1cm}
-\hrule
-\caption{\label{tab:structproof}Structured proofs}
-\end{table}
-
-\begin{table}[!h]
-\hrule\vspace{0.1cm}
-\begin{tabular}{l}%{0.47\textwidth}p{0.47\textwidth}}
- $\sem{fst} = \pi_1$\\
- $\sem{snd} = \pi_2$\\
- $\sem{conj} = \lambda x:\sem{P}.\lambda y:\sem{Q}.\pair{x}{y}$\\
- $\sem{false\_ind} = \canonical_{\sem{Q}}$\\
- $\sem{discriminate} = \lambda \_:\N.\lambda \_:\one.\star$\\
- $\sem{injS}= \lambda \_:\N. \lambda \_:\N.\lambda \_:\one.\star$\\
- $\sem{plus\_O} = \sem{times\_O} = \lambda \_:\N.\star$\\
- $\sem{nat\_ind} = R$ \\
- $\sem{plus\_S} = \sem{times\_S} = \lambda \_:\N. \lambda \_:\N.\star$ \\
- $\sem{ex\_intro} = \lambda x:\N.\lambda f:\sem{P}.\pair{x}{f}$ \\
- $\sem{ex\_ind} = \lambda f:(\N \to \sem{P} \to \sem{Q}).$\\
- $\qquad\lambda p:\N\times \sem{P}.f~(fst~p)~(snd~p)$
-\end{tabular}\vspace{0.1cm}
-\hrule
-\caption{\label{tab:axioms}Axioms translation}
-\end{table}
-
-\begin{table}[!h]
-\hrule\vspace{0.1cm}
-\begin{tabular}{l}%p{0.23\textwidth}p{0.23\textwidth}}
- $\canonical_\one = \lambda x:\one.x$ \\
- $\canonical_N = \lambda x:\one.0$ \\
- $\canonical_{U\times V} = \lambda x:\one.\pair{\canonical_{U}
- x}{\canonical_{V} x}$ \\
- $\canonical_{U\to V} = \lambda x:\one.\lambda \_:U. \canonical_{V} x$
-\end{tabular}\vspace{0.1cm}
-\hrule
-\caption{\label{tab:canonical}Canonical element}
-\end{table}
-
-
-\Section{Realizability}
-The realizability relation is a relation $f \R P$ where $f: \sem{P}$, and
-$P$ is a closed formula.
-In particular:
-\begin{itemize}
-\item $\neg (\star \R \bot)$
-\item $* \R (t_1=t_2)$ iff $t_1=t_2$ is true ...
-\item $\pair{f}{g} \R (P\land Q)$ iff $f \R P$ and $g \R Q$
-\item $f \R (P\to Q)$ iff for any $m$ such that $m \R P$, $(f \,m) \R Q$
-\item $f \R (\forall x.P)$ iff for any natural number $n$ $(f n) \R P[\underline{n}/x]$
-\item $\pair{n}{g}\R (\exists x.P)$ iff $g \R P[\underline{n}/x]$
-\end{itemize}
-%We need to generalize the notion of realizability to sequents.
-%Given a sequent $B_1, \ldots, B_n \vdash A$ with free variables in
-%$\vec{x} = x_1,\ldots, x_m$, we say that $f \R B1, \ldots, B_n \vdash A$ iff
-%forall natural numbers $n_1, \ldots, n_m$,
-%if forall $i \in {1,\ldots,n}$
-%$m_i \R B_i[\vec{\underline{n}}/\vec{x}]$ then
-%$$f <m_1, \ldots, m_n> \R A[\vec{\underline{n}}/\vec{x}]$$.
-%
-\noindent
-We need to generalize the notion of realizability to sequents.\\
-Let $\vec{x} = FV_{\N}( B_1, \ldots, B_n, P)$ a vector of variables of type
-$\N$ that occur free in $B_1, \ldots, B_n, P$. Let $\vec{b:B}$ the vector
-$b_1:B_1, \ldots, b_n:B_n$.\\
-We say that $f \R B_1, \ldots, B_n \vdash A:P$ iff
-$$\lambda \vec{x:\N}. \lambda \vec{b:B}.f \R
-\forall \vec{x}. B_1 \to \ldots \to B_n \to P$$
-Note that $\forall \vec{x}. B_1 \to \ldots \to B_n \to P$ is a closed formula,
-so we can use the previous definition of realizability on it.
-
-\noindent
-We proceed to prove that all axioms $ax:Ax$ are realized by $\sem{ax}$.
-
-\begin{itemize}
-\item $nat\_ind$.
- We must prove that the recursion schema $R$ realizes the induction principle.
- To this aim we must prove that for any $a$ and $f$ such that $a \R P(0)$ and
- $f \R \forall x.(P(x) \to P(S(x)))$, and any natural number $n$, $(R \,a \,f
- \,n) \R P(\underline{n})$.\\
- We proceed by induction on n.\\
- If $n=O$, $(R \,a \,f \,O) = a$ and by hypothesis $a \R P(0)$.\\
- Suppose by induction that
- $(R \,a \,f \,n) \R P(\underline{n})$, and let us prove that the relation
- still holds for $n+1$. By definition
- $(R \,a \,f \,(n+1)) = f \,n \,(R \,a \,f \,n)$,
- and since $f \R \forall x.(P(x) \to P(S(x)))$,
- $(f n (R a f n)) \R P(S(\underline{n}))=P(\underline{n+1})$.
-
-\item $ex\_ind$.
- We must prove that $$\underline{ex\_ind} \R (\forall x:(P x)
- \to Q) \to (\exists x:(P x)) \to Q$$ Following the definition of $\R$ we have
- to prove that given\\ $f~\R~\forall~x:((P~x)~\to~Q)$ and
- $p~\R~\exists~x:(P~x)$, then $\underline{ex\_ind}~f~p \R Q$.\\
- $p$ is a couple $\pair{n_p}{g_p}$ such that $g_p \R P[\underline{n_p}/x]$, while
- $f$ is a function such that forall $n$ and for all $m \R P[\underline{n}/x]$
- then $f~n~m \R Q$ (note that $x$ is not free in $Q$ so $[\underline{n}/x]$
- affects only $P$).\\
- Expanding the definition of $\underline{ex\_ind}$, $fst$
- and $snd$ we obtain $f~n_p~g_p$ that we know is in relation $\R$ with $Q$
- since $g_p \R P[\underline{n_p}/x]$.
-
-\item $ex\_intro$.
- We must prove that
- $$\lambda x:\N.\lambda f:\sem{P}.\pair{x}{f} \R \forall x.(P\to\exists x.P(x)$$
- that leads to prove that for each n
- $\underline{ex\_into}~n \R (P\to\exists x.P(x))[\underline{n}/x]$.\\
- Evaluating the substitution we have
- $\underline{ex\_into}~n \R (P[\underline{n}/x]\to\exists x.P(x))$.\\
- Again by definition of $\R$ we have to prove that given a
- $m \R P[\underline{n}/x]$ then $\underline{ex\_into}~n~m \R \exists x.P(x)$.
- Expanding the definition of $\underline{ex\_intro}$ we have
- $\pair{n}{m} \R \exists x.P(x)$ that is true since $m \R P[\underline{n}/x]$.
-
-\item $fst$.
- We have to prove that $\pi_1 \R P \land Q \to P$, that is equal to proving
- that for each $m \R P \land Q$ then $\pi_1~m \R P$ .
- $m$ must be a couple $\pair{f_m}{g_m}$ such that $f_m \R P$ and $g_m \R Q$.
- So we conclude that $\pi_1~m$ reduces to $f_m$ that is in relation $\R$
- with $P$.
-
-\item $snd$. The same for $fst$.
-
-\item $conj$.
- We have to prove that
- $$\lambda x:\sem{P}. \lambda y:\sem{Q}.\pair{x}{y}\R P \to Q \to P \land Q$$
- Following the definition of $\R$ we have to show that
- for each $m \R P$ and for each $n \R Q$ then
- $(\lambda x:\sem{P}. \lambda y:\sem{Q}.\pair{x}{y})~m~n \R P \land Q$.\\
- This is the same of $\pair{m}{n} \R P \land Q$ that is verified since
- $m \R P$ and $n \R Q$.
-
-
-\item $false\_ind$.
- We have to prove that $\bot_{\sem{Q}} \R \bot \to Q$.
- Trivial, since there is no $m \R \bot$.
-
-\item $discriminate$.
- Since there is no $n$ such that $0 = S n$ is true... \\
- $\underline{discriminate}~n \R 0 = S~\underline{n} \to \bot$ for each n.
-
-\item $injS$.
- We have to prove that for each $n_1$ and $n_2$\\
- $\lambda \_:\N. \lambda \_:\N.\lambda \_:\one.*~n_1~n_2 \R
- (S(x)=S(y)\to x=y)[n_1/x][n_2/y]$.\\
- We assume that $m \R S(n_1)=S(n_2)$ and we have to show that
- $\lambda \_:\N. \lambda \_:\N.\lambda \_:\one.*~n_1~n_2~m$ that reduces to
- $*$ is in relation $\R$ with $n_1=n_2$. Since in the standard model of
- natural numbers $S(n_1)=S(n_2)$ implies $n_1=n_2$ we have that
- $* \R n_1=n_2$.
-
-\item $plus\_O$.
- Since in the standard model for natural numbers $0$ is the neutral element
- for addition $\lambda \_:\N.\star \R \forall x.x + 0 = x$.
-
-\item $plus\_S$.
- In the standard model of natural numbers the addition of two numbers is the
- operation of counting the second starting from the first. So
- $$\lambda \_:\N. \lambda \_:\N. \star \R \forall x,y.x+S(y)=S(x+y)$$.
-
-\item $times\_O$.
- Since in the standard model for natural numbers $0$ is the absorbing element
- for multiplication $\lambda \_:\N.\star \R \forall x.x \mult 0 = 0$.
-
-\item $times\_S$.
- In the standard model of natural numbers the multiplications of two
- numbers is the operation of adding the first to himself a number of times
- equal to the second number. So
- $$\lambda \_:\N. \lambda \_:\N. \star \R \forall x,y.x+S(y)=S(x+y)$$.
-
-\end{itemize}
-
-
-\noindent
-{\bf example}\\
-Let us prove the following principle of well founded induction:
-\[(\forall m.(\forall p. p < m \to P~p) \to P~m) \to \forall n.P~n\]
-In the following proof we shall make use of proof-terms, since we finally
-wish to extract the computational content; we leave to reader the easy
-check that the proof object describes the usual and natural proof
-of the statement.
-
-We assume to have already proved the following lemmas (having trivial
-realizers):\\
-\[L : \forall p, q.p < q \to q \le 0 \to \bot\]
-\[M : \forall p,q,n.p < q \to q \le (S n) \to p \le n \]
-Let us assume $h : \forall m.(\forall p. p < m \to P~p) \to P~m$.
-We prove by induction on $n$ that $\forall q. q \le n \to P~q$.
-For $n=0$, we get a proof of $P ~q$ by
-\begin{eqnarray}
-B & \equiv & \lambda q.\lambda h_0:q \le 0. h ~q~ \nonumber\\
-& & \quad (\lambda p.\lambda k:p < q. false\_ind ~(L~p~q~k~h_0)) \nonumber
-\end{eqnarray}
-In the inductive case, we must prove that, for any $n$,
-\[(\forall q. q \le n \to P~q) \to (\forall q. q \le S n \to P~q)\]
-Assume $h_1: \forall q. q \le n \to P q$ and
-$h_2: q \le S ~n$. Let us prove $\forall p. p < q \to P~p$.
-If $h_3: p < q$ then $(M~ p~ q~ n~ h_3~ h_2): p \le n$, hence
-$h_1 ~p ~ (M~ p~ q~ n~ h_3~ h_2): P~p$.\\
-In conclusion, the proof of the
-inductive case is
-\begin{eqnarray}
-I & \equiv & \lambda n.\lambda h_1:\forall q. q \le n \to P~ q.\lambda q.\lambda h_2:q \le S n. \nonumber\\
- & & \quad h ~ q ~ (\lambda p.\lambda h_3:p < q.h_1 ~p~ (M~ p~ q~ n~ h_3~ h_2))
- \nonumber
-\end{eqnarray}
-(where $h$ is free in I).
-The full proof is
-\begin{eqnarray}
-& \lambda h:\forall m.(\forall p. p < m\to P~p)\to P~m.\lambda m. &\nonumber\\
-& \quad nat\_ind ~B ~ I ~m~m~ (le\_n ~ m) & \nonumber
-\end{eqnarray}
-
-where $le\_n$ is a proof that $\forall n. n \le n$, and the free $P$ in the definition of $nat_{ind}$ is instantiated with $\forall m.m \le m \to P~m$.\\
-Form the previous proof,after stripping terminal objects,
-and a bit of eta-contraction to make
-the term more readable, we extract the following term (types are omitted):
-
-\[R' \equiv \lambda f.\lambda m.
-R~ (\lambda n.f ~n~ (\lambda q.*))~
-(\lambda n\lambda g\lambda q.f ~q~g)~m ~m\]
-
-The intuition of this operator is the following: supose to
-have a recursive definition $h q = F[h]$ where $q:\N$ and
-$F[h]: A$. This defines a functional
-$f: \lambda q.\lambda g.F[g]: N\to(N\to A) \to A$, such that
-(morally) $h$ is the fixpoint of $f$. For instance,
-in the case of the fibonacci function, $f$ is
-\begin{eqnarray}
-fibo & \equiv & \lambda q. \lambda g. if~ q = 0~then~ 1~ else \nonumber\\
-& & \quad if~ q = 1~ then~ 1~ else ~ g (q-1)+g (q-2) \nonumber
-\end{eqnarray}
-
-So $f$ build a new
-approximation of $h$ from the previous approximation $h$ taken
-as input. $R'$ precisely computes the mth-approximation starting
-from a dummy function $(\lambda q.*_A)$. Alternatively,
-you may look at $g$ as the ``history'' (curse of values) of $h$
-for all values less or equal to $q$; then $f$ extend $g$ to
-$q+1$.
-
-Let's compute for example
-\begin{eqnarray}
-R'~fibo~2 & \leadsto &
- R~ (\lambda n.fibo ~n~ (\lambda q.*))~
- (\lambda n\lambda g\lambda q.fibo ~q~g)~2 ~2\nonumber\\
-& \leadsto &
- (\lambda n\lambda g\lambda q.fibo ~q~g)~1~
- (R~
- (\lambda n.fibo ~n~ (\lambda q.*))~
- (\lambda n\lambda g\lambda q.fibo ~q~g)~1)~
- 2 \nonumber\\
-& \leadsto &
- \lambda q.fibo ~q~
- (R~
- (\lambda n.fibo ~n~ (\lambda q.*))~
- (\lambda n\lambda g\lambda q.fibo ~q~g)~1)~
- 2 \nonumber\\
-& \leadsto &
- \lambda q.fibo ~q~
- ((\lambda n\lambda g\lambda q.fibo ~q~g)~0~
- (R~
- (\lambda n.fibo ~n~ (\lambda q.*))~
- (\lambda n\lambda g\lambda q.fibo ~q~g)~0))~
- 2 \nonumber\\
-& \leadsto &
- \lambda q.fibo ~q~
- (\lambda q.fibo ~q~
- (R~
- (\lambda n.fibo ~n~ (\lambda q.*))~
- (\lambda n\lambda g\lambda q.fibo ~q~g)~0)
- )2 \nonumber\\
-& \leadsto &
- \lambda q.fibo ~q~
- (\lambda q.fibo ~q~
- (\lambda n.fibo ~n~ (\lambda q.*)))2
- \nonumber\\
-& \leadsto &
- fibo~2~(\lambda q.fibo ~q~ (\lambda n.fibo ~n~ (\lambda q.*))) \nonumber\\
-& \leadsto &
- (\lambda q.fibo ~q~ (\lambda n.fibo ~n~ (\lambda q.*))) 1 +
- (\lambda q.fibo ~q~ (\lambda n.fibo ~n~ (\lambda q.*))) 0 \nonumber\\
-& \leadsto &
- fibo ~1~ (\lambda n.fibo ~n~ (\lambda q.*)) +
- fibo ~0~ (\lambda n.fibo ~n~ (\lambda q.*)) \nonumber\\
-& \leadsto &
- 1 + 1 \nonumber
-\end{eqnarray}
-Note that the second argument of $fibo$ is always a method to calculate all the prvious values of $fibo$. DA CAPIRE (per me) come mai $\lambda n$ non viene usata...
-CAPITA CON csc:
-
-n non serve perche' c'e' una relazione logica di n con q,
-in particolare $q <= Sn$ ... quindi $q < n$ (lemma M)...
-e quindi posso usare come history $< n$ una history $< q$.
-il $\lambda h2$ essendo $[[q <= Sn]]$ = 1 viene scartata.
-
-se si spiega come array viene decente... forse. lunedi' provo a scrivere
-meglio.
-
-\Section{Inductive types}
-The notation we will use is similar to the one used in
-\cite{Werner} and \cite{Paulin89} but we prefer
-giving a label to each constructor and use that label instead of the
-longer $Constr(n,\ind\{\ldots\})$ to indicate the $n^{th}$ constructor.
-We adopt the vector notation to make things more readable.
-$\vec{m}$ has to be intended as $m_1~\ldots~m_n$ where $n$ may
-be equal to 0 (we use $m_1~\vec{m}$ when we want to give a
-name to the first $m$ and assert $n>0$). If the vector notation is
-used inside an arrow type it has a slightly different meaning,
-$A \to \vec{B} \to C$ is a shortcut for
-$A \to B_1 \to \ldots \to B_n \to C$.
-
-%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
-\SubSection{Extensions to the logic framework}
-To talk about arbitrary inductive types (and not hard coded natural numbers) we
-have to extend a bit our framework.
-
-First we admit quantification over inductive types $T$, thus $\forall x:T.A$
-and $\exists x:T.A$ are allowed. Then rules 4 and 5 of the $\sem{\cdot}$
-definition are replaced by $\sem{\forall x:T.P} = T \to \sem{P}$ and
-$\sem{\exists x:T.P} = T \times \sem{P}$.
-
-For each inductive type we will describe the formation rules and the
-corresponding induction principle schema.
-
-Symmetrically we have to extend System T with arbitrary inductive types and
-we will see how theyr recursors are defined in the following sections.
-
-The definition of $\R$ is modified substituting each occurrence of $\N$ with
-a generic inductive type $T$.
-
-%%%%%%%%%%%%%%%%%%%%%%%%%%%%
-\SubSection{Type definition}
-$$\ind\{c_1:C(X); \ldots ; c_n:C(X)\}$$
-$$C(X) ::= X \| T \to C(X) \| X \to C(X)$$
-In the second case we mean $T \neq X$.
-
-%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
-\SubSection{Induction principle}
-The induction principle for an inductive type $X$ and a predicate $Q$
-is a constant with the following type
-$$\Xind:\vec{\triUP\{C(X), c\}} \to \forall t:X.Q(t)$$
-$\triUP$ takes a constructor type $C(X)$ and a term $c$ (initially $c$ is a
-constructor of X, and $c:C(X)$) and is defined by recursion as follows:
-\begin{eqnarray}
-\triUP\{X, c\} & = & Q(c) \nonumber\\
-\triUP\{T \to C(X), c\} & = &
- \forall m:T.\triUP\{C(X),c~m\} \nonumber\\
-\triUP\{X \to C(X), c\} & = &
- \forall t:X.Q(t) \to \triUP\{C(X), c~t\} \nonumber
-\end{eqnarray}
-
-%%%%%%%%%%%%%%%%%%%%%
-\SubSection{Recursor}
-%\SubSubSection{Type}
-The type of the recursor $\Rx$ on an inductive type $X$ is
-$$\Rx : \vec{\square\{C(X)\}} \to X \to \alpha$$
-$\square$ is defined by recursion on the constructor type $C(X)$.
-\begin{eqnarray}
-\square\{X\} & = & \alpha \nonumber \\
-\square\{T \to C(X)\} & = & T \to \square\{C(X)\}\nonumber \\
-\square\{X \to C(X)\} & = & X \to \alpha \to \square\{C(X)\}\nonumber
-\end{eqnarray}
-%\SubSubSection{Reduction rules}
-We say that
-$$\Rx~\vec{f}~(c_i~\vec{m}) \leadsto
-\triDOWN\{C(X)_i, f_i, \vec{m}\}$$
-$\triDOWN$ takes a constructor type $C(X)$, a term $f$
-(of type $\square\{C(X)\}$) and is defined by recursion as follows:
-\begin{eqnarray}
-\triDOWN\{X, f, \} & = & f\nonumber \\
-\triDOWN\{T \to C(X), f, m_1~\vec{m}\} & = &
- \triDOWN\{C(X), f~m_1, \vec{m}\}\nonumber \\
-\triDOWN\{X \to C(X), f, m_1~\vec{m}\} & = &
- \triDOWN\{C(X), f~m_1~(\Rx~\vec{f}~m_1),
- \vec{m}\}\nonumber
-\end{eqnarray}
-We assume $\Rx~\vec{f}~(c_i~\vec{m})$ is well typed, so in the first case we
-can omit $\vec{m}$ since it is an empty sequence.
-
-%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
-\SubSection{Realizability of the induction principle}
-Once we have inductive types and their induction principle we want to show that
-the recursor $\Rx$ realizes $\Xind$, that is that $\Rx$ has type
-$\sem{\Xind}$ and is in relation $\R$ with $\Xind$.
-
-\begin{thm}$\Rx : \sem{\Xind}$\end{thm}
-\begin{proof}
-We have to compare the definition of $\square$ and $\triUP$
-since they play the same role in constructing respectively the types of
-$\Rx$ and
-$\Xind$. If we assume $\alpha = \sem{Q}$ and we apply the $\sem{\cdot}$
-function to each right side of the $\triUP$ definition we obtain
-exactly $\square$. The last two elements of the arrows $\Rx$ and
-$\Xind$ are again the same up to $\sem{\cdot}$.
-\end{proof}
-
-\begin{thm}$\Rx\R \Xind$\end{thm}
-\begin{proof}
-To prove that $\Rx\R \Xind$ we must assume that for each $i$ index
-of a constructor of $X$, $f_i \R \triUP\{C(X)_i, c_i\}$ and we
-have to prove that for each $t:X$
-$$\Rx~\vec{f}~t \R Q(t)$$
-\noindent
-We proceed by induction on the structure of $t$.
-\\
-The base case is when the
-type of the head constructor of $t$ has no recursive arguments (i.e. the type
-is generated using only the first two rules $C(X)$), so
-$(\Rx~\vec{f}~(c_i~\vec{m}))$ reduces in one step to $(f_i~\vec{m})$. $f_i$
-realizes $\triUP\{C(X)_i, c_i\}$ by assumption and since we are in the base
-case $\triUP\{C(X)_i, c_i\}$ is of the form $\vec{\forall t:T}.Q(c_i~\vec{t})$.
-Thus $f_i~\vec{m} \R Q(c_i~\vec{m})$.
-\\
-In the induction step we have as induction hypothesis that for each recursive
-argument $t_i$ of the head constructor $c_i$, $r_i\equiv
-\Rx~\vec{f}~t_i \R Q(t_i)$. By the third rule of $\triDOWN$ we obtain the reduct
-$f_i~\vec{m}~\vec{t~r}$ (here we write first all the non recursive arguments,
-then all the recursive one. In general they can be mixed and the proof is
-exactly the same but the notation is really heavier). We know by hypothesis
-that $f_i \R \triUP\{C(X)_i, c_i\} \equiv \vec{\forall m:T}.\vec{\forall
-t:X.Q(t)} \to Q(c_i~\vec{m}~\vec{t})$, thus $f_i~\vec{m}~\vec{t~r} \R
-Q(c_i~\vec{m}~\vec{t})$.
-\end{proof}
-%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
-\Section{Strong normalization of extended system T}
-Strong normalization for system T is a well know result\cite{GLT}
-that can be easily extended to System T with this kind of inductive
-types. The first thing we have to do is to extend the definition of
-neutral term to the terms not of the form $<u,v>$, $\lambda x.u$,
-$c_i~\vec{m}$.
-
-In conformity with the demonstration we are extending we call $\nu(t)$
-the length of the longest reduction path from $t$ and $\ell(t)$ the
-number of symbols in the normal form of $t$.
-
-For an inductive type $\ind\{c_1:C(X); \ldots ; c_n:C(X)\}$
-we have to prove that for each $i$,
-given a proper sequence of reducible arguments $\vec{m}$ and $\vec{f}$,
-$(c_i~\vec{m})$ and $\Rx~\vec{f}~(c_i~\vec{m})$ are reducible.
-
-First the simple case of constructors. If the constructor $c_i$ takes
-no arguments then it is already in normal form. If it takes
-$m_1,\ldots,m_n$ reducible arguments, then $\nu(c_i~\vec{m}) = max \{m_1,
-\ldots,m_n\}$ and so $c_i~\vec{m}$ is strongly nomalizable thus
-reducible for the definition of reducibility for base types.
-
-To show that $\Rx~\vec{f}~(c_i~\vec{m})$ is reducible we can use
-(\textbf{CR 3}) that states that if $t$ is neutral and every $t'$ obtained by
-executing one redex of $t$ is reducible, then $t$ is reducible.
-
-Now we have to show that each term that can be obtained by a
-reduction step is reducible. We can procede induction on
-$\Sigma\nu(f_i) + \nu(c_i~\vec{m}) +
-\ell(c_i~\vec{m})$ since we know by hypothesis that $\vec{f}$ and
-$(c_i~\vec{m})$ are reducible and consequently strongly normalizing.
-\\
-The base case is when $c_i$ takes no arguments and $\vec{f}$ are
-normal. In this case the only redex we can compute is
-$$\Rx~\vec{f}~c_i~\leadsto~f_i$$ that is reducible by hypothesis.
-\\
-The interesting inductive case is when $\vec{m}$ and $\vec{f}$ are
-normal, so the only reduction step we can execute is
-$$\Rx~\vec{f}~(c_i~\vec{m})~\leadsto~f_i~\vec{m}~\vec{(\Rx~\vec{f}~n)}$$
-where $\vec{n}$ are the recursive arguments of $c_i$ (here we wrote
-the recursive calls as the last parameters of $f_i$ just to lighten
-notation). Since $\ell(n_j)$ is less than $\ell(c_i~\vec{m})$ for
-every $j$ we can apply the inductive hypothesis and state that
-$\Rx~\vec{f}~n_j$ is reducible. Then by definition of reducibility of
-the arrow types and by the hypothesis that $f_i$ and $\vec{m}$ are
-reducible, we obtain that $$f_i~\vec{m}~\vec{(\Rx~\vec{f}~n)}$$ is
-reducible.
-\\
-All other cases, when we execute a redex in $\vec{m}$ or $\vec{f}$,
-are straightforward applications of the induction hypothesis.
-
-
-%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
-\Section{Improving inductive types}
-It is possible to parametrise inductive types over other inductive types
-without much difficulties since the type $T$ in $C(X)$ is free. Both the
-recursor and the induction principle are schemas, parametric over $T$.
-
-Possiamo anche definire $X_{\vec{P}}\equiv Ind(P|X)={c_i : C(P|X)}$ e poi
-fare variare $T$ su $\vec{P}$, ma non ottengo niente di meglio.
-
-Credo anche che quantificare su eventuali variabili di tipo non cambi niente
-visto che non abbiamo funzioni.
-
-Se ammettiamo che i tipi dipendano da termini di tipo induttivo
-
-
-%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
-\bibliographystyle{latex8}
-%\bibliography{latex8}
-
-\begin{thebibliography}{}
-\bibitem{AL91}A.Asperti, G.Longo. Categories, Types and Structures.
-Foundations of Computing, Cambrdidge University press, 1991.
-\bibitem{Girard86}G.Y.Girard. The system F of variable types, fifteen
-years later. Theoretical Computer Science 45, 1986.
-\bibitem{Girard87}G.Y.Girard. Proof Theory and Logical Complexity.
-Bibliopolis, Napoli, 1987.
-\bibitem{GLT}G.Y.Girard, Y.Lafont, P.Tailor. Proofs and Types.
-Cambridge Tracts in Theoretical Computer Science 7.Cambridge University
-Press, 1989.
-\bibitem{Godel58}K.G\"odel. \"Uber eine bisher noch nicht ben\"utzte Erweiterung
-des finiten Standpunktes. Dialectica, 12, pp.34-38, 1958.
-\bibitem{Godel90}K.G\"odel. Collected Works. Vol.II, Oxford University Press,
-1990.
-\bibitem{HS86}J.R.Hindley, J. P. Seldin. Introduction to Combinators and
-Lambda-calculus, Cambridge University Press, 1986.
-\bibitem{Howard68}W.A.Howard. Functional interpretation of bar induction
-by bar recursion. Compositio Mathematica 20, pp.107-124. 1958
-\bibitem{Howard80}W.A.Howard. The formulae-as-types notion of constructions.
-in J.P.Seldin and j.R.Hindley editors, to H.B.Curry: Essays on Combinatory
-Logic, Lambda calculus and Formalism. Acedemic Press, 1980.
-\bibitem{Kleene45}S.C.Kleene. On the interpretation of intuitionistic
-number theory. Journal of Symbolic Logic, n.10, pp.109-124, 1945.
-\bibitem{Kreisel59} G.Kreisel. Interpretation of analysis by means of
-constructive functionals of finite type. In. A.Heyting ed.
-{\em Constructivity in mathematics}. North Holland, Amsterdam,1959.
- \bibitem{Kreisel62} G.Kreisel. On weak completeness of intuitionistic
-predicatelogic. Journal of Symbolic Logic 27, pp. 139-158. 1962.
-\bibitem{Letouzey04}P.Letouzey. Programmation fonctionnelle
-certifi\'ee; l'extraction
-de programmes dans l'assistant Coq. Ph.D. Thesis, Universit\'e de
-Paris XI-Orsay, 2004.
-\bibitem{Loef}P.Martin-L\"of. Intuitionistic Type Theory.
-Bibliopolis, Napoli, 1984.
-\bibitem{Paulin87}C.Paulin-Mohring. Extraction de programme dans le Calcul de
-Constructions. Ph.D. Thesis, Universit\'e de
-Paris 7, 1987.
-\bibitem{Paulin89}C.Paulin-Mohring. Extracting $F_{\omega}$ programs
-from proofs in the Calculus of Constructions. In proc. of the Sixteenth Annual
-ACM Symposium on
-Principles of Programming Languages, Austin, January, ACML Press 1989.
-\bibitem{Sch}K.Sch\"utte. Proof Theory. Grundlehren der mathematischen
-Wissenschaften 225, Springer Verlag, Berlin, 1977.
-\bibitem{Troelstra}A.S.Troelstra. Metamathemtical Investigation of
-Intuitionistic
-Arithmetic and Analysis. Lecture Notes in Mathematics 344, Springer Verlag,
-Berlin, 1973.
-\bibitem{TS}A.S.Troelstra, H.Schwichtenberg. Basic Proof Theory.
-Cambridge Tracts in Theoretical Computer Science 43.Cambridge University
-Press, 1996.
-\bibitem{Werner}B.Werner. Une Th\'eorie des Constructions Inductives.
-Ph.D.Thesis, Universit\'e de Paris 7, 1994.
-
-
-\end{thebibliography}
-
-\end{document}
-
projects / helm.git / blobdiff