Research indexJournal article
Storage operators and directed lambda-calculus
David, Nour
Journal of Symbolic Logic1 Dec 1995Open access
Storage operators and directed lambda-calculus
David, Nour · Journal of Symbolic Logic · 1995
Abstract
Abstract Storage operators have been introduced by J. L. Krivine in [5] they are closed λ -terms which, for a data type, allow one to simulate a “call by value” while using the “call by name” strategy. In this paper, we introduce the directed λ -calculus and show that it has the usual properties of the ordinary λ -calculus. With this calculus we get an equivalent—and simple—definition of the storage operators that allows to show some of their properties: • the stability of the set of storage operators under the β -equivalence (Theorem 5.1.1); • the undecidability (and semidecidability) of the problem “is a closed λ -term t a storage operator for a finite set of closed normal λ -terms?” (Theorems 5.2.2 and 5.2.3); • the existence of storage operators for every finite set of closed normal λ -terms (Theorem 5.4.3); • the computation time of the “storage operation” (Theorem 5.5.2).