Intersection Typed λ-calculus

The aim of this paper is to discuss the design of an explicitly typed λ-calculus corresponding to the Intersection Type Assignment System (IT) which assigns intersection types to the untyped λ-calculus. Two different proposals are given. The logical foundation of all of them is the Intersection Logic IL.     

Intersection and Union Types: Syntax and Semantics

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.     

Filter models for conjunctive-disjunctive λ-calculi

The distinction between the conjunctive nature of non-determinism as opposed to the disjunctive character of parallelism constitutes the motivation and the starting point of the present work. λ-calculus is extended with both a non-deterministic choice and a parallel operator; a notion of reduction is introduced, extending β-reduction of the classical calculus. We study type assignment systems for this calculus, together with a denotational semantics which is initially defined constructing a set semimodel via simple types. We enrich the type system with intersection and union types, dually reflecting the disjunctive and conjunctive behaviour of the operators, and we build a filter model. The theory of this model is compared both with a Morris-style operational semantics and with a semantics based on a notion of capabilities.     

Subtyping in Logical Form

By using intersection types and filter models we formulate a theory of types for a λ-calculus with record subtyping via a finitary programming logic. Types are interpreted as spaces of filters over a subset of the language of properties (the intersection types) which describes the underlying type free realizability structure. We show that such an interpretation is a PER semantics, proving that the quotient space arising from “logical” PERs taken with the intrinsic ordering is isomorphic to the filter semantics of types.     

Database Query Languages Embedded in the Typed Lambda Calculus

We investigate the expressive power of the typedλ-calculus when expressing computations over finite structures, i.e., databases. We show that the simply typedλ-calculus can express various database query languages such as the relational algebra, fixpoint logic, and the complex object algebra. In our embeddings, inputs and outputs areλ-terms encoding databases, and a program expressing a query is aλ-term which types when applied to an input and reduces to an output. Our embeddings have the additional property that PTIME computable queries are expressible by programs that, when applied to an input, reduce to an output in a PTIME sequence of reduction steps. Under our database input-output conventions, all elementary queries are expressible in the typedλ-calculus and the PTIME queries are expressible in the order-5 (order-4) fragment of the typedλ-calculus (with equality).     

Term Collections in λ and ρ-calculi

The ρ-calculus generalises term rewriting and the λ-calculus by defining abstractions on arbitrary patterns and by using a pattern-matching algorithm which is a parameter of the calculus. In particular, equational theories that do not have unique principal solutions may be used. In the latter case, all the principal solutions of a matching problem are stored in a “structure” that can also be seen as a collection of terms.Motivated by the fact that there are various approaches to the definition of structures in the ρ-calculus, we study in this paper a version of the λ-calculus with term collections.The contributions of this work include a new syntax and operational semantics for a λ-calculus with term collections, which is related to the λ-calculi with strict parallel functions studied by Boudol and Dezani et al. and a proof of the confluence of the β-reduction relation defined for the calculus (which is a suitable extension of the standard rule of β-reduction in the λ-calculus).     

Perpetual Reductions inλ-Calculus

This paper surveys a part of the theory ofβ-reduction inλ-calculus which might aptly be calledperpetual reductions. The theory is concerned withperpetual reduction strategies, i.e., reduction strategies that compute infinite reduction paths fromλ-terms (when possible), and withperpetual redexes, i.e., redexes whose contraction inλ-terms preserves the possibility (when present) of infinite reduction paths. The survey not only recasts classical theorems in a unified setting, but also offers new results, proofs, and techniques, as well as a number of applications to problems inλ-calculus and type theory.     

Interaction Nets vs. the ρ-calculus: Introducing Bigraphical Nets

The ρ-calculus generalises both term rewriting and the λ-calculus in a uniform framework. Interaction nets are a form of graph rewriting which proved most successful in understanding the dynamics of the λ-calculus, the prime example being the implementation of optimal β-reduction. It is thus natural to study interaction net encodings of the ρ-calculus as a first step towards the definition of efficient reduction strategies. We give two interaction net encodings which bring a new understanding to the operational semantics of the ρ-calculus; however, these encodings have some drawbacks and to overcome them we introduce bigraphical nets—a new paradigm of computation inspired by Lafont's interactions nets and Milner's bigraphs.     

On the representation of McCarthy's in the -calculus

We study the encoding of , the call-by-name λ-calculus enriched with McCarthy's amb operator, into the π-calculus. Semantically, amb is a challenging operator, for the fairness constraints that it expresses. We prove that, under a certain interpretation of divergence in the λ-calculus (weak divergence), a faithful encoding is impossible. However, with a different interpretation of divergence (strong divergence), the encoding is possible, and for this case we derive results and coinductive proof methods to reason about that are similar to those for the encoding of pure λ-calculi. We then use these methods to derive the most important laws concerning amb. We take bisimilarity as behavioural equivalence on the π-calculus, which sheds some light on the relationship between fairness and bisimilarity.     

Simple Easy Terms

We illustrate the use of intersection types as a semantic tool for proving easiness result on λ-terms. We single out the notion of simple easiness for λ-terms as a useful semantic property for building filter models with special purpose features. Relying on the notion of easy intersection type theory, given λ-terms M and E, with E simple easy, we successfully build a filter model which equates interpretation of M and E, hence proving that simple easiness implies easiness. We finally prove that a class of λ-terms generated by ω₂ω₂ are simple easy, so providing alternative proof of easiness for them.     

Revisiting the notion of function

Functions play a central role in type theory, logic and computation. We describe how the notions of functionalisation (the way in which functions can be constructed) and instantiation (the process of applying a function to an argument) have been developed in the last century. We explain how both processes were implemented in Frege’s Begriffschrift, Russell’s Ramified Type Theory, and the λ-calculus (originally introduced by Church) showing that the λ-calculus misses a crucial aspect of functionalisation. We then pay attention to some special forms of function abstraction that do not exist in the λ-calculus and we show that various logical constructs (e.g., let expressions and definitions and the use of parameters in mathematics), can be seen as forms of the missing part of functionalisation. Our study of the function concept leads to: (a) an extension of the Barendregt cube [4] with all of definitions, Π-reduction and explicit substitutions giving all their advantages in one system; and (b) a natural refinement of the cube with parameters. We show that in the refined Barendregt cube, systems like A , LF, and ML, can be described more naturally and accurately than in the original cube.     

Descendants and Origins in Term Rewriting

In this paper we treat various aspects of a notion that is central in term rewriting, namely that of descendants or residuals. We address both first-order term rewriting and λ-calculus, their finitary as well as their infinitary variants. A recurrent theme is the parallel moves lemma. Next to the classical notion of descendant, we introduce an extended version, known as origin tracking. Origin tracking has many applications. Here it is employed to give new proofs of three classical theorems: the genericity lemma in λ-calculus, the theorem of Huet and Lévy on needed reductions in first-order term rewriting, and Berry's sequentiality theorem in (infinitary) λ-calculus.     

Realizability Models for Type Theories

This tutorial aims at giving an account on the realizability models for several constructive type theories. These range from simply typed λ-calculus over second-order polymorphic λ-calculus to the Calculus of Constructions as an example of dependent type theory. The models are made from partial equivalence relations (pers) and realizability sets over an arbitrary partial combinatory algebra. Realizability semantics does not only provide intuitive models but can also be used for proving independence results of type theories. Finally, by considering complete extensional pers, an approach to bridge the gap from type theory to constructive domain theory is discussed.     

Call-by-name, call-by-value and the λ-calculus

This paper examines the old question of the relationship between ISWIM and the λ-calculus, using the distinction between call-by-value and call-by-name. It is held that the relationship should be mediated by a standardisation theorem. Since this leads to difficulties, a new λ-calculus is introduced whose standardisation theorem gives a good correspondence with ISWIM as given by the SECD machine, but without the letrec feature. Next a call-by-name variant of ISWIM is introduced which is in an analogous correspondence withthe usual λ-calculus. The relation between call-by-value and call-by-name is then studied by giving simulations of each language by the other and interpretations of each calculus in the other. These are obtained as another application of the continuation technique. Some emphasis is placed throughout on the notion of operational equality (or contextual equality). If terms can be proved equal in a calculus they are operationally equal in the corresponding language. Unfortunately, operational equality is not preserved by either of the simulations.     

A Symmetric Lambda Calculus for Classical Program Extraction

We introduce aλ-calculus with symmetric reduction rules and “classical” types, i.e., types corresponding to formulas of classical propositional logic. The strong normalization property is proved to hold for such a calculus, as well as for its extension to a system equivalent to Peano arithmetic. A theorem on the shape of terms in normal form is also proved, making it possible to get recursive functions out of proofs ofΠ⁰₂formulas, i.e., those corresponding to program specifications.     

Bounded Model Generation for Isabelle/HOL

A translation from higher-order logic (on top of the simply typed λ-calculus) to propositional logic is presented, such that the resulting propositional formula is satisfiable iff the HOL formula has a model of a given finite size. A standard SAT solver can then be used to search for a satisfying assignment, and such an assignment can be transformed back into a model for the HOL formula. The algorithm has been implemented in the interactive theorem prover Isabelle/HOL, where it is used to automatically generate countermodels for non-theorems.     

Token-Passing Nets: Call-by-Need for Free

Recently, encodings in interaction nets of the call-by-name and call-by-value strategies of the λ-calculus have been proposed. The purpose of these encodings was to bridge the gap between interaction nets and traditional abstract machines, which are both used to provide lower-level specifications of strategies of the λ-calculus, but in radically different ways. The strength of these encodings is their simplicity, which comes from the simple idea of introducing an explicit syntactic object to represent the flow of evaluation. In particular, no artifact to represent boxes is needed. However, these encodings purposefully follow as closely as possible the implemented strategies, call-by-name and call-by-value, hence do not benefit from the ability of interaction nets to easily represent sharing. The aim of this note is to show that sharing can indeed be achieved without adding any structure. We thus present the call-by-need strategy following the same philosophy, which is indeed not any more complicated than call-by-name. This continues the task of bridging the gap between interaction nets and abstract machines, thus pushing forward a more uniform framework for implementations of the λ-calculus.     

Normalization Results for Typeable Rewrite Systems

In this paper we introduce Curryfied term rewriting systems, and a notion of partial type assignment on terms and rewrite rules that uses intersection types with sorts andω. Three operations on types—substitution, expansion, and lifting—are used to define type assignment and are proved to be sound. With this result the system is proved closed for reduction. Using a more liberal approach to recursion, we define a general scheme for recursive definitions and prove that, for all systems that satisfy this scheme, every term typeable without using the type-constantωis strongly normalizable. We also show that, under certain restrictions, all typeable terms have a (weak) head-normal form, and that terms whose type does not containωare normalizable.