helm/papers/system_T/t.tex

   1 \documentclass[a4paper]{article}
   2 \pagestyle{headings}
   3 %\usepackage{graphicx}
   4 \usepackage{amssymb,amsmath,mathrsfs}
   5 %\usepackage{hyperref}
   6 %\usepackage{picins}
   7
   8 \newcommand{\sem}[1]{[\![ #1 ]\!]}
   9 \newcommand{\R}{\;\mathscr{R}\;}
  10 \newcommand{\N}{\,\mathbb{N}\,}
  11 \newcommand{\NT}{\,\mathbb{N}\,}
  12 \newcommand{\NH}{\,\mathbb{N}\,}
  13 \renewcommand{\star}{\ast}
  14 \newcommand{\one}{\mathbb{1}}
  15 \renewcommand{\times}{\cdot}
  16 \title{A gentle approach to program extraction and realizability}
  17 \author{...}
  18
  19
  20 \begin{document}
  21 \maketitle
  22
  23 \begin{abstract}
  24 ...
  25 \end{abstract}
  26
  27 \section{Heyting's arithmetics}
  28
  29 {\bf Axioms}
  30
  31 \begin{itemize}
  32
  33 \item $nat\_ind: P(0) \to (\forall x.P(x) \to P(S(x))) \to \forall x.P(x)$
  34 \item $ex\_ind: (\forall x.P(x) \to Q) \to \exists x.P(x) \to Q$
  35 \item $ex\_intro: \forall x.(P \to \exists x.P)$
  36 \item $fst: P \land Q \to P$
  37 \item $snd: P \land Q \to Q$
  38 \item $conj: P \to Q \to P \land Q$
  39 \item $false\_ind: \bot \to Q$
  40 \item $discriminate:\forall x.0 = S(x) \to \bot$
  41 \item $injS: \forall x,y.S(x) = S(y) \to x=y$
  42 \item $plus\_O:\forall x.x+0=x$
  43 \item $plus\_S:\forall x,y.x+S(y)=S(x+y)$
  44 \item $times\_O:\forall x.x\times0=0$
  45 \item $times\_S:\forall x,y.x\times S(y)=x+(x\times y)$
  46 \end{itemize}
  47
  48 \noindent
  49 {\bf Inference Rules}
  50
  51 \[
  52    (\to_i)\frac{\Gamma,x:A \vdash M:Q}{\Gamma \vdash \lambda x:A.M: A \to Q} \hspace{2cm}
  53    (\to_e)\frac{\Gamma \vdash M: A \to Q \hspace{1cm}\Gamma \vdash N: A}
  54     {\Gamma \vdash M N: Q}
  55 \]
  56
  57 %\[
  58 %   (\land_i)\frac{\Gamma \vdash M:A \hspace{1cm}\Gamma \vdash N:B}
  59 %   {\Gamma \vdash <M,N> : A \land B}
  60 %\hspace{2cm}
  61 %   (\land_{el})\frac{\Gamma \vdash A \land B}{\Gamma \vdash A}
  62 %\hspace{2cm}
  63 %   (\land_{er})\frac{\Gamma \vdash A \land B}{\Gamma \vdash B}
  64 %\]
  65
  66 \[
  67    (\forall_i)\frac{\Gamma \vdash M:P}{\Gamma \vdash
  68    \lambda x:\N.M: \forall x.P}(*) \hspace{2cm}
  69    (\forall_e)\frac{\Gamma \vdash M :\forall x.P}{\Gamma \vdash M t: P[t/x]}
  70 \]
  71
  72
  73 %\[
  74 %   (\exists_i)\frac{\Gamma \vdash P[t/x]}{\Gamma \vdash \exists x.P}\hspace{2cm}
  75 %   (\exists_e)\frac{\Gamma \vdash \exists x.P\hspace{1cm}\Gamma \vdash \forall x.P \to Q}
  76 %{\Gamma \vdash Q}
  77 %\]
  78
  79 \section{Extraction}
  80
  81 \begin{itemize}
  82 \item $\sem{A} = 1$ if A is atomic
  83 \item $\sem{A \land B} = \sem{A}\times \sem{B}$
  84 \item $\sem{A \to B} = \sem{A}\to \sem{B}$
  85 \item $\sem{\forall x.P} = \N \to \sem{P}$
  86 \item $\sem{\exists x.P} = \N \times \sem{P}$
  87 \end{itemize}
  88
  89 definition.
  90 For any type T of system T $\bot_T: 1 \to T$  is inuctively defined as follows:
  91 \begin{enumerate}
  92 \item $\bot_1 = \lambda x:1.x$
  93 \item $\bot_N = \lambda x:1.0$
  94 \item $\bot_{U\times V} = \lambda x:1.<\bot_{U} x,\bot_{V} x>$
  95 \item $\bot_{U\to V} = \lambda x:1.\lambda \_:U. \bot_{V} x$
  96 \end{enumerate}
  97
  98 \begin{itemize}
  99 \item $\sem{nat\_ind} = R$
 100 \item $\sem{ex\_ind} = (\lambda f:(\N \to \sem{P} \to \sem{Q}).
 101 \lambda p:\N\times \sem{P}.f (fst \,p) (snd \,p)$.
 102 \item $\sem{ex\_intro} = \lambda x:\N.\lambda f:\sem{P}.<x,f>$
 103 \item $\sem{fst} = \pi_1$
 104 \item $\sem{snd} = \pi_2$
 105 \item $\sem{conj} = \lambda x:\sem{P}.\lambda y:\sem{Q}.<x,y>$
 106 \item $\sem{false\_ind} = \bot_{\sem{Q}}$
 107 \item $\sem{discriminate} = \lambda \_:\N.\lambda \_:1.\star$
 108 \item $\sem{injS}= \lambda \_:\N. \lambda \_:\N.\lambda \_:1.\star$
 109 \item $\sem{plus\_O} = \sem{times\_O} = \lambda \_:\N.\star$
 110 \item $\sem{plus\_S} = \sem{times_S} = \lambda \_:\N. \lambda \_:\N.\star$
 111 \end{itemize}
 112
 113 In the case of structured proofs:
 114 \begin{itemize}
 115 \item $\sem{M N} = \sem{M} \sem{N}$
 116 \item $\sem{\lambda x:A.M} = \lambda x:\sem{A}.\sem{M}$
 117 \item $\sem{\lambda x:\N.M} = \lambda x:\N.\sem{M}$
 118 \item $\sem{M t} = \sem{M} \sem{t}$
 119 \end{itemize}
 120
 121 \section{Realizability}
 122 The realizability relation is a relation $f \R P$ where $f: \sem{P}$.
 123 In particular:
 124 \begin{itemize}
 125 \item $\neg (\star \R \bot)$
 126 \item $* \R (t_1=t_2)$ iff $t_1=t_2$ is true ...
 127 \item $<f,g> \R (P\land Q)$ iff $f \R P$ and $g \R Q$
 128 \item $f \R (P\to Q)$ iff for any $m$ such that $m \R P$, $(f \,m) \R Q$
 129 \item $f \R (\forall x.P)$ iff for any natural number $n$ $(f n) \R P[\underline{n}/x]$
 130 \item $<n,g> \R (\exists x.P)$ iff $g \R P[\underline{n}/x]$
 131 \end{itemize}
 132
 133 \noindent
 134 We proceed to prove that all axioms $ax:Ax$ are realized by $\sem{ax}$.
 135
 136 \begin{itemize}
 137 \item $nat\_ind$.
 138   We must prove that the recursion schema $R$ realizes the induction principle.
 139   To this aim we must prove that for any $a$ and $f$ such that $a \R P(0)$ and
 140   $f \R \forall x.(P(x) \to P(S(x)))$, and any natural number $n$, $(R \,a \,f
 141   \,n) \R P(\underline{n})$.\\
 142   We proceed by induction on n.\\
 143   If $n=O$, $(R \,a \,f \,O) = a$ and by hypothesis $a \R P(0)$.\\
 144   Suppose by induction that
 145   $(R \,a \,f \,n) \R P(\underline{n})$, and let us prove that the relation
 146   still holds for $n+1$.  By definition
 147   $(R \,a \,f \,(n+1)) = f \,n \,(R \,a \,f \,n)$,
 148   and since $f \R \forall x.(P(x) \to P(S(x)))$,
 149   $(f n (R a f n)) \R P(S(\underline{n}))=P(\underline{n+1})$.
 150
 151 \item $ex\_ind$.
 152   We must prove that $$\underline{ex\_ind} \R (\forall x:(P x)
 153   \to Q) \to (\exists x:(P x)) \to Q$$ Following the definition of $\R$ we have
 154   to prove that given\\ $f~\R~\forall~x:((P~x)~\to~Q)$ and
 155   $p~\R~\exists~x:(P~x)$, then $\underline{ex\_ind}~f~p \R Q$.\\
 156   $p$ is a couple $<n_p,g_p>$ such that $g_p \R P[\underline{n_p}/x]$, while
 157   $f$ is a function such that forall $n$ and for all $m \R P[\underline{n}/x]$
 158   then $f~n~m \R Q$ (note that $x$ is not free in $Q$ so $[\underline{n}/x]$
 159   affects only $P$).\\
 160   Exapanding the definition of $\underline{ex\_ind}$, $fst$
 161   and $snd$ we obtain $f~n_p~g_p$ that we know is in relation $\R$ with $Q$
 162   since $g_p \R P[\underline{n_p}/x]$.
 163
 164 \item $ex\_intro$.
 165   We must prove that
 166   $$\lambda x:\N.\lambda f:\sem{P}.<x,f> \R \forall x.(P\to\exists x.P(x)$$
 167   that leads to prove that foreach n
 168   $\underline{ex\_into}~n \R (P\to\exists x.P(x))[\underline{n}/x]$.\\
 169   Evaluating the substitution we have
 170   $\underline{ex\_into}~n \R (P[\underline{n}/x]\to\exists x.P(x))$.\\
 171   Again by definition of $\R$ we have to prove that given a
 172   $m \R P[\underline{n}/x]$ then $\underline{ex\_into}~n~m \R \exists x.P(x)$.
 173   Expanding the definition of $\underline{ex\_intro}$ we have
 174   $<n,m> \R \exists x.P(x)$ that is true since $m \R P[\underline{n}/x]$.
 175
 176 \item $fst$.
 177   Wehave to prove that $\pi_1 \R P \land Q \to P$, that is equal to proving
 178   that for each $m \R P \land Q$ then $\pi_1~m \R P$ .
 179   $m$ must be a couple $<f_m,g_m>$ such that $f_m \R P$ and $g_m \R Q$.
 180   So we conclude that $\pi_1~m$ reduces to $f_m$ that is in relation $\R$
 181   with $P$.
 182
 183 \item $snd$. The same for $fst$.
 184
 185 \item $conj$.
 186   We have to prove that
 187   $$\lambda x:\sem{P}. \lambda y:\sem{Q}.<x,y> \R P \to Q \to P \land Q$$
 188   Following the definition of $\R$ we have to show that
 189   foreach $m \R P$ and foreach $n \R Q$ then
 190   $(\lambda x:\sem{P}. \lambda y:\sem{Q}.<x,y>)~m~n \R P \land Q$.\\
 191   This is the same of $<m,n> \R P \land Q$ that is verified since
 192   $m \R P$ and $n \R Q$.
 193
 194
 195 \item $false\_ind$.
 196   We have to prove that $\bot_{\sem{Q}} \R \bot \to Q$.
 197   Trivial, since there is no $m \R \bot$.
 198
 199 \item $discriminate$.
 200   Since there is no $n$ such that $0 = S n$ is true... \\
 201   $\underline{discriminate}~n \R 0 = S~\underline{n} \to \bot$ for each n.
 202
 203 \item $injS$.
 204   We have to prove that for each $n_1$ and $n_2$\\
 205   $\lambda \_:\N. \lambda \_:\N.\lambda \_:1.*~n_1~n_2 \R
 206   (S(x)=S(y)\to x=y)[n_1/x][n_2/y]$.\\
 207   We assume that $m \R S(n_1)=S(n_2)$ and we have to show that
 208   $\lambda \_:\N. \lambda \_:\N.\lambda \_:1.*~n_1~n_2~m$ that reduces to
 209   $*$ is in relation $\R$ with $n_1=n_2$. Since in the standard model of
 210   natural numbers  $S(n_1)=S(n_2)$ implies $n_1=n_2$ we have that
 211   $* \R n_1=n_2$.
 212
 213 \item $plus\_O$.
 214   Since in the standard model for natural numbers $0$ is the neutral element
 215   for addition $\lambda \_:\N.\star \R \forall x.x + 0 = x$.
 216
 217 \item $plus\_S$.
 218   In the standard model of natural numbers the addition of two numbers is the
 219   operation of counting the second starting from the first. So
 220   $$\lambda \_:\N. \lambda \_:\N. \star \R \forall x,y.x+S(y)=S(x+y)$$.
 221
 222 \item $times\_O$.
 223   Since in the standard model for natural numbers $0$ is the absorbing element
 224   for multiplication $\lambda \_:\N.\star \R \forall x.x \times 0 = x$.
 225
 226 \item $times\_S$.
 227   In the standard model of natural numbers the multiplications of two
 228   numbers is the operation of adding the first to himself a number of times
 229   equal to the second number. So
 230   $$\lambda \_:\N. \lambda \_:\N. \star \R \forall x,y.x+S(y)=S(x+y)$$.
 231
 232
 233 \end{itemize}
 234
 235 \begin{thebibliography}{}
 236 \bibitem{GLT}G.Y.Girard. Proof Theory and Logical Complexity.
 237 Bibliopolis, Napoli, 1987.
 238 \bibitem{GLT}G.Y.Girard, Y.Lafont, P.Tailor. Proofs and Types.
 239 Cambridge Tracts in Theoretical Computer Science 7.Cambridge University
 240 Press, 1989.
 241 \bibitem{God}K.G\"odel. \"Uber eine bisher noch nicht ben\"utzte Erweiterung
 242 des finiten Standpunktes. Dialectica, 12, pp.34-38, 1958.
 243 \bibitem{God}K.G\"odel. Collected Works. Vol.II, Oxford University Press,
 244 1990.
 245 \bibitem{How}W.A.Howard. The formulae-as-types notion of constructions.
 246 in J.P.Seldin and j.R.Hindley editors, to H.B.Curry: Essays on Combinatory
 247 Logic, Lambda calculus and Formalism. Acedemic Press, 1980.
 248 \bibitem{Let}P.Letouzey. Programmation fonctionnelle certifi\'ee; l'extraction
 249 de programmes dans l'assistant Coq. Ph.D. Thesis, Universit\'e de
 250 Paris XI-Orsay, 2004.
 251 \bibitem{Loef}P.Martin-L\"of. Intuitionistic Type Theory.
 252 Bibliopolis, Napoli, 1984.
 253 \bibitem{Pau87}C.Paulin-Mohring. Extraction de programme dans le Calcul de
 254 Constructions. Ph.D. Thesis, Universit\'e de
 255 Paris 7, 1987.
 256 \bibitem{Pau89}C.Paulin-Mohring. Extracting $F_{\omega}$ programs from proofs
 257 in the Calculus of Constructions. In proc. of the Sixteenth Annual
 258 ACM Symposium on
 259 Principles of Programming Languages, Austin, January, ACML Press 1989.
 260 \bibitem{Sch}K.Sch\"utte. Proof Theory. Grundlehren der mathematischen
 261 Wissenschaften 225, Springer Verlag, Berlin, 1977.
 262 \bibitem{Tro}A.S.Troelstra. Metamathemtical Investigation of Intuitionistic
 263 Arithmetic and Analysis. Lecture Notes in Mathematics 344, Springer Verlag,
 264 Berlin, 1973.
 265 \bibitem{TS}A.S.Troelstra, H.Schwichtenberg. Basic Proof Theory.
 266 Cambridge Tracts in Theoretical Computer Science 43.Cambridge University
 267 Press, 1996.
 268
 269
 270 \end{thebibliography}
 271
 272 \end{document}
 273