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{...}
  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
 237
 238 \end{thebibliography}
 239
 240 \end{document}
 241