Definition of system T.

diff --git a/helm/papers/system_T/t.tex b/helm/papers/system_T/t.tex
index a438e59a32e3619f0002f45f5fbd3a16c3587977..62d27031e4edab63e19f0e81b59f69086a830b5a 100644 (file)
--- a/helm/papers/system_T/t.tex
+++ b/helm/papers/system_T/t.tex
@@ -8,6 +8,7 @@
 \newcommand{\semT}[1]{\ensuremath{\llbracket #1 \rrbracket}}
 \newcommand{\sem}[1]{\llbracket \ensuremath{#1} \rrbracket}
 \newcommand{\pair}[2]{<\!#1,#2\!>}
+\newcommand{\canonical}{\bot}
 \newcommand{\R}{\;\mathscr{R}\;}
 \newcommand{\N}{\,\mathbb{N}\,}
 \newcommand{\B}{\,\mathbb{B}\,}
@@ -131,6 +132,18 @@ and the following type specific reductions:
 \[(*)\;\; M \leadsto * \]
 where (*) holds for any $M$ of type $\one$.
 
+Note that using the well known isomorpshims 
+$\one \to A \cong A$, $A \to \one \cong \one$
+and $A \times \one \cong A \cong \one\times A$ (see \cite{AL91}, pp.231-239)
+we may always get rid of $\one$ (apart the trivial case).
+The terminal object does not play a major role in our treatment, but 
+it allows to extract better algorithms. In particular we use it 
+to realize atomic proposition, and stripping out the terminal object using 
+the above isomorphisms gives a simple way of just keeping the truly 
+informative part of the algorithms.
+
+
+
 \section{Heyting's arithmetics}
 
 {\bf Axioms}
@@ -204,12 +217,12 @@ $\sem{\cdot}$ takes in input formulae in HA and returns types in T.
 \end{enumerate}
 
 definition.
-For any type T of system T $\bot_T: \one \to T$  is inductively defined as follows:
+For any type T of system T $\canonical_T: \one \to T$  is inductively defined as follows:
 \begin{enumerate}
-\item $\bot_\one = \lambda x:\one.x$
-\item $\bot_N = \lambda x:\one.0$
-\item $\bot_{U\times V} = \lambda x:\one.\pair{\bot_{U} x}{\bot_{V} x}$
-\item $\bot_{U\to V} = \lambda x:\one.\lambda \_:U. \bot_{V} x$
+\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}
 
 \begin{itemize}
@@ -220,7 +233,7 @@ For any type T of system T $\bot_T: \one \to T$  is inductively defined as follo
 \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} = \bot_{\sem{Q}}$
+\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$