We 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.
In 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.
Invariance of interpretation by
β
-conversion is one of the minimal requirements for any standard model for the
λ
-calculus. With the intersection-type systems being a general framework for the study ...of semantic domains for the
λ
-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
β
,
η
, but also for a number of relevant restrictions of those. Characterisations will be also provided for (intersection) filter structures that are indeed
λ
-models.
We construct two inverse limit
λ-models which completely characterise sets of terms with similar computational behaviours: the sets of normalising, head normalising, weak head normalising
λ-terms, ...those corresponding to the persistent versions of these notions, and the sets of closable, closable normalising, and closable head normalising
λ-terms. More precisely, for each of these sets of terms there is a corresponding element in at least one of the two models such that a term belongs to the set if and only if its interpretation (in a suitable environment) is greater than or equal to that element. We use the finitary logical description of the models, obtained by defining suitable intersection type assignment systems, to prove this.
Intersection types for explicit substitutions Lengrand, Stéphane; Lescanne, Pierre; Dougherty, Dan ...
Information and computation,
02/2004, Letnik:
189, Številka:
1
Journal Article
Recenzirano
Odprti dostop
We present a new system of intersection types for a composition-free calculus of explicit substitutions with a rule for garbage collection, and show that it characterizes those terms which are ...strongly normalizing. This system extends previous work on the natural generalization of the classical intersection types system, which characterized head normalization and weak normalization, but was not complete for strong normalization. An important role is played by the notion of
available variable in a term, which is a generalization of the classical notion of free variable.
We use intersection types as a tool for obtaining
λ-models. Relying on the notion of
easy intersection type theory, we successfully build a
λ-model in which the interpretation of an arbitrary simple ...easy term is any filter which can be described by a continuous predicate. This allows us to prove two results. The first gives a proof of consistency of the
λ-theory where the
λ-term (
λx.
xx)(
λx.
xx) is forced to behave as the join operator. This result has interesting consequences on the algebraic structure of the lattice of
λ-theories. The second result is that for any simple easy term, there is a
λ-model, where the interpretation of the term is the
minimal fixed point operator.
Type assignment systems with intersection and union types are introduced. Although the subject reduction property with respect to β-reduction does not hold for a natural deduction-like system, we ...manage to overcome this problem in two, different ways. The first is to adopt a notion of parallel reduction, which is a refinement of Gross-Knuth reduction. The second is to introduce type theories to refine the system, among which is the theory called Π that induces an assignment system preserving β-reduction. This type assignment system further clarifies the relation with the intersection discipline through the decomposition, first, of a disjunctive type into a set of conjunctive types and, second, of a derivation in the new type assignment system into a set of derivations in the intersection type assignment system. For this system we propose three semantics and prove soundness and completeness theorems.
This paper analyses the computational behaviour of lambda-term applications. The properties we are interested in are weak normalisation (i.e. there is a terminating reduction) and strong ...normalisation (i.e. all reductions are terminating). One can prove that the application of a lambda-term M to a fixed number n of copies of the same arbitrary strongly normalising lambda-term is strongly normalising if and only if the application of M to n different arbitrary strongly normalising lambda-terms is strongly normalising, i.e. one has that M (X ... X)/n is strongly normalising, for an arbitrary strongly normalising X, if and only if MX 1 ...X n is strongly normalising for arbitrary strongly normalising X 1 , ..., X n . The analogous property holds when replacing strongly normalising by weakly normalising. As an application of the result on strong normalisation the lambda-terms whose interpretation is the top element (in the environment which associates the top element to all variables) of the Honsell-Lenisa model turn out to be exactly the lambda-terms which, applied to an arbitrary number of strongly normalising lambda-terms, always produces strongly normalising lambda-terms. This proof uses a finitary logical description of the model by means of intersection types. This answers an open question stated by Dezani, Honsell and Motohama
Recent 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 of this idea (namely the construction of a filter model) a quite difficult task.
PDF
