Storage Operators and Directed Lambda-Calculus
David, Rene ; Nour, Karim
J. Symbolic Logic, Tome 60 (1995) no. 1, p. 1054-1086 / Harvested from Project Euclid
Storage operators have been introduced by J. L. Krivine in [5] they are closed $\lambda$-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 $\lambda$-calculus and show that it has the usual properties of the ordinary $\lambda$-calculus. With this calculus we get an equivalent--and simple--definition of the storage operators that allows to show some of their properties: $\bullet$ the stability of the set of storage operators under the $\beta$-equivalence (Theorem 5.1.1); $\bullet$ the undecidability (and semidecidability) of the problem "is a closed $\lambda$-term $t$ a storage operator for a finite set of closed normal $\lambda$-terms?" (Theorems 5.2.2 and 5.2.3); $\bullet$ the existence of storage operators for every finite set of closed normal $\lambda$-terms (Theorem 5.4.3); $\bullet$ the computation time of the "storage operation" (Theorem 5.5.2).
Publié le : 1995-12-14
Classification: 
@article{1183744863,
     author = {David, Rene and Nour, Karim},
     title = {Storage Operators and Directed Lambda-Calculus},
     journal = {J. Symbolic Logic},
     volume = {60},
     number = {1},
     year = {1995},
     pages = { 1054-1086},
     language = {en},
     url = {http://dml.mathdoc.fr/item/1183744863}
}
David, Rene; Nour, Karim. Storage Operators and Directed Lambda-Calculus. J. Symbolic Logic, Tome 60 (1995) no. 1, pp.  1054-1086. http://gdmltest.u-ga.fr/item/1183744863/