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

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\).