Confluence of Curried Term-Rewriting Systems

Term rewriting systems operate on first-order terms. Presenting such terms in curried form is usually regarded as a trivial change of notation. However, in the absence of a type-discipline, or in the presence of a more powerful type-discipline than simply typed λ-calculus, the change is not as trivial as one might first think.It is shown that currying preserves confluence of arbitrary term rewriting systems. The structure of the proof is similar to Toyama's proof that confluence is a modular property of TRS.     

De Bruijn''s syntax and reductional behaviour of λ-terms: the typed case

In this paper, we consider the typed versions of the λ-calculus written in a notation which helps describe canonical forms more elegantly than the classical notation, and enables to divide terms into classes according to their reductional behaviour. In this notation, β-reduction can be generalised from a relation on terms to one on equivalence classes. This class reduction covers many known notions of generalised reduction. We extend the Barendregt cube with our class reduction and show that the subject reduction property fails but that this is not unique to our class reduction. We show that other generalisations of reduction (such as the σ-reduction of Regnier) also behave badly in typed versions of the λ-calculus. Nevertheless, solution is at hand for these generalised reductions by adopting the useful addition of definitions in the contexts of type derivations. We show that adding such definitions enables the extensions of type systems with class reduction and σ-reduction to satisfy all the desirable properties of type systems, including subject reduction and strong normalisation. Our proposed typing relation ^c is the most general relation in the literature that satisfies all the desirable properties of type systems. We show that classes contain all the desirable information related to a term with respect to typing, strong normalisation, subject reduction, etc.     

A semantic characterization of the well-typed formulae of λ-calculus

A model-theoretic operation is characterized that preserves the property of being a model of typed λ-calculus (i.e., the result of applying it to a model of typed λ-calculus is another model of typed λ-calculus). An expression is well-typed iff the class of its models is closed under this operation.     

Reducibility: A ubiquitous method in lambda calculus with intersection types

A general reducibility method is developed for proving reduction properties of lambda terms typeable in intersection type systems with and without the universal type Ω. Sufficient conditions for its application are derived. This method leads to uniform proofs of confluence, standardization, and weak head normalization of terms typeable in the system with the type Ω. The method extends Tait's reducibility method for the proof of strong normalization of the simply typed lambda calculus, Krivine's extension of the same method for the strong normalization of intersection type system without Ω, and Statman-Mitchell's logical relation method for the proof of confluence of βη-reduction on the simply typed lambda terms. As a consequence, the confluence and the standardization of all (untyped) lambda terms is obtained.     

Strong normalisation in the π-calculus

We introduce a typed π-calculus where strong normalisation is ensured by typability. Strong normalisation is a useful property in many computational contexts, including distributed systems. In spite of its simplicity, our type discipline captures a wide class of converging name-passing interactive behaviour. The proof of strong normalisability combines methods from typed λ-calculi and linear logic with process-theoretic reasoning. It is adaptable to systems involving state, non-determinism, polymorphism, control and other extensions. Strong normalisation is shown to have significant consequences, including finite axiomatisation of weak bisimilarity, a fully abstract embedding of the simply typed λ-calculus with products and sums and basic liveness in interaction. Strong normalisability has been extensively studied as a fundamental property in functional calculi, term rewriting and logical systems. This work is one of the first steps to extend theories and proof methods for strong normalisability to the context of name-passing processes.     

A direct proof of the confluence of combinatory strong reduction

I give a proof of the confluence of combinatory strong reduction that does not use the one of λ$\lambda$-calculus. I also give simple and direct proofs of a standardization theorem for this reduction and the strong normalization of simply typed terms.     

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.     

The Mechanisation of Barendregt-Style Equational Proofs (the Residual Perspective)

We show how to mechanise equational proofs about higher-order languages by using the primitive proof principles of first-order abstract syntax over one-sorted variable names. We illustrate the method here by proving (in Isabelle/HOL) a technical property which makes the method widely applicable for the λ-calculus: the residual theory of β is renaming-free up-to an initiality condition akin to the so-called Barendregt Variable Convention. We use our results to give a new diagram-based proof of the development part of the strong finite development property for the λ-calculus. The proof has the same equational implications (e.g., confluence) as the proof of the full property but without the need to prove SN. We account for two other uses of the proof method, as presented elsewhere. One has been mechanised in full in Isabelle/HOL.     

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).     

Remarks on Isomorphisms of Simple Inductive Types

We study isomorphisms of types in the system of simply-typed λ-calculus with inductive types and recursion operators. It is shown that in some cases (multiproducts, copies of types), it is possible to add new reductions in such a way that strong normalisation and confluence of the calculus are preserved, and the isomorphisms may be regarded as intensional w.r.t. a stronger equality relation.     

Equational programming in λ-calculus via SL-systems. Part 1

A system of equations in the λ-calculus is a set of formulas of Λ (the equations) together with a finite set of variables of Λ (the unknowns). A system s is said to be β-solvable (βη-solvable) iff there exists a simultaneous substitution with closed λ-terms for the unknowns that makes the equations of s theorems in the theory β (βη). A system s can be viewed as a set of specifications (the equations) for a finite set of programs (the unknowns) whereas a solution for s yields executable codes for such programs.

A class of systems for which the solvability problem is effectively decidable defines an equational programming language and a system solving algorithm for defines a compiler for such language.

This leads us to consider separation-like systems (SL-systems), i.e. systems with equations having form , where x is an unknown and z is a free variable which is not an unknown.

We show that the β (βη)-solvability problem for SL-systems is undecidable.

On the other hand we are able to define a class of SL-systems (regular SL-systems) for which the β-solvability problem is decidable in Polynomial Time. Such class yields an equational programming language in which self-application is handled, constraints on executable code to be generated by the compiler can be specified by the user and (properties of) data structures can be described in an abstract way.     

Eliminating Proofs from Programs

This paper presents a step in the development of an operational approach to program extraction in type theory. In order to get a program from a lambda term, the logical parts need to be removed. This is done by a reduction relation →_ε. We study the combination of β-reduction and ε-reduction, both in the setting of simply typed lambda calculus and for pure type systems. In the general setting the properties confluence, subject reduction, and strong normalization are studied.     

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.     

Strong Normalization with Singleton Types

This paper presents a new lambda-calculus with singleton types, called λ_≤{}^βδ. The main novelty of λ_≤{}^βδ is the introduction of a new reduction, the δ-reduction, replacing any variable declared of singleton type by its value, and the definition of equality as the syntactic equality of βδ-normal forms. The δ-reduction has a very odd behavior on untyped terms, which renders its metatheoretical study difficult since the usual proof method for subject-reduction and Church-Rosser property are inapplicable. Nevertheless, these properties can be proved simultaneously with strong normalization on typed terms using a proof method à la Coquand-Gallier, borrowing ideas to Goguen. In spite of its complex metatheory, our calculus enjoys a simple, sound and complete type-inference algorithm.     

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.     

A formalised first-order confluence proof for the λ-calculus using one-sorted variable names

We present the titular proof development that has been verified in Isabelle/HOL. As a first, the proof is conducted exclusively by the primitive proof principles of the standard syntax and of the considered reduction relations: the naive way, so to speak. Curiously, the Barendregt Variable Convention takes on a central technical role in the proof. We also show: (i) that our presentation of the λ-calculus coincides with Curry’s and Hindley’s when terms are considered equal up to α-equivalence and (ii) that the confluence properties of all considered systems are equivalent.     

Constructive logics Part I: A tutorial on proof systems and typed λ-calculi

The purpose of this paper is to give an exposition of material dealing with constructive logics, typed λ-calculi, and linear logic. The emergence in the past ten years of a coherent field of research often named “logic and computation” has had two major (and related) effects: firstly, it has rocked vigorously the world of mathematical logic; secondly, it has created a new computer science discipline, which spans a range of subjects from what is traditionally called the theory of computation, to programming language design. Remarkably, this new body of work relies heavily on some “old” concepts found in mathematical logic, like natural deduction, sequent calculus, and λ-calculus (but often viewed in a different light), and also on some newer concepts. Thus, it may be quite a challenge to become initiated to this new body of work (but the situation is improving, and there are now some excellent texts on this subject matter). This paper attempts to provide a coherent and hopefully “gentle” initiation to this new body of work. We have attempted to cover the basic material on natural deduction, sequent calculus, and typed λ-calculus, but also to provide an introduction to Girard's linear logic, one of the most exciting developments in logic these past six years. The first part of these notes gives an exposition of the background material (with some exceptions, such as “contraction-free” systems for intuitionistic propositional logic and the Girard translation of classical logic into intuitionistic logic, which is new). The second part is devoted to more current topics such as linear logic, proof nets, the geometry of interaction, and unified systems of logic (LU).     

Equational programming in λ-calculus via SL-systems. Part 2

A system of equations in the λ-calculus is a set of formulas of Λ (the equations) together with a finite set of variables of Λ (the unknowns). A system s is said to be β-solvable (βη-solvable) iff there exists a simultaneous substitution with closed λ-terms for the unknowns that makes the equations of s theorems in the theory β (βη). A system s can be viewed as a set of specifications (the equations) for a finite set of programs (the unknowns) whereas a solution for s yields executable codes for such programs.

A class of systems for which the solvability problem is effectively decidable defines an equational programming language and a system solving algorithm for defines a compiler for such language.

This leads us to consider separation-like systems (SL-systems), i.e. systems with equations having form , wherex is an unknown and z is a free variable which is not an unknown.

It is known that the β (βη)-solvability problem for SL-systems is undecidable.

Here we show that there is a class of SL-systems (NP-regular SL-systems) for which the β-solvability problem is NP-complete. Moreover, we show that any SL-system s can be transformed into an NP-regular SL-system s. This transformation consists of adding abstractions to the LHS occurrences of the RHS variables of s. In this sense NP-regular SL-systems isolate the source of undecidability for SL-systems, namely: a shortage of abstractions on the LHS occurrences of the RHS variables.

NP-regular SL-systems yield an equational programming language in which unrestrained self-application is handled, constraints on executable code to be generated by the compiler can be specified by the user and (properties of) data structures can be described in an abstract way. However, existence of executable code satisfying a specification in such language is an NP-complete problem. This is the price we have to pay for allowing unrestrained self-application in our language.     

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).