Wyniki wyszukiwania - BazTech

1

The Algebra of Expansion

Carlier S., Wells J. B.

Fundamenta Informaticae

|

2012

|

Vol. 121, nr 1/4

43-82

EN

Expansion is an operation on typings (pairs of type environments and result types) in type systems for the λ-calculus. Expansion was originally introduced for calculating possible typings of a l-term in systems with intersection types. This paper aims to clarify expansion and make it more accessible to a wider community by isolating the pure notion of expansion on its own, independent of type systems and types, and thereby make it easier for non-specialists to obtain type inference with flexible precision by making use of theory and techniques that were originally developed for intersection types. We redefine expansion as a simple algebra on terms with variables, substitutions, composition, and miscellaneous constructors such that the algebra satisfies 8 simple axioms and axiom schemas: the 3 standard axioms of a monoid, 4 standard axioms or axiom schemas of substitutions (including one that corresponds to the usual "substitution lemma" that composes substitutions), and 1 very simple axiom schema for expansion itself. Many of the results on the algebra have also been formally checked with the Coq proof assistant. We then take System E, a λ-calculus type system with intersection types and expansion variables, and redefine it using the expansion algebra, thereby demonstrating how a single uniform notion of expansion can operate on both typings and proofs. Because we present a simplified version of System E omitting many features, this may be independently useful for those seeking an easier-tocomprehend version.

2

Reducibility Proofs in the λ-Calculus

Kamareddine F., Rahli V., Wells J. B.

Fundamenta Informaticae

|

2012

|

Vol. 121, nr 1/4

121-152

EN

Reducibility, despite being quite mysterious and inflexible, has been used to prove a number of properties of the λ-calculus and is well known to offer general proofs which can be applied to a number of instantiations. In this paper, we look at two related but different results in λ-calculi with intersection types. 1. We show that one such result (which aims at giving reducibility proofs of Church-Rosser, standardisation and weak normalisation for the untyped λ-calculus) faces serious problems which break the reducibility method. We provide a proposal to partially repair the method. 2. We consider a second result whose purpose is to use reducibility for typed terms in order to show the Church-Rosser of &lbeta;-developments for the untyped terms (and hence the Church- Rosser of β-reduction). In this second result, strong normalisation is not needed. We extend the second result to encompass both βI- and βη-reduction rather than simply β-reduction.

3

On Realisability Semantics for Intersection Types with Expansion Variables

Kamareddine F., Nour K., Rahli V., Wells J. B.

Fundamenta Informaticae

|

2012

|

Vol. 121, nr 1/4

153-184

EN

Expansion is a crucial operation for calculating principal typings in intersection type systems. Because the early definitions of expansion were complicated, E-variables were introduced in order to make the calculations easier to mechanise and reason about. Recently, E-variables have been further simplified and generalised to also allow calculating other type operators than just intersection. There has been much work on semantics for type systems with intersection types, but none whatsoever before our work, on type systems with E-variables. In this paper we expose the challenges of building a semantics for E-variables and we provide a novel solution. Because it is unclear how to devise a space of meanings for E-variables, we develop instead a space of meanings for types that is hierarchical. First, we index each type with a natural number and show that although this intuitively captures the use of E-variables, it is difficult to index the universal type ωwith this hierarchy and it is not possible to obtain completeness of the semantics if more than one E-variable is used. We then move to a more complex semantics where each type is associated with a list of natural numbers and establish that both ů and an arbitrary number of E-variables can be represented without losing any of the desirable properties of a realisability semantics.