helm/papers/system_T/t.tex

   1 \documentclass[a4paper]{article}
   2 \pagestyle{headings}
   3 %\usepackage{graphicx}
   4 \usepackage{amssymb,amsmath}
   5 %\usepackage{hyperref}
   6 %\usepackage{picins}
   7
   8 \newcommand{\sem}[1]{[\![ #1 ]\!]}
   9 \title{...}
  10 \author{...}
  11
  12
  13 \begin{document}
  14 \maketitle
  15
  16 \begin{abstract}
  17 ...
  18 \end{abstract}
  19
  20 \section{Heyting's arithmetics}
  21
  22 {\bf Axioms}
  23
  24 \begin{itemize}
  25
  26 \item $nat\_ind: P(0) \to (\forall x.P(x) \to P(S(x))) \to \forall x.P(x)$
  27 \item $ex\_ind: (\forall x.P(x) \to Q) \to \exists x.P(x) \to Q$
  28 \item $ex\_intro: \forall x.(P \to \exists x.P)$
  29 \item $fst: P \land Q \to P$
  30 \item $snd: P \land Q \to Q$
  31 \item $conj: P \to Q \to P \land Q$
  32 \item $false\_ind: \bot \to Q$
  33 \item $discriminate:\forall x.0 = S(x) \to \bot$
  34 \item $injS: \forall x,y.S(x) = S(y) \to x=y$
  35 \item $plus\_O:\forall x.x+0=x$
  36 \item $plus\_S:\forall x,y.x+S(y)=S(x+y)$
  37 \item $times\_O:\forall x.x*0=0$
  38 \item $timies\_S:\forall x,y.x*S(y)=x+(x*y)$
  39 \end{itemize}
  40
  41 \noindent
  42 {\bf Inference Rules}
  43
  44 \[
  45    (\to_i)\frac{\Gamma,x:A \vdash M:Q}{\Gamma \vdash \lambda x:A.M: A \to Q} \hspace{2cm}
  46    (\to_e)\frac{\Gamma \vdash M: A \to Q \hspace{1cm}\Gamma \vdash N: A}
  47     {\Gamma \vdash M N: Q}
  48 \]
  49
  50 %\[
  51 %   (\land_i)\frac{\Gamma \vdash M:A \hspace{1cm}\Gamma \vdash N:B}
  52 %   {\Gamma \vdash <M,N> : A \land B}
  53 %\hspace{2cm}
  54 %   (\land_{el})\frac{\Gamma \vdash A \land B}{\Gamma \vdash A}
  55 %\hspace{2cm}
  56 %   (\land_{er})\frac{\Gamma \vdash A \land B}{\Gamma \vdash B}
  57 %\]
  58
  59 \[
  60    (\forall_i)\frac{\Gamma \vdash M:P}{\Gamma \vdash
  61    \lambda x:N.M: \forall x.P}(*) \hspace{2cm}
  62    (\forall_e)\frac{\Gamma \vdash M :\forall x.P}{\Gamma \vdash M t: P[t/x]}
  63 \]
  64
  65
  66 %\[
  67 %   (\exists_i)\frac{\Gamma \vdash P[t/x]}{\Gamma \vdash \exists x.P}\hspace{2cm}
  68 %   (\exists_e)\frac{\Gamma \vdash \exists x.P\hspace{1cm}\Gamma \vdash \forall x.P \to Q}
  69 %{\Gamma \vdash Q}
  70 %\]
  71
  72 \section{Extraction}
  73
  74 \begin{itemize}
  75 \item $\sem{A} = 1$ if A is atomic
  76 \item $\sem{A \land B} = \sem{A}\times \sem{B}$
  77 \item $\sem{A \to B} = \sem{A}\to \sem{B}$
  78 \item $\sem{\forall x.P} = N \to \sem{P}$
  79 \item $\sem{\exists x.P} = N \times \sem{P}$
  80 \end{itemize}
  81
  82 definition.
  83 For any type T of system T $\bot_T: 1 \to T$  is inuctively defined as follows:
  84 \begin{enumerate}
  85 \item $\bot_1 = \lambda x:1.x$
  86 \item $\bot_N = \lambda x:1.0$
  87 \item $\bot_{U\times V} = \lambda x:1.<\bot_{U} x,\bot_{V} x>$
  88 \item $\bot_{U\to V} = \lambda x:1.\lambda \_:U. \bot_{V} x$
  89 \end{enumerate}
  90
  91 \begin{itemize}
  92 \item $\sem{nat\_ind} = R$
  93 \item $\sem{ex\_ind} = (\lambda f:(N \to \sem{P} \to \sem{Q}).
  94 \lambda p:N\times \sem{P}.f (fst \,p) (snd \,p)$.
  95 \item $\sem{ex\_intro} = \lambda x:N.\lambda f:\sem{P}.<x,f>$
  96 \item $\sem{fst} = fst$
  97 \item $\sem{snd} = snd$
  98 \item $\sem{conj} = \lambda x:\sem{P}.\lambda y:\sem{Q}.<x,y>$
  99 \item $\sem{false\_ind} = \bot_{\sem{Q}}$
 100 \item $\sem{discriminate} = \lambda \_:N.\lambda \_:1.*$
 101 \item $\sem{injS}= \lambda \_:N. \lambda \_:N.\lambda \_:1.*$
 102 \item $\sem{plus\_O} = \sem{times\_O} = \lambda \_:N.*$
 103 \item $\sem{plus\_S} = \sem{times_S} = \lambda \_:N. \lambda \_:N.*$
 104 \end{itemize}
 105
 106 In the case of structured proofs:
 107 \begin{itemize}
 108 \item \sem{M N} = \sem{M} \sem{N}
 109 \item \sem{\lambda x:A.M} = \lambda x:\sem{A}.\sem{M}
 110 \item \sem{\lambda x:N.M} = \lambda x:N.\sem{M}
 111 \item \sem{M t} = \sem{M} \sem{t}
 112 \end{itemize}
 113
 114 \section{Realizability}
 115 The realizability relation is a relation $f \, R \, P$ where $f: \sem{P}$.
 116 In particular:
 117 \begin{itemize}
 118 \item $\neg (* \, R \bot)$
 119 \item $* \, R \, (t_1=t_2)$ iff $t_1=t_2$ is true ...
 120 \item $<f,g> R P\land Q$ iff $f R P$ and $g R Q$
 121 \item $f R P\to Q$ iff for any $m$ such that $m R P$, $(f m) \, R \, Q$
 122 \item $f R \forall x.P$ iff for any $n$ $(f \underline{n}) \, R \, P$
 123 \item $<n,g> R \exists x.P$ iff $g R P[n/x]$
 124 \end{itemize}
 125
 126 \begin{thebibliography}{}
 127
 128
 129 \end{thebibliography}
 130
 131 \end{document}
 132