X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fpapers%2Fsystem_T%2Ft.tex;h=7804118ab5a00d8284195acd07f3dc8460dba1be;hb=4167cea65ca58897d1a3dbb81ff95de5074700cc;hp=a438e59a32e3619f0002f45f5fbd3a16c3587977;hpb=6d6a2cceca53d661e478bfc6046845727e2049ce;p=helm.git

diff --git a/helm/papers/system_T/t.tex b/helm/papers/system_T/t.tex
index a438e59a3..7804118ab 100644
--- a/helm/papers/system_T/t.tex
+++ b/helm/papers/system_T/t.tex
@@ -8,7 +8,8 @@
 \newcommand{\semT}[1]{\ensuremath{\llbracket #1 \rrbracket}}
 \newcommand{\sem}[1]{\llbracket \ensuremath{#1} \rrbracket}
 \newcommand{\pair}[2]{<\!#1,#2\!>}
-\newcommand{\R}{\;\mathscr{R}\;}
+\newcommand{\canonical}{\bot}
+\newcommand{\R}{~\mathscr{R}~}
 \newcommand{\N}{\,\mathbb{N}\,}
 \newcommand{\B}{\,\mathbb{B}\,}
 \newcommand{\NT}{\,\mathbb{N}\,}
@@ -18,7 +19,9 @@
 \newcommand{\one}{{\bf 1}}
 \newcommand{\mult}{\cdot}
 \newcommand{\ind}{Ind(X)}
+\newcommand{\indP}{Ind(\vec{P}~|~X)}
 \newcommand{\Xind}{\ensuremath{X_{ind}}}
+\newcommand{\XindP}{\ensuremath{X_{ind}}}
 \renewcommand{\|}{\ensuremath{\quad | \quad}}
 \newcommand{\triUP}{\ensuremath{\Delta}}
 \newcommand{\triDOWN}{\ensuremath{\nabla}}
@@ -118,19 +121,31 @@ with explicit pairs, plus the following additional constants:
 \item $O:\N$, $S:\N \to \N$, $R:A \to (A \to \N \to A) \to \N \to A$,
 \end{itemize}
 Redexes comprise $\beta$-reduction
-\[(\beta)\;\; \lambda x:U.M \; N \leadsto M[N/x]\]
+\[(\beta)~~ \lambda x:U.M ~ N \leadsto M[N/x]\]
 projections
 
-\[(\pi_1)\;\;fst \pair{M}{N} \leadsto M\\ \hspace{.6cm} (\pi_2)\;\; snd \pair{M}{N} 
+\[(\pi_1)~~fst \pair{M}{N} \leadsto M\\ \hspace{.6cm} (\pi_2)~~ snd \pair{M}{N} 
 \leadsto N \] 
 and the following type specific reductions:
-\[(D_{true})\;\;\\D\;M\;N\; true \leadsto M  \hspace{.6cm} 
-  (D_{false})\;\;  D\;M\;N\;false \leadsto N \] 
-\[(R_0)\;\;\\R\;M\;F\; 0 \leadsto M  \hspace{.6cm} 
-  (R_S)\;\;  R\;M\;F\;(S\;n) \leadsto F\;n\;(R\;M\;F\;n) \] 
-\[(*)\;\; M \leadsto * \]
+\[(D_{true})~~\\D~M~N~ true \leadsto M  \hspace{.6cm} 
+  (D_{false})~~  D~M~N~false \leadsto N \] 
+\[(R_0)~~\\R~M~F~ 0 \leadsto M  \hspace{.6cm} 
+  (R_S)~~  R~M~F~(S~n) \leadsto F~n~(R~M~F~n) \] 
+\[(*)~~ 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 +219,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 +235,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$
@@ -371,7 +386,7 @@ We proceed to prove that all axioms $ax:Ax$ are realized by $\sem{ax}$.
 \noindent
 {\bf example}\\
 Let us prove the following principle of well founded induction:
-\[(\forall m.(\forall p. p < m \to P p) \to P m) \to \forall n.P n\]
+\[(\forall m.(\forall p. p < m \to P~p) \to P~m) \to \forall n.P~n\]
 In the following proof we shall make use of proof-terms, since we finally
 wish to extract the computational content; we leave to reader the easy
 check that the proof object describes the usual and natural proof
@@ -379,35 +394,35 @@ of the statement.
 
 We assume to have already proved the following lemmas (having trivial
 realizers):\\
-\[L: \lambda b.p < 0 \to \bot\]
-\[M: \lambda p,q,n.p < q \to q \le (S n) \to p \le n \]
-Let us assume $h: \forall m.(\forall p. p < m \to P p) \to P m$.
-We prove by induction on n that $\forall q. q \le n \to P q$.
-For $n=0$, we get a proof of $P \;0$ by 
-\[ B: \lambda q.\lambda \_:q \le n. h \;0\; 
-(\lambda p.\lambda k:p < 0. false\_ind \;(L\;p\; k)) \]
-In the inductive case, we must prove that, for any n, 
-\[(\forall q. q \le n \to P q) \to (\forall q. q \le S n \to P q)\]
-Assume $h1: \forall q. q \le n \to P q$ and
-$h2: q \le S \;n$. Let us prove $\forall p. p < q \to P p$.
-If $h3: p < q$ then $(M\; p\; q\; n\; h3\; h2): p \le n$, hence 
-$h1 \;p \; (M\; p\; q\; n\; h3\; h2): P p$.\\ 
+\[L : \forall p, q.p < q \to q \le 0 \to \bot\]
+\[M : \forall p,q,n.p < q \to q \le (S n) \to p \le n \]
+Let us assume $h : \forall m.(\forall p. p < m \to P~p) \to P~m$.
+We prove by induction on $n$ that $\forall q. q \le n \to P~q$.
+For $n=0$, we get a proof of $P ~q$ by 
+\[ B \equiv \lambda q.\lambda h_0:q \le 0. h ~q~ 
+(\lambda p.\lambda k:p < q. false\_ind ~(L~p~q~k~h_0)) \]
+In the inductive case, we must prove that, for any $n$, 
+\[(\forall q. q \le n \to P~q) \to (\forall q. q \le S n \to P~q)\]
+Assume $h_1: \forall q. q \le n \to P q$ and
+$h_2: q \le S ~n$. Let us prove $\forall p. p < q \to P~p$.
+If $h_3: p < q$ then $(M~ p~ q~ n~ h_3~ h_2): p \le n$, hence 
+$h_1 ~p ~ (M~ p~ q~ n~ h_3~ h_2): P~p$.\\ 
 In conclusion, the proof of the 
 inductive case is
-\[I: \lambda h1:\forall q. q \le n \to P\; q.\lambda q.\lambda h2:q \le S n.
-h \; q \; (\lambda p.\lambda h3:p < q.h1 \;p\; (M\; p\; q\; n\; h3\; h2)) \]
+\[I \equiv \lambda n.\lambda h_1:\forall q. q \le n \to P~ q.\lambda q.\lambda h_2:q \le S n.
+h ~ q ~ (\lambda p.\lambda h_3:p < q.h_1 ~p~ (M~ p~ q~ n~ h_3~ h_2)) \]
 (where $h$ is free in I).
 The full proof is
-\[ \lambda m.\lambda h: \forall m.(\forall p. p < m \to P p) \to P m.
-nat\_ind \;B \; I \;m\; (le\_n \; m) \]
-where $le\_n$ is a proof that $\forall n. n \le n$.\\
+\[ \lambda h: \forall m.(\forall p. p < m \to P~p) \to P~m.\lambda m.
+nat\_ind ~B ~ I ~m~m~ (le\_n ~ m) \]
+where $le\_n$ is a proof that $\forall n. n \le n$, and the free $P$ in the definition of $nat_{ind}$ is instantiated with $\forall m.m \le m \to P~m$.\\
 Form the previous proof,after stripping terminal objects, 
 and a bit of eta-contraction to make
 the term more readable, we extract the following term (types are omitted):
 
-\[R' = \lambda m.\lambda f.
-R\; (f \; O\; (\lambda q.*_A))\; 
-(\lambda n\lambda g\lambda q.f \;q\;g)\;m \;m\]
+\[R' \equiv \lambda f.\lambda m.
+R~ (\lambda n.f ~n~ (\lambda q.*))~ 
+(\lambda n\lambda g\lambda q.f ~q~g)~m ~m\]
 
 The intuition of this operator is the following: supose to
 have a recursive definition $h q = F[h]$ where $q:\N$ and 
@@ -415,8 +430,8 @@ $F[h]: A$. This defines a functional
 $f: \lambda q.\lambda g.F[g]: N\to(N\to A) \to A$, such that
 (morally) $h$ is the fixpoint of $f$. For instance, 
 in the case of the fibonacci function, $f$ is 
-\[\lambda q. \lambda g.
-if\; q = 0\;then\; 1\; else\; if\; q = 1\; then\; 1\; else\; g (q-1)+g (q-2)\]
+\[fibo \equiv \lambda q. \lambda g.
+if~ q = 0~then~ 1~ else~ if~ q = 1~ then~ 1~ else~ g (q-1)+g (q-2)\]
 
 So $f$ build a new 
 approximation of $h$ from the previous approximation $h$ taken
@@ -426,6 +441,64 @@ you may look at $g$ as the ``history'' (curse of values) of $h$
 for all values less or equal to $q$; then $f$ extend $g$ to
 $q+1$.
 
+Let's compute for example 
+\begin{eqnarray} 
+R'~fibo~2 & \leadsto & 
+  R~ (\lambda n.fibo ~n~ (\lambda q.*))~ 
+  (\lambda n\lambda g\lambda q.fibo ~q~g)~2 ~2\nonumber\\
+& \leadsto & 
+  (\lambda n\lambda g\lambda q.fibo ~q~g)~1~
+  (R~ 
+    (\lambda n.fibo ~n~ (\lambda q.*))~
+    (\lambda n\lambda g\lambda q.fibo ~q~g)~1)~
+  2 \nonumber\\
+& \leadsto &  
+  \lambda q.fibo ~q~
+  (R~ 
+    (\lambda n.fibo ~n~ (\lambda q.*))~
+    (\lambda n\lambda g\lambda q.fibo ~q~g)~1)~
+  2 \nonumber\\
+& \leadsto &  
+  \lambda q.fibo ~q~
+  ((\lambda n\lambda g\lambda q.fibo ~q~g)~0~
+  (R~ 
+    (\lambda n.fibo ~n~ (\lambda q.*))~
+    (\lambda n\lambda g\lambda q.fibo ~q~g)~0))~
+  2 \nonumber\\
+& \leadsto &  
+  \lambda q.fibo ~q~
+  (\lambda q.fibo ~q~
+  (R~ 
+    (\lambda n.fibo ~n~ (\lambda q.*))~
+    (\lambda n\lambda g\lambda q.fibo ~q~g)~0)
+  )2 \nonumber\\
+& \leadsto &  
+  \lambda q.fibo ~q~
+  (\lambda q.fibo ~q~
+  (\lambda n.fibo ~n~ (\lambda q.*)))2
+  \nonumber\\
+& \leadsto &  
+  fibo~2~(\lambda q.fibo ~q~ (\lambda n.fibo ~n~ (\lambda q.*))) \nonumber\\
+& \leadsto &  
+  (\lambda q.fibo ~q~ (\lambda n.fibo ~n~ (\lambda q.*))) 1 + 
+  (\lambda q.fibo ~q~ (\lambda n.fibo ~n~ (\lambda q.*))) 0 \nonumber\\
+& \leadsto &  
+  fibo ~1~ (\lambda n.fibo ~n~ (\lambda q.*)) + 
+  fibo ~0~ (\lambda n.fibo ~n~ (\lambda q.*)) \nonumber\\
+& \leadsto &  
+  1 + 1 \nonumber
+\end{eqnarray}
+Note that the second argument of $fibo$ is always a method to calculate all the prvious values of $fibo$. DA CAPIRE (per me) come mai $\lambda n$ non viene usata...
+CAPITA CON csc:
+
+n non serve perche' c'e' una relazione logica di n con q,
+in particolare $q <= Sn$ ... quindi $q < n$ (lemma M)...
+e quindi posso usare come history $< n$ una history $< q$.
+il $\lambda h2$ essendo $[[q <= Sn]]$ = 1 viene scartata.
+
+se si spiega come array viene decente... forse. lunedi' provo a scrivere
+meglio.
+
 \section{Inductive types}
 The notation we will use is similar to the one used in 
 \cite{Werner} and \cite{Paulin89} but we prefer
@@ -468,7 +541,7 @@ In the second case we mean $T \neq X$.
 \subsection{Induction principle}
 The induction principle for an inductive type $X$ and a predicate $Q$ 
 is a constant with the following type
-$$\Xind:\vec{\triUP\{C(X), c\}} \to \forall t:X.Q(x)$$
+$$\Xind:\vec{\triUP\{C(X), c\}} \to \forall t:X.Q(t)$$
 $\triUP$ takes a constructor type $C(X)$ and a term $c$ (initially $c$ is a
 constructor of X, and $c:C(X)$) and is defined by recursion as follows:
 \begin{eqnarray}
@@ -552,6 +625,20 @@ t:X.Q(t)} \to Q(c_i~\vec{m}~\vec{t})$, thus $f_i~\vec{m}~\vec{t~r} \R
 Q(c_i~\vec{m}~\vec{t})$.
 \end{proof}
 
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+\section{Improoving inductive types}
+It is possible to parametrize inductive types over other inductive types
+without much difficulties since the type $T$ in $C(X)$ is free. Both the
+recursor and the induction principle are schemas, parametric over $T$.
+
+Possiamo anche definire $X_{\vec{P}}\equiv Ind(P|X)={c_i : C(P|X)}$ e poi
+fare variare $T$ su $\vec{P}$, ma non ottengo niente di meglio.
+
+Credo anche che quantificare su eventuali variabili di tipo non cambi niente
+visto che non abbiamo funzioni.
+
+Se ammettiamo che i tipi dipendano da termini di tipo induttivo
+
 
 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
 \begin{thebibliography}{}