X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fpapers%2Fsystem_T%2Ft.tex;h=7804118ab5a00d8284195acd07f3dc8460dba1be;hb=4167cea65ca58897d1a3dbb81ff95de5074700cc;hp=614037caafb97c75a526dc255511e724222c7be0;hpb=d10018fb879fe85d595750903a7e168372bba257;p=helm.git diff --git a/helm/papers/system_T/t.tex b/helm/papers/system_T/t.tex index 614037caa..7804118ab 100644 --- a/helm/papers/system_T/t.tex +++ b/helm/papers/system_T/t.tex @@ -7,16 +7,21 @@ \newcommand{\semT}[1]{\ensuremath{\llbracket #1 \rrbracket}} \newcommand{\sem}[1]{\llbracket \ensuremath{#1} \rrbracket} -\newcommand{\R}{\;\mathscr{R}\;} +\newcommand{\pair}[2]{<\!#1,#2\!>} +\newcommand{\canonical}{\bot} +\newcommand{\R}{~\mathscr{R}~} \newcommand{\N}{\,\mathbb{N}\,} +\newcommand{\B}{\,\mathbb{B}\,} \newcommand{\NT}{\,\mathbb{N}\,} \newcommand{\NH}{\,\mathbb{N}\,} \renewcommand{\star}{\ast} \renewcommand{\vec}{\overrightarrow} -\newcommand{\one}{\mathscr{1}} +\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}} @@ -103,6 +108,44 @@ logic and adding little by little small bits of logical power. This paper is the first step in this direction. %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% +\section{G\"odel system T} +We shall use a variant of system T with three atomic types $\N$ (natural +numbers), $\B$ (booleans) and $\one$ (a terminal object), and two binary +type constructors $\times$ (product) and $\to$ (arrow type). + +The terms of the language comprise the usual simply typed lambda terms +with explicit pairs, plus the following additional constants: +\begin{itemize} +\item $*:\one$, +\item $true: \B$, $false:\B$, $D:A\to A \to \B \to A$ +\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]\] +projections + +\[(\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 * \] +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} @@ -142,7 +185,7 @@ say that ax:AX refers to the previous Axioms list... %\[ % (\land_i)\frac{\Gamma \vdash M:A \hspace{1cm}\Gamma \vdash N:B} -% {\Gamma \vdash : A \land B} +% {\Gamma \vdash \pair{M}{N} : A \land B} %\hspace{2cm} % (\land_{el})\frac{\Gamma \vdash A \land B}{\Gamma \vdash A} %\hspace{2cm} @@ -176,23 +219,23 @@ $\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.<\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} \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}.$ +\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}.$ -\item $\sem{false\_ind} = \bot_{\sem{Q}}$ +\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$ @@ -214,10 +257,10 @@ In particular: \begin{itemize} \item $\neg (\star \R \bot)$ \item $* \R (t_1=t_2)$ iff $t_1=t_2$ is true ... -\item $ \R (P\land Q)$ iff $f \R P$ and $g \R Q$ +\item $\pair{f}{g} \R (P\land Q)$ iff $f \R P$ and $g \R Q$ \item $f \R (P\to Q)$ iff for any $m$ such that $m \R P$, $(f \,m) \R Q$ \item $f \R (\forall x.P)$ iff for any natural number $n$ $(f n) \R P[\underline{n}/x]$ -\item $ \R (\exists x.P)$ iff $g \R P[\underline{n}/x]$ +\item $\pair{n}{g}\R (\exists x.P)$ iff $g \R P[\underline{n}/x]$ \end{itemize} %We need to generalize the notion of realizability to sequents. %Given a sequent $B_1, \ldots, B_n \vdash A$ with free variables in @@ -261,7 +304,7 @@ We proceed to prove that all axioms $ax:Ax$ are realized by $\sem{ax}$. \to Q) \to (\exists x:(P x)) \to Q$$ Following the definition of $\R$ we have to prove that given\\ $f~\R~\forall~x:((P~x)~\to~Q)$ and $p~\R~\exists~x:(P~x)$, then $\underline{ex\_ind}~f~p \R Q$.\\ - $p$ is a couple $$ such that $g_p \R P[\underline{n_p}/x]$, while + $p$ is a couple $\pair{n_p}{g_p}$ such that $g_p \R P[\underline{n_p}/x]$, while $f$ is a function such that forall $n$ and for all $m \R P[\underline{n}/x]$ then $f~n~m \R Q$ (note that $x$ is not free in $Q$ so $[\underline{n}/x]$ affects only $P$).\\ @@ -271,7 +314,7 @@ We proceed to prove that all axioms $ax:Ax$ are realized by $\sem{ax}$. \item $ex\_intro$. We must prove that - $$\lambda x:\N.\lambda f:\sem{P}. \R \forall x.(P\to\exists x.P(x)$$ + $$\lambda x:\N.\lambda f:\sem{P}.\pair{x}{f} \R \forall x.(P\to\exists x.P(x)$$ that leads to prove that for each n $\underline{ex\_into}~n \R (P\to\exists x.P(x))[\underline{n}/x]$.\\ Evaluating the substitution we have @@ -279,12 +322,12 @@ We proceed to prove that all axioms $ax:Ax$ are realized by $\sem{ax}$. Again by definition of $\R$ we have to prove that given a $m \R P[\underline{n}/x]$ then $\underline{ex\_into}~n~m \R \exists x.P(x)$. Expanding the definition of $\underline{ex\_intro}$ we have - $ \R \exists x.P(x)$ that is true since $m \R P[\underline{n}/x]$. + $\pair{n}{m} \R \exists x.P(x)$ that is true since $m \R P[\underline{n}/x]$. \item $fst$. We have to prove that $\pi_1 \R P \land Q \to P$, that is equal to proving that for each $m \R P \land Q$ then $\pi_1~m \R P$ . - $m$ must be a couple $$ such that $f_m \R P$ and $g_m \R Q$. + $m$ must be a couple $\pair{f_m}{g_m}$ such that $f_m \R P$ and $g_m \R Q$. So we conclude that $\pi_1~m$ reduces to $f_m$ that is in relation $\R$ with $P$. @@ -292,11 +335,11 @@ We proceed to prove that all axioms $ax:Ax$ are realized by $\sem{ax}$. \item $conj$. We have to prove that - $$\lambda x:\sem{P}. \lambda y:\sem{Q}. \R P \to Q \to P \land Q$$ + $$\lambda x:\sem{P}. \lambda y:\sem{Q}.\pair{x}{y}\R P \to Q \to P \land Q$$ Following the definition of $\R$ we have to show that for each $m \R P$ and for each $n \R Q$ then - $(\lambda x:\sem{P}. \lambda y:\sem{Q}.)~m~n \R P \land Q$.\\ - This is the same of $ \R P \land Q$ that is verified since + $(\lambda x:\sem{P}. \lambda y:\sem{Q}.\pair{x}{y})~m~n \R P \land Q$.\\ + This is the same of $\pair{m}{n} \R P \land Q$ that is verified since $m \R P$ and $n \R Q$. @@ -343,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 @@ -351,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 @@ -387,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 @@ -398,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 @@ -440,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} @@ -524,9 +625,25 @@ 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}{} +\bibitem{AL91}A.Asperti, G.Longo. Categories, Types and Structures. +Foundations of Computing, Cambrdidge University press, 1991. \bibitem{Girard86}G.Y.Girard. The system F of variable types, fifteen years later. Theoretical Computer Science 45, 1986. \bibitem{Girard87}G.Y.Girard. Proof Theory and Logical Complexity. @@ -545,6 +662,8 @@ by bar recursion. Compositio Mathematica 20, pp.107-124. 1958 \bibitem{Howard80}W.A.Howard. The formulae-as-types notion of constructions. in J.P.Seldin and j.R.Hindley editors, to H.B.Curry: Essays on Combinatory Logic, Lambda calculus and Formalism. Acedemic Press, 1980. +\bibitem{Kleene45}S.C.Kleene. On the interpretation of intuitionistic +number theory. Journal of Symbolic Logic, n.10, pp.109-124, 1945. \bibitem{Kreisel59} G.Kreisel. Interpretation of analysis by means of constructive functionals of finite type. In. A.Heyting ed. {\em Constructivity in mathematics}. North Holland, Amsterdam,1959.