-\documentclass[a4paper]{article}
+\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}
\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}
+\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
This paper is the first step in this direction.
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
-\section{G\"odel system T}
+\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).
\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$.
+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$
the above isomorphisms gives a simple way of just keeping the truly
informative part of the algorithms.
-
-
-\section{Heyting's arithmetics}
+\Section{Heyting's arithmetics}
{\bf Axioms}
{\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)\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}
-\]
+%\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}
% (\land_{er})\frac{\Gamma \vdash A \land B}{\Gamma \vdash B}
%\]
-\[
- (\forall_i)\hspace{0.2cm}\frac{\Gamma \vdash M:P}{\Gamma \vdash
- \lambda x:\N.M: \forall x.P}(*) \hspace{2cm}
- (\forall_e)\hspace{0.2cm}\frac{\Gamma \vdash M :\forall x.P}{\Gamma \vdash M t: P[t/x]}
-\]
-
%\[
% (\exists_i)\frac{\Gamma \vdash P[t/x]}{\Gamma \vdash \exists x.P}\hspace{2cm}
%{\Gamma \vdash Q}
%\]
-\section{Extraction}
-
-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:\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 $\canonical_T: \one \to T$ is inductively defined as follows:
-\begin{enumerate}
-\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}.\pair{x}{f}$
-\item $\sem{fst} = \pi_1$
-\item $\sem{snd} = \pi_2$
-\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 $\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}
+\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:
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)) \]
+\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_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)) \]
+\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
-\[ \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) \]
+\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
$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)\]
+\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
se si spiega come array viene decente... forse. lunedi' provo a scrivere
meglio.
-\section{Inductive types}
+\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
$A \to B_1 \to \ldots \to B_n \to C$.
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
-\subsection{Extensions to the logic framework}
+\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.
a generic inductive type $T$.
%%%%%%%%%%%%%%%%%%%%%%%%%%%%
-\subsection{Type definition}
+\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}
+\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)$$
\end{eqnarray}
%%%%%%%%%%%%%%%%%%%%%
-\subsection{Recursor}
-\subsubsection{Type}
+\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)$.
\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}
+%\SubSubSection{Reduction rules}
We say that
$$\Rx~\vec{f}~(c_i~\vec{m}) \leadsto
\triDOWN\{C(X)_i, f_i, \vec{m}\}$$
can omit $\vec{m}$ since it is an empty sequence.
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
-\subsection{Realizability of the induction principle}
+\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$.
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{Improoving inductive types}
-It is possible to parametrize inductive types over other inductive types
+\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$.
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+\bibliographystyle{latex8}
+%\bibliography{latex8}
+
\begin{thebibliography}{}
\bibitem{AL91}A.Asperti, G.Longo. Categories, Types and Structures.
Foundations of Computing, Cambrdidge University press, 1991.
projects / helm.git / blobdiff