%\usepackage{picins}
\newcommand{\sem}[1]{[\![ #1 ]\!]}
-\newcommand{\R}{\,\mathscr{R}\,}
-\title{...}
+\newcommand{\R}{\;\mathscr{R}\;}
+\newcommand{\N}{\,\mathbb{N}\,}
+\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}
\author{...}
\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*0=0$
-\item $timies\_S:\forall x,y.x*S(y)=x+(x*y)$
+\item $times\_O:\forall x.x\times0=0$
+\item $times\_S:\forall x,y.x\times S(y)=x+(x\times y)$
\end{itemize}
\noindent
\[
(\forall_i)\frac{\Gamma \vdash M:P}{\Gamma \vdash
- \lambda x:N.M: \forall x.P}(*) \hspace{2cm}
+ \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]}
\]
\item $\sem{A} = 1$ 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}$
+\item $\sem{\forall x.P} = \N \to \sem{P}$
+\item $\sem{\exists x.P} = \N \times \sem{P}$
\end{itemize}
definition.
\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{fst} = fst$
-\item $\sem{snd} = snd$
+\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{fst} = \pi_1$
+\item $\sem{snd} = \pi_2$
\item $\sem{conj} = \lambda x:\sem{P}.\lambda y:\sem{Q}.<x,y>$
\item $\sem{false\_ind} = \bot_{\sem{Q}}$
-\item $\sem{discriminate} = \lambda \_:N.\lambda \_:1.*$
-\item $\sem{injS}= \lambda \_:N. \lambda \_:N.\lambda \_:1.*$
-\item $\sem{plus\_O} = \sem{times\_O} = \lambda \_:N.*$
-\item $\sem{plus\_S} = \sem{times_S} = \lambda \_:N. \lambda \_:N.*$
+\item $\sem{discriminate} = \lambda \_:\N.\lambda \_:1.\star$
+\item $\sem{injS}= \lambda \_:\N. \lambda \_:\N.\lambda \_:1.\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{\lambda x:\N.M} = \lambda x:\N.\sem{M}$
\item $\sem{M t} = \sem{M} \sem{t}$
\end{itemize}
The realizability relation is a relation $f \R P$ where $f: \sem{P}$.
In particular:
\begin{itemize}
-\item $\neg (* \R \bot)$
+\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 $f \R (P\to Q)$ iff for any $m$ such that $m \R P$, $(f \,m) \R Q$
\end{itemize}
\noindent
-We proceed to prove that alla axioms $ax:Ax$ are realized by $\sem{ax}$.
+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 $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 $<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$
+ and $snd$ we obtain $f~n_p~g_p$ that we know is in relation $\R$ with $Q$
+ since $g_p \R P[\underline{n_p}/x]$.
+
+\item $ex\_intro$.
+ We must prove that
+ $$\lambda x:\N.\lambda f:\sem{P}.<x,f> \R \forall x.(P\to\exists x.P(x)$$
+ that leads to prove that foreach n
+ $\underline{ex\_into}~n \R (P\to\exists x.P(x))[\underline{n}/x]$.\\
+ Evaluating the substitution we have
+ $\underline{ex\_into}~n \R (P[\underline{n}/x]\to\exists x.P(x))$.\\
+ Again by definition of $\R$ we have to prove that given a
+ $m \R P[\underline{n}/x]$ then $\underline{ex\_into}~n~m \R \exists x.P(x)$.
+ Expanding the definition of $\underline{ex\_intro}$ we have
+ $<n,m> \R \exists x.P(x)$ that is true since $m \R P[\underline{n}/x]$.
+
+\item $fst$.
+ Wehave 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$.
+ 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}.<x,y> \R P \to Q \to P \land Q$$
+ Following the definition of $\R$ we have to show that
+ foreach $m \R P$ and foreach $n \R Q$ then
+ $(\lambda x:\sem{P}. \lambda y:\sem{Q}.<x,y>)~m~n \R P \land Q$.\\
+ This is the same of $<m,n> \R P \land Q$ that is verified since
+ $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 \_:1.*~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
+ $*$ 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 \times 0 = x$.
+
+\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}
\begin{thebibliography}{}
+\bibitem{GLT}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
+des finiten Standpunktes. Dialectica, 12, pp.34-38, 1958.
+\bibitem{God}K.G\"odel. Collected Works. Vol.II, Oxford University Press,
+1990.
+\bibitem{How}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
+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
+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
+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
+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.
\end{thebibliography}
projects / helm.git / blobdiff