First draft of the introduction.

diff --git a/helm/papers/system_T/t.tex b/helm/papers/system_T/t.tex
index df00823e88061ee5f08fd0491ee09126571cffc8..2766e16ff5eb305546d4fa5717de0a69fbd5df2f 100644 (file)
--- 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}