Hostname: page-component-78c5997874-v9fdk Total loading time: 0 Render date: 2024-11-03T00:26:05.732Z Has data issue: false hasContentIssue false

A semantics for lambda calculi with resources

Published online by Cambridge University Press:  01 August 1999

GÉRARD BOUDOL
Affiliation:
INRIA, BP93, F-06902 Sophia Antipolis Cedex
PIERRE-LOUIS CURIEN
Affiliation:
ENS DMI, 45 Rue d'Ulm, F-75230 Paris, Cedex 05
CAROLINA LAVATELLI
Affiliation:
ENS DMI, 45 Rue d'Ulm, F-75230 Paris, Cedex 05

Abstract

We present the λ-calculus with resources λr, and two variants of it: a deterministic restriction λm and an extension λcr with a convergence testing operator. These calculi provide a control on the substitution process – deadlocks may arise if not enough resources are available to carry out all the substitutions needed to pursue a computation. The design of these calculi was motivated by Milner's encoding of the λ-calculus in the π-calculus. As Boudol and Laneve have shown elsewhere, the discriminating power of λm (given by the contextual observational equivalence) over λ-terms coincides with that induced by Milner's π-encoding, and coincides also with that provided by the lazy algebraic semantics (Lévy–Longo trees). The main contribution of this paper is model-theoretic. We define and solve an appropriate domain equation, and show that the model thus obtained is fully abstract with respect to λcr. The techniques used are in the line of those used by Abramsky for the lazy λ-calculus, the main departure being that the resource-consciousness of our calculi leads us to introduce a non-idempotent form of intersection types.

Type
Research Article
Copyright
© 1999 Cambridge University Press

Access options

Get access to the full version of this content by using one of the access options below. (Log in options will check for institutional or personal access. Content may require purchase if you do not have access.)