From b0495e87b8c71686bedab62253cfe2f85c6aa672 Mon Sep 17 00:00:00 2001 From: Andrea Asperti Date: Mon, 7 Nov 2005 11:31:00 +0000 Subject: [PATCH] First draft of the introduction. --- helm/papers/system_T/t.tex | 104 +++++++++++++++++++++++++++++++++---- 1 file changed, 94 insertions(+), 10 deletions(-) diff --git a/helm/papers/system_T/t.tex b/helm/papers/system_T/t.tex index df00823e8..2766e16ff 100644 --- a/helm/papers/system_T/t.tex +++ b/helm/papers/system_T/t.tex @@ -13,7 +13,7 @@ \renewcommand{\star}{\ast} \newcommand{\one}{\mathbb{1}} \renewcommand{\times}{\cdot} -\title{A gentle approach to\\program extraction and realizability} +\title{Modified Realizability and Inductive Types} \author{...} @@ -24,6 +24,77 @@ ... \end{abstract} +\section{Introduction} +The characterization of the provable recursive functions of +Peano Arithmetic as the terms of system T is a well known +result of G\"odel \cite{Godel58,Godel90}. Although many authors acknowledge +that the functional interpretation of the Dialectica paper +is not among the major achievements of the author (see e.g. \cite{Girard87}), +the result has been extensively investigated and there is a wide +literature on the +topic (see e.g. \cite{Howard68,Troelstra,Girard87}. + +A different, more neglected, but for many respects much more +direct relation between Peano (or Heyting) Arithmetics and +G\"odel System T is provided +by the so called {\em modified realizability}. Modified realizability +was first introduced by Kreisel in \cite{Kreisel59} - although it will take you +a bit of effort to recognize it in the few lines of paragraph 3.52 - +and later in \cite{Kreisel62} under the name of generalized realizability. +The name of modified realizability seems to be due to Troelstra +\cite{Troelstra} +- who contested Kreisel's name but unfortunately failed in proposing +a valid alternative; we shall reluctantly adopt this latter name +to avoid further confusion. Modified realizability is a typed variant of +realizability, essentially providing interpretations +of $HA^{\omega}$ into itself: each theorem is realized by a typed function +of system T, that also gives the actual computational content extracted +from the proof. +In spite of the simplicity and the elegance of the proof, it is extremely +difficult to find a modern discussion of this result; the most recent +exposition we are aware of is in the encyclopedic (typewritten!) work by +Troelstra \cite{Troelstra} (pp.213-229). Even modern introductory books +to Type Theory and Proof Theory devoting much space to system T +such as \cite{GLT} and \cite{TS} surprisingly leave out this simple and +illuminating result. Both \cite{GLT} and \cite{TS} +prefer to focus on higher order arithmetics and its relation with +Girard's System $F$ \cite{Girard86}, but the technical complexity and +the didactical value of the two proofs is not comparable: when you +prove that the Induction Principle is realized by the recursor $R$ +of system $T$ you catch a sudden gleam of intelligence in the +students eyes; usually, the same does not happen when you show, say, +that the ``forgetful'' intrepretation of the higher order predicate defining +the natural numbers is the system $F$ encoding +$\forall X.(X\to X) \to X \to X$ of $\N$. +Moreover, after a first period of enthusiasm, the impredicative +encoding of inductive types in Logical Frameworks has shown several +problems and limitations (see e.g. \cite{Werner} pp.24-25) mostly +solved by assuming inductive types as a primitive logical notion +(leading e.g. form the Calculus of Constructions to the Calculus +of Inductive Constructions - CIC). Even the extraction algorithm of +CIC, strictly based on realizability principles, and in a first time +still oriented towards System F \cite{Paulin87,Paulin89} has been +recently rewritten \cite{Letouzey04} +to take advantage of concrete types and pattern matching of ML-like +languages. Unfortunately, systems like the Calculus of Inductive +Constructions are so complex, from the logical point of view, to +substantially prevent a really neat theoretical exposition (at present, +it does not +even exists a truly complete consistency proofs covering all aspects +of such systems); moreover, not eveybody may be interested in all the features +offered by these frameworks, from polymorphism to types depending on +proofs. Our program is to restart the analysis of logical systems with +primitive inductive types in a smooth way, starting form first order +logic and adding little by little small bits of logical power. +This paper is the first step in this direction. + + + + + + + + \section{Heyting's arithmetics} {\bf Axioms} @@ -233,38 +304,51 @@ We proceed to prove that all axioms $ax:Ax$ are realized by $\sem{ax}$. \end{itemize} \begin{thebibliography}{} -\bibitem{GLT}G.Y.Girard. Proof Theory and Logical Complexity. +\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. Bibliopolis, Napoli, 1987. \bibitem{GLT}G.Y.Girard, Y.Lafont, P.Tailor. Proofs and Types. Cambridge Tracts in Theoretical Computer Science 7.Cambridge University Press, 1989. -\bibitem{God}K.G\"odel. \"Uber eine bisher noch nicht ben\"utzte Erweiterung +\bibitem{Godel58}K.G\"odel. \"Uber eine bisher noch nicht ben\"utzte Erweiterung des finiten Standpunktes. Dialectica, 12, pp.34-38, 1958. -\bibitem{God}K.G\"odel. Collected Works. Vol.II, Oxford University Press, +\bibitem{Godel90}K.G\"odel. Collected Works. Vol.II, Oxford University Press, 1990. -\bibitem{How}W.A.Howard. The formulae-as-types notion of constructions. +\bibitem{Howard68}W.A.Howard. Functional interpretation of bar induction +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{Let}P.Letouzey. Programmation fonctionnelle certifi\'ee; l'extraction +\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. + \bibitem{Kreisel62} G.Kreisel. On weak completeness of intuitionistic +predicatelogic. Journal of Symbolic Logic 27, pp. 139-158. 1962. +\bibitem{Letouzey04}P.Letouzey. Programmation fonctionnelle +certifi\'ee; l'extraction de programmes dans l'assistant Coq. Ph.D. Thesis, Universit\'e de Paris XI-Orsay, 2004. \bibitem{Loef}P.Martin-L\"of. Intuitionistic Type Theory. Bibliopolis, Napoli, 1984. -\bibitem{Pau87}C.Paulin-Mohring. Extraction de programme dans le Calcul de +\bibitem{Paulin87}C.Paulin-Mohring. Extraction de programme dans le Calcul de Constructions. Ph.D. Thesis, Universit\'e de Paris 7, 1987. -\bibitem{Pau89}C.Paulin-Mohring. Extracting $F_{\omega}$ programs from proofs -in the Calculus of Constructions. In proc. of the Sixteenth Annual +\bibitem{Paulin89}C.Paulin-Mohring. Extracting $F_{\omega}$ programs +from proofs in the Calculus of Constructions. In proc. of the Sixteenth Annual ACM Symposium on Principles of Programming Languages, Austin, January, ACML Press 1989. \bibitem{Sch}K.Sch\"utte. Proof Theory. Grundlehren der mathematischen Wissenschaften 225, Springer Verlag, Berlin, 1977. -\bibitem{Tro}A.S.Troelstra. Metamathemtical Investigation of Intuitionistic +\bibitem{Troelstra}A.S.Troelstra. Metamathemtical Investigation of +Intuitionistic Arithmetic and Analysis. Lecture Notes in Mathematics 344, Springer Verlag, Berlin, 1973. \bibitem{TS}A.S.Troelstra, H.Schwichtenberg. Basic Proof Theory. Cambridge Tracts in Theoretical Computer Science 43.Cambridge University Press, 1996. +\bibitem{Werner}B.Werner. Une Th\'eorie des Constructions Inductives. +Ph.D.Thesis, Universit\'e de Paris 7, 1994. \end{thebibliography} -- 2.39.2