From 82b5d7944ba0d238f696207cf4bb4c3549dabddd Mon Sep 17 00:00:00 2001 From: Enrico Tassi Date: Fri, 11 Nov 2005 18:11:37 +0000 Subject: [PATCH] added an example of reduction of R' and some comments (plus a fix in the demonstration) --- helm/papers/system_T/t.tex | 140 ++++++++++++++++++++++++++++--------- 1 file changed, 107 insertions(+), 33 deletions(-) diff --git a/helm/papers/system_T/t.tex b/helm/papers/system_T/t.tex index 62d27031e..7804118ab 100644 --- a/helm/papers/system_T/t.tex +++ b/helm/papers/system_T/t.tex @@ -9,7 +9,7 @@ \newcommand{\sem}[1]{\llbracket \ensuremath{#1} \rrbracket} \newcommand{\pair}[2]{<\!#1,#2\!>} \newcommand{\canonical}{\bot} -\newcommand{\R}{\;\mathscr{R}\;} +\newcommand{\R}{~\mathscr{R}~} \newcommand{\N}{\,\mathbb{N}\,} \newcommand{\B}{\,\mathbb{B}\,} \newcommand{\NT}{\,\mathbb{N}\,} @@ -19,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}} @@ -119,17 +121,17 @@ 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 @@ -384,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 @@ -392,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 @@ -428,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 @@ -439,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 @@ -481,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} @@ -565,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}{} -- 2.39.2