STORAGE OPERATORS AND DIRECTED LAMBDA-CALCULUS
David, René ; Nour, Karim
HAL, hal-00385174 / Harvested from HAL
Storage operators have been introduced by J.L. Krivine in [5] ; they are closed l-terms which, for a data type, allow to simulate a "call by value" while using the "call by name" strategy. In this paper, we introduce the directed l-calculus and show that it has the usual properties of the ordinary l-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 b-equivalence (theorem 5.1.1) ; - the undecidability ( and its semi-decidability ) of the problem "is a closed l-term t a storage operator for a finite set of closed normal l-terms ? " (theorems 5.2.2 and 5.2.3) ; - the existence of storage operators for every finite set of closed normal l-terms (theorem 5.4.3) ; - the computation time of the "storage operation" (theorem 5.5.2).
Publié le : 1995-12-18
Classification:  [MATH.MATH-LO]Mathematics [math]/Logic [math.LO],  [INFO.INFO-LO]Computer Science [cs]/Logic in Computer Science [cs.LO]
@article{hal-00385174,
     author = {David, Ren\'e and Nour, Karim},
     title = {STORAGE OPERATORS AND DIRECTED LAMBDA-CALCULUS},
     journal = {HAL},
     volume = {1995},
     number = {0},
     year = {1995},
     language = {en},
     url = {http://dml.mathdoc.fr/item/hal-00385174}
}
David, René; Nour, Karim. STORAGE OPERATORS AND DIRECTED LAMBDA-CALCULUS. HAL, Tome 1995 (1995) no. 0, . http://gdmltest.u-ga.fr/item/hal-00385174/