1,721,109 research outputs found
Extending the lambda-calculus with unbind and rebind
No full textWe extend the simply typed lambda-calculus with unbind and rebind primitive constructs. That is, a value can be a fragment of open code, which in order to be used should be explicitly rebound. This mechanism nicely coexists with standard static binding. The motivation is to provide an unifying foundation for mechanisms of dynamic scoping, where the meaning of a name is determined at runtime, rebinding, such as dynamic updating of resources and exchange of mobile code, and delegation, where an alternative action is taken if a binding is missing. Depending on the application scenario, we consider two extensions which differ in the way type safety is guaranteed. The former relies on a combination of static and dynamic type checking. That is, rebind raises a dynamic error if for some variable there is no replacing term or it has the wrong type. In the latter, this error is prevented by a purely static type system, at the price of more sophisticated types
Compositional characterisations of lambda-terms using intersection types
No full textWe show how to characterise compositionally a number of evaluation properties of λ-terms using Intersection Type assignment systems. In particular, we focus on termination properties, such as strong normalisation, normalisation, head normalisation, and weak head normalisation. We consider also the persistent versions of such notions. By way of example, we consider also another evaluation property, unrelated to termination, namely reducibility to a closed term. Many of these characterisation results are new, to our knowledge, or else they streamline, strengthen, or generalise earlier results in the literature. The completeness parts of the characterisations are proved uniformly for all the properties, using a set-theoretical semantics of intersection types over suitable kinds of stable sets. This technique generalises Krivine's and Mitchell's methods for strong normalisation to other evaluation properties
Approximation Theorems for intersection type systems
No full textIn this paper we prove that many intersection type theories of interest (including those which induce as filter models, Scott's and Park's D∞ models, the models studied in Barendregt Coppo Dezani, Abramsky Ong, and Honsell Ronchi) satisfy an Approximation Theorem with respect to a suitable notion of approximant. This theorem implies that a λ-term has a type if and only if there exists an approximant of that term which has that type. We prove this result uniformly for all the intersection type theories under consideration using a Kripke version of stable sets where bases correspond to worlds
Intersection types and lambda models
No full textInvariance of interpretation by beta-conversion is one of the minimal requirements for any standard model for the gimel-calculus. With the intersection-type systems being a general framework for the study of semantic domains for the gimel-calculus, the present paper provides a (syntactic) characterisation of the above mentioned requirement in terms of characterisation results for intersection-type assignment systems. Instead of considering conversion as a whole, reduction and expansion will be considered separately. Not only for usual computational rules like beta, eta, but also for a number of relevant restrictions of those. Characterisations will be also provided for (intersection) filter structures that are indeed gimel-models. (c) 2006 Elsevier B.V. All rights reserved
INFINITE LAMBDA CALCULUS AND TYPES
No full textRecent work on infinitary versions of the lambda calculus has shown that the infinite lambda calculus can be a useful tool to study the unsolvable terms of the classical lambda calculus. Working in the framework of the intersection type disciplines, we devise a type assignment system such that two terms are equal in the infinite lambda calculus iff they can be assigned the same types in any basis. A novel feature of the system is the presence of a type constant to denote the set of all terms of order zero, and the possibility of applying a type to another type. We prove a completeness and an approximation theorem for our system. Our results can be considered as a first step towards the goal of giving a denotational semantics for the lambda calculus which is suited for the study of the unsolvable terms. However, some noncontinuity phenomena of the infinite lambda calculus make a full realization construction of a filter model) a quite difficult task
- …
