Germain Faure
email: germain.faure@inria.fr

HIGHER-ORDER MATCHING MODULO (SUPER)DEVELOPMENTS APPLICATIONS TO SECOND-ORDER MATCHING

Keywords: F.4.1, F.3.1 Matching, λ-calculus, developments, superdevelopments, higher-order matching, second-order matching, patterns à la Miller, higher-order rewriting

To perform higher-order matching, we need to decide the βη-equivalence on λ-terms. The first way to do it is to use simply typed λ-calculus and this is the usual framework where higher-order matching is performed. Another approach consists in deciding a restricted equivalence. This restricted equivalence can be based on finite developments or more interestingly on finite superdevelopments. We consider higher-order matching modulo (super)developments over untyped λ-terms for which we propose terminating, sound and complete matching algorithms. This is in particular of interest since all second-order β-matches are matches modulo superdevelopments. We further propose a restriction to second-order matching that gives exactly all second-order matches. We finally apply these results in the context of higherorder rewriting.

Contents

1. Normalization in the lambda-calculus 3 2. Matching modulo beta (and eta) 9

3. Matching modulo superdevelopments (and eta) 11

4. Algorithm for matching modulo superdevelopments 15 5. Algorithm for matching modulo superdevelopments and eta 23 6. Algorithm for second-order matching 26 7. Algorithm for matching modulo developments (and eta) 31

8. Applications to higher-order rewriting 32

Introduction

Higher-order matching and unification are two operations fundamental in various fields such as higher-order logic programming [START_REF] Miller | Higher-order logic programming[END_REF] and logical frameworks [START_REF] Pfenning | Logical frameworks[END_REF], computational linguistics [START_REF] Dalrymple | Ellipsis and higher-order unification[END_REF], program transformation [HL78, Shi94, Vis05], higher-order rewriting [vOvR93, MN98, NP98], proof theory etc.

Higher-order matching and unification in the λ-calculus cannot be studied directly since this requires to decide the equality between two terms and the equality modulo β of terms of the λ-calculus is undecidable as it was shown by Church. Nevertheless, in practice we do not need the full power of the pure λ-calculus. For example, in the context of automated deduction we study unification in a typed setting (Curry-Howard-de Bruijn isomorphism).

Unification in this context is still undecidable [Hue75] but the terms written in practice often satisfy some properties that make unification decidable [Mil91] and even linear [Qia96].

The work presented in this paper is dealing with higher-order matching. Higher-order matching is usually defined as the following problem: given a set of equations s i = t i between typed λ-terms where the terms t i do not contain free variables, is there a substitution σ such that for all i s i σ is equal to t i modulo the usual β(η) relation. If we solve the equations modulo the βη relation, the problem is known to be decidable [START_REF] Stirling | Decidability of higher-order matching[END_REF]. But if we solve the equations modulo the β relation, it is undecidable [Loa03].

Even if higher-order matching is a particular case of unification, it requires dedicated works (see e.g. [START_REF] Huet | Proving and applying program transformations expressed with second-order patterns[END_REF]). But until now, most of the algorithms are specializations of the general unification algorithm introduced in [Hue75]. This makes them unnecessarily difficult to understand and to use in practice.

We propose a new approach to deal with higher-order matching. Instead of deciding the equality modulo the β-equivalence in the typed λ-calculus, we propose to decide the equality modulo a restriction of the β-equivalence in the pure λ-calculus. The standard restriction of the β-equivalence is given by finite developments [Bar84]. Unfortunately, this restriction is too rough for being useful in the context of higher-order matching. We will show that it is neither complete for tackling second-order matching problems nor matching of patterns à la Miller .

We thus consider the more general notion of superdevelopments [vR96, vR93]. A superdevelopment is a reduction sequence that may reduce the redexes of the term, its residuals (like in developments) and some created redexes but not those created by the substitution of a variable in functional position by a λ-abstraction.

In this work, we thus consider matching equations built over untyped λ-terms and solve them modulo superdevelopments. The matching problems are of interest particularly because the set of matches modulo superdevelopments contains, but is not restricted to, second-order β-matches.

We propose a sound complete and terminating algorithm for matching modulo superdevelopments. We show that we can decline this algorithm in several ways: to deal with matching modulo developments, to deal with second-order matching etc. We also show that whereas in a typed context the use of η-long normal form is fundamental, in the context of matching modulo superdevelopments the use of the η-equivalence does not impact our algorithms.

The paper also deals with higher-order rewriting [START_REF]Term Rewriting Systems[END_REF]. Higher-order rewriting is usually build on a given instance of the λ-calculus, called the substitution calculus [Oos94], for which matching is decidable. Typically, we consider simply typed λ-calculus modulo βη [MN98] or untyped λ-calculus modulo developments [START_REF] Willem | Combinatory Reduction Systems[END_REF][START_REF] Klop | Combinatory reduction systems: introduction and survey[END_REF]. Higherorder matching is used in the context of higher-order rewriting to decide whether a rewrite rule can be applied. Our contributions in this context are (1) to give an algorithm for matching modulo developments and (2) to show that the λ-calculus modulo superdevelopments is a very good substitution calculus.

Higher-order matching in an untyped setting was already been studied in [Sit01,dMS01] where matching equations are solved modulo a one-step reduction that generalizes the Tait and Martin-Löf parallel reduction. But this one-step reduction is, like the authors of the original paper said, difficult to understand. We show in this paper that it is nothing but a parallel reduction that corresponds [vR96, vR93] to superdevelopments.

The theory of superdevelopments plays a central role in the work presented here. It makes clear the comparison of higher-order match modulo superdevelopments and other approaches, it gives nice intuitions for the properties as well as their proofs. These proofs are per se simpler than the one given in the original paper [Sit01,dMS01]. This paper is structured as follows. Section 1 deals with normalization in the λ-calculus.

It sets the notations and presents the material used through the paper. In particular, it gives a detailed presentation of the notion of superdevelopments. Section 2 recalls the basic definitions for higher-order matching modulo β in the simply typed λ-calculus. Section 3 defines higher-order matching modulo superdevelopments and studies its expressiveness w.r.t. other approaches. Both sections consider the case of η. Section 4 presents an algorithm for matching modulo superdevelopments. We study its properties mainly termination, soundness and completeness. Section 5 presents an algorithm for matching modulo superdevelopments and η. We prove the minimality for Miller patterns. Section 6 and 7 present two declinations of the algorithm for matching modulo superdevelopments: one for second-order matching and one for matching modulo developments. Finally Section 8 applies the results in the context of higher-order rewriting.

An abstract of this work was presented in [Fau06]. The thesis of the author [Fau07] also contains part of the work presented here.

Normalization in the lambda-calculus

In this section, we first recall some basic definitions and set some notations related to the λ-calculus. We refer the reader to [Bar84, Dow01] for the fundamental definitions and results on the λ-calculus.

We then define developments, resp. superdevelopments, in two different ways: using the underlined, resp. the labelled, λ-calculus and using appropriate parallel reductions. This section is freely inspired by the second chapter of [vR96].

1.1. Typed λ-calculus and β-reduction. Given a set of base types T 0 , we define the set of types T inductively as the smallest set containing T 0 and such that if α and β ∈ T then

(α → β) ∈ T. The order of a type α denoted o(α) is equal to 1, if α ∈ T 0 . The order of a type α → β is equal to max(o(α) + 1, o(β)).
Definition 1.1 (Typed λ-terms). Let K be a set of constants, having a unique type. For each type α ∈ T, we assume given two countably infinite sets of variables of that type, denoted X α and V α . Let X = ∪ α∈T X α be the set of variables and let V = ∪ α∈T V α be the set of matching variables. The set T t of typed λ-terms is inductively defined as the smallest set containing all variables, all matching variables and all constants, and closed under the following rules:

• If A, B ∈ T t with type resp. α → β and α then (A B) ∈ T t with type β.

• If A ∈ T t with type β, and x ∈ X α then λx. A ∈ T t with type α → β.

There are two different sets of "variables": the variables belonging to X on which we abstract and the matching variables belonging to V.

The symbols A, B, C, . . . range over the set T t of terms, the symbols x, y, z, . . . range over the set X of variables (X ⊆ T t ), the symbols a, b, c, . . . , f, g, h range over a set K of term constants (K ⊆ T t ). The symbols X, Y, . . . range over the set V of matching variables.

Finally, the symbol ε ranges over the set of atoms, which consists of variables, matching variables and constants. To increase the readability, we often write ε(A 1 , A 2 , . . . , A n ) for (. . . ((ε A 1 ) A 2 ) . . .) A n ) where ε is an atom and A 1 , . . . , A n are arbitrary terms. All symbols can be indexed. Positions in λ-terms are denoted by p 1 , ..., p n . We denote by the order on positions (prefix order). The subterm of A at position p 1 is denoted by A |p 1 .

Given the term A 1 A 2 , by definition the term A 2 is said to be in applicative position while the term A 1 is said to be in functional position.

The order of a constant or a matching variable is defined as the order of its type. The order of a redex (λx. A) B is defined as the order of the abstraction λx. A. We consider the usual notion of free and bound variables that concerns the variables (matching variables cannot be bound). A term is said to be V-closed if it contains no matching variables and it is X -closed if it contains no free variables. We denote by fv(A) the free variables of A.

The substitution of variables is defined as usual and avoids variable capture using αconversion when needed. The substitution of the variable x by A in B is denoted by

B[x := A].
As in any calculus involving some binders, we work modulo the α-conversion of Church, and modulo the hygiene-convention of Barendregt, i.e., free and bound variables have different names.

It may be helpful for the reader familiar with the Combinatory Reduction Systems (CRS) terminology [START_REF] Willem | Combinatory Reduction Systems[END_REF][START_REF] Klop | Combinatory reduction systems: introduction and survey[END_REF] to note (1) that our matching variables are nothing but the meta-variables of CRS, (2) that terms containing matching variables are nothing but meta-terms of CRS and (3) that V-closed terms are nothing but the terms of CRS. In the same way, substitutions of matching variables defined below correspond to assignments of CRS.

The relation β is defined over the set T t of typed λ-terms by

(λx. A)B → β A[x := B]
and we denote by → → β its reflexive and transitive closure and by = β its reflexive, symmetric and transitive closure. A λ-term is said to be β-normal or simply normal if it is in normal form for the β-rule. We recall that the β-reduction over typed λ-terms is confluent and strongly normalising.

A substitution of matching variables is a function from matching variables to the set of V-closed terms. It is denoted B{A/X}. We use the standard definitions for domain, codomain, union and composition of substitutions. When it is clear from the context, substitutions of matching variables are simply called substitutions. Substitutions can be compare using the usual subsumption order : for two substitutions ψ and ϕ, we say that ψ ≤ ϕ when there exists a substitution ξ such that ϕ = ξ • ψ where • denotes substitution composition. In this work, we only consider closed and normal substitutions that are substitutions of closed and normal terms.

1.2. Untyped λ-calculus and developments. We define developments as a subset of the β-reduction which reduces only the redexes initially present in the term as well as its residuals. This is formalized by defining the underlined λ-calculus : we initially underline all the redexes present in the term and we replace the β-reduction by the β u -reduction which only reduces underlined redexes. Then, the redexes created during reduction are no longer reduced (since they are not underlined).

1.2.1. Untyped underlined λ-calculus and β u -reduction. We define the set of underlined terms. In case they do not use any type information, we use without ambiguity the definitions and notations given for typed λ-terms in the previous section.

Definition 1.2 (Underlined λ-terms). Let K be a set of constants. Let X and V be two countably infinite and disjoint sets respectively for variables and matching variables. The set T u of underlined λ-terms is defined as the smallest set containing all variables, matching variables, constants and closed under the following rules:

• If A and B are elements of the set T u then (AB) is an element of T u ;

• If A is an element of T u and x is a variable of X , then λx. A is an element of T u ;

• If A and B are elements of T u then (λx.A)B belong to T u .

Note that the set of underlined terms is not closed by subterm: for example λx.A is not an element of T u .

The relation β u is defined over the set T u of underlined terms by

(λx.A)B → βu A[x := B]
The β u -reduction is consuming at each step an underlined redex, it can duplicate but cannot create new ones. This relation is thus strongly normalising. Moreover, the relation is confluent. These results are known as the finite developments theorem (see below).

1.2.2. Untyped λ-calculus and developments. The set of terms in the pure λ-calculus is defined in the same way of typed λ-terms except that we do take care of type constraints.

It is denoted by T . We can define a mapping Υ from underlined terms to terms that replaces β-redexes by their corresponding β-redexes 1 . This mapping can be extended to any sequence of β u -reductions. We can then define developments. • Every development is finite.

• If two developments ζ 1 and ζ 2 start with the same initial term then the two final terms must be equal.

We now introduce a big-step semantics [START_REF] Despeyroux | Natural semantics: specifications and proofs[END_REF] of developments. This definition is due to Tait and Martin-Löf and can be given for every left linear higher-order rewrite systems [START_REF]Term Rewriting Systems[END_REF].

1 The formal definition will be given in the more general case of superdevelopments.

Definition 1.5 (Parallel reduction). The parallel reduction in the λ-calculus is inductively defined by

ε =⇒ β ε (Red -ε) A 1 =⇒ β A 2 λx. A 1 =⇒ β λx. A 2 (Red -λ) A 1 =⇒ β A 2 B 1 =⇒ β B 2 A 1 B 1 =⇒ β A 2 B 2 (Red -@) λx. A 1 =⇒ β λx. A 2 B 1 =⇒ β B 2 (λx. A 1 )B 1 =⇒ β A 2 [x := B 2 ] (Red -β)
Theorem 1.6 (Parallel reduction and developments). The notions of parallel reduction and developments coincide in the following sense. For every terms A, B ∈ T

there exists a development A → → β B iff A =⇒ β B
This characterization of developments is the essence of the corresponding matching algorithm.

1.3. Untyped λ-calculus and superdevelopments. We have seen in the previous section that developments reduce the redexes initially present in the term and its residuals.

This gives a first approximation of the β-normal form. Unfortunately, this approximation is too rough for being useful in the context of higher-order matching as we will see in Section 3.5.

We then introduce a generalization of developments called superdevelopments. A superdevelopment [vR93] is a reduction sequence that may reduce the redexes of the term, its residuals and some created redexes. The redexes created by the substitution of a variable in functional position by a λ-abstraction are not reduced.

The notion of superdevelopments is related to the three ways redexes are created in the λ-calculus. This taxonomy was proposed in [START_REF] Lévy | Reductions Correctes et Optimales dans le Lambda-Calcul[END_REF].

(type 1)

((λx. (λy. A))B)C → β (λy. A[x := B])C (type 2) ((λx. x)(λy. A))B → β (λy. A)B (type 3) (λx. A)(λy. B) → β A[x := (λy. B)]
if ∃p such that A| p = xA 0 For the first two ways of creating a β-redex, one can say that the creation is "upwards", whereas in the last case it can be said to be "downwards".

Note that in the first and second ways, the redex is created by the reduction of a term in functional position whereas in the third way the redex is created by the substitution for a variable in functional position of a λ-abstraction. This gives the intuition for the equivalence between superdevelopments and the strong parallel reduction defined below. Definition 1.7 (Labelled λ-terms). Let K be a set of constants. Let X and V be two countably infinite and disjoint sets respectively for variables and matching variables. The set T l of labelled λ-terms is defined as the smallest set containing all variables, matching variables, constants and closed under the following rules:

• If A ∈ T l and p ∈ N, then λ p x.A ∈ T l . • If M, N ∈ T l and p ∈ N, then (M N ) p ∈ T l .
The relation β l is defined over the set T l of labelled λ-terms by

((λ p x.A)B) p → β l A[x := B]
In order to define superdevelopements we will restrict attention to terms that are labelled such that the label of an application cannot be equal to the label of a λ-abstraction that is not in its scope. This corresponds exactly to "upwards" redex creations.

Definition 1.8 (Well-labelled and initially labelled terms). A labelled term A ∈ T l is said to be well-labelled if for all positions such that A |p1 = (B 0 B 1 ) p and A |p2 = λ p x.C then p 1 p 2 . It is initially labelled if moreover for all positions such that A |p1 = λ p x.C and

A |p2 = λ p x ′ .C ′ then p 1 = p 2 .
In the following, we will suppose that all labelled terms are well-labelled. We can remark that the set of well-labelled terms is closed by β l -reduction.

1.3.2. Untyped λ-calculus and superdevelopments. Before giving the formal definition of superdevelopments, we define an erasing morphism from labelled λ-terms to λ-terms. Without any ambiguity, we overload the notation of the previous section.

Definition 1.9 (Erasing mapping). The mapping Υ : T l → T that erases labels is defined as follows

• Υ(ε) = ε • Υ((AB) p ) = Υ(A)Υ(B) • Υ(λ p x . A) = λx. Υ(A)
Note that the mapping Υ can be extended into a morphism from β l -reductions to

β-reductions.
A superdevelopment is a β-rewrite sequence that may reduce both the redexes that are residuals of redex occurrences in the initial term (like in developments) and the redex occurrences that are created in the first or second way. In the λ-calculus, superdevelopments are, as developments, finite.

Definition 1.10 (Superdevelopments). A β-rewrite sequence ς of the λ-calculus is a βsuperdevelopment if there exists a β l -rewrite sequence σ in the labelled λ-calculus that starts with an initially labelled term and stops on a term in β l -normal form and such that

Υ(σ) = ς.
We extend the finite developments theorem to superdevelopements.

Theorem 1.11 (Finite superdeveloppements [vR96]).

• Every superdevelopment is finite.

• If two superdevelopments ζ 1 and ζ 2 start with the same initial term then the two final terms must be equal.

As finite developments coincide with the parallel reduction of Tait and Martin-Löf, finite superdevelopments coincide with Aczel's parallel reduction [START_REF] Aczel | A general Church-Rosser theorem[END_REF] called in the following strong parallel reduction. It is denoted by ⇒ β sd and we say that a term A β sd -reduces to a

term B if A ⇒ β sd B.
Definition 1.12 (Strong parallel reduction). The strong parallel reduction in the λ-calculus is defined inductively by

ε ⇒ β sd ε (Red-ε) A 1 ⇒ β sd A 2 B 1 ⇒ β sd B 2 A 1 B 1 ⇒ β sd A 2 B 2 (Red-@) A 1 ⇒ β sd A 2 λx. A 1 ⇒ β sd λx. A 2 (Red-λ) A 1 ⇒ β sd λx. A 2 B 1 ⇒ β sd B 2 A 1 B 1 ⇒ β sd A 2 [x := B 2 ] (Red-β s )
The only difference with the parallel reduction of Tait and Martin-Löf is the rule (Red-β s ) that replaces the rule (Red-β) of the parallel reduction. The redex reduced by the rule (Red-β s ) is obtained from the reduct of A 1 . This redex is not necessarily present in the initial term A 1 A 2 . It may have been created and this creation is of type 1 or 2 but not of type 3 (an upwards creation but not a downwards creation).

Theorem 1.13 (Strong parallel reduction and superdevelopments). The notions of strong parallel reduction and superdevelopments coincide in the following sense. For every terms

A, B ∈ T there exists a superdevelopment A → → β B iff A ⇒ β sd B.
This characterization of superdevelopments is the essence of the corresponding matching algorithm. We conclude this section by examples.

Example 1.14. In this example, we show how to associate, when it exists, the β l -rewrite sequence corresponding to a β-rewrite sequence.

• The β-rewrite sequence

(λx. λy. xy)zz ′ → β (λy. zy)z ′ → β zz ′
is a superdevelopment since it corresponds to the β l -rewrite sequence

(((λ 1 x.λ 2 y.xy)z) 1 )z ′ ) 2 → β l ((λ 2 y.zy)z ′ ) 2 → β l zz ′ .
• However, the rewrite sequence

(λx. xx)(λx. xx) → β (λx. xx)(λx. xx) → β . . .
is not a superdevelopment. We show that it is not possible to label the term (λx. xx)(λx. xx) and find an adequate β l -reduction sequence. We can first try to label the λ-abstractions. Since we consider only initially well-labeled λ-terms, each λ-abstraction must have a different label. Moreover, if we want the term to be β l -reducible, we necessary have

((λ 1 x . xx)(λ 2 x . xx)) 1 .
To conclude the labelling of (λx. xx)(λx. xx), we have to find two labels p 1 and p 2 such that the term

((λ 1 x . (xx) p 1 )(λ 2 x . (xx) p 2 )) 1
is well-labelled. Since we want the term to be reducible after one β l -reduction then p 1 must be equal to 2. But this is impossible since we consider a well-labelled term.

Given a λ-term, we can thus "label" this term (and thus obtaining a labelled λ-term)

in order to β l -reduce redexes created in the first or in the second way but not in the third way. This is exactly why we restrict ourselves to well-labelled terms.

The corresponding β l -rewrite sequence associated to a superdevelopment is no more given in the following.

Example 1.15. In this example, we illustrate the link with developments, superdevelopments and redex creations.

• Finite development Residuals of redexes present in the initial term can be contracted:

(λx. f (x, x)) ((λy. y) a) → β f ((λy. y) a, (λy. y) a) → β f (a, (λy. y) a) → β f (a, a)
• Redex creation of type 1 In the following superdevelopment, the new redex obtained after one β-rewrite step is reduced:

((λx. λy. f (x, y))a)b → β (λy. f (a, y))b → β f (a, b)
• Redex creation of type 2 As in the previous example, a redex is created and reduced during the reduction, but in a different way:

((λx. x)(λy. y))a → β (λy. y)a → β a
• Redex creation of type 3 There is no superdevelopment from the term (λx. xa)(λy. y) to the term a:

(λx. xa)(λy. y) → β (λy. y)a

Matching modulo beta (and eta)

In this section, we consider terms of the simply λ-calculus that is, elements of T t . We are going to solve equations modulo the full β-equivalence (possibly with η).

Matching modulo β.

Definition 2.1 (β-equation/system). A β-equation is a pair of β-normal typed λ-terms of the same type denoted A β B such that B is V-closed. A β-system is a multiset (possibly empty) of β-equations.

Union of multisets is written using the symbol ∪. If E 1 and E 2 are matching equations, we simply write (E 1 ) ∪ (E 2 ) for the multiset of the two matching equations.

For example, let us consider a base type ι, a constant a of type ι and two matching variables X and Y with respective types ι → ι and ι. Then, the pair (XY, a) is a β-equation.

Definition 2.2 (β-match). A substitution ϕ, that preserves types, is a β-match for the matching equation A β B if and only if Aϕ= β B. A substitution is a β-match for a system S if it is a β-match for each equation of S.

For example, the substitution {λx. x/X, a/Y } is a β-match for XY β a.

2.2. Nth order matching. In practice, we only consider algorithms to solve a subset of β-equations (higher-order matching modulo β is undecidable [Loa03]). Either we consider some restrictions on the order of matching variables and constants or we consider matching modulo βη. Definition 2.3 (Order of an equation/system). A β-equation is said to be of order at most n if all its matching variables are of order at most n and all its constants are of order at most n + 1. A system is said to be of order at most n if it is composed of equations of order at most n. We define the nth order matching as the operation that solves β-equations of order at most n.

For example, the above equation XY β a is of order 2. 2.3. Matching modulo βη. In practice, the adequate equivalence modulo which we want to consider matching equations is the βη-equivalence where the equation η is defined as

(η) λx. (Ax) = A if x ∈ fv(A)
The decidability of second-order matching was proved in [START_REF] Huet | Proving and applying program transformations expressed with second-order patterns[END_REF], of third order matching in [Dow94] and of fourth order matching in [START_REF] Padovani | Decidability of fourth-order matching[END_REF]. The general decidability proof appears recently in [START_REF] Stirling | Decidability of higher-order matching[END_REF] using game theory.

In this section, we simply reformulate the previously given definitions to take into account η-equivalence.

Definition 2.4 (βη-equation/system). A βη-equation is a pair of typed λ-terms in βη-long normal form of the same type denoted

A βη B such that B is V-closed. A βη-

Matching modulo superdevelopments (and eta)

In this section, we first define matching modulo superdevelopments, that we also call β sd -matching. We then relate it with second and third order matching.

3.1. Matching modulo superdevelopments. In this section, we consider terms of pure λ-calculus (elements of T ). We are going to solve equations modulo superdevelopments.

We first define the notion of equation and then the corresponding notion of solutions.

Definition 3.1 (β sd -matching equation/system). A β sd -matching equation or simply a matching equation is a pair of terms denoted A β sd B such that B is normal and V-closed. A matching system is a multiset (potentially empty) of matching equations.

We say that a matching variable belongs to a system S and we note X ∈ S if X occurs in one equation of S.

For example, the pairs (XY, λx. x) and ((λx. x)X, a) are β sd -matching equations whereas (XY, (λx. x)a) is not since the term (λx. x)a is not normal.

Higher-order matching and unification algorithms that can be found in the literature [Hue75, SG89, Dow01] usually consider matching equations of terms in normal form and this property is preserved during the matching process by using normalizing substitutions. Note that this is not the case here: the term A of an equation A β sd B is not necessarily in normal form.

Definition 3.2 (β sd -match). A substitution ϕ on matching variables is a β sd -match or simply a match for the matching equation A β sd B if there exists a superdevelopment from Aϕ and B (that is, Aϕ ⇒ β sd B). A substitution is a match of a system if it matches each equation. The set of all matches of a system S is denoted M(S).

We can associate to a typed λ-term an untyped term. In the same way, we can associate A β sd -system can have an infinite number of solutions but we can always find a finite set of minimal solutions such that every solution is subsumed by a minimal solution.

Example 3.4 (Infinite number of β sd -matches). Following Example 3.3, we can notice that all the substitutions that coincide with σ 3 are solutions of the equations, independently from the term associated to the matching variable Y . For example, σ 5 = {λx. λy. y/X, λx. x/Y, ab/Z} and σ 6 = {λx. λy. y/X, λx. λy. y/Y, ab/Z}.

are solutions. They are subsumed by σ 3 in the following sense σ 3 ≤ σ 5 and σ 3 ≤ σ 6

The following example shows that there is no most general match.

Example 3.5 (Independant β sd -match). Following example 3.3 we can notice that the substitution σ 1 and σ 2 are not comparable since σ 1 ≤ σ 2 and σ 2 ≤ σ 1 .

In the following we are going to solve β sd -equations by transformation rules. We simplify a system until getting a 'normal form' for which we can extract a substitution (if it exists).

Such a system is said to be in solved form in the sense of the following definition.

Definition 3.6 (Solved form). A matching equation X β sd A is in solved form if A contain no free variables. The corresponding substitution is defined by {A/X}. A system is in solved form if all its equations are in solved form and if the left-hand sides are pairwise disjoint. The corresponding substitution of such a system is the union of the corresponding substitutions of each equation (of the system). It is denoted by σ S .

Definition 3.7 (Complete match set). Let S be a matching system. A complete match set of S is a set of substitutions M such that:

(1) Soundness For all ϕ ∈ M, ϕ is a β sd -match of S.

(2) Completeness For all ϕ such that ϕ is a β sd -match of S there exists ψ ∈ M such that ψ ≤ ϕ, i.e., there exists a substitution ξ such that ϕ = ξ • ψ where • denotes substitution composition.

The following lemma gives the relevance of solved forms.

Lemma 3.8. If S is a system in solved form then {σ S } is a complete match set of S.

3.2.

Comparison with second-order matching. In this section, we are going to prove that matching modulo superdevelopments is complete for second-order matching. The following results were already proved in [dMS01]. Nevertheless, the technical material presented here (creations of redexes, superdevelopments) gives simple and intuitive proofs.

First, a technical result on the creation of redexes.

Lemma 3.9. For all terms A 1 , A 2 , • • • , A n such that A n contains a redex of third order (or more) and there exists a superdevelopment A 1 → β A 2 → β . . . → β A n , then A 1 contains also a redex of third order (or more).

Proof. We prove the result by induction on n. We look at the induction case. By induction hypothesis, we know that A 2 contains a redex of a least third order that we call in the following R = (λx. C) D. First, if R is a residual of a redex of A 1 then the result is obvious.

Secondly, if not, and if R is created during the reduction from A 1 to A 2 in the first way mentioned before then A 1 must contain a subterm of the form (((λz. λx. C ′ ) E) D with

C = C ′ [z := E].
Then the order of the redex (λz. λx. C ′ ) E is greater or equal to the order of R. This concludes the case. Finally, if not, and if R is created during the reduction from Proof. The proof is by contradiction. Let ϕ be a β-match of the β-matching equation A β B that is not a β sd -match. Then we have that A does not contain any β-redex and that ϕ does not contain any term of order greater than 2. Finally, Aϕ ⇒ β sd B and Aϕ= β B.

A 1 to A 2 in

Thus there exist (

A i ) i such that Aϕ → β A 1 → β • • • → β sd A n is a superdevelopments and
A n contains a β-redex (λx. C)D which is not reduced by superdevelopments. This means that this redex is a residual of a redex created when reducing A i 0 . Since the redex is not reduced by superdevelopments then this creation is of type 3 and thus induces a redex of order at least 3. Lemma 3.9 implies that Aϕ contains a redex of order at least 3. Since both A and ϕ range in the set of β-normal forms, then there exists a position p 1 and a term E such that A |p1 = XE where X is mapped by ϕ to a λ-abstraction of at least third order.

This contradicts the hypothesis on the order of the initial matching problem.

This proposition for second-order β-equations can be easily generalised to second-order β-systems.

Creations of redexes in the third way induce intrinsically redexes of at least third order.

This intuitively explains why second-order matches modulo β are β sd -matches. The reader familiar with the second-order matching algorithm of G. Huet and B. Lang may notice that during their matching process, we can restrict β-normalization to β sd -normalization.

3.3.

Comparison with third-order matching. As soon as we consider third-order matching problems, the set of minimal solutions may be infinite. Since matching modulo superdevelopments generates finitely many minimal solutions, we remark that matching modulo superdevelopments cannot be complete w.r.t. third-order matching.

Example 3.11. The substitution {λx. λf. f x/X} is a β-match for the matching equation λz. (X z (λy. y)) λz. z whereas it is not a β sd -match. In fact, λz. ((λx. λf. f x) z (λy. y))

β sd -reduces to λz. (λy. y)z but not to λz. z.

The last example is classical and taken from [Dow01]. The third-order matching equation has an infinite number of (minimal) solutions of type ι → (ι → ι) → ι that are given by the Church numbers λx. λf. (f . . . (f x) . . .).

3.4.

Comparison with matching of Miller patterns. In the case of matching of Miller patterns [Mil91, Qia96], the restriction of the β-reduction given by superdevelopments is powerful enough:

Proposition 3.12. Let ϕ be a match of an equation P β A where P is a Miller pattern.

Then there exists a superdevelopment P ϕ → → β A.

Proof. For all Miller patterns, only a subset of the β-reduction is needed [Mil91]. This restriction is defined by

(λy. M )x → β 0 M [y := x]
We recall that redex creations of type 2 or 3 require to reduce a redex whose term in application position is a λ-abstraction. Then since β 0 -reduction only reduces redexes whose term in application position is a variable, only redex creations of type 1 can occur in the context of the β 0 -reduction. These created redexes will be reduced by superdevelopments.

3.5. Matching modulo superdevelopments and eta. In the simply typed λ-calculus, matching modulo βη strongly relies on the η-long normal form. This makes an important difference with matching modulo β: using the η-equivalence, we move from a undecidable [Loa03] to a decidable problem [START_REF] Stirling | Decidability of higher-order matching[END_REF].

In the context of matching modulo superdevelopments, the use of η does not influence neither fundamentally nor technically the design of matching algorithms, as we will see in Section 5.

The use of η-long normal form is here replaced by the use of η-reduction to consider terms in η-normal form. We recall the definition of η-reduction.

λx. (Ax)

→ η A if x ∈ fv(A)
Definition 3.13 (β sd η-equation and β sd η-system). A β sd η-matching equation is defined by a pair of terms (A, B) such that B is βη-normal and V-closed. We denote such an equation by A η β sd B. A β sd η-system is a multiset of equations.

Definition 3.14 (β sd η-match). We say that ϕ is a β sd η-match for the

β sd η-equation A η β sd B if there exists a term C such that Aϕ ⇒ β sd C → → η B.
These two notions will be illustrated in Section 5.

(x β sd x) ∪ S → ε v S (a β sd a) ∪ S → ε c S (X β sd A) ∪ S → ε X (X β sd A) ∪ {A/X}S if fv(A) = ∅ and X ∈ S (λx. A β sd λx. B) ∪ S → λ λ (A β sd B) ∪ S (A 1 B 1 β sd A 2 B 2 ) ∪ S → @ @ (A 1 β sd A 2 ) ∪ (B 1 β sd B 2 ) ∪ S (A 1 B 1 β sd C) ∪ S → @ π (A 1 β sd λx. C) ∪ S
where x fresh variable

(A 1 B 1 β sd C) ∪ S → @ β (A 1 β sd λx. A 2 ) ∪ (B 1 β sd B 2 ) ∪ S
where A 2 [x := B 2 ] = C and x fresh variable x ∈ fv(A 2 ) and A 2 , B 2 β-normal • a system is transformed step by step until getting to a normal from (the set of rules is terminating); this normal form can be a resolved form and then gives a solution to the original matching problem (the algorithm is sound);

• by exploring all the possible reductions (the application of rules is non deterministic meaning that two reductions of the same initial system may lead to different normal forms) and collecting all the resolved forms we get a complete match set (the algorithm is sound and complete).

We denote S → S ′ when one of the transformation rules given in Figure 1 can be applied to transform S into S ′ . We also denote S → →S ′ when it exists n 0 systems S 1 , . . . , S n such that S = S 1 → . . . → S n = S ′ .

The transformation rules of Figure 1 mimicked the definition of strong parallel reduction as we explain now in details by examining transformations rules one by one.

The ε rules deal with atoms. The rules (ε c ) and (ε v ) are removing directly solved equations. Note that when the rules (ε c ) is applied to the singleton system a β sd a then the resulting system is the empty multiset.

The rule (ε X ) is substituting a matching variable with its corresponding value. Note that we substitute only X -closed terms. For the reader familiar with 'classical' presentation of higher-order matching algorithms, it may be useful to recall again that we do not consider normalizing substitutions. This is not a matter of taste but rather a matter of soundness.

In fact, let us consider the following variation of the ε X rule

(X β sd A) ∪ S → ε ↓ X (X β sd A) ∪ (S{A/X}) ↓
where (S{A/X}) ↓ denotes the β sd -normal form of S{A/X} and the following equation

f (XYZ, X, Y, Z) β sd f (1, λx. λy. xy, λz. z, 1)
which can be transformed into

(XYZ β sd 1) ∪ (X β sd λx. λy. xy) ∪ (Y β sd λz. z) ∪ (Z β sd 1)
By applying the (ε ↓ X ) rule three times and the (ε c ) rule once we get:

(X β sd λx. λy. xy) ∪ (Y β sd λz. z) ∪ (Z β sd 1)
We obtain a normal form in solved form whereas the corresponding substitution is not a match modulo superdevelopments (even if this is of course a match modulo β): the rule (ε ↓ X ) is thus not sound.

Finally, note that the side condition X ∈ S of the (ε X ) rule is used to guarantee the termination of the algorithm (see the proof of Proposition 4.8).

The (λ λ ) rule is dealing with λ-abstractions like the (Red-λ) does. Note that this way to deal with abstractions is sound since we only consider closed substitutions. In many higher-order matching algorithms, the λ-abstractions are kept prenex. The two choices are possible. We will present the algorithm for matching modulo superdevelopments using the second choice. A similar rule to (λ λ ) can be found in the context of higher-order unification in the λ-calculus with de Bruijn indices and explicit substitutions [DHK00].

The @ rules deal with the application. The rule (@ @ ) is directly related to the rule (Red-@) and thus requires no more comments. The rules (@ π ) and (@ β ) are both related to the rule (Red-β s ). We are trying to express the right hand side C of the equation as the result of a β-reduction, let us say A 2 [x := B 2 ]. Depending on the belonging of x in A 2 , we obtain either the rule (@ π ) or the rule (@ β ).

• If x does not belong to A 2 , we obtain the rule (@ π ): we associate the left hand side with an abstraction ignoring its argument and returning the right hand side of the initial equation.

• If not, that is if x belongs to A 2 , then we obtain the (@ β ) rule by mimicking the (Red-β s ) rule for all terms such that C = A 2 [x := B 2 ] where x belongs to A 2 and A 2 and B 2 are β-normal. Let us examine how we can find such terms. First, remark that B 2 is necessarily a subterm of C (since x belongs to A 2 ). Let us consider one of this subterm. We choose a subset of the set of positions of C such that the subterm of C at these positions is B 2 . The term A 2 is obtained from C by replacing the subterm at each of the position of the chosen subset by x. Note that there exists only a finite number of such pairs (A 2 , B 2 ) which satisfy these conditions.

Comparing with the approach like the one presented in [START_REF] Huet | Proving and applying program transformations expressed with second-order patterns[END_REF], we do not introduce new matching variables during the matching process. The solutions of a system S given by our algorithm have then a domain included in the matching variables of S. The advantage is that when we compare such a solution with an arbitrary solution of S, it is not technically necessary to restrict this comparison to matching variables of S unlike for example in [START_REF] Hans-Jürgen | Matching -A special case of unification? In Unification[END_REF].

Example 4.1 (Computing the solutions of a β sd -equation). We consider the equation XY β sd ab. As the left and right hand sides of the equation are applications, we can apply the rules (@ @ ), (@ π ) or (@ β ).

(1) Rule (@ @ ):

(XY β sd ab) → (X β sd a) ∪ (Y β sd b).
(2) Rule (@ π ):

(XY β sd ab) → (X β sd λx. ab).

(3) Rule (@ β ): to find A 1 and A 2 such that A 1 [x := A 2 ] = ab, we first choose A 2 as a subterm of "ab": a, b and ab. The set of positions of ab for which A 2 is the corresponding subterm of C is a singleton since each subterm of ab appears only once in ab. We obtain three ways to apply the rule (@ β ) corresponding to the three subterms of the right hand side of the equation XY β sd ab:

(a) (XY β sd ab) → (X β sd λx. xb) ∪ Y β sd a). (b) (XY β sd ab) → (X β sd λx. ax) ∪ (Y β sd b). (c) (XY β sd ab) → (X β sd λx. x) ∪ (Y β sd ab).
Example 4.2 (Computing the solutions of a β sd -equation). We consider the equation X(Y X) β sd a. We can apply the rules (@ π ) or (@ β ).

(1) Rule (@ π ):

(X(Y X)

β sd a) → (X β sd λx. a). (2) Rule (@ β ): (X(Y X) β sd a) → (X β sd λx. x) ∪ (Y X β sd a).
To simplify Y X β sd a we can apply the rule (@ π ) or the rule (@ β ).

(a) Rule (@ π ):

(X β sd λx. x) ∪ (Y X β sd a) → (X β sd λx. x) ∪ (Y β sd λx. a). (b) Rule (@ β ): (X β sd λx. x) ∪ (Y X β sd a) → (X β sd λx. x) ∪ (Y β sd λx. x) ∪ (X β sd a) → (X β sd λx. x) ∪ (Y β sd λx. x) ∪ (λx. x β sd a).
In the last case, the system is not in solved form (even if it is in normal form) and thus does not give a solution. The initial matching problem has thus only two solutions.

Remark 4.3 (Application of the (@ β ) rule). The application of the rule (@ β ) is driven by the choice of the term B 2 which must match the term B 1 . In implementations of the algorithm, this restriction on the choice of B 2 is very useful. For example, if B 1 is a constant or a variable then necessarily B 2 = B 1 . This is always the case in the case of Miller patterns since a matching variable can only be applied to bound variables. 4.2. Termination property. We show that the algorithm is terminating. We first define the size of a term (resp. of a matching equation, resp. of a system). Definition 4.4 (Size). The size of a term A denoted S (A) is defined by induction

S (ε) = 1 for all atoms ε ε S (λx. B) = S (B) + 1 S (BC) = S (B) + S (C) + 1
The size of a matching equation A β sd B is the size of A. The size of a system is the sum of the sizes of each equation of the system. We use the same notation for the size of terms, equations and systems.

For every system S, we denote by U (S) the number of unsolved variables of S in the sense of the following definition.

Definition 4.5 (Solved variable). A matching variable of an equation X β sd A belonging to a system S is a solved variable if X occurs nowhere else in S.

Lemma 4.6 (Unsolved variables). For all systems S and S ′ such that S → S ′ we have the following inequality U (S) U S ′ The inequality is strict if the reduction is done using the rule (ε X ).

Lemma 4.7 (Size decreasing ). For all systems S and S ′ such that S → S ′ using any of the transformation rules of Figure 1 except the rule (ε X ), we have

S (S) > S S ′
Proof. We prove that the inequality is valid for each transformation rule. Note that the size only depends on the right hand side of equations: the inequality is thus in particular true for rule (@ β ).

ε v S ((x β sd x) ∪ S) = S (x β sd x) + S (S) > S (S) ε c S ((c β sd c) ∪ S) = S (c β sd c) + S (S) > S (S) λ λ S ((λx. A β sd λx. B) ∪ S) = S (λx. A β sd λx. B) + S (S) = 1 + S (A) + S (S) > S (A β sd B) + S (S) @ @ S ((A 1 B 1 β sd A 2 B 2 ) ∪ S) = S (A 1 B 1 ) + S (S) = 1 + S (A 1 ) + S (B 1 ) + S (S) > S (A 1 β sd A 2 ) + S (B 1 β sd B 2 ) + S (S) @ π S ((A 1 B 1 β sd A 2 ) ∪ S) = S (A 1 B 1 ) + S (S) = 1 + S (A 1 ) + S (B 1 ) + S (S) > S (A 1 β sd λx. A 2 ) + S (S) @ β S ((A 1 B 1 β sd C) ∪ S) = S (A 1 B 1 ) + S (S) = 1 + S (A 1 ) + S (B 1 ) + S (S) > S (A 1 β sd λx. A 2 ) + S (B 1 β sd B 2 ) + S (S)
for all normal terms A 2 and B 2 Proposition 4.8 (Termination of the algorithm). The set of transformation rules given in Figure 1 is terminating.

Proof. For all systems S and S ′ such that S → S ′ , the lexical product of the number of unsolved variables U ( ) and the size of the system S ( ) decreases for each rule:

U ( ) S ( ) ε v = > ε c = > λ λ > ε X > @ @ > @ π > @ β
> Note that the rule (ε X ) makes decrease the number of unsolved variables thanks to the side condition X ∈ S.

Completeness property.

We define an extension of the relation ⇒ β sd to multisets.

To ease the reading in this section, we write (A 1 , B 1 ) ∈ β s for A 1 ⇒ β sd B 1 . Lemma 4.12. For all systems S and S ′ such that S → S ′ using the rules (@ @ ), (@ π ) or (@ β ) we have M(S ′ ) ⊆ M(S).

Proof. We prove the result for each rule.

@ @ ϕ ∈ M((A 1 β sd A 2 ) ∪ (B 1 β sd B 2 ) ∪ S) ⇐⇒ ϕ ∈ M(A 1 β sd A 2 ) and ϕ ∈ M(B 1 β sd B 2 ) and ϕ ∈ M(S) ⇐⇒ A 1 ϕ ⇒ β sd A 2 and B 1 ϕ ⇒ β sd B 2 and ϕ ∈ M(S) =⇒ (A 1 B 1 )ϕ ⇒ β sd A 2 B 2 and ϕ ∈ M(S) ⇐⇒ ϕ ∈ M((A 1 B 2 β sd A 2 B 2 ) ∪ S) @ π ϕ ∈ M((A 1 β sd λx. A 2 ) ∪ S) ⇐⇒ A 1 ϕ ⇒ β sd λx. A 2 and ϕ ∈ M(S) =⇒ (A 1 B 1 )ϕ ⇒ β sd A 2 [x := (B 1 ϕ)] and ϕ ∈ M(S) ⇐⇒ (A 1 B 1 )ϕ ⇒ β sd A 2 and ϕ ∈ M(S) since x is fresh from A 1 , B 1 , A 2 , S ⇐⇒ ϕ ∈ M((A 1 B 1 β sd A 2 ) ∪ S) @ β ϕ ∈ M((A 1 β sd λx. A 2 ) ∪ (B 1 β sd B 2 ) ∪ S) ⇐⇒ A 1 ϕ ⇒ β sd λx. A 2 and B 1 ϕ ⇒ β sd B 2 and ϕ ∈ S =⇒ (A 1 B 1 )ϕ ⇒ β sd A 2 [x := B 1 ] and ϕ ∈ S ⇐⇒ ϕ ∈ M((A 1 B 1 β sd A 2 [x := B 1 ]) ∪ S)
Proposition 4.13 (Correctness). For all systems S and S ′ such that S → →S ′ and S ′ is in solved form we have σ S ′ ∈ M(S).

Proof. The proof is a simple induction on the length of the sequence of transformations and is using the previous lemmas for the induction step.

4.5. Finite complete match set property. The correctness and completeness properties entail that there exists a complete match set. It is obtained by exploring all the possible reductions and by constructing the set of substitutions obtained from the solved forms. We know that this process is finite since the algorithm terminates and thus the complete match set is also finite.

Proposition 4.14 (Finite complete match set ). For a given system S, there exists a finite complete match set M given by M = {σ ′ S | S → →S ′ and S ′ is in solved form} .

5.

Algorithm for matching modulo superdevelopments and eta 5.1. Presentation of the algorithm. The algorithm for matching modulo superdevelopments given in Figure 1 must be customized to take into account η-conversion. First,

(λx n . x β sd λx n . x) ∪ S → ε v S (λx n . a β sd λx n . a) ∪ S → ε c S (λx n . X β sd λx n . A) ∪ S → ε X (λx n . X β sd λx n . A) ∪ S{A/X} if fv(A) = ∅ and X ∈ S (λx n . A β sd λx n-k . B) ∪ S → λ (λx n . A β sd λx n-k+1 . Bx n-k+1 ) ∪ S (λx n . (A 1 B 1 ) β sd λx n . (A 2 B 2 )) ∪ S → @ @ (λx n . A 1 β sd λx n . A 2 )∪ (λx n . B 1 β sd λx n . B 2 ) ∪ S (λx n . (A 1 B 1 ) β sd λx n . C) ∪ S → @ π (λx n . A 1 β sd λx n . (λy. C)) ∪ S
where y fresh variable Figure 1) one head λ-abstraction. Then, we must add a side condition to the rule (@ β ) for λx. A 2 and A 1 to be in βη-normal form (and not only in β-normal form).

(λx n . (A 1 B 1 ) β sd λx n . C) ∪ S → @ β (λx n . A 1 β sd λx n . (λx. A 2 ))∪ (λx n . B 1 β sd λx n . B 2 ) ∪ S
By making these two changes, we obtain an algorithm for matching modulo superdevelopments and η. We give it explicitly in Figure 2. We have chosen to present this algorithm in a slightly different way: instead of removing λ-abstractions, we keep them prenex (and thus the rule (λ λ ) is no more useful).

We can prove that this algorithm has the termination, soundness and completeness property. The termination and the correctness proofs are similar to the one given in the previous section. The completeness proof is slightly more technical although it is fundamentally the same as the one given in Section 4.3. We show that the algorithm for matching modulo superdevelopments and η given in Figure 2 gives at most one solution when it is applied to a Miller pattern equation. Since the algorithm is sound and complete this gives the most general match. First, note that all the reducts of a system of Miller pattern equations are systems of Miller pattern equations.

Proposition 5.3. Let P η β sd B be a Miller pattern equation which has a solution and let A be a typed term. Then the set of solved forms given by the transformation rules of Figure 2 is a singleton.

Proof. First, we can remark that when the rule (λ ) can be applied, it is the only one and thus does not introduce any non-determinism in the application of the transformation rules.

We thus exclude it in the remaining of this proof. We prove the result by induction on the size of patterns. We distinguish three cases according to the head symbol of the pattern.

(

↓ (λx. (A i σ ′ ) βη λx. B) ∪ (Sσ ′ ), σ ′ • σ where σ ′ = {λy n . y i /X} for 1 ≤ i ≤ n (Imitation) (λx. X(A 1 , . . . , A n ) βη λx. ε(B 1 , . . . , B m ) ∪ S, σ ↓ (λx. H 1 (A 1 σ ′ , . . . , A ′ n σ ′ ) βη λx. B 1 ) ∪ . . . ∪ (λx. H m (A 1 σ ′ , . . . , A ′ n σ ′ ) βη λx. B m ), σ ′ • σ ∪ Sσ ′
where σ ′ = {λy n . ε(H 1 (y 1 , . . . , y n ), . . . H m (y 1 , . . . , y n ))/X} and H 1 , . . . , H n are fresh variables of adequate types The set of transformations rules given in Figure 3 are managing a pair made with a multiset of equations and a substitution. Given a pair S, id the algorithm is said to be successful if there exists a sequence of transformations ending on ∅, σ . The substitution σ is a match for S (correctness). The first rule (Decomposition) simplifies equations whose head symbols are identical. The rules (Projection) and (Imitation) are dealing with equations whose left hand side head symbols are matching variables. In the first case, the variable is instantiated by a projection function. We then have to require that the projected argument is equal to the right hand side. In the second case, the variable is partially instantiated in the following sense: the head symbol of the term associated to that variable is set to be equal to the right hand side head symbol; we introduce new matching variables to postpone the remaining choices 2 .

The algorithms given in previous section could also have been presented by constructing the substitution at the same time as we transform the system. We did not do it to simplify the presentation (whereas here it is strictly necessary). We now illustrate the algorithm given in Figure 3 The solving of the equations related to H 1 , H 2 and H 3 gives the following solutions

{λz 1 z 2 . a/H 1 } or {λz 1 z 2 . z 2 /H 1 } {λz 1 z 2 . z 1 /H 2 } {λz 1 z 2 . a/H 3 } or {λz 1 z 2 . z 2 /H 3 }
The initial problem has thus four solutions given by {λy 1 y 2 . f (a, y 1 , a)/X} {λy 1 y 2 . f (a, y 1 , y 2 )/X} {λy 1 y 2 . f (y 2 , y 1 , a)/X} {λy 1 y 2 . f (y 2 , y 1 , y 2 )/X} 6.2. Second-order matching algorithm based on superdevelopments.

6.2.1. Matching modulo superdevelopments and types. We say that an (untyped) term is typable when it belongs to typed terms. A system is typable when for each equation the two terms are typable and of the same type. Otherwise, we say it is untypable.

First, we can remark that if a system is build only with typable terms then its reducts are also build with typable terms. The algorithm given in Figure 1 has a nice behaviour w.r.t. types in the following sense: a sequence of transformations ending with a typable system involve only intermediate systems which are typable.

Proposition 6.2. For all systems S and S ′ such that S → →S ′ , if the system S ′ is typable then the system S is also typable.

This proposition is directly obtained from the following lemma Lemma 6.3. For every system S and S ′ such that S → S ′ , if S is not typable then S ′ is not typable .

2 The partial instantiation implies that we can now substitute matching variables by term not necessarily V-closed. We are then out of the scope of the framework defined above but this is only to give the standard presentation of Huet and Lang algorithm.

7. Algorithm for matching modulo developments (and eta)

In the previous sections, we have presented some works on matching modulo superdevelopments. One may wonder if these works can be adapted for the more restrictive notion of matching modulo developments. We show in this section that it is indeed the case.

This section is organised as follows. We first give a precise definition of matching modulo developments. We show that it is neither complete for second-order matching nor for Miller pattern matching. We finally conclude by giving explicitly a sound, complete and terminating algorithm for matching modulo developments. We recall that the parallel reduction and the strong parallel reduction differ only on one rule: the (Red-β) of the parallel reduction is replaced by the (Red-β s ) of strong parallel reduction. Then the corresponding algorithms only differ on the rules in relationship with the (Red-β) and (Red-β s ) rules: the transformation rules @ π and @ β for matching modulo developments are given in Figure 4.

Theorem 7.5 (Algorithm for matching modulo developments). The algorithm for matching modulo developments consisting of the rules (ε v , ε c , ε X , λ λ , @ @ ) given in Figure 1 plus the rules (@ π ) and (@ β ) given in Figure 4 is sound, complete and terminating. It has the finite complete match set property (there is no most general match).

Proof. To prove these results, it is very easy to adapt the proofs given in Section 4. The case of matching modulo developments and η, not presented here, is also easily deduced from the previous sections.

Applications to higher-order rewriting

Higher-order rewriting can be defined [MN98] modulo the βη-equivalence of the simply typed λ-calculus. Since this calculus is used to instantiate terms, we call it a substitution calculus according to the terminology of presented in [Oos94, vR96].

Other higher-order rewriting frameworks choose other substitution calculi. For example, Combinatory Reduction Systems (CRS) [START_REF] Willem | Combinatory Reduction Systems[END_REF][START_REF] Klop | Combinatory reduction systems: introduction and survey[END_REF] use the λ-calculus modulo developments as a substitution calculus. To our knowledge, the work presented in this paper is the first one giving an algorithm for the CRS matching, that is for higher-order matching modulo developments.

Polyadic developments and superdevelopments. Higher-order rewriting frameworks that use the λ-calculus modulo developments as a substitution calculus are enough ex- It is a generalization of developments that also reduce redexes created in the in the first way (according to the taxonomy given page 6). The only difference with superdevelopments is then that polyadic developments do not reduce redex occurrences that are created in the second way.

In the context of higher-order rewriting, we do not see the added value of reducing the redexes created in the second way when instantiating a term. We believe that polyadic developments and superdevelopments are essentially the same. We consider redex creations of type 2 as syntactical accidents.

Although λ-calculus modulo polyadic developments is a natural choice to be a substitution calculus for higher-order rewriting (as suggested in [START_REF]Term Rewriting Systems[END_REF]), we are not aware of any algorithm dealing with higher-order matching modulo polyadic developments. In particular, polyadic developments do not have a big step semantics that can guide the design of a corresponding algorithm in the spirit of this paper.

Untyped λ-calculus modulo superdevelopments as a substitution calculus. It thus appears that λ-calculus modulo superdevelopments is a very good compromise to be a substitution calculus for higher-order rewriting: the matching is complete for second-order and Miller pattern-matching and the corresponding matching algorithm does not depend one a particular type system and makes an optional use of η-equivalence.

Conclusion

We propose a new approach to study higher-order matching: instead of working in the typed λ-calculus modulo the full β-reduction we propose to work in the untyped λ-calculus modulo a restriction of the β-equivalence, namely superdevelopments. This is in the spirit of J.J. Levy works: we prefer to use the (hidden) typing on the reduction than the typing on terms. Higher-order matching modulo superdevelopments is of particular interest since all second-order β-matches are matches modulo.

We present and study an algorithm for matching modulo superdevelopments. We prove it to be sound, complete and terminating. We also show that this algorithm can be adapted to deal with second-order matching as well as with matching modulo developments. We

show that since we consider untyped frameworks, the use of the η-equivalence does not influence the design and behavior of our algorithms. We describe the algorithms in a mathematically elegant way that allow us to write intuitive proofs.

We finally apply these ideas in the context of higher-order rewriting. We give an algorithm for matching modulo developments, which is at the heart of Combinatory Reduction Systems. We also notice that higher-order rewriting with the untyped λ-calculus modulo superdevelopments as a meta-language is of particular interest.

Even if unification modulo superdevelopments is undecidable (by reduction to the undecidability of second-order unification [Gol81]), it might be relevant to study it. In particular, one may wonder if the work presented in this paper suggests another approach for unification of Miller patterns.

As far as it concerns the transformations of pattern-matching programs, the work of [dMS01] motivates by several examples higher-order matching in extensions of λ-calculus with patterns such as the pure pattern calculus [START_REF] Jay | First-class patterns[END_REF] or the rewriting calculus [START_REF] Cirstea | The rewriting calculus -Part I and II[END_REF].

Since a simple type system that ensures termination is difficult to find in this context, this paper should give useful guidelines.

Definition 1. 3 (

 3 Developments). A sequence of β-reductions ζ is a development (also called a complete development) if there exists a sequence σ of β u -reductions in the underlined λ-calculus which terminates on a term in β u -normal form and such that Υ(σ) = ζ. Theorem 1.4 (Finite developments [Bar84]).

1.3. 1 .

 1 Untyped labelled λ-calculus and β l -reduction. By definition, labels are simply elements of N.

  to a β-equation a β sd -equation. By a little abuse of notation, we simply denote by A β sd B the β sd -equation associated to the β-equation A β B.Recall that we only consider substitutions of closed and normal terms. In particular, a β sd -match is thus a substitution of closed and normal terms.The application of a substitution to a matching equation B β sd C is the equation Bϕ β sd C. The application of a substitution ϕ to a system, denoted Sϕ consists in the application of the substitution ϕ to each matching equation of S. Example 3.3 (β sd -matches). Consider the equation (XY )Z β sd ab and the substitutions σ 1 = { λx. x /X, a/Y, b /Z} σ 2 = { λx. λy. xy /X, a/Y, b /Z} σ 3 = { λx. λy. y /X, ab /Z} σ 4 = { λy. λx. xy /X, b/Y, λz. az /Z} The substitutions σ 1 , σ 2 and σ 3 are β sd -matches since ((XY )Z)σ 1 = ((λx. x)a)b ⇒ β sd ab ((XY )Z)σ 2 = ((λx. λy. xy)a)b ⇒ β sd ab ((XY )Z)σ 3 = ((λx. λy. y)Y ) (ab) ⇒ β sd ab The substitution σ 4 is not a β sd -match since ((XY )Z)σ 4 = ((λy. λx. xy)b)(λz. az) ⇒ β sd ab even if these terms are β-convertible.

  the second way mentioned before then A 1 must contain a subterm of the form (λy. y) (λx. C) D. The order of the redex (λy. y) (λx. C) is strictly greater than the one of R. This concludes the case. Proposition 3.10. Consider a second-order β-matching equation. If a substitution ϕ is a β-match then it is a β sd -match.

Figure 1 :

 1 Figure 1: Matching modulo superdevelopments

where A 2 Figure 2 :

 22 Figure 2: Transformation for matching modulo superdevelopments and η

  Example 5.1 (β sd η-matches). Consider the equation given in Example 4.1. If we solve this equation modulo β sd η we obtain only 4 solutions. In fact, the two solutions (X β sd a) ∪ (Y β sd b) and (X β sd λx. ax) ∪ (Y β sd b) are η-equivalents. Example 5.2 (Solutions of a β sd η-equation). Consider the pair of terms (λx. X(Y x), a).

Figure 3 :

 3 Figure 3: Transformation rules for Huet and Lang second-order matching algorithm

(

  Figure4: The @ π and @ β transformation rules for matching modulo developments

  pressive. We give examples where matching modulo developments is too rough. This was already noticed [vOvR93] when comparing CRS and HRS. Indeed, to encode HRS in CRS we use instead of developments the more general notion of polyadic developments. Polyadic developments are developments with steps of the form(. . . (λx 1 . . . λx n . A)B 1 ) . . .)B n → A[x 1 := B 1 ] . . . [x n := B n ]

  Definition 2.6(Miller Patterns). A simply typed λ-term A in β-normal form is a (higherorder) Miller pattern if every free occurrence of a variable X is in a subterm X(u 1 , . . . , u n ) of A such that (u 1 , . . . , u n ) is η-equivalent to a list of distinct bound variables.Unlike the higher-order unification which is undecidable in general[START_REF] Huet | A mechanization of type theory[END_REF] Gol81], the unification of Miller patterns is decidable and there exists a more general unifier (when the equation has a solution) that can be computed in linear time [Qia96]. In Section 5, we will give an algorithm for matching modulo superdevelopments and η that gives exactly (when it exists) the more general match for equations based on Miller patterns.

system is a multiset (possibly empty) of βη-equations.

Definition 2.5 (βη-match). A substitution ϕ, that preserves types, is a βη-match for the matching equation A β B if and only if Aϕ= βη B. A substitution is a βη-match for a system S if it is a βη-match for each equation of S. 2.4. Matching of Miller patterns. We first define Miller patterns.

  This pair is a β sd -equation with no β sd -match. But this equation has two β sd η-matches given Minimality for Miller patterns. In Section 3.4, we show that matching modulo superdevelopments is complete for matching of Miller patterns. In this section, by Miller pattern equations we mean a β sd -equation whose first term is a Miller pattern.

	by
	{a/X, λz. z/Y }	and	{λz. z/X, a/Y }.
	In fact,
	(λx. (X(Y x) η β sd a)	→	(λx. X(Y x) η β sd λx. ax)
		→	(λx. X η β sd λx. a) ∪ (λx. Y x η β sd λx. x)
		→	(λx. X η β sd λx. a) ∪ (λx. Y η β sd λx. λz. z)
	(λx. X(Y x) η β sd a)	→	(λx. X(Y x) η β sd λx. ax)
		→	(λx. X η β sd λx. λz. z) ∪ (λx. Y x η β sd λx. ax)
		→	(λx. X η β sd λx. λz. z) ∪ (λx. Y η β sd λx. a)
	5.2.

  1) If P = λx n . f (A 1 , . . . , A n ) then for the equation to be a solution, the term B must be of the form B = λx n . f (B 1 , . . . , B p ). All derivations that lead to a solution must reduceP β sd B into (λx n . A 1 β sd λx n . B 1 ) ∪ . . . ∪ (λx n . A p β sd λx n . B p ) (modulothe application order of the rules). Since λx n . A 1 , . . . λx n . A p are Miller patterns we can apply the induction hypothesis and conclude that λx n . A 1 β sd λx n . B 1 has σ 1 as a unique solution . . . λx n . A p β sd λx n . B p has σ p as a unique solution then the initial problem has a unique solution σ 1 ∪ . . . ∪ σ p . , . . . , A n ) βη λx. ε(B 1 , . . . , B n )) ∪ S, σ ↓ (λx. A 1 βη λx. B 1 ) ∪ . . . ∪ (λx. A n βη λx. B n ) ∪ S, σ (Projection) (λx. X(A 1 , . . . , A n ) βη λx. B) ∪ S, σ

	(Decomposition)	(λx. ε(A 1

  on an example. We consider the equation (λx. X(x, a) βη λx. f (a, x, a)) where a and f are constants of adequate types. It is clear that the rule (Decomposition) cannot be applied. Applying the rule (Projection) leads to a blocking state since the two arguments of X (that is, x and a) are not matching with the right hand side. Nevertheless, the rule (Imitation) can be applied and gives(λx. H 1 (x, a) βη λx. a) ∪ (λx. H 2 (x, a) βη λx. x), {λy 1 y 2 . f (H(y 1 , y 2 ), H 2 (y 1 , y 2 ), H 3 (y 1 , y 2 )/X} ∪ (λx. H 3 (x, a) βη λx. a)

	Example 6.1.

Acknowledgements

We would like to thank E. Bonelli for some comments that motivated this work. It benefited of the discussions we had with H. Cirstea, C. Kirchner and G. Nadathur.

Definition 4.9 (Multiset extension of ⇒ β sd ). We note ∅ the empty multiset. The multiset extension of ⇒ β sd is defined by

Proposition 4.10 (Completeness). For every system S, if ϕ ∈ M(S) then there exists a sequence of transformations S = S 0 → S 1 → . . . → S n where S n is in solved form and σ Sn ≤ ϕ.

Proof. We suppose given a system S 0 such that ϕ ∈ M(S 0 ). We want to show that there exists a derivation such that S = S 0 → S 1 → . . . → S n where S n is in solved form and σ Sn ≤ ϕ. Let S 0 = (A 1 β sd B 1 ) ∪ . . . (A p β sd B p ) and let E 0 be the multiset defined by E 0 = (A 1 ϕ, B 1 ) ∪ . . . ∪ (A p ϕ, B p ) Note that ϕ ∈ M(S 0 ) is equivalent to E 0 ∈ β s . We show the proposition by induction on

(1) If E 0 = ∅ then S 0 = ∅ and σ S 0 is the identity substitution id. The result is obvious since for every subsection ϕ we have id ϕ.

(2

By induction hypothesis, there exists a derivation (D)

Suppose first that A 1 is a constant or a variable. Then the derivation

n is the desired one.

Suppose now that A 1 is a matching variable. Then if there is no reduction step in the derivation (D) where X is substituted (application of the rule (ε X ) to the matching variable X), the derivation

is the desired one.

In the other cases (that is to say if there exists a derivation i 0 in (D) where X is instantiated) then X must be instantiated by B 1 and the following derivation is the desired one:

(X

We analyze the last rule used in the proof of (A 1 ϕ, B 1 ) ∈ β s .

• Rule (Red -@) Then we have

) ∪ E ∈ β s By induction hypothesis, there exists a derivation such that (A 1 1

with σ Sn ϕ.

If A 1 = X we also have (since then A 1 1 = B 1 1 and A 2 1 = B 2 1 and thus the two corresponding equations are V-closed and do not influence the derivation)

We conclude like in the previous case.

If not then the derivation

is the desired one.

• Rule (Redβ s ) Then we have

) ∪ E ∈ β s By induction hypothesis, there exists a derivation such that

is the desired one (4) This case is similar to the previous one.

Correctness property.

Lemma 4.11. For all systems S and S ′ such that S → S ′ using the rules (ε c ), (ε v ), (λ λ )

or (ε X ), we have M(S ′ ) = M(S).

Proof. The only trivial case concerns the rule (ε X ). Let X be a matching variable, S be a system and A be a term such that fv(A) = ∅ and X ∈ S.

(2) The case P = λx n . x(A 1 , . . . , A n ) is similar to the previous one.

(3) If P = λx n . X(x i 1 , . . . , x ip ) where the variables x i 1 , . . . , x ip are pairwise distinct.

Then three rules (@ π ), (@ @ ) and (@ β ) can be applied. We show that in all cases only one of this choice leads to a solution. In the remaining of this proof, we will always use the fact that if the application of the rule (@ @ ) leads to a solution then we must have B = B 1 x ip . In the same way, if the rule (@ β ) leads to a solution then

and thus x ip ∈ fv(B).

Let us suppose first that the application of the rule (@ π ) leads to a solution. We show that neither the application of the rule (@ @ ) nor the application of the rule (@ β ) lead to a solution. We have

The term B cannot contain the variable x ip (since none of the variables x i 1 , . . . , x i p-1 are equal to x ip ). The result is thus obvious.

Let us suppose now that the application of the rule (@ @ ) leads to a solution. We show that neither the application of the rule (@ π ) nor the application of the rule (@ β ) lead to a solution. We have

From the second equation, we deduce x ip ∈ fv(B) and thus (see below) the rule (@ π ) does not lead to a solution. From the first equation we deduce x ip ∈ fv(B 1 ).

Let us try to apply the rule (@ β ). We are looking for a term C 1 such that we have

) but the term λz. B 1 z is not βη-normal and thus the rule cannot be applied. This concludes the proof.

Algorithms for second-order matching

In this section, we consider second-order matching modulo βη. We show that the algorithm for matching modulo superdevelopments applied in a typed context gives an algorithm for second-order matching. We first recall the second-order matching algorithm given in [START_REF] Huet | Proving and applying program transformations expressed with second-order patterns[END_REF]. A more efficient algorithm has been proposed in [CQS96].

Proof. We suppose given a system S which is not typable. We show that all reducts of S are not typable by case analysis on the transformation rule involved.

• Rules (ε v ) and (ε c ): obvious.

• Rule (ε X ): The systems S and S ′ are defined by S = (X β sd A) ∪ S 0 and S ′ = (X β sd A) ∪ S 0 {A/X}. If the equation (X β sd A) is not typable then the result follows. If not (that is if X and A are typable and of the same type), the system S 0 is not typable. But since X and A are of the same type, S 0 {A/X} is not typable.

• Rule (λ λ ): obvious.

• Rule (@ β ): If S = (AB β sd C) ∪ S 0 and S 0 is not typable then the result follows.

Otherwise, we suppose that the equation AB β sd C is not typable. Then let σ be the type of AB and τ the one of C with τ = σ. There exist υ 0 and υ 1 possibly equal and such that the term A is of type υ 0 → σ and the term λx. C is of type υ 1 → τ .

The equation A β sd λx. C is not typable. This concludes the case.

• Rule (@ π ) and (@ @ ): Similar to the previous case.

Nevertheless, the reducts of a typable system are not necessarily typable, as the following example shows.

Example 6.4 (Reducts of a typable system). Suppose given the equation XY β sd f a.

and a is of type r where ι, r and s are three different basic types then the equation is a typable system. Nevertheless, by applying the transformation rule (@ @ ) we get the system (X β sd f ) ∪ (Y β sd a) which is not typable. By the way, this equation has a solution {λx. x/X, f a/Y } which is typable.

At this point, one may wonder if there exists a second-order typable β sd -equation with only untypable solutions. If no, one would prove the NP-completeness of matching modulo superdevelopments from the NP-completeness of second-order matching [START_REF] Denver | The complexity of unification[END_REF]. But the answer is positive as the following example shows. Example 6.5 (Typable β sd -equation with only untypable solutions). Let a and b two constants of type r. Let f be a constant of type r → ι and let g be a constant of type ι → ι → ι. Let X be a matching variable of type s → ι. Let Y and Z be two matching variables of type s. Let us consider the second-order typable equation

The equation XY β sd f a has 5 solutions given by

In the same way, the equation XZ β sd f b has 5 solutions given by:

In each case, only one solution is typable: X β sd λx. f a and X β sd λx. f b respectively. But these solutions are of course incompatible. The only solution to the initial equation is

which is untypable. We have exhibited a second-order β-equation with no solution while the corresponding β sd -equation has one.

6.2.2. Second-order matching algorithm based on superdevelopments. The context of this section is the typed λ-calculus. We want to determine β-matches of second-order equations.

Note that the η-rule does not have a fundamental impact on the algorithm. This section could have be written for second-order matching modulo βη (including the paragraph related to the comparison with Huet and Lang algorithm).

First, we can remark that we can restrict ourselves to typable equations (this is justified by Proposition 6.2). Then the rule given in Figure 1 are applied only if the system obtained after reduction is typable. This is a common restriction when dealing with higher-order matching in a typed context (see for example the rule (Projection)).

Moreover, we have shown (Proposition 3.10) that every β-match of a second-order equation is also a β sd -match for the corresponding equation. We thus deduce that the algorithm given in Figure 1 applied in a typed context (only typable systems) gives an algorithm for second-order matching Theorem 6.6 (Second-order matching algorithm). The rules of Figure 1 applied in a typed context give a sound and complete algorithm for second-order matching.

We illustrate the algorithm on an example.

Example 6.7. We consider the equation λx. X(x, a) βη λx. f (a, x, a) given in example 6.1.

We first apply the rule (λ λ ) to remove all head λ-abstractions. We now look at the different opportunities to apply the (@ β ) rule, namely how we can instantiate the terms B 1 and B 2 (following the notations used in Fig. 1). Since we must have a β sd B 2 , necessarily B 2 = a.

Then there are three choices for B 1

(1) B 1 = λy 2 . f (y 2 , x, y 2 ) ;

(2) B 1 = λy 2 . f (y 2 , x, a) ;

(3) B 1 = λy 2 . f (a, x, y 2 ).

Each of these choices lead to the solutions {λy 1 y 2 . f (y 2 , y 1 , y 2 )/X} {λy 1 y 2 . f (y 2 , y 1 , a)/X} {λy 1 y 2 . f (a, y 1 , y 2 )/X} Finally, by applying the rule (@ π ) we found the fourth solution given by {λy 1 y 2 . f (a, y 1 , a)/X}.