zbMATH — the first resource for mathematics

Lambda-calcul, évaluation paresseuse et mise en mémoire. (Lambda calculus, lazy evaluation and storage operators). (French) Zbl 0717.03003
The abstract of the paper seems to be the best way to resume this very nice paper: “In pure \(\lambda\)-calculus, we identify lazy evaluation with leftmost \(\beta\)-reduction. This strategy of reduction has many advantages (in particular, it always gives normal form when there exists one); but it has the following drawback: the argument of a function must be evaluated as many times as it is used. To avoid this defect, we introduce, for each data type (like Booleans, integers, lists...), some terms called “storage operators”. For example, if \(\nu\) is \(\beta\)- equivalent to an integer, and \(\phi\) is any term, we replace \(\phi\nu\) by \(T\nu\phi\), where T is a storage operator for integers; during lazy evaluation of \(T\nu\phi\), \(\nu\) will be evaluated only once.
We give a general definition for the notion of storage operator for a set of \(\lambda\)-calculus terms. We show how to construct such operators, using a system of typed \(\lambda\)-calculus of second order. To this end, we use Gödel’s \(\neg \neg\)-translation, which transforms a proof in classical logic into an intuitionistic proof.”
Reviewer: R.David

03B40 Combinatory logic and lambda calculus
68Q60 Specification and verification (program logics, model checking, etc.)
Full Text: DOI EuDML
[1] 1. H. P. BARENDREGT, The lambda calculus, North Holland, 1984. Zbl0551.03007 MR774952 · Zbl 0551.03007
[2] 2. J. Y. GIRARD, Une extension de l’interprétation de Gödel à l’analyse, et son application à l’élimination des coupures, Proc. 2nd Scand. Logic Symp., 1970, North Holland, p. 63-92. Zbl0221.02013 MR409133 · Zbl 0221.02013
[3] 3. J. L. KRIVINE, Lambda-calcul typé, Masson, 1990. MR1162977
[4] 4. J. L. KRIVINE et M. PARIGOT, Programming with proofs, 6th Symp.. Comp. Theory 87, J. Inf. Process. Cybern., 3, 1990, p. 149-157. Zbl0699.68020 MR1056588 · Zbl 0699.68020
[5] 5. D. LEIVANT, Reasoning about Functional Programs and Complexity Classes Associated with Type Disciplines, 24th Symp. on Found. of Comp. Sci., 1983, p. 460-469.
[6] 6. M. PARIGOT, Programming with Proofs: a Second Order Type Theory, Proc. ESOP’88, Lect. Notes in Comp. Sci., 300, p. 145-159.
[7] 7. J. L. KRIVINE, Opérateurs de mise en mémoire et traduction de Gödel, Archiv for math. Logic (à paraître). Zbl0712.03009 MR1080590 · Zbl 0712.03009 · doi:10.1007/BF01792986
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.