The Pure Pattern Calculus (PPC) extends the lambda-calculus, as well as the family of algebraic pattern calculi, with first-class patterns; that is, patterns can be passed as arguments, evaluated and returned as results. The notion of matching failure of the PPC not only provides a mechanism to define functions by pattern matching on cases but also supplies PPC with parallel-or-like, non-sequential behaviour. Therefore, devising normalising strategies for PPC to obtain well-behaved implementations turns out to be challenging. This paper focuses on normalising reduction strategies for PPC. We define a (multistep) strategy and show that it is normalising. The strategy generalises the leftmost-outermost strategy for lambda-calculus and is strictly finer than parallel-outermost. The normalisation proof is based on the notion of necessary set of redexes, a generalisation of the notion of needed redex encompassing non-sequential reduction systems.

Abstract We present an extension of the λ(η)-calculus with a case construct that propagates through functions like a head linear substitution, and show that this construction permits to recover the expressiveness of ML-style pattern matching. We then prove that this system enjoys the Church–Rosser property using a semi-automatic ‘divide and conquer’ technique by which we determine all the pairs of commuting subsystems of the formalism (considering all the possible combinations of the nine primitive reduction rules). Finally, we prove a separation theorem similar to Böhm's theorem for the whole formalism.

In this paper we encode higher-order rewriting with names into higher-order rewriting in de Bruijn notation. This notation not only is defined for terms (as usually done in the literature) but also for metaterms, which are the syntactical objects used to express the rewriting rules of higher-order systems. Several examples are discussed. Fundamental properties such as confluence and normalisation are shown to be preserved.

We define a formal encoding from higher-order rewriting into first-order rewriting modulo an equational theory ℰ. In particular, we obtain a characterization of the class of higher-order rewriting systems which can be encoded by first-order rewriting modulo an empty equational theory (that is, ℰ = ∅). This class includes of course the λ-calculus. Our technique does not rely on the use of a particular substitution calculus but on an axiomatic framework of explicit substitutions capturing the notion of substitution in an abstract way. The axiomatic framework specifies the properties to be verified by a substitution calculus used in the translation. Thus, our encoding can be viewed as a parametric translation from higher-order rewriting into first-order rewriting, in which the substitution calculus is the parameter of the translation.

Nowadays, type theory has many applications and is used in many different disciplines. Within computer science, logic and mathematics there are many different type systems. They serve several purposes and are formulated in various ways. A general framework called Pure Type Systems (PTSs) has been introduced independently by Terlouw and Berardi in order to provide a unified formalism in which many type systems can be represented. In particular, PTSs allow the representation of the simple theory of types, the polymophic theory of types, the dependent theory of types and various other well-known type systems such as the Edinburgh Logical Frameworks and the Automath system. PTSs are usually presented using variable names. In this article, we present a formulation of PTSs with de Bruijn indices. De Bruijn indices avoid the problems caused by variable names during the implementation of type systems. We show that PTSs with variable names and PTSs with de Bruijn indices are isomorphic. This isomorphism enables us to answer questions about PTSs with de Bruijn indices including confluence, termination (strong normalization) and safety (subject reduction).

The aim of this article is to compare two styles of Explicit Substitutions: the λσ- and λs-styles. We start by introducing a criterion of adequacy to simulate β-reduction in calculi of explicit substitutions and we apply it to several calculi: λσ, λσ⇑, λv, λs, λt, and λu. The latter is presented here for the first time and may be considered as an adequate variant of λs. By doing so, we establish that calculi à la λs are usually more adequate at simulating β-reduction than calculi in the λσ-style. In fact, we prove that λt is more adequate than λv and that λu is more adequate than λv, λσ⇑ and λs. We also give counterexamples to show that all other comparisons are impossible according to our criterion. Our next step consists in presenting the λω and λωe calculi, the two-sorted (term and substitution) versions of the λs and λse calculi, respectively. We establish an isomorphism between the λse and the term restriction of λωe. Since the λω and λωe calculi are given in the style of the λσ-calculus they are bridge calculi between λs and λσ and between λse and λσ and thus we are able to better understand one calculus in terms of the other. Finally, we present typed versions of all the calculi and check that the above mentioned isomorphism preserves types. As a consequence, the λω-calculus is a calculus in the λσ-style that has the following properties: (a) λω simulates one step β-reduction, (b) λω is confluent (on closed terms), λω preserves strong normalization, (d) λω's associated calculus of substitutions is SN, (e) the simply typed λω calculus is SN, (f) the λω-calculus possesses and extension λωe that is confluent on open terms (terms with eventual metavariables of sort term only), and (g) the simply typed λωe calculus is weakly normalizing (on open term). As far as we know, the λω-calculus is the first calculus in the λσ-style that has all the properties (a)-(g). However, the open problem of the SN of the associated calculus of substitution of λωe remains unsolved and like in the case of λσ, λv and λse, lgr;ωe does not have PSN.

The last 15 years have seen an explosion in work on explicit substitution, most of which is done in the style of the λσ-calculus. In Kamareddine and Ríos (1995a), we extended the λ-calculus with explicit substitutions by turning de Bruijn's meta-operators into object-operators offering a style of explicit substitution that differs from that of λσ. The resulting calculus, λ s , remains as close as possible to the λ-calculus from an intuitive point of view and, while preserving strong normalisation (Kamareddine and Ríos, 1995a), is extended in this paper to a confluent calculus on open terms: the λ s e -caculus. Since the establishment of these results, another calculus, λζ, came into being in Muñoz Hurtado (1996) which preserves strong normalisation and is itself confluent on open terms. However, we believe that λ s e still deserves attention because, while offering a new style to work with explicit substitutions, it is able to simulate one step of classical β-reduction, whereas λζ is not. To prove confluence we introduce a generalisation of the interpretation method (cf. Hardin, 1989; Curien et al ., 1992) to a technique which uses weak normal forms (instead of strong ones). We consider that this extended method is a useful tool to obtain confluence when strong normalisation of the subcalculus of substitutions is not available. In our case, strong normalisation of the corresponding subcalculus of substitutions s e , is still a challenging open problem to the rewrite community, but its weak normalisation is established here via an effective strategy.

ασ-calculus is an extended λ-calculus where substitutions are handled explicitly. It is similar to, and inspired by, Categorical Combinatory logic (CCL). The strong normalization of σ, the subcalculus which computes substitutions, may be inferred from the strong normalization of the similar subsystem SUBST of CCL. We present here an independent proof of the termination of several substitution calculi, including σ and SUBST.