Opérateurs de mise en mémoire et traduction de Gödel. (Storage operators and Gödel translation). (French) Zbl 0712.03009

Krivine, Jean-Louis

Arch. Math. Logic 30, No. 4, 241-267 (1990).

The leftmost reduction strategy S of \(\lambda\)-calculus (“call by name”) has many mathematical advantages: for example it always terminates when applied to a normalizable term. A practical advantage of S is that the argument of a function is evaluated only if it is really needed; on the negative side it will be evaluated each time it is used.
The author remedies to this drawback by means of “storage operators” (for each data type). A storage operator T, say for the integers, will be a term of pure \(\lambda\)-calculus, with the property that: for each \(\lambda\)-term \(\phi\) and for each \(\nu\) which is \(\beta\)-equivalent to an integer there will be a reduced form \(\nu_ 0\) of \(\nu\) (not far from its normal form) such that the left computation of \(T\nu\) f is equivalent (same length and same result) to the computation of \(\nu\) to \(\nu_ 0\) followed by the (left) computation of \(\phi \nu_ 0\). Thus, the call-by- value computation of \(\phi\nu\) will be simulated by the call-by-name computation of \(T\nu\phi\).
Let D[x] be a formula of second order functional arithmetic defining a data type D, and let \(D^*[x]\) be a Gödel transform of D[x]. The main theorem of the paper states that any term T of \(\lambda\)-calculus which encodes a 2nd order intuitionistic proof of the theorem \(\forall x(D[x]^*\to \neg \neg D[x])\) will be a storage operator. This solves the conjecture raised by the author [RAIRO, Inf. Théor. Appl. 25, No.1, 67-84 (1991)] (with a slightly different definition of storage operators).
The logical framework (and type system) is the second order functional arithmetic, \(AF_ 2\), developed by the author in his book [Lambda- calcul, types et modèles (1990; Zbl 0697.03004)], however the paper is self-contained. The conceptual part of the proof, which is also highly technical, relies on a simple version of Gödel’s translation and a systematic use of realisability in standard models of \(AF_ 2\).

Reviewer: C.Berline

MSC:

03B40	Combinatory logic and lambda calculus
68Q65	Abstract data types; algebraic specification
03F35	Second- and higher-order arithmetic and fragments

Keywords:

leftmost reduction strategy; \(\lambda \) -calculus; call by name; storage operators; second order functional arithmetic; data type

Citations:

Zbl 0697.03004

References:

[1]	Barendregt, H.: The lambda calculus. Amsterdam: North-Holland 1984 · Zbl 0551.03007
[2]	Girard, J.-Y.: Une extension de l’interprétation de Gödel à l’analyse. In: Fenstad, J. (ed.) Proc. 2nd Scand. Logic Symp., pp. 63–92. Amsterdam: North-Holland 1971
[3]	Krivine, J.-L.: Lambda-calcul, évaluation paresseuse et mise en mémoire. A paraître dans Informatique théorique et applications (R.A.I.R.O.)
[4]	Krivine, J.-L.: Lambda-calcul, types et modèles. Paris: Masson 1990 · Zbl 0697.03004
[5]	Leivant, D.: Reasoning about functional programs and complexity classes associated with type disciplines. 24th Annual Symp. on Found. of Comp. Sci. pp. 460–469, 1983
[6]	Krivine, J.-L., Parigot, M.: Programming with proofs. 6th Symp. Comp. Theory 87. J. Inf. Process. Cybern.3, 149–167 (1990) · Zbl 0699.68020