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 characterize those
type preorders
which yield complete
intersection-type assignment systems
for λ-calculi, with respect to the three canonical set-theoretical semantics for intersection-types: the ...inference semantics, the simple semantics, and the F-semantics. These semantics arise by taking as interpretation of types subsets of applicative structures, as interpretation of the
preorder relation
, ≤, set-theoretic inclusion, as interpretation of the
intersection constructor
, ∩, set-theoretic intersection, and by taking the interpretation of the
arrow constructor
, → à
la
Scott, with respect to either
any possible functionality set
, or the
largest
one, or the
least
one.These results strengthen and generalize significantly all earlier results in the literature, to our knowledge, in at least three respects. First of all the inference semantics had not been considered before. Second, the characterizations are all given just in terms of simple closure conditions on the
preorder relation
, ≤, on the types, rather than on the typing judgments themselves. The task of checking the condition is made therefore considerably more tractable. Last, we do not restrict attention just to λ-models, but to arbitrary applicative structures which admit an interpretation function. Thus we allow also for the treatment of models of restricted λ-calculi. Nevertheless the characterizations we give can be tailored just to the case of λ-models.
In the age of the world-wide web and mobile computing, programming communication-centric software is essential. Thus, programmers and program designers are exposed to new levels of complexity, such ...as ensuring the correct composition of communication behaviours and guaranteeing deadlock-freedom of their protocols.
This paper proposes the language \documentclass12pt{minimal}
\usepackage{amsmath}
\usepackage{wasysym}
\usepackage{amsfonts}
\usepackage{amssymb}
\usepackage{amsbsy}
\usepackage{mathrsfs}
\usepackage{upgreek}
\setlength{\oddsidemargin}{-69pt}
\begin{document}$\mathcal{L}_{doos}$\end{document}, a simple distributed object-oriented language augmented with session communication primitives and types. \documentclass12pt{minimal}
\usepackage{amsmath}
\usepackage{wasysym}
\usepackage{amsfonts}
\usepackage{amssymb}
\usepackage{amsbsy}
\usepackage{mathrsfs}
\usepackage{upgreek}
\setlength{\oddsidemargin}{-69pt}
\begin{document}$\mathcal{L}_{doos}$\end{document} provides a flexible object-oriented programming style for structural interaction protocols by prescribing channel usages within signatures of distributed classes.
We develop a typing system for \documentclass12pt{minimal}
\usepackage{amsmath}
\usepackage{wasysym}
\usepackage{amsfonts}
\usepackage{amssymb}
\usepackage{amsbsy}
\usepackage{mathrsfs}
\usepackage{upgreek}
\setlength{\oddsidemargin}{-69pt}
\begin{document}$\mathcal{L}_{doos}$\end{document} and prove its soundness with respect to the operational semantics. We also show that in a well-typed \documentclass12pt{minimal}
\usepackage{amsmath}
\usepackage{wasysym}
\usepackage{amsfonts}
\usepackage{amssymb}
\usepackage{amsbsy}
\usepackage{mathrsfs}
\usepackage{upgreek}
\setlength{\oddsidemargin}{-69pt}
\begin{document}$\mathcal{L}_{doos}$\end{document} program, there will never be a connection error, a communication error, nor an incorrect completion between server-client interactions. These results demonstrate that a consistent integration of object-oriented language features and session types can statically check the consistent composition of communication protocols.
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.
More dynamic object reclassification Drossopoulou, Sophia; Damiani, Ferruccio; Dezani-Ciancaglini, Mariangiola ...
ACM transactions on programming languages and systems,
03/2002, Letnik:
24, Številka:
2
Journal Article
Recenzirano
Reclassification
changes the class membership of an object at run-time while retaining its identity. We suggest language features for object reclassification, which extend an imperative, typed, ...class-based, object-oriented language.We present our proposal through the language
Fickle
⋄⋄
. The imperative features, combined with the requirement for a static and safe type system, provided the main challenges. We develop a type and effect system for
Fickle
⋄⋄
and prove its soundness with respect to the operational semantics. In particular, even though objects may be reclassified across classes with different members, there will never be an attempt to access nonexisting members.
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.
PDF
