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

*(French)*Zbl 0712.03009The 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\).

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
PDF
BibTeX
XML
Cite

\textit{J.-L. Krivine}, Arch. Math. Logic 30, No. 4, 241--267 (1990; Zbl 0712.03009)

Full Text:
DOI

##### 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 |

This reference list is based on information provided by the publisher or from digital mathematics libraries. Its items are heuristically matched to zbMATH identifiers and may contain data conversion errors. It attempts to reflect the references listed in the original paper as accurately as possible without claiming the completeness or perfect precision of the matching.