From: Andrea Asperti Date: Mon, 10 Oct 2005 13:57:38 +0000 (+0000) Subject: First draft. X-Git-Tag: V_0_7_2_3~226 X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=890385fa69623abbcfbfe758218c080b7c80903e;p=helm.git First draft. --- diff --git a/helm/papers/system_T/t.tex b/helm/papers/system_T/t.tex index c9bf726c8..30cbd5732 100644 --- a/helm/papers/system_T/t.tex +++ b/helm/papers/system_T/t.tex @@ -5,7 +5,7 @@ %\usepackage{hyperref} %\usepackage{picins} - +\newcommand{\sem}[1]{[\![ #1 ]\!]} \title{...} \author{...} @@ -17,10 +17,111 @@ ... \end{abstract} -\section{Introduction} +\section{Heyting's arithmetics} + +{\bf Axioms} + +\begin{itemize} + +\item $nat\_ind: P(0) \to (\forall x.P(x) \to P(S(x))) \to \forall x.P(x)$ +\item $ex\_ind: (\forall x.P(x) \to Q) \to \exists x.P(x) \to Q$ +\item $ex\_intro: \forall x.(P \to \exists x.P)$ +\item $fst: P \land Q \to P$ +\item $snd: P \land Q \to Q$ +\item $conj: P \to Q \to P \land Q$ +\item $false\_ind: \bot \to Q$ +\item $discriminate:\forall x.0 = S(x) \to \bot$ +\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)$ +\end{itemize} + +\noindent +{\bf Inference Rules} + +\[ + (\to_i)\frac{\Gamma,x:A \vdash M:Q}{\Gamma \vdash \lambda x:A.M: A \to Q} \hspace{2cm} + (\to_e)\frac{\Gamma \vdash M: A \to Q \hspace{1cm}\Gamma \vdash N: A} + {\Gamma \vdash M N: Q} +\] + +%\[ +% (\land_i)\frac{\Gamma \vdash M:A \hspace{1cm}\Gamma \vdash N:B} +% {\Gamma \vdash : A \land B} +%\hspace{2cm} +% (\land_{el})\frac{\Gamma \vdash A \land B}{\Gamma \vdash A} +%\hspace{2cm} +% (\land_{er})\frac{\Gamma \vdash A \land B}{\Gamma \vdash B} +%\] + +\[ + (\forall_i)\frac{\Gamma \vdash M:P}{\Gamma \vdash + \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]} +\] + + +%\[ +% (\exists_i)\frac{\Gamma \vdash P[t/x]}{\Gamma \vdash \exists x.P}\hspace{2cm} +% (\exists_e)\frac{\Gamma \vdash \exists x.P\hspace{1cm}\Gamma \vdash \forall x.P \to Q} +%{\Gamma \vdash Q} +%\] + +\section{Extraction} + +\begin{itemize} +\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}$ +\end{itemize} + +definition. +For any type T of system T $\bot_T: 1 \to T$ is inuctively defined as follows: +\begin{enumerate} +\item $\bot_1 = \lambda x:1.x$ +\item $\bot_N = \lambda x:1.0$ +\item $\bot_{U\times V} = \lambda x:1.<\bot_{U} x,\bot_{V} x>$ +\item $\bot_{U\to V} = \lambda x:1.\lambda \_:U. \bot_{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}.$ +\item $\sem{fst} = fst$ +\item $\sem{snd} = snd$ +\item $\sem{conj} = \lambda x:\sem{P}.\lambda y:\sem{Q}.$ +\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.*$ +\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{M t} = \sem{M} \sem{t} +\end{itemize} +\section{Realizability} +The realizability relation is a relation $f \, R \, P$ where $f: \sem{P}$. +In particular: +\begin{itemize} +\item $\neg (* \, R \bot)$ +\item $* \, R \, (t_1=t_2)$ iff $t_1=t_2$ is true ... +\item $ 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$ +\item $f R \forall x.P$ iff for any $n$ $(f \underline{n}) \, R \, P$ +\item $ R \exists x.P$ iff $g R P[n/x]$ +\end{itemize} \begin{thebibliography}{}