λν is an extension of the λ-calculus which internalises the calculus of substitutions. In the current paper, we investigate the combinatorial properties of λν focusing on the quantitative aspects of substitution resolution. We exhibit an unexpected correspondence between the counting sequence for λν-terms and famous Catalan numbers. As a by-product, we establish effective sampling schemes for random λν-terms. We show that typical λν-terms represent, in a strong sense, non-strict computations in the classic X-calculus. Moreover, typically almost all substitutions are in fact suspended, i.e. unevaluated, under closures. Consequently, we argue that λν is an intrinsically non-strict calculus of explicit substitutions. Finally, we investigate the distribution of various redexes governing the substitution resolution in λν and investigate the quantitative contribution of various substitution primitives.

Affine λ-terms are λ-terms in which each bound variable occurs at most once, and linear λ-terms are λ-terms in which each bound variable occurs once and only once. In this article, we count the number of affine closed λ-terms of size n , linear closed λ-terms of size n , affine closed β-normal forms of size n , and linear closed β-normal forms of size n , for several measures of the size of λ-terms. From these formulas, we show how we can derive programs for generating all the terms of size n for each class. The foundation of all of this is a specific data structure, made of contexts in which one counts all the holes at each level of abstractions by λ’s.

We consider combinatorial aspects of |$\lambda$|-terms in the model based on de Bruijn indices where each building constructor is of size one. Surprisingly, the counting sequence for |$\lambda$|-terms corresponds also to two families of binary trees, namely black-white trees and zigzag-free ones. We provide a constructive proof of this fact by exhibiting appropriate bijections. Moreover, we identify the sequence of Motzkin numbers with the counting sequence for neutral |$\lambda$|-terms, giving a bijection which, in consequence, results in an exact-size sampler for the latter based on the exact-size sampler for Motzkin trees of Bodini et alli. Using the powerful theory of analytic combinatorics, we state several results concerning the asymptotic growth rate of |$\lambda$|-terms in neutral, normal, and head normal forms. Finally, we investigate the asymptotic density of |$\lambda$|-terms containing arbitrary fixed subterms showing that, inter alia, strongly normalising or typeable terms are asymptotically negligible in the set of all |$\lambda$|-terms.

Abstract In a paper, entitled Binary lambda calculus and combinatory logic , John Tromp presents a simple way of encoding lambda calculus terms as binary sequences. In what follows, we study the numbers of binary strings of a given size that represent lambda terms and derive results from their generating functions, especially that the number of terms of size n grows roughly like 1.963447954. . . n . In a second part we use this approach to generate random lambda terms using Boltzmann samplers.

Abstract Lambda calculus is the basis of functional programming and higher order proof assistants. However, little is known about combinatorial properties of lambda terms, in particular, about their asymptotic distribution and random generation. This paper tries to answer questions like: How many terms of a given size are there? What is a ‘typical’ structure of a simply typable term? Despite their ostensible simplicity, these questions still remain unanswered, whereas solutions to such problems are essential for testing compilers and optimizing programs whose expected efficiency depends on the size of terms. Our approach toward the aforementioned problems may be later extended to any language with bound variables, i.e., with scopes and declarations. This paper presents two complementary approaches: one, theoretical, uses complex analysis and generating functions, the other, experimental, is based on a generator of lambda terms. Thanks to de Bruijn indices (de Bruijn, N. (1972) Lambda calculus notation with nameless dummies, a tool for automatic formula manipulation, with application to the Church-Rosser theorem. Indagat. Math. 34 (5), 381–392), we provide three families of formulas for the number of closed lambda terms of a given size and we give four relations between these numbers which have interesting combinatorial interpretations. As a by-product of the counting formulas, we design an algorithm for generating λ-terms. Performed tests provide us with experimental data, like the average depth of bound variables and the average number of head lambdas. We also create random generators for various sorts of terms. Thereafter, we conduct experiments that answer questions like: What is the ratio of simply typable terms among all terms? ( Very small! ) How are simply typable lambda terms distributed among all lambda terms? ( A typable term almost always starts with an abstraction .) In this paper, abstractions and applications have size 1 and variables have size 0.

$\X$ is an untyped continuation-style formal language with a typed subset that provides a Curry–Howard isomorphism for a sequent calculus for implicative classical logic. $\X$ can also be viewed as a language for describing nets by composition of basic components connected by wires. These features make ${\X}$ an expressive platform on which many different (applicative) programming paradigms can be mapped. In this paper we will present the syntax and reduction rules for $\X$ ; in order to demonstrate its expressive power, we will show how elaborate calculi can be embedded, such as the λ-calculus, Bloo and Rose's calculus of explicit substitutions λx, Parigot's λμ and Curien and Herbelin's $\lmmt$ . ${\X}$ was first presented in Lengrand (2003), where it was called the λξ-calculus. It can be seen as the pure untyped computational content of the reduction system for the implicative classical sequent calculus of Urban (2000).

We present a formalism called addressed term rewriting systems, which can be used to model implementations of theorem proving, symbolic computation and programming languages, especially aspects of sharing, recursive computations and cyclic data structures. Addressed Term Rewriting Systems are therefore well suited to describing object-based languages, and as an example we present a language called and prove a type soundness result.

We investigate some fundamental properties of the reduction relation in the untyped term calculus derived from Curien and Herbelin's λμμ. The original λμμ has a system of simple types, based on sequent calculus, embodying a Curry-Howard correspondence with classical logic; the significance of the untyped calculus of raw terms is that it is a Turing-complete language for computation with explicit representation of control as well as code. We define a type assignment system for the raw terms satisfying: a term is typable if and only if it is strongly normalizing. The intrinsic symmetry in the λμμ calculus leads to an essential use of both intersection and union types; in contrast to other union-types systems in the literature, our system enjoys the Subject Reduction property.

This paper is part of a general programme of treating explicit substitutions as the primary λ-calculi from the point of view of foundations as well as applications. We work in a composition-free calculus of explicit substitutions and an augmented calculus obtained by adding explicit garbage-collection, and explore the relationship between intersection-types and reduction. We show that the terms that normalise by leftmost reduction and the terms that normalise by head reduction can each be characterised as the terms typable in a certain system. The relationship between typability and strong normalisation is subtly different from the classical case: we show that typable terms are strongly normalising but give a counterexample to the converse. Our notions of leftmost and head reduction are non-deterministic, and our normalisation theorems apply to any computations obeying these strategies. In this way we refine and strengthen the classical normalisation theorems. The proofs require some new techniques in the presence of reductions involving explicit substitutions. Indeed, our proofs do not rely on results from classical λ-calculus, which in our view is subordinate to the calculus of explicit substitution.

Abstract Explicit substitutions were proposed by Abadi, Cardelli, Curien, Hardin and Lévy to internalise substitutions into λ-calculus and to propose a mechanism for computing on substitutions. λν is another view of the same concept which aims to explain the process of substitution and to decompose it in small steps. It favours simplicity and preservation of strong normalisation. This way, another important property is missed, namely confluence on open terms. In spirit, λν is closely related to another calculus of explicit substitutions proposed by de Bruijn and called C λξΦ. In this paper, we introduce λν, we present C λξΦ in the same framework as λν and we compare both calculi. Moreover, we prove properties of λν; namely λν correctly implements β reduction, λν is confluent on closed terms, i.e. on terms of classical λ-calculus and on all terms that are derived from those terms, and finally λν preserves strong normalisation in the following sense: strongly β normalising terms are strongly λν normalising.

Abstract We focus on termination proofs of rewrite systems, especially of rewrite systems containing associative and commutative operators. We prove their termination by elementary interpretations, more specifically, by functions defined by addition, multiplication and exponentiation. We discuss a method based on polynomial interpretations and propose an implementation of a mechanisation of the comparison of expressions built with polynomials and exponentials.

This paper gives a systematic description of several calculi of explicit substitutions. These systems are orthogonal and have easy proofs of termination of their substitution calculus. The last system, called λv, entails a very simple environment machine for strong normalization of λ-terms.

A study is made of well (quasi) orderings which are described as rewrite orderings, and a family of well (quasi) orderings that extends the embedding or divisibility order of G. Higman (1952) is presented. For instance, the well (quasi) orderings proposed by the author may contain pairs of the form f(f(x))>f(g(f(x))). Conditions under which the transitive closures of a well-founded relation is a well-quasi-ordering are given. Finally, an attempt to extend the recursive path ordering is proposed.>

A term rewriting system generator called REVE is described. REVE builds confluent and uniformly terminating term rewriting systems from sets of equations. Particular emphasis is placed on mechanization of termination proof. Indeed, REVE is one of the few such systems which can actually be called automatic because termination is fully integrated into the algorithms. REVE uses an incremental termination method based on recursive decomposition ordering which constructs the termination proof step by step from the presentation of the set of equations and which requires little knowledge of termination methods from the user. All examples from this paper are taken from abstract data type specifications.

In this note we want to present the concept of behavioural categoricity of an abstract data type specification. Intuitively, a specification is behaviourally categoric if it captures the external views the user can have on the data type. More specifically, using this specification, it is possible to prove that two objects are equal if and only if they behave the same, or informally speaking, if and only if they implement the same black box. Providing a general algorithm for proving the behavioural categoricity of any specification is impossible because that algorithm could also decide whether a finite presentation of a group presents the trivial group or not, which Rabin proved to be undecidable. We show by an example of a specification of circular lists that the proof of the categoricity must be done carefully.