Name
Abstract | ||
|---|---|---|
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 5 to show some of their properties:the stability of the set of storage operators under the beta-equivalence (Theorem 5.1.1);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);the existence of storage operators for every finite set of closed normal lambda-terms (Theorem 5.4.3);the computation time of the ''storage operation'' (Theorem 5.5.2). |
Year | DOI | Venue |
|---|---|---|
1995 | 10.2307/2275874 | JOURNAL OF SYMBOLIC LOGIC |
DocType | Volume | Issue |
Journal | 60 | 4 |
ISSN | Citations | PageRank |
0022-4812 | 5 | 0.67 |
References | Authors | |
3 | 2 | |
Name | Order | Citations | PageRank |
|---|---|---|---|
| René David | 1 | 196 | 21.98 |
| Karim Nour | 2 | 65 | 15.07 |