From 68c7886ff8d1105b545a5e1ece2f84f43e2f5568 Mon Sep 17 00:00:00 2001 From: Andrea Asperti Date: Fri, 11 Nov 2005 08:19:48 +0000 Subject: [PATCH] Definition of system T. --- helm/papers/system_T/t.tex | 25 +++++++++++++++++++------ 1 file changed, 19 insertions(+), 6 deletions(-) diff --git a/helm/papers/system_T/t.tex b/helm/papers/system_T/t.tex index a438e59a3..62d27031e 100644 --- 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$ -- 2.39.2