From: Enrico Tassi Date: Tue, 11 Oct 2005 13:20:11 +0000 (+0000) Subject: fixed some typos X-Git-Tag: V_0_7_2_3~220 X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=d928ebab750b6ac49b3ae97e2f9d1634c18a43fa;p=helm.git fixed some typos --- diff --git a/helm/papers/system_T/Makefile b/helm/papers/system_T/Makefile new file mode 100644 index 000000000..fb2792fc5 --- /dev/null +++ b/helm/papers/system_T/Makefile @@ -0,0 +1,5 @@ +all: + latex t + latex t + latex t + dvips -ta4 t diff --git a/helm/papers/system_T/t.tex b/helm/papers/system_T/t.tex index d3ca4e6a1..d6a1b6de1 100644 --- a/helm/papers/system_T/t.tex +++ b/helm/papers/system_T/t.tex @@ -7,6 +7,9 @@ \newcommand{\sem}[1]{[\![ #1 ]\!]} \newcommand{\R}{\,\mathscr{R}\,} +\newcommand{\N}{\,\mathbb{N}\,} +\newcommand{\NT}{\,\mathbb{N}\,} +\newcommand{\NH}{\,\mathbb{N}\,} \title{...} \author{...} @@ -36,7 +39,7 @@ \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\_S:\forall x,y.x*S(y)=x+(x*y)$ \end{itemize} \noindent @@ -59,7 +62,7 @@ \[ (\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]} \] @@ -76,8 +79,8 @@ \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. @@ -91,24 +94,24 @@ For any type T of system T $\bot_T: 1 \to T$ is inuctively defined as follows: \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{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.*$ +\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{\lambda x:\N.M} = \lambda x:\N.\sem{M}$ \item $\sem{M t} = \sem{M} \sem{t}$ \end{itemize} @@ -125,7 +128,7 @@ In particular: \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