Storage operators and directed lambda-calculus

Journal of Symbolic Logic 60 (4):1054-1086 (1995)
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: $\bullet$ the stability of the set of storage operators under the β-equivalence (Theorem 5.1.1); $\bullet$ 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); $\bullet$ the existence of storage operators for every finite set of closed normal λ-terms (Theorem 5.4.3); $\bullet$ the computation time of the "storage operation" (Theorem 5.5.2)
Keywords No keywords specified (fix it)
Categories (categorize this paper)
DOI 10.2307/2275874
Options
Edit this record
Mark as duplicate
Export citation
Find it on Scholar
Request removal from index
Revision history

Download options

Our Archive


Upload a copy of this paper     Check publisher's policy     Papers currently archived: 33,762
Through your library

References found in this work BETA

Opérateurs de Mise En Mémoire Et Traduction de Gödel.Jean-Louis Krivine - 1990 - Archive for Mathematical Logic 30 (4):241-267.

Add more references

Citations of this work BETA

No citations found.

Add more citations

Similar books and articles

On the Logic of Β -Pregroups.Aleksandra Kiślak-Malinowska - 2007 - Studia Logica 87 (2-3):323 - 342.
Compact Bracket Abstraction in Combinatory Logic.Sabine Broda & Luís Damas - 1997 - Journal of Symbolic Logic 62 (3):729-740.
The Abstract Variable-Binding Calculus.Don Pigozzi & Antonino Salibra - 1995 - Studia Logica 55 (1):129 - 179.
-Calculus and Böhm's Theorem.René David & Walter Py - 2001 - Journal of Symbolic Logic 66 (1):407-413.
Variable Binding Term Operators in $\Lambda $-Calculus.M. W. Bunder - 1979 - Notre Dame Journal of Formal Logic 20 (4):876-878.
Topological Representation of the Lambda-Calculus.Steve Awodey - 2000 - Mathematical Structures in Computer Science 10 (1):81-96.

Analytics

Added to PP index
2009-01-28

Total downloads
45 ( #134,983 of 2,263,146 )

Recent downloads (6 months)
2 ( #211,446 of 2,263,146 )

How can I increase my downloads?

Monthly downloads

My notes

Sign in to use this feature