say that ax:AX refers to the previous Axioms list...
\[
- (Proj)\hspace{0.2cm} \Gamma, x:A, \Delta \vdash x:A
+ (Proj)\hspace{0.1cm} \Gamma, x:A, \Delta \vdash x:A
\hspace{2cm}
- (Const)\hspace{0.2cm} \Gamma \vdash ax : AX
+ (Const)\hspace{0.1cm} \Gamma \vdash ax : AX
\]
\[
- (\to_i)\hspace{0.2cm}\frac{\Gamma,x:A \vdash M:Q}{\Gamma \vdash \lambda x:A.M: A \to Q} \hspace{2cm}
- (\to_e)\hspace{0.2cm}\frac{\Gamma \vdash M: A \to Q \hspace{1cm}\Gamma \vdash N: A}
+ (\to_i)\hspace{0.1cm}\frac{\Gamma,x:A \vdash M:Q}{\Gamma \vdash \lambda x:A.M: A \to Q} \hspace{2cm}
+ (\to_e)\hspace{0.1cm}\frac{\Gamma \vdash M: A \to Q \hspace{1cm}\Gamma \vdash N: A}
{\Gamma \vdash M N: Q}
\]
%\]
\[
- (\forall_i)\hspace{0.2cm}\frac{\Gamma \vdash M:P}{\Gamma \vdash
+ (\forall_i)\hspace{0.1cm}\frac{\Gamma \vdash M:P}{\Gamma \vdash
\lambda x:\N.M: \forall x.P}(*) \hspace{2cm}
- (\forall_e)\hspace{0.2cm}\frac{\Gamma \vdash M :\forall x.P}{\Gamma \vdash M t: P[t/x]}
+ (\forall_e)\hspace{0.1cm}\frac{\Gamma \vdash M :\forall x.P}{\Gamma \vdash M t: P[t/x]}
\]
\section{Extraction}
-The formulae to types translation function
-$\sem{\cdot}$ takes in input formulae in HA and returns types in T.
-
-\begin{enumerate}
-\item $\sem{A} = \one$ 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:\N.P} = \N \to \sem{P}$
-\item $\sem{\exists x:\N.P} = \N \times \sem{P}$
-\end{enumerate}
-
-definition.
-For any type T of system T $\canonical_T: \one \to T$ is inductively defined as follows:
-\begin{enumerate}
-\item $\canonical_\one = \lambda x:\one.x$
-\item $\canonical_N = \lambda x:\one.0$
-\item $\canonical_{U\times V} = \lambda x:\one.\pair{\canonical_{U} x}{\canonical_{V} x}$
-\item $\canonical_{U\to V} = \lambda x:\one.\lambda \_:U. \canonical_{V} x$
-\end{enumerate}
+The formulae to types translation function $\sem{\cdot}$, see table
+\ref{tab:formulae2types}, takes in input formulae in HA and returns
+types in T. In table \ref{tab:structproof} we the proofs to terms
+function for structured proofs. Axiom translation is reported in table
+\ref{tab:axioms}. In table \ref{tab:canonical} we define how the
+canoniac element is formed.
+
+\begin{table}[!h]
+\hrule\vspace{0.1cm}
+\begin{tabular}{p{0.47\textwidth}p{0.47\textwidth}}
+ $\sem{A} = \one$ if A is atomic &
+ $\sem{A \land B} = \sem{A}\times \sem{B}$ \\
+ $\sem{A \to B} = \sem{A}\to \sem{B}$ &
+ $\sem{\forall x:\N.P} = \N \to \sem{P}$ \\
+ $\sem{\exists x:\N.P} = \N \times \sem{P}$ &
+\end{tabular}\vspace{0.1cm}
+\hrule
+\caption{\label{tab:formulae2types}Formulae to types translation}
+\end{table}
+
+\begin{table}[!h]
+\hrule\vspace{0.1cm}
+\begin{tabular}{p{0.47\textwidth}p{0.47\textwidth}}
+ $\semT{M N} = \semT{M} \semT{N}$ &
+ $\semT{\lambda x:A.M} = \lambda x:\sem{A}.\semT{M}$ \\
+ $\semT{\lambda x:\N.M} = \lambda x:\N.\semT{M}$ &
+ $\semT{M t} = \semT{M} \semT{t}$
+\end{tabular}\vspace{0.1cm}
+\hrule
+\caption{\label{tab:structproof}Structured proofs}
+\end{table}
+
+\begin{table}[!h]
+\hrule\vspace{0.1cm}
+\begin{tabular}{p{0.47\textwidth}p{0.47\textwidth}}
+ $\sem{fst} = \pi_1$&
+ $\sem{snd} = \pi_2$\\
+ $\sem{conj} = \lambda x:\sem{P}.\lambda y:\sem{Q}.\pair{x}{y}$&
+ $\sem{false\_ind} = \canonical_{\sem{Q}}$\\
+ $\sem{discriminate} = \lambda \_:\N.\lambda \_:\one.\star$&
+ $\sem{injS}= \lambda \_:\N. \lambda \_:\N.\lambda \_:\one.\star$\\
+ $\sem{plus\_O} = \sem{times\_O} = \lambda \_:\N.\star$&
+ $\sem{nat\_ind} = R$ \\
+ \multicolumn{2}{l}{
+ $\sem{plus\_S} = \sem{times\_S} = \lambda \_:\N. \lambda \_:\N.\star$
+ }\\
+ \multicolumn{2}{l}{
+ $\sem{ex\_intro} = \lambda x:\N.\lambda f:\sem{P}.\pair{x}{f}$
+ }\\
+ \multicolumn{2}{l}{
+ $\sem{ex\_ind} =
+ \lambda f:(\N \to \sem{P} \to \sem{Q}).
+ \lambda p:\N\times \sem{P}.f~(fst~p)~(snd~p)$.
+ }
+\end{tabular}\vspace{0.1cm}
+\hrule
+\caption{\label{tab:axioms}Axioms translation}
+\end{table}
+
+\begin{table}[!h]
+\hrule\vspace{0.1cm}
+\begin{tabular}{p{0.47\textwidth}p{0.47\textwidth}}
+ $\canonical_\one = \lambda x:\one.x$ &
+ $\canonical_N = \lambda x:\one.0$ \\
+ $\canonical_{U\times V} = \lambda x:\one.\pair{\canonical_{U}
+ x}{\canonical_{V} x}$ &
+ $\canonical_{U\to V} = \lambda x:\one.\lambda \_:U. \canonical_{V} x$
+\end{tabular}\vspace{0.1cm}
+\hrule
+\caption{\label{tab:canonical}Canonical element}
+\end{table}
-\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}.\pair{x}{f}$
-\item $\sem{fst} = \pi_1$
-\item $\sem{snd} = \pi_2$
-\item $\sem{conj} = \lambda x:\sem{P}.\lambda y:\sem{Q}.\pair{x}{y}$
-\item $\sem{false\_ind} = \canonical_{\sem{Q}}$
-\item $\sem{discriminate} = \lambda \_:\N.\lambda \_:\one.\star$
-\item $\sem{injS}= \lambda \_:\N. \lambda \_:\N.\lambda \_:\one.\star$
-\item $\sem{plus\_O} = \sem{times\_O} = \lambda \_:\N.\star$
-\item $\sem{plus\_S} = \sem{times_S} = \lambda \_:\N. \lambda \_:\N.\star$
-\end{itemize}
-
-In the case of structured proofs:
-\begin{itemize}
-\item $\semT{M N} = \semT{M} \semT{N}$
-\item $\semT{\lambda x:A.M} = \lambda x:\sem{A}.\semT{M}$
-\item $\semT{\lambda x:\N.M} = \lambda x:\N.\semT{M}$
-\item $\semT{M t} = \semT{M} \semT{t}$
-\end{itemize}
\section{Realizability}
The realizability relation is a relation $f \R P$ where $f: \sem{P}$, and
projects / helm.git / blobdiff