1 \documentclass[a4paper]{article}
4 \usepackage{amssymb,amsmath,mathrsfs}
8 \newcommand{\sem}[1]{[\![ #1 ]\!]}
9 \newcommand{\R}{\;\mathscr{R}\;}
10 \newcommand{\N}{\,\mathbb{N}\,}
11 \newcommand{\NT}{\,\mathbb{N}\,}
12 \newcommand{\NH}{\,\mathbb{N}\,}
13 \renewcommand{\star}{\ast}
14 \newcommand{\one}{\mathbb{1}}
15 \renewcommand{\times}{\cdot}
16 \title{Modified Realizability and Inductive Types}
27 \section{Introduction}
28 The characterization of the provable recursive functions of
29 Peano Arithmetic as the terms of system T is a well known
30 result of G\"odel \cite{Godel58,Godel90}. Although many authors acknowledge
31 that the functional interpretation of the Dialectica paper
32 is not among the major achievements of the author (see e.g. \cite{Girard87}),
33 the result has been extensively investigated and there is a wide
35 topic (see e.g. \cite{Howard68,Troelstra,Girard87}.
37 A different, more neglected, but for many respects much more
38 direct relation between Peano (or Heyting) Arithmetics and
39 G\"odel System T is provided
40 by the so called {\em modified realizability}. Modified realizability
41 was first introduced by Kreisel in \cite{Kreisel59} - although it will take you
42 a bit of effort to recognize it in the few lines of paragraph 3.52 -
43 and later in \cite{Kreisel62} under the name of generalized realizability.
44 The name of modified realizability seems to be due to Troelstra
46 - who contested Kreisel's name but unfortunately failed in proposing
47 a valid alternative; we shall reluctantly adopt this latter name
48 to avoid further confusion. Modified realizability is a typed variant of
49 realizability, essentially providing interpretations
50 of $HA^{\omega}$ into itself: each theorem is realized by a typed function
51 of system T, that also gives the actual computational content extracted
53 In spite of the simplicity and the elegance of the proof, it is extremely
54 difficult to find a modern discussion of this result; the most recent
55 exposition we are aware of is in the encyclopedic (typewritten!) work by
56 Troelstra \cite{Troelstra} (pp.213-229). Even modern introductory books
57 to Type Theory and Proof Theory devoting much space to system T
58 such as \cite{GLT} and \cite{TS} surprisingly leave out this simple and
59 illuminating result. Both \cite{GLT} and \cite{TS}
60 prefer to focus on higher order arithmetics and its relation with
61 Girard's System $F$ \cite{Girard86}, but the technical complexity and
62 the didactical value of the two proofs is not comparable: when you
63 prove that the Induction Principle is realized by the recursor $R$
64 of system $T$ you catch a sudden gleam of intelligence in the
65 students eyes; usually, the same does not happen when you show, say,
66 that the ``forgetful'' intrepretation of the higher order predicate defining
67 the natural numbers is the system $F$ encoding
68 $\forall X.(X\to X) \to X \to X$ of $\N$.
69 Moreover, after a first period of enthusiasm, the impredicative
70 encoding of inductive types in Logical Frameworks has shown several
71 problems and limitations (see e.g. \cite{Werner} pp.24-25) mostly
72 solved by assuming inductive types as a primitive logical notion
73 (leading e.g. form the Calculus of Constructions to the Calculus
74 of Inductive Constructions - CIC). Even the extraction algorithm of
75 CIC, strictly based on realizability principles, and in a first time
76 still oriented towards System F \cite{Paulin87,Paulin89} has been
77 recently rewritten \cite{Letouzey04}
78 to take advantage of concrete types and pattern matching of ML-like
79 languages. Unfortunately, systems like the Calculus of Inductive
80 Constructions are so complex, from the logical point of view, to
81 substantially prevent a really neat theoretical exposition (at present,
83 even exists a truly complete consistency proofs covering all aspects
84 of such systems); moreover, not eveybody may be interested in all the features
85 offered by these frameworks, from polymorphism to types depending on
86 proofs. Our program is to restart the analysis of logical systems with
87 primitive inductive types in a smooth way, starting form first order
88 logic and adding little by little small bits of logical power.
89 This paper is the first step in this direction.
98 \section{Heyting's arithmetics}
104 \item $nat\_ind: P(0) \to (\forall x.P(x) \to P(S(x))) \to \forall x.P(x)$
105 \item $ex\_ind: (\forall x.P(x) \to Q) \to \exists x.P(x) \to Q$
106 \item $ex\_intro: \forall x.(P \to \exists x.P)$
107 \item $fst: P \land Q \to P$
108 \item $snd: P \land Q \to Q$
109 \item $conj: P \to Q \to P \land Q$
110 \item $false\_ind: \bot \to Q$
111 \item $discriminate:\forall x.0 = S(x) \to \bot$
112 \item $injS: \forall x,y.S(x) = S(y) \to x=y$
113 \item $plus\_O:\forall x.x+0=x$
114 \item $plus\_S:\forall x,y.x+S(y)=S(x+y)$
115 \item $times\_O:\forall x.x\times0=0$
116 \item $times\_S:\forall x,y.x\times S(y)=x+(x\times y)$
120 {\bf Inference Rules}
123 (\to_i)\frac{\Gamma,x:A \vdash M:Q}{\Gamma \vdash \lambda x:A.M: A \to Q} \hspace{2cm}
124 (\to_e)\frac{\Gamma \vdash M: A \to Q \hspace{1cm}\Gamma \vdash N: A}
125 {\Gamma \vdash M N: Q}
129 % (\land_i)\frac{\Gamma \vdash M:A \hspace{1cm}\Gamma \vdash N:B}
130 % {\Gamma \vdash <M,N> : A \land B}
132 % (\land_{el})\frac{\Gamma \vdash A \land B}{\Gamma \vdash A}
134 % (\land_{er})\frac{\Gamma \vdash A \land B}{\Gamma \vdash B}
138 (\forall_i)\frac{\Gamma \vdash M:P}{\Gamma \vdash
139 \lambda x:\N.M: \forall x.P}(*) \hspace{2cm}
140 (\forall_e)\frac{\Gamma \vdash M :\forall x.P}{\Gamma \vdash M t: P[t/x]}
145 % (\exists_i)\frac{\Gamma \vdash P[t/x]}{\Gamma \vdash \exists x.P}\hspace{2cm}
146 % (\exists_e)\frac{\Gamma \vdash \exists x.P\hspace{1cm}\Gamma \vdash \forall x.P \to Q}
153 \item $\sem{A} = 1$ if A is atomic
154 \item $\sem{A \land B} = \sem{A}\times \sem{B}$
155 \item $\sem{A \to B} = \sem{A}\to \sem{B}$
156 \item $\sem{\forall x.P} = \N \to \sem{P}$
157 \item $\sem{\exists x.P} = \N \times \sem{P}$
161 For any type T of system T $\bot_T: 1 \to T$ is inuctively defined as follows:
163 \item $\bot_1 = \lambda x:1.x$
164 \item $\bot_N = \lambda x:1.0$
165 \item $\bot_{U\times V} = \lambda x:1.<\bot_{U} x,\bot_{V} x>$
166 \item $\bot_{U\to V} = \lambda x:1.\lambda \_:U. \bot_{V} x$
170 \item $\sem{nat\_ind} = R$
171 \item $\sem{ex\_ind} = (\lambda f:(\N \to \sem{P} \to \sem{Q}).
172 \lambda p:\N\times \sem{P}.f (fst \,p) (snd \,p)$.
173 \item $\sem{ex\_intro} = \lambda x:\N.\lambda f:\sem{P}.<x,f>$
174 \item $\sem{fst} = \pi_1$
175 \item $\sem{snd} = \pi_2$
176 \item $\sem{conj} = \lambda x:\sem{P}.\lambda y:\sem{Q}.<x,y>$
177 \item $\sem{false\_ind} = \bot_{\sem{Q}}$
178 \item $\sem{discriminate} = \lambda \_:\N.\lambda \_:1.\star$
179 \item $\sem{injS}= \lambda \_:\N. \lambda \_:\N.\lambda \_:1.\star$
180 \item $\sem{plus\_O} = \sem{times\_O} = \lambda \_:\N.\star$
181 \item $\sem{plus\_S} = \sem{times_S} = \lambda \_:\N. \lambda \_:\N.\star$
184 In the case of structured proofs:
186 \item $\sem{M N} = \sem{M} \sem{N}$
187 \item $\sem{\lambda x:A.M} = \lambda x:\sem{A}.\sem{M}$
188 \item $\sem{\lambda x:\N.M} = \lambda x:\N.\sem{M}$
189 \item $\sem{M t} = \sem{M} \sem{t}$
192 \section{Realizability}
193 The realizability relation is a relation $f \R P$ where $f: \sem{P}$.
196 \item $\neg (\star \R \bot)$
197 \item $* \R (t_1=t_2)$ iff $t_1=t_2$ is true ...
198 \item $<f,g> \R (P\land Q)$ iff $f \R P$ and $g \R Q$
199 \item $f \R (P\to Q)$ iff for any $m$ such that $m \R P$, $(f \,m) \R Q$
200 \item $f \R (\forall x.P)$ iff for any natural number $n$ $(f n) \R P[\underline{n}/x]$
201 \item $<n,g> \R (\exists x.P)$ iff $g \R P[\underline{n}/x]$
205 We proceed to prove that all axioms $ax:Ax$ are realized by $\sem{ax}$.
209 We must prove that the recursion schema $R$ realizes the induction principle.
210 To this aim we must prove that for any $a$ and $f$ such that $a \R P(0)$ and
211 $f \R \forall x.(P(x) \to P(S(x)))$, and any natural number $n$, $(R \,a \,f
212 \,n) \R P(\underline{n})$.\\
213 We proceed by induction on n.\\
214 If $n=O$, $(R \,a \,f \,O) = a$ and by hypothesis $a \R P(0)$.\\
215 Suppose by induction that
216 $(R \,a \,f \,n) \R P(\underline{n})$, and let us prove that the relation
217 still holds for $n+1$. By definition
218 $(R \,a \,f \,(n+1)) = f \,n \,(R \,a \,f \,n)$,
219 and since $f \R \forall x.(P(x) \to P(S(x)))$,
220 $(f n (R a f n)) \R P(S(\underline{n}))=P(\underline{n+1})$.
223 We must prove that $$\underline{ex\_ind} \R (\forall x:(P x)
224 \to Q) \to (\exists x:(P x)) \to Q$$ Following the definition of $\R$ we have
225 to prove that given\\ $f~\R~\forall~x:((P~x)~\to~Q)$ and
226 $p~\R~\exists~x:(P~x)$, then $\underline{ex\_ind}~f~p \R Q$.\\
227 $p$ is a couple $<n_p,g_p>$ such that $g_p \R P[\underline{n_p}/x]$, while
228 $f$ is a function such that forall $n$ and for all $m \R P[\underline{n}/x]$
229 then $f~n~m \R Q$ (note that $x$ is not free in $Q$ so $[\underline{n}/x]$
231 Exapanding the definition of $\underline{ex\_ind}$, $fst$
232 and $snd$ we obtain $f~n_p~g_p$ that we know is in relation $\R$ with $Q$
233 since $g_p \R P[\underline{n_p}/x]$.
237 $$\lambda x:\N.\lambda f:\sem{P}.<x,f> \R \forall x.(P\to\exists x.P(x)$$
238 that leads to prove that foreach n
239 $\underline{ex\_into}~n \R (P\to\exists x.P(x))[\underline{n}/x]$.\\
240 Evaluating the substitution we have
241 $\underline{ex\_into}~n \R (P[\underline{n}/x]\to\exists x.P(x))$.\\
242 Again by definition of $\R$ we have to prove that given a
243 $m \R P[\underline{n}/x]$ then $\underline{ex\_into}~n~m \R \exists x.P(x)$.
244 Expanding the definition of $\underline{ex\_intro}$ we have
245 $<n,m> \R \exists x.P(x)$ that is true since $m \R P[\underline{n}/x]$.
248 Wehave to prove that $\pi_1 \R P \land Q \to P$, that is equal to proving
249 that for each $m \R P \land Q$ then $\pi_1~m \R P$ .
250 $m$ must be a couple $<f_m,g_m>$ such that $f_m \R P$ and $g_m \R Q$.
251 So we conclude that $\pi_1~m$ reduces to $f_m$ that is in relation $\R$
254 \item $snd$. The same for $fst$.
257 We have to prove that
258 $$\lambda x:\sem{P}. \lambda y:\sem{Q}.<x,y> \R P \to Q \to P \land Q$$
259 Following the definition of $\R$ we have to show that
260 foreach $m \R P$ and foreach $n \R Q$ then
261 $(\lambda x:\sem{P}. \lambda y:\sem{Q}.<x,y>)~m~n \R P \land Q$.\\
262 This is the same of $<m,n> \R P \land Q$ that is verified since
263 $m \R P$ and $n \R Q$.
267 We have to prove that $\bot_{\sem{Q}} \R \bot \to Q$.
268 Trivial, since there is no $m \R \bot$.
270 \item $discriminate$.
271 Since there is no $n$ such that $0 = S n$ is true... \\
272 $\underline{discriminate}~n \R 0 = S~\underline{n} \to \bot$ for each n.
275 We have to prove that for each $n_1$ and $n_2$\\
276 $\lambda \_:\N. \lambda \_:\N.\lambda \_:1.*~n_1~n_2 \R
277 (S(x)=S(y)\to x=y)[n_1/x][n_2/y]$.\\
278 We assume that $m \R S(n_1)=S(n_2)$ and we have to show that
279 $\lambda \_:\N. \lambda \_:\N.\lambda \_:1.*~n_1~n_2~m$ that reduces to
280 $*$ is in relation $\R$ with $n_1=n_2$. Since in the standard model of
281 natural numbers $S(n_1)=S(n_2)$ implies $n_1=n_2$ we have that
285 Since in the standard model for natural numbers $0$ is the neutral element
286 for addition $\lambda \_:\N.\star \R \forall x.x + 0 = x$.
289 In the standard model of natural numbers the addition of two numbers is the
290 operation of counting the second starting from the first. So
291 $$\lambda \_:\N. \lambda \_:\N. \star \R \forall x,y.x+S(y)=S(x+y)$$.
294 Since in the standard model for natural numbers $0$ is the absorbing element
295 for multiplication $\lambda \_:\N.\star \R \forall x.x \times 0 = x$.
298 In the standard model of natural numbers the multiplications of two
299 numbers is the operation of adding the first to himself a number of times
300 equal to the second number. So
301 $$\lambda \_:\N. \lambda \_:\N. \star \R \forall x,y.x+S(y)=S(x+y)$$.
306 \begin{thebibliography}{}
307 \bibitem{Girard86}G.Y.Girard. The system F of variable types, fifteen
308 years later. Theoretical Computer Science 45, 1986.
309 \bibitem{Girard87}G.Y.Girard. Proof Theory and Logical Complexity.
310 Bibliopolis, Napoli, 1987.
311 \bibitem{GLT}G.Y.Girard, Y.Lafont, P.Tailor. Proofs and Types.
312 Cambridge Tracts in Theoretical Computer Science 7.Cambridge University
314 \bibitem{Godel58}K.G\"odel. \"Uber eine bisher noch nicht ben\"utzte Erweiterung
315 des finiten Standpunktes. Dialectica, 12, pp.34-38, 1958.
316 \bibitem{Godel90}K.G\"odel. Collected Works. Vol.II, Oxford University Press,
318 \bibitem{Howard68}W.A.Howard. Functional interpretation of bar induction
319 by bar recursion. Compositio Mathematica 20, pp.107-124. 1958
320 \bibitem{Howard80}W.A.Howard. The formulae-as-types notion of constructions.
321 in J.P.Seldin and j.R.Hindley editors, to H.B.Curry: Essays on Combinatory
322 Logic, Lambda calculus and Formalism. Acedemic Press, 1980.
323 \bibitem{Kreisel59} G.Kreisel. Interpretation of analysis by means of
324 constructive functionals of finite type. In. A.Heyting ed.
325 {\em Constructivity in mathematics}. North Holland, Amsterdam,1959.
326 \bibitem{Kreisel62} G.Kreisel. On weak completeness of intuitionistic
327 predicatelogic. Journal of Symbolic Logic 27, pp. 139-158. 1962.
328 \bibitem{Letouzey04}P.Letouzey. Programmation fonctionnelle
329 certifi\'ee; l'extraction
330 de programmes dans l'assistant Coq. Ph.D. Thesis, Universit\'e de
331 Paris XI-Orsay, 2004.
332 \bibitem{Loef}P.Martin-L\"of. Intuitionistic Type Theory.
333 Bibliopolis, Napoli, 1984.
334 \bibitem{Paulin87}C.Paulin-Mohring. Extraction de programme dans le Calcul de
335 Constructions. Ph.D. Thesis, Universit\'e de
337 \bibitem{Paulin89}C.Paulin-Mohring. Extracting $F_{\omega}$ programs
338 from proofs in the Calculus of Constructions. In proc. of the Sixteenth Annual
340 Principles of Programming Languages, Austin, January, ACML Press 1989.
341 \bibitem{Sch}K.Sch\"utte. Proof Theory. Grundlehren der mathematischen
342 Wissenschaften 225, Springer Verlag, Berlin, 1977.
343 \bibitem{Troelstra}A.S.Troelstra. Metamathemtical Investigation of
345 Arithmetic and Analysis. Lecture Notes in Mathematics 344, Springer Verlag,
347 \bibitem{TS}A.S.Troelstra, H.Schwichtenberg. Basic Proof Theory.
348 Cambridge Tracts in Theoretical Computer Science 43.Cambridge University
350 \bibitem{Werner}B.Werner. Une Th\'eorie des Constructions Inductives.
351 Ph.D.Thesis, Universit\'e de Paris 7, 1994.
354 \end{thebibliography}