Adel Bouhoula
email: adel.bouhoula@supcom.rnu.tn

Florent Jacquemard
email: florent.jacquemard@inria.fr

Automated Induction with Constrained Tree Automata

We propose a procedure for automated implicit inductive theorem proving for equational specifications made of rewrite rules with conditions and constraints. The constraints are interpreted over constructor terms (representing data values), and may express syntactic equality, disequality, ordering and also membership in a fixed tree language. Constrained equational axioms between constructor terms are supported and can be used in order to specify complex data structures like sets, sorted lists, trees, powerlists... Our procedure is based on tree grammars with constraints, a formalism which can describe exactly the initial model of the given specification (when it is sufficiently complete and terminating). They are used in the inductive proofs first as an induction scheme for the generation of subgoals at induction steps, second for checking validity and redundancy criteria by reduction to an emptiness problem, and third for defining and solving membership constraints. We show that the procedure is sound and refutationally complete. It generalizes former test set induction techniques and yields natural proofs for several non-trivial examples presented in the paper, these examples are difficult (if not impossible) to specify and carry on automatically with other induction procedures.

Introduction

Given a specification R of a program or system S made of equational Horn clauses, proving a property P for S generally amounts to show the validity of P in the minimal Herbrand model of R, also called initial model of R (inductive validity). In this perspective, it is important to have automated induction theorem proving procedures supporting a specification language expressive enough to axiomatize complex data structures like sets, sorted lists, powerlists, complete binary trees, etc. Moreover, it is also important to be able to automatically generate induction schemas used for inductive proofs in order to minimize user interaction. However, theories of complex data structures generate complex induction schemes, and the automation of inductive proofs is therefore difficult for such theories.

It is common to assume that R is built with constructor function symbols (to construct terms representing data) and defined symbols (representing the operations defined on constructor terms). Assuming in addition the sufficient completeness of R (every ground (variable-free) term is reducible, using the axioms of R, to a constructor term) and the strong termination of the axioms of R, a set of representants for the initial model of R (the model in which we want to proof the validity of conjectures) is the set of ground constructor terms not reducible by R C (the subset of equations of R between terms made of constructor symbols), called constructor normal forms.

In the case where the constructors are free (R C = ∅), the set of constructor normal forms is simply the set of ground terms built with constructors and it is very easy to define an induction schema. This situation is therefore convenient for inductive reasoning, and many inductive theorem provers require free constructors, termination and sufficient completeness. However, it is not expressive enough to define complex data structures. With rewrite rules between constructors, the definition of induction schema is more complex, and requires a finite description of the set of constructor normal-forms. Some progress has been done e.g. in [START_REF] Bouhoula | Automata-driven automated induction[END_REF] and [START_REF] Bouhoula | Specification and proof in membership equational logic[END_REF] in the direction of handling specification with non-free constructors, with severe restrictions (see related work below).

Tree automata (TA), or equivalently regular tree grammars, permit a finite representation of the set of constructor normal-forms when R C is a left-linear rewrite system (set of rewrite rules without multiple occurrences of variables in their left-hand-sides). Indeed, on one hand TA can do linear pattern-matching, hence they can recognize terms which are reducible by R C , and on the other hand, the class of TA languages is closed under complementation. When the axioms of R C are not linear, or are constrained, some extensions of TA (or grammars) are necessary, with transitions able to check constraints on the term in input, see e.g. [START_REF] Comon | Tree automata techniques and applications[END_REF].

In this paper, we propose a framework for inductive theorem proving for theories containing constrained rewrite rules between constructor terms and conditional and constrained rewrite rules for defined functions. The key idea is a strong and natural integration of tree grammars with constraints in an implicit induction procedure, where they are used as induction schema. Very roughly, our procedure starts with the automatic computation of an induction schema, in the form of a constrained tree grammar generating constructor normal form. This grammar is used later for the generation of subgoals from a conjecture C, by instantiation of variables using the grammar's production rules, triggering induction steps during the proof. All generated subgoals are either deleted, following some criteria, or they are reduced, using axioms or induction hypotheses, or conjectures not yet proved, providing that they are smaller than the goal to be proved. Reduced subgoals become then new conjectures and C becomes an induction hypothesis. Moreover, constrained tree grammars are used as a decision procedure for checking the deletion criteria during induction steps.

Our method subsumes former test set induction procedures like [START_REF] Bouhoula | Implicit induction in conditional theories[END_REF][START_REF] Bouhoula | Automated theorem proving by test set induction[END_REF][START_REF] Bouhoula | Automata-driven automated induction[END_REF], by reusing former theoretical works on tree automata with constraints. It is sound and refutationally complete (any conjecture that is not valid in the initial model will be disproved) when R is sufficiently complete and the constructor subsystem R C is terminating. Without the above hypotheses, it still remains sound and refutationally complete for a restricted kind of conjectures, where all the variables are constrained to belong to the language of constructor normal forms. This restriction is expressible in the specification language (see below). When the procedure fails, it implies that the conjecture is not an inductive theorem, provided that R is strongly complete (a stronger condition for sufficient completeness) and ground confluent. There is no requirement for termination of the whole set of rules R, unlike [START_REF] Bouhoula | Implicit induction in conditional theories[END_REF][START_REF] Bouhoula | Automated theorem proving by test set induction[END_REF], but instead only for separate termination of the respective sets of rules for defined function and for the constructors.

Moreover, if a conjecture C restricted as above is proved in a sufficiently complete specification R and R is further consistently extended into R with additional axioms for specifying partial (non-constructor) functions, then the former proof of C remains valid in R , see Section 5.

The support of constraints permits in some cases to use the constrained completion technique of [START_REF] Kirchner | Deduction with symbolic constraints[END_REF] in order to transform a non-terminating theory into a terminating one, by the addition of ordering constraints in constructor rules, see Section 4.5. It permits in particular to make proofs modulo non orientable axioms, without having to modify the core of our procedure.

We shall consider a specification of ordered lists as a running example throughout the paper. Consider first non-stuttering lists (lists which do not contain two equal successive elements) built with the constructor symbols ∅ (empty list) and ins (list insertion) and following this rewrite rule:

ins(x, ins(x, y)) → ins(x, y) ( c 0 )
Rewrite rules can be enriched with constraints built on predicates with a fixed interpretation on ground constructor terms. For example, using ordering constraints built with we can specify ordered lists by the following axiom:

ins(x 1 , ins(x 2 , y)) → ins(x 2 , ins(x 1 , y)) x 1 x 2 (c 1 )
Another interesting example is the case of membership constraints of the form x : L where L is a fixed regular tree language (containing only terms made of constructor symbols). We consider also stronger constraints which restrict constructor terms to be in normal form (i.e. not reducible by the axioms). Let us come back to the example of non-stuttering sorted lists (sorted lists without duplication), and add to the above rules the axioms below which define a membership predicate , using the information that lists are sorted:

x ∅ → false (m 0 ) x 1 ins(x 2 , y 2 ) → true x 1 ≈ x 2 (m 1 ) x 1 y 1 → false y 1 ≈ ins(x 2 , y 2 ), x 1 ≺ x 2 , y 1 :NF (m 2 ) x 1 ins(x 2 , y 2 ) → x 1 y 2 x 2 ≺ x 1 (m 3 )
The constraint y 1 :NF expresses the fact that this subterm is a constructor term in normal form, i.e. that it is a sorted list. Without this constraint, the specification would be inconsistent. Indeed, let us consider the ground term t = 0 ins(s(0), ins(0, ∅)). This term t can be reduced into both true and false, since ins(s(0), ins(0, ∅)) is not in normal form. Using constraints of the form . : NF as above also permits the user to specify, directly in the rewrite rules, some adhoc reduction strategies for the application of rewriting. Such strategies include for instance several refinements of the innermost strategy which corresponds to the call by value computation in functional programming languages, where arguments are fully evaluated before the function application. Related work. The principle of our procedure is close to test-set induction approaches [START_REF] Bouhoula | Implicit induction in conditional theories[END_REF][START_REF] Bouhoula | Automated theorem proving by test set induction[END_REF]. The real novelty here is that test-sets are replaced by constrained tree grammars, the latter being more precise induction schemes. Indeed, they provide an exact finite description of the initial model of the given specification, (under some assumptions like sufficient completeness and termination for axioms), whereas cover-sets and test-sets are over-approximative in similar cases.

The first author and Jouannaud [START_REF] Bouhoula | Automata-driven automated induction[END_REF] have used tree automata techniques to generalize test set induction to specifications with non-free constructors. This work has been generalized in [START_REF] Bouhoula | Specification and proof in membership equational logic[END_REF] for membership equational logic. These approaches, unlike the procedure presented in this paper, work by transforming the initial specification in order to get rid of rewrite rules for constructors. Moreover, the axioms for constructors are assumed to be unconstrained and unconditional left-linear rewrite rules, which is still too restrictive for the specification of structures like sets or sorted lists... Kapur [15] has proposed a method (implemented in the system RRL) for mechanizing cover set induction if the constructors are not free. This handles in particular the specification of powerlists or sorted lists. We show in Section 5 how our method can address similar problems.

We describe in [START_REF] Bouhoula | Automated induction with constrained tree automata[END_REF] two proofs, done resp. by Jared Davis and Sorin Stratulat, of a conjecture on sorted lists, done resp. by Jared Davis and Sorin Stratulat, with ACL2 using a library for ordered sets [START_REF] Davis | Finite set theory based on fully ordered lists[END_REF] and with SPIKE [START_REF] Bouhoula | Implicit induction in conditional theories[END_REF][START_REF] Bouhoula | Automated theorem proving by test set induction[END_REF][START_REF] Stratulat | A general framework to build contextual cover set induction provers[END_REF]. Both proofs require the addition of non-trivial lemmas whereas our procedure can prove the conjecture without additional lemma.

Preliminaries

The reader is assumed familiar with the basic notions of term rewriting [START_REF] Dershowitz | Rewrite systems[END_REF] and first-order logic. Notions and notations not defined here are standard. Terms and substitutions. We assume given a many sorted signature (S, F ) (or simply F , for short) where S is a set of sorts and F is a finite set of function symbols with arities. We assume moreover that the signature F comes in two parts, F = C D where C a set of constructor symbols, and D is a set of defined symbols. Let X be a family of sorted variables. We sometimes denote variables with sort exponent like x S in order to indicate that x has sort S ∈ S. The set of well-sorted terms over F (resp. constructor well-sorted terms) with variables in X will be denoted by T (F , X ) (resp. T (C, X )). The subset of T (F , X ) (resp. T (C, X )) of variable-free terms, or ground terms, is denoted T (F ) (resp. T (C)). We assume that each sort contains a ground term. The sort of a term t ∈ T (F , X ) is denoted sort (t).

A term t is identified as usual with a function from its set of positions (strings of positive integers) Pos(t) to symbols of F and X , where positions are strings of positive integers. We denote the empty string (root position) by Λ. The length of a position p is denoted |p|. The depth of a term t, denoted d (t), is the maximum of {|p| | p ∈ Pos(t)}. The subterm of t at position p is denoted by t| p . The result of replacing t| p with s at position p in t is denoted by t[s] p . This notation is also used to indicate that s is a subterm of t, in which case p may be omitted. We denote the set of variables occurring in t by var (t). A term t is linear if every variable of var (t) occurs exactly once in t.

A substitution is a finite mapping {x 1 → t 1 , . . . , x n → t n } where x 1 , . . . , x n ∈ X and t 1 , . . . t n ∈ T (F , X ). As usual, we identify substitutions with their morphism extension to terms. A variable renaming is a substitution mapping variables to variables. We use postfix notation for substitutions application and composition. A substitution σ is grounding for a term t if tσ is ground.

Constraints and constrained terms. We assume given a constraint language L, which is a finite set of predicate symbols with a recursive Boolean interpretation in the domain of ground constructor terms of T (C). Typically, L may contain the syntactic equality . ≈ . (syntactic disequality . ≈ .), some (recursive) simplification ordering . ≺ . on ground constructor terms (for instance a lexicographic path ordering [START_REF] Dershowitz | Rewrite systems[END_REF]), and membership . :L to a fixed tree language L ⊆ T (C) (like for instance the languages of well sorted terms or constructor terms in normal-form). Constraints on the language L are Boolean combinations of atoms of the form P (t 1 , . . . , t n ) where P ∈ L and t 1 , . . . , t n ∈ T (C, X ). By convention, an empty combination is interpreted to true.

The application of substitutions is extended from terms to constraints in a straightforward way, and we may therefore define a solution for a constraint c as a (constructor) substitution σ grounding for all terms in c and such that cσ is interpreted to true. The set of solutions of the constraint c is denoted sol (c). A constraint c is satisfiable if sol (c) = ∅ (and unsatisfiable otherwise).

A constrained term t c is a linear term t ∈ T (F , X ) together with a constraint c, which may share some variables with t. Note that the assumption that t is linear is not restrictive, since any non linearity may be expressed in the constraint, for instance f (x, x) c is semantically equivalent to f (x, x ) c ∧ x ≈ x , where the variable x does not occur in c.

Constrained clauses. A literal is an equation

s = t or a disequation s = t or an oriented equation s → t between two terms. A constrained clause C c is a disjunction C of literals together with a constraint c. A constrained clause C c is said to subsume a constrained clause C c if there is a substitution σ such that Cσ is a sub-clause of C and c ∧ ¬cσ is unsatisfiable. A tautology is a constrained clause s 1 = t 1 ∨ . . . ∨ s n = t n d such that d is a conjunction of equational constraints, d = u 1 ≈ v 1 ∧ . . . ∧ u k ≈ v k and there exists i ∈ [1.
.n] such that s i σ = t i σ where σ is the mgu of d.

Constrained rewriting. A conditional constrained rewrite rule is a constrained clause of the form Γ ⇒ l → r c such that Γ is a conjunction of equations, called the condition of the rule, the terms l and r (called resp. left-and right-hand side) are linear and have the same sort, and c is a constraint. When the condition Γ is empty, it is called a constrained rewrite rule. A set of conditional constrained, resp. constrained, rules is called a conditional constrained (resp. constrained ) rewrite system. Let R be a conditional constrained rewrite system. The relation s d rewrites to t d by R, denoted s d --→ R t d , is defined recursively by the existence of a rule ρ ≡ Γ ⇒ → r c ∈ R, a position p ∈ Pos(s), and a substitution σ such that s| p = σ, t| p = rσ, dσ ∧ ¬cσ is unsatisfiable, and uσ ↓ R vσ for all u = v ∈ Γ . The transitive and reflexive transitive closures, of

--→ R are denoted --→ + R and --→ * R , and u ↓ R v stands for ∃w, u --→ * R w ← -- * R v.
Note the semantical difference between conditions and constraints in rewrite rules. The validity of the condition is defined wrt the system R whereas the interpretation of constraint is fixed and independent from R.

A constrained term s c is reducible by R if there is some t c such that

s c --→ R t c . Otherwise s c is called irreducible, or an R-normal form. A substitution σ is irreducible by R if its image contains only R-normal forms.
A constrained term t c is ground reducible (resp. ground irreducible) if tσ is reducible (resp. irreducible) for every irreducible solution σ of c grounding for t.

The system R is terminating if there is no infinite sequence

t 1 --→ R t 2 --→ R . . ., R is ground confluent if for any ground terms u, v, w ∈ T (F ), v ← -- * R u --→ * R w, implies that v ↓ R
w, and R is ground convergent if R is both ground confluent and terminating. The depth of a non-empty set R of rules, denoted d (R), is the maximum of the depths of the left-hand sides of rules in R.

Constructor specifications. We assume from now on given a conditional constrained rewrite system R. The subset of R containing only function symbols from

C is denoted R C and R \ R C is denoted R D . Inductive theorems. A clause C is a deductive theorem of R (denoted R |= C) if it is valid in any model of R. A clause C is an inductive theorem of R (denoted R |= Ind C) iff
for all for all substitution σ grounding for C, R |= Cσ.

We shall need below to generalize the definition of inductive theorems to constrained clauses as follows: a constrained clause C c is an inductive theorem of R (denoted R |= Ind C c ) if for all substitutions σ ∈ sol (c) grounding for C we have R |= Cσ.

Completeness. A function symbol f ∈ D is sufficiently complete wrt R iff for all t 1 , . . . , t n ∈ T (C), there exists t in T (C) such that f (t 1 , . . . , t n ) --→ + R t.
We say that the system R is sufficiently complete iff every defined operator f ∈ D is sufficiently complete wrt R. Let f ∈ D be a function symbol and let:

Γ 1 ⇒ f (t 1 1 , . . . , t 1 k ) → r 1 c 1 , . . . , Γ n ⇒ f (t n 1 , . . . , t n k ) → r n c n
be a maximal subset of rules of R D whose left-hand sides are identical up to variable renamings µ 1 , . . . , µ n , i.e.

f (t 1 1 , . . . , t 1 k )µ 1 = f (t 2 1 , . . . , t 2 k )µ 2 = . . . f(t n 1 , . . . , t n k )µ n .
We say that f is strongly complete wrt R (see [START_REF] Bouhoula | Automated theorem proving by test set induction[END_REF]) if f is sufficiently complete wrt R and R |= Ind Γ 1 µ 1 c 1 µ 1 ∨ . . . ∨ Γ n µ n c n µ n for every subset of R as above. The system R is said strongly complete if every function symbol f ∈ D is strongly complete wrt R.

Constrained Grammars

Constrained tree grammars have been introduced in [START_REF] Comon | Unification et disunification[END_REF], in the context of automated induction. The idea of using such formalism for induction theorem proving is also in e.g. [START_REF] Bouhoula | Automata-driven automated induction[END_REF][START_REF] Comon-Lundh | Handbook of Automated Reasoning, chapter Inductionless Induction[END_REF], because it is known that they can generate the languages of normal-forms for arbitrary term rewriting systems. We present in this section the definitions and results suited to our purpose. Definition 1. A constrained grammar G = (Q, ∆) is given by: 1. a finite set Q of non-terminals of the form u , where u is a linear term of T (F , X ), 2. a finite set ∆ of production rules of the form v := f ( u 1 , . . . , u n ) c where f ∈ F, v , u 1 ,. . . , u n ∈ Q (modulo variable renaming) and c is a constraint.

The non-terminals are always considered modulo variable renaming. In particular, we assume wlog (for technical convenience) that the above term f (u 1 , . . . , u n ) is linear and that var (v) ∩ var (f (u 1 , . . . , u n )) = ∅.

Term Generation

We associate to a given constrained grammar G = (Q, ∆) a finite set of new unary predicates of constraint of the form . : u , where u ∈ Q (modulo variable renaming). Constraints of the form t: u called membership constraints and their interpretation is given below. The production relation between constrained terms y G is defined by:

t[y] y: v ∧d y G t[f (y 1 , . . . , y n )] y 1 : u 1 ∧ . . . ∧ y n : u n ∧c ∧ dτ if there exists v := f ( u 1 , . . . , u n ) c ∈ ∆ such that f (u 1 , . . . , u n ) =
vτ , and y 1 ,. . . ,y n are fresh variables. The variable y, constrained to be in the language defined by the non-terminal v is replaced by f (y 1 , . . . , y n ) where the variables y 1 , . . . , y n are constrained to the respective languages of non-terminals u 1 , . . . , u n . The union of the relations y G for all y is denoted G and the reflexive transitive and transitive closures of the relation G are respectively denoted by * G and + G (G may be omitted). Definition 2. The language L(G, u ) is the set of ground terms t generated by G from a non-terminal u , i.e. such that y y: u * t c where c is satisfiable.

Given Q ⊆ Q, we write L(G, Q ) = u ∈Q L(G, u ) and L(G) = L(G, Q). Given a constrained grammar G = (Q, ∆), we can now define sol (t: u ), where u ∈ Q, as {σ | tσ ∈ L(G, u )}.
Example 1. Let us consider the sort Nat of natural integers built with the constructor symbols 0 and s. These terms are generated by the grammar with production rules x Nat := 0 and x Nat := s( x 2 Nat ). 3

Normal Forms

In [START_REF] Bouhoula | Automated induction with constrained tree automata[END_REF], we present the automatic construction of a constrained grammar

G NF (R C ) = (Q NF (R C ), ∆ NF (R C ))
which generates the language of ground R Cnormal forms. Its construction is a generalization of the one of [START_REF] Comon | Ground reducibility is exptime-complete[END_REF]. Intuitively, it corresponds to the complementation and completion of a grammar for R Creducible terms (such a grammar does mainly pattern matching of left members of rewrite rules), where every subset of states (for the complementation) is represented by the most general common instance of its elements (if they are unifiable). Due to space limitations, we cannot describe the general construction of G NF (R C ) here but we rather present the case where R C contains the constructor axioms given in introduction.

Example 2. Let R C contain the axioms (c 0 ) and (c 1 ) given in introduction. Let G NF (R C ) contain the two productions rules given Example 1 and x Set := ∅, ins(x, y) := ins( x Nat , x Set ) (for singleton lists) and ins(x, y) := ins( x Nat , ins(x 2 , y 2 ) ) x Nat ≺ x 2 . Note that the variables in the non terminal ins(x 2 , y 2 ) in the right member of the latter production rule have been renamed in order to be distinguished from the variables in the non terminal in the left member. This grammar G NF (R C ) generates the set of ground constructor terms in normal-form for R C . They represent the ordered lists of natural numbers (of sort List). 3

Inference System

In this section, we present an inference system for our inductive theorem proving procedure. The principle is the following: given a goal (conjecture) C, we use the grammar G NF (R C ) of Section 3.2 in order to expand C into some subgoals. All the generated subgoals must then either be deleted, following some criteria, or be reduced, using axioms or induction hypotheses, or conjectures not yet proved, providing that they are smaller than the goal to be proved. Reduced subgoals become then new conjectures and C becomes an induction hypothesis. The deletion criteria include tautologies, forward subsumption, clauses with an unsatisfiable constraint, and constructor clause that can be detected as inductively valid, under some conditions defined precisely below. The decision of these criteria, using G NF (R C ), is discussed in Section 4.6.

The reduction of subgoals is performed with the rules defined in Sections 4.1 and 4.2. If a subgoal generated cannot be deleted or reduced, then the procedure stop with a refutation (the initial goal is not an inductive theorem of R). If every subgoal is deleted, then the initial goal is an inductive theorem of R.

The procedure may not terminate (the conditions in inference rules other than the deletion criteria are recursive calls of the procedure of the form R |= Ind subgoal ). In this case appropriate lemmas should be added by the user in order to achieve termination.

Simplification Rules for Defined Functions

Our procedure uses the simplification rules for defined symbols presented in Figure 1. They simplify constrained clauses according to R D and to a set H of induction hypotheses (constrained clauses), which is given as the second component of the left-hand sides of rules. Inductive Rewriting simplifies goals using the axioms as well as instances of the induction hypotheses of H, provided that they are smaller than the goal. The underlying induction principle is based on a well-founded ordering on constrained clauses (see [START_REF] Bouhoula | Automated induction with constrained tree automata[END_REF]). This approach is more general than structural induction which is more restrictive concerning simplification with induction hypotheses (see e.g. [START_REF] Bouhoula | Implicit induction in conditional theories[END_REF]). Inductive Contextual Rewriting can be viewed as a generalization of a rule in [START_REF] Zhang | Implementing contextual rewriting[END_REF] to handle constraints by recursively discharging them as inductive conjectures. Rewrite Splitting simplifies a clause which contains a subterm matching some left member of rule of R D . This inference checks moreover that all cases are covered for the application of R D , i.e. that for each ground substitution τ , the conditions and the constraints of at least one rule is true wrt τ . Note that this condition is always true when R is sufficiently complete, and hence that this check is superfluous in this case. Inductive Deletion deletes tautologies and clauses with unsatisfiable constraints. H misleading in Fig. 2 add C c to H here but alread used for simplification before.

Induction Inference Rules

The main inference system is displayed in Figure 3. Its rules apply to pairs (E, H) whose components are respectively the sets of current conjectures and of inductive hypotheses. Two inference rules below, Narrowing and Inductive Narrowing, use the grammar G NF (R C ) for instantiating variables. In order to be able to apply these inferences, we shall initiate the process by adding to the conjectures one membership constraint for each variable.

i ∈ [1..n], u i ∈ Q NF (R C ), sort (u i ) = sort (x i
), and d does not contain membership constraints. Simplification, resp. Inductive Simplification, reduces conjectures according to the rules of Section 4.2, resp. 4.1. Inductive Narrowing generates new subgoals by application of the production rules of the constrained grammar G NF (R C ) until the obtained clause is deep enough to cover left-hand side of rules of R D . Each obtained clause must be simplified by one the rules of Figure 1 (otherwise, if one instance cannot be simplified, then the rule Inductive Narrowing cannot be applied). For sake of efficiency, the application can be restricted to so called induction variables, as defined in [START_REF] Bouhoula | Automated theorem proving by test set induction[END_REF] while preserving all the results of the next section. Narrowing is similar and uses the rules of Figure 2 for simplification. This rule permits to eliminate the ground reducible constructor terms in a clause by Simplification:

E ∪ C c , H E ∪ E , H if C c →C E Inductive Simplification: E ∪ C c , H E ∪ E , H if {C c }, E ∪ H →D E Narrowing: E ∪ C c , H E ∪ E1 ∪ . . . ∪ En, H ∪ {C c } if Ci ci →C Ei, where {C1 c1 , . . . , Cn cn } is the set of all clauses such that C c * Ci ci and d (Ci) -d (C) ≤ d (R) -1 Inductive Narrowing: E ∪ C c , H E ∪ E1 ∪ . . . ∪ En, H ∪ {C c } if Ci ci , E ∪ H ∪ {C c } →D Ei, where {C1 c1 , . . . , Cn cn } is the set of all clauses such that C c + Ci ci and d (Ci) -d (C) ≤ d (R) -1 Subsumption: E ∪ C c , H (E , H) if C c is subsumed by another clause of R ∪ E ∪ H Disproof: E ∪ C c , H (⊥, H)
if no other rule applies to the clause C c simplifying their instances, while deriving conjectures considered as new subgoals. The criteria on depth is the same for Inductive Narrowing and Narrowing and is a bit rough, for sake of clarity of the inference rules. However, in practice, it can be replaced by a tighter condition (with, e.g., a distinction between R C and R D ) while preserving the results of the next section. Subsumption deletes clauses redundant with axioms of R, induction hypotheses of H and other conjectures not yet proved (in E).

Example 3. Let us come back to the running example of sorted lists, with the constructor system R C containing (c 0 ) and (c 1 ) and the defined system R D containing the axioms (m 0 -m 3 ) given in introduction3 together with the following axioms defining a variant ∈ for the membership:

x ∈ ∅ → false (m 0 ) x 1 ∈ ins(x 2 , y) → true x 1 ≈ x 2 (m 1 ) x 1 ∈ ins(x 2 , y) → x 1 ∈ y x 1 ≈ x 2 (m 2 )
We show, using our procedure, that the conjecture x y = x ∈ y is an inductive theorem of R, i.e. that the two variants and ∈ of membership are equivalent. The normal-form grammar G NF (R C ) is described in example 2. The decoration of the conjecture with its non-terminal gives the two clauses: x y = x ∈ y x: x Nat , y: x Set and x y = x ∈ y x: x Nat , y: ins(x 1 , y 1 ) .

The application of the production rules of G NF (R C ) to the first of these clauses (in Narrowing) gives: x ∅ = x ∈ ∅ which is reduced, using (m 0 ) and (m 0 ), to the tautology false = false. For the second clause, applying G NF (R C ) returns:

x ins(x 1 , ∅) = x ∈ ins(x 1 , ∅) x, x 1 : x Nat (1)
x

ins(x 1 , ins(x 2 , ∅)) = x ∈ ins(x 1 , ins(x 2 , ∅)) x, x 1 , x 2 : x Nat , x 1 ≺ x 2 (2) x ins(x 1 , ins(x 2 , y 2 )) = x ∈ ins(x 1 , ins(x 2 , y 2 )) x, x 1 , x 2 : x Nat , y 2 : ins(x 3 , y 3 ) , x 1 ≺ x 2 , x 2 ≺ x 3 (3)
The subgoals ( 1) and ( 2) can be simplified by Rewrite Splitting with (m 1 ), (m 2 ) and (m 3 ) into clauses reduced into tautologies (see [START_REF] Bouhoula | Automated induction with constrained tree automata[END_REF] for details).

The subgoal (3) is implified by Rewrite Splitting with (m 1 -m 3 ) into 3 clauses. Let us consider the third one, obtained with (m 3 ):

x ins(x 2 , y 2 ) = x ∈ ins(x 1 , ins(x 2 , y 2 )) x, x 1 , x 2 , x 3 : x Nat , y 2 : ins(x 3 , y 3 ) , x 1 ≺ x 2 , x 2 ≺ x 3 , x 1 ≺ x .
It is simplified by Inductive Rewriting with (m 2 ) into:

x ins(x 2 , y 2 ) = x ∈ ins(x 2 , y 2 ) x, x 2 , x 3 : x Nat , y 2 : ins(x 3 , y 3 ) , x 2 ≺ x 3 . At this point, we are allowed to use the conjecture x y = x ∈ y as an induction hypothesis with Inductive Rewriting, it returns the tautology:

x ins(x 2 , y 2 ) = x ins(x 2 , y 2 ) x, x 2 , x 3 : x Nat , y 2 : ins(x 3 , y 3 ) , x 2 ≺ x 3

The ommited details in the proof of the conjecture can be found in [START_REF] Bouhoula | Automated induction with constrained tree automata[END_REF]. Note that this proof does not require the manual addition of lemma. 3

Soundness and Completeness

We show now that our inference system is sound and refutationally complete.

The proof of soundness is not straightforward. The main difficulty is to make sure that the exhaustve application of the rules preserve a counterexample when one exists. We will show more precisely that a minimal counterexample is preserved along a fair derivation.

A derivation is a sequence of inference steps generated by a pair of the form (E 0 , ∅), using the inference rules in I, written (E 0 , ∅) I (E 1 , H 1 ) I . . . It is called fair if the set of persistent constrained clauses (∪ i ∩ j≥i E j ) is empty or equal to {⊥}. The derivation is said to be a disproof in the latter case, and a success in the former.

Finite success is obtained when the set of conjectures to be proved is exhausted. Infinite success is obtained when the procedure diverges, assuming fairness. When it happens, the clue is to guess some lemmas which are used to subsume or simplify the generated infinite family of subgoals, therefore stopping the divergence. This is possible in principle with our approach, since lemmas can be specified in the same way as axioms are.

Theorem 1 (Soundness of successful derivations). Assume that R C is terminating and that R is sufficiently complete. Let D 0 be a set of unconstrained clauses and let E 0 = decorate(D 0 ). If there exists a successful derivation

(E 0 , ∅) I (E 1 , H 1 ) I • • • then R |= Ind D 0 .
Proof. (sketch, see [START_REF] Bouhoula | Automated induction with constrained tree automata[END_REF] for a complete proof). The proof uses the fact that, under the hypotheses of Theorem 1, R |= Ind E 0 implies R |= Ind D 0 .

Intuitively, the reason is that in order to show that R |= Ind D 0 , it is sufficient to show that R |= D 0 σ for all substitutions σ whose images contain only ground constructor terms in normal form. Every ground σ can indeed be normalized into a substitution of this form because R C is terminating and R sufficiently complete. By definition of the decoration, the membership constraints and by construction of G NF (R C ), this sufficient condition is a consequence of R |= Ind E 0 .

We then show that R |= Ind E 0 by minimal counter-example. Assume that R |= Ind E 0 and let D 0 be a clause, minimal wrt , in the set: Let C c be a clause of ∪ i E i minimal by subsumption ordering and θ ∈ sol (c), irreducible and constructor ground substitution, be such that Cθ = D 0 . We show in [START_REF] Bouhoula | Automated induction with constrained tree automata[END_REF] that whatever inference, other than Disproof, is applied to C c , a contradiction is obtained, hence that the above derivation is not successful.

Dσ D d ∈ ∪ i E i , σ ∈ sol (d)
Since there are only two kinds of fair derivations, we obtain as a corollary:

Corollary 1 (Refutational completeness). Assume that R C is terminating and that R is sufficiently complete. Let D 0 be a set of unconstrained clauses and let E 0 = decorate(D 0 ). If R |= Ind E 0 , then all fair derivations starting from (E 0 , ∅) end up with (⊥, H).

When we assume that all the variables in goals are decorated (restricting the domain for this variables to ground constructor irreducible terms), the above hypotheses that R C is terminating and R is sufficiently complete can be dropped.

Theorem 2 (Soundness of successful derivations). Let E 0 be a set of decorated constrained clauses. If there exists a successful derivation (E 0 , ∅)

I (E 1 , H 1 ) I • • • then R |= Ind E 0 .
Proof. (sketch). We use the second part of the proof of Theorem 1 (which does not use the sufficient completeness of R and termination of R C ). With the hypothesis that the clauses of E 0 are decorated, the fact given at the beginning of this proof is indeed no more needed (D 0 = E 0 ). The restriction to substitutions into ground constructor normal forms in order to show that R |= Ind E 0 is made explicit by the membership constraints in the decoration.

Corollary 2 (Refutational completeness). Let E 0 be a set of decorated constrained clauses. If R |= Ind E 0 , then all fair derivations starting from (E 0 , ∅) end up with (⊥, H).

We shall see in Section 5 some example of applications of Theorem 2 and Corollary 2 to specifications which are not sufficiently complete.

Theorem 3 (Soundness of disproof ). Assume that R is strongly complete and ground confluent. If a derivation starting from (E 0 , ∅) returns the pair (⊥, H), then R |= Ind E 0 .

Handling Non-Terminating Constructor Systems

Our procedure applies rules of R C and R D only when they reduce the terms wrt the given simplification ordering >. This is ensured when the rewrite relation induced by R C and R D is compatible with >, and hence that R C and R D are terminating (separately). Note that this is in contrast with other procedures like [START_REF] Kirchner | Deduction with symbolic constraints[END_REF] where the termination of the whole system R is required.

If R C is non-terminating then one can apply a constrained completion technique [START_REF] Kirchner | Deduction with symbolic constraints[END_REF] in order to generate an equivalent orientable theory (with ordering constraints). The theory obtained (if the completion succeeds) can then be handled by our approach.

Example 4. Consider this non-terminating system for sets: {ins(x, ins(x, y)) = ins(x, y), ins(x, ins(x , y)) = ins(x , ins(x, y))}. Applying the completion procedure we obtain the constrained rules (c 0 ) and (c 1 ). 3

Decision Procedures for Conditions in Inferences

Constrained tree grammars are involved in the inferences Narrowing and Inductive Narrowing in order to generate subgoals from goals, by instantiation using the productions rules. They are also the key for the decision procedures applied in order to check the conditions of constraint unsatisfiability (in rules for rewriting and Inductive Deletion, Deletion, Subsumption), ground irreducibility and validity of ground irreducible constructor clauses (in the rules Validity, hence Simplification, and Disproof). These conditions are decided by reduction into the decision problem of emptiness (of L(G, u )) for constrained tree grammars build from G NF (R C ). The decision rely on similar decision results for constrained tree automata, some cases are summarized in [START_REF] Comon | Tree automata techniques and applications[END_REF]. The reductions are detailed in [START_REF] Bouhoula | Automated induction with constrained tree automata[END_REF].

Handling Partial Specifications

The example of sorted lists (Example 3) can be treated with our procedure because it is based on a sufficiently complete and ground confluent conditional constrained TRS R whose constructor part R C is terminating. Indeed, under these hypotheses, Theorem 1 ensures the soundness of our procedure for proving inductive conjectures on this specification, and Corollary 1 and Theorem 3 ensure respectively refutational completeness and soundness of disproof. For sound proofs of inductive theorems wrt specifications which are not sufficiently complete, we can rely on Theorem 2 and Corollary 2 which do not require sufficient completeness of the specification but instead suppose that the conjecture is decorated, i.e. that each of its variables is constrained to belong to a language associated to a non-terminal of the normal-form (constrained) grammar. In this section, we propose two applications of this principle of decoration of conjectures to the treatment of partial specifications. Partially Defined Functions. An inductive proof of a decorated conjecture C in R remains valid in an extension of R (possibly not complete).

Theorem 4. Assume that R is sufficiently complete and let R be an consistent extension of R where R C = R C and R D = R D ∪ R D (R D defines additional partial defined functions). Let E 0 be a set of decorated constrained clauses. Every derivation (E 0 , ∅) I • • • successful wrt R is also a successful derivation wrt R .

In [START_REF] Bouhoula | Automated induction with constrained tree automata[END_REF], we use Theorem 4 for the proof of conjectures on an extension of the specification of Example 3 with the incomplete definition of a function min. Partial Constructors. The restriction to decorated conjectures also permits to deal with partial constructor functions. In this case, we are generally interested in proving conjectures only for constructor terms in the definition domain of the defined function (well-formed terms).

In [START_REF] Bouhoula | Automated induction with constrained tree automata[END_REF], we present an example of automatic proof where R C is such that the set of well-formed terms is the set of constructor R C -normal forms. Hence, decorating the conjecture with grammar's non-terminals, as in Theorem 2, amounts in this case at restricting the variables to be instantiated by well-formed terms.

The example is a specification of powerlists (lists of 2 n integers stored in the leaves of a complete binary tree) also treated in [START_REF] Kapur | Constructors can be partial too[END_REF]. A particularity of this example is that R C contains constraints of the form t ∼ t meaning that t and t are well-formed lists of the same length (i.e. balanced trees of the same depth). Such constraints are added to G NF (R C ) and we show that emptiness is decidable for these grammars by reduction to the same problem for visibly tree automata with one memory [START_REF] Comon-Lundh | Tree automata with memory, visibility and structural constraints[END_REF].

Conclusion

We have proposed a procedure for automated inductive theorem proving in specification made of conditional and constrained rewrite rules. Constraints in rules can serve to transform non terminating specifications into terminating ones (ordering constraints), define ad-hoc evaluation strategies (normal form constraints), or for the analysis of trace properties of infinite state systems like security protocols (constraints of membership in a regular tree language representing faulty traces [START_REF] Bouhoula | Verifying regular trace properties of security protocols with explicit destructors and implicit induction[END_REF]). The expressiveness and efficiency of the procedure are obtained by the use of constrained tree grammars as a finite representation of the initial model of specifications. They are used both as induction schema and for decision procedures.

The procedure presented in this paper is currently under implementation, on the top of the theorem prover SPASS, whose main loop is used for TA decision procedure by saturation, following the approach of e.g. [START_REF] Jacquemard | Tree automata with equality constraints modulo equational theories[END_REF].

Figure 1 :Figure 2 :

 12 Figure 1: Simplification Rules for Defined Functions

Definition 3 .

 3 Let C c be a constrained clause such that c contains no membership constraint. The decoration of C c , denoted decorate(C c ) is the set of clauses C c ∧ x 1 : u 1 ∧ . . . ∧ x n : u n where {x 1 , . . . , x n } = var (C), and for all i ∈ [1..n], u i ∈ Q NF (R C ) and sort (u i ) = sort (x i ). The definition of decorate is extended to set of constrained clauses as expected. A constrained clause C c is said decorated if c = d ∧ x 1 : u 1 ∧ . . . ∧ x n : u n where {x 1 , . . . , x n } = var (C), and for all

Figure 3 :

 3 Figure 3: Induction Inference Rules

  is constructor and irreducible and R |= Dσ .

In (m 2 ), the constraints y1 ≈ ins(x2, y2), y1:NF can be replaced by y1: ins(x2, y2) .

Acknowledgments

We wish to thank Michael Rusinowitch, Hubert Comon-Lundh, Laurent Fribourg and Deepak Kapur for the fruitful discussions that we had together regarding this work. We are also grateful to Jared Davis and Sorin Stratulat for having processed the example on sorted lists with respectively ACL2 and SPIKE.

A long version of this extended abstract is available as a research report [3]. This work has been partially supported by INRIA/DGRSRT grants 06/I09 and 0804.


Ichiro Mitsuhashi

Michio Oyamaguch

Florent Jacquemard
email: florent.jacquemard@lsv.ens-cachan.fr

The Confluence Problem for Flat TRSs

Keywords: Term rewriting system, Decision problem, Confluence, Flat

We prove that the properties of reachability, joinability and confluence are undecidable for flat TRSs. Here, a TRS is flat if the heights of the left and right-hand sides of each rewrite rule are at most one.

Introduction

A term rewriting system (TRS) is a set of directed equations called rewrite rules. It defines a binary relation on terms by replacement of a subterm matching a left member of a rewrite rule by the corresponding right member. A TRS is called confluent (or Church-Rosser) if any two terms obtained, by the rewriting relation, from the same term are joinable. The confluence is a crucial property for the application of rewriting as a model for computation as it ensures the uniqueness of normal forms [START_REF] Baader | Term Rewriting and All That[END_REF], and it has received much attention so far.

Confluence is undecidable in general, and even for restricted classes of TRS like monadic or semi-constructor TRSs [START_REF] Mitsuhashi | The reachability and related decision problems for monadic and semi-constructor TRSs[END_REF]. On the other hand, decidability results have been established for several classes of TRSs, like e.g. ground (rewrite rules having no variables) TRSs [START_REF] Oyamaguchi | The Church-Rosser property for ground term-rewriting systems is decidable[END_REF][START_REF] Dauchet | Decidability of the confluence of finite ground term rewrite systems and of other related term rewrite systems[END_REF][START_REF] Comon | The confluence of ground term rewrite systems is decidable in polynomial time[END_REF], flat (left and right members of rewrite rules having height at most one) and rule-linear (a variable cannot occur more than once in a rewrite rule) TRSs [START_REF] Tiwari | Deciding confluence of certain term rewriting systems in polynomial time[END_REF], and more recently for flat and rightlinear (a variable cannot occur more than once in a right member of rewrite rule) TRSs [START_REF] Godoy | Confluence of shallow right-linear rewrite systems[END_REF].

In this paper, we demonstrate that the above linearity restriction is necessary for decidability, showing that confluence is undecidable for flat TRSs, even with only one non-right-linear flat rewrite rule. A previous proof of this result has been published in [START_REF] Jacquemard | Reachability and confluence are undecidable for flat term rewriting systems[END_REF]. However, we have found some technical flaws in this proof. This paper presents a correct and detailed undecidability proof, which is also significantly simpler than the one of [START_REF] Jacquemard | Reachability and confluence are undecidable for flat term rewriting systems[END_REF].

The related properties of reachability (whether a given term can be reached from another given term by rewriting) and joinability (whether two given terms can be rewritten to the same term) are decidable for right-ground (right members of rewrite rules have no variable) TRSs [START_REF] Oyamaguchi | The reachability and joinability problems for right-ground termrewriting systems[END_REF], for right-linear monadic TRSs [START_REF] Salomaa | Deterministic tree pushdown automata and monadic tree rewriting systems[END_REF][START_REF] Nagaya | Decidability for left-linear growing term rewriting systems[END_REF], and for right-linear and finite-path-overlapping TRSs [START_REF] Takai | Right-linear finite path overlapping term rewriting systems effectively preserve recognizability[END_REF]. The latter two classes properly include the class of flat and right-linear TRSs. We show in this paper that reachability and joinability are undecidable if we drop the rightlinearity condition, i.e. it is undecidable for general flat TRSs.

The paper is organized as follows: after giving the definitions and notations in Section 2, we show in Section 3 that reachability is undecidable for flat TRSs by reduction of the Post's correspondence problem. It follows as a corollary that joinability is also undecidable for the same class. Then, in Section 4, we show that confluence is undecidable for flat TRSs, by a reduction of reachability.

Preliminaries

We assume that the reader is familiar with the standard definitions of rewrite systems [START_REF] Dershowitz | Rewrite systems[END_REF][START_REF] Baader | Term Rewriting and All That[END_REF] and we just recall here the main notations used in this paper.

Let ε be the empty string. Let X be a set of variables. Let F be a finite set of operation symbols graded by an arity function ar :

F → N(= {0, 1, 2, • • • }), F n = {f ∈ F | ar(f ) = n}.
Let T be the set of terms built from X and F . A substitution is a finite mapping from X to T . As usual, we identify substitutions with their morphism extension to terms, and we use a postfix notation for the application of substitutions. We use x as a variable, f, h as function symbols, r, s, t as terms, θ as a substitution. A term s is ground if s has no variable. The height of a term is defined as follows: height(a) = 0 if a is a variable or a constant and height(f

(t 1 , . . . , t n )) = 1 + max{height(t 1 ), . . . , height(t n )} if n > 0.
A position in a term a sequence of positive integers, and positions are partially ordered by the prefix ordering ≥. Let s| p be the subterm of s at position p. Let s ≥ sub t if t is a subterm of s. For a position p and a term t, we use s[t] p to denote the term obtained from s by replacing the subterm s| p by t.

A rewrite rule α → β is a directed equation over terms. A TRS R is a finite set of rewrite rules. A term s reduces to t at position p by the TRS R, denoted s --→ p R t (p and R may be omitted), if s| p = αθ and t = s[βθ] p for some rewrite rule α → β and substitution θ. Let --→ = be → ∪ =, ← be the inverse of → and -→ * be the reflexive and transitive closure of →. The terms s and t are

joinable if s -→ * • ← - * t, which is denoted s ↓ t. The term t is reachable from s if s -→ * t. The term r is confluent on the TRS R if for every peak s ← -- * R r --→ * R t, we have s ↓ t. The TRS R is confluent if every term is confluent on R. Let γ : s 1 --→ p1 s 2 • • • ----→ pn-1
s n be a rewrite sequence. This sequence is abbreviated by γ : s 1 -→ * s n and γ is called p-invariant if p i > p for every redex position p i of γ; this is denoted by γ :

s 1 ----→ >p * s n . Definition 1. A rule α → β is flat if height(α) ≤ 1 and height(β) ≤ 1. A rule α → β is monadic if height(β) ≤ 1. A term s is shallow if s is a variable or s = f (s 1 , • • • , s n ) for some function symbol f and terms s 1 , • • • , s n such that every s i (1 ≤ i ≤ n) is either a variable or ground. A rule α → β is shallow if both α and β are shallow. For C ∈ {flat, monadic, shallow}, R is C if every rule in R is C.
We are interested in the following decision problems:

Reachability Given a TRS R and two terms s, t, does there exist a rewrite sequence s --→ Definition 2. A finite automaton is a 5-tuple (Q, Σ, δ, F Q , q 0 ) where Q is a finite set of states, Σ is a finite set of input symbols, δ :

Q × Σ → Q is a function, F Q ⊆ Q is a
finite set of final states, and q 0 ∈ Q is the initial state.

3 Reachability and joinability for flat TRSs

In [START_REF] Jacquemard | Reachability and confluence are undecidable for flat term rewriting systems[END_REF], it has been reported that reachability and joinability are also undecidable for flat TRSs. But, the undecidability proof of reachability contains a flaw. We propose a repaired proof of undecidability for reachability which is simpler than the former one. The proof is a reduction of the Post's Correspondence Problem (PCP) into the reachability of a constant 1 from a constant 0 using a a flat TRS R 1 . This TRS, constructed from the given instance of PCP, is such that every rewrite sequence 0 --→ *

R1

1 contains a representation of a solution of the PCP as a term t. This property is ensured, informally, by running separately several sub-TRS of R 1 on several copies of t, where all copies have different colors and are under a function symbol of arity 6 or 7. Moreover, some equality tests are performed during the rewrite sequence using R 1 , by means of a flat rewrite rules in R 1 containing some non-linear variables.

Let

P = { u i , v i ∈ Σ + × Σ + | 1 ≤ i ≤ k} be an instance of PCP.
The goal of the problem is to find a sequence of indices i 1 , . . . , i n , possibly with repetitions, such that the concatenations u i1 . . . , u in and v i1 . . . , v in are equal. Note that the alphabet Σ is fixed. Let l P = max 1≤i≤k (|u i |, |v i |). Let _ be a new symbol and ∆ = {1, • • • , l P }×(Σ ∪{_}) 2 . We shall use a product operator ⊗ which associates to two non-empty strings of Σ + of length smaller than or equal to l P a word of ∆ * of length l P as follows:

a 1 • • • a n ⊗ a 1 • • • a m = 1, a 1 , a 1 • • • l P , a lP , a lP , where a 1 , • • • , a n , a 1 , • • • , a m ∈ Σ, a i = _ for all i ∈ {n + 1, • • • , l P }
, and a j = _ for all j ∈ {m + 1, • • • , l P }. Note that 1, _, _ (s), 1, _, a 1 (s), or 1, a 1 , _ (s) can not be returned by operator ⊗.

Example 1. Let l P = 4, then a ⊗ bab = 1, a, b 2, _, a 3, _, b 4, _, _ . Let A = (Q A , ∆, δ A , F QA , q A ) and B = (Q B , Σ, δ B , F QB , q B ) be two finite automata recognizing the respective sets L(A) = {u i ⊗ v i | u i , v i ∈ P } + and L(B) = Σ + .
We may assume that both q A and q B are non final. We assume that the automata A and B are clean (i.e., any state accepts some input string and is reachable from the initial state q A (or q B ) by some input string). We associate automata A, B with the following ground TRSs T A , T B , respectively:

T (i,j) A = {q (i) → d (j) (q (i) ) | q ∈ δ A (q, d)} ∪ {q (i) → e | q ∈ F QA } T (i,j) B = {q (i) → a (j) (q (i) ) | q ∈ δ B (q, a)} ∪ {q (i) → e | q ∈ F QB }
We assume given 13 disjoint copies of the above signatures, colored with color i ∈ {0, • • • , 12}: 5) , and

Σ (i) = {a (i) | a ∈ Σ} ∆ (i) = {d (i) | d ∈ ∆} Q (i) A = {q (i) | q ∈ Q A } Q (i) B = {q (i) | q ∈ Q B } Let Θ 012 = ∆ (0) ∪ Σ (1) ∪ Σ (2) , Θ 345 = ∆ (3) ∪ ∆ (4) ∪ Σ (
Q = Q (6) A ∪ Q (7) A ∪ Q (8) A ∪ Q (9) A ∪ Q (10) B ∪ Q (11) B ∪ Q (12)
A . Let e be a constant. We assume that ar(f ) = 1 for every f ∈ ∆ ∪ Σ. For a ground term t built from ∆ ∪ Σ ∪ {e}, t (i) is defined as follows: e (i) = e and (f (t 1 )

) (i) = f (i) (t (i) 1 ) for f ∈ ∆ ∪ Σ and term t 1 .
Now, we define the flat TRS R 1 on an extended signature

F 0 = Q ∪ {e, 0, 1}, F 1 = Θ 012 ∪ Θ 345 , F 6 =
{f}, and F 7 = {g}. First, we color T A and T B :

T (i,j) A = {q (i) → d (j) (q (i) ) | q ∈ δ A (q, d)} ∪ {q (i) → e | q ∈ F QA } T (i,j) B = {q (i) → a (j) (q (i) ) | q ∈ δ B (q, a)} ∪ {q (i) → e | q ∈ F QB }
Next, we define recoloring TRSs S, P and projection TRSs Π 1 , Π 2 :

S (i,j) = {a (i) (x) → a (j) (x) | a ∈ Σ} P (i,j) = {d (i) (x) → d (j) (x) | d ∈ ∆} Π (i,j) 1 = { n, a, a (i) (x) → a (j) (x) | n ∈ {1, • • • , l P }, a ∈ Σ, a ∈ Σ ∪ {_}} ∪{ n, _, a (i) (x) → x | n ∈ {2, • • • , l P }, a ∈ Σ ∪ {_}} Π (i,j) 2 = { n, a, a (i) (x) → a (j) (x) | n ∈ {1, • • • , l P }, a ∈ Σ ∪ {_}, a ∈ Σ} ∪{ n, a, _ (i) (x) → x | n ∈ {2, • • • , l P }, a ∈ Σ ∪ {_}}
The flat TRS R 1 is defined as follows:

R 0 = T (6,3) A ∪ T (7,3) A ∪ T (8,4) A ∪ T (9,4) A ∪ T (10,5) B ∪ T (11,5) B ∪P (3,0) ∪ Π (3,1) 1 ∪ Π (4,2) 2 ∪ P (4,0) ∪ S (5,1) ∪ S (5,2) ∪ T (12,0) A R 1 = R 0 ∪      0 → f(q (6) A , q (7) A , q (8) A , q (9)
A , q

(10) B , q (11) B ), f(x 3 , x 3 , x 4 , x 4 , x 5 , x 5 ) → g(x 3 , x 3 , x 4 , x 4 , x 5 , x 5 , q (12) A ), g(x 0 , x 1 , x 2 , x 0 , x 1 , x 2 , x 0 ) → 1      By construction of R 1 , if 0 --→ * R1
1 then the rules of R 1 are applied as described in the following picture.

0 ε → f( q (6) A , q (7)
A , q

A , q

A , q

B , q

(11) B ) * ↓ T (6,3) A * ↓ T (7,3) A * ↓ T (8,4) A * ↓ T (9,
A ) *

↓ P (3,0) * ↓ Π (3,1) 1 * ↓ Π (4,2) 2 * ↓ P (4,0) * ↓ S (5,1) * ↓ S (5,2) * ↓ T (12,0) A g( t 0 , t 1 , t 2 , t 0 , t 1 , t 2 , t 0 ) ε → 1
Indeed, each of the symbols 0 and 1 occurs in only one rewrite rule of R 1 , and there is only one rule to transform the function symbol f into g. Moreover, in the above rewrite sequence by R 1 , we have a subsequence q

(12) A -----→ * T (12,0) A t 0 , which means that t 0 has the form ((u i1 ⊗v i1 ) • • • (u im ⊗v im )(e)) (0) for some i 1 , • • • , i m ∈ {1, • • • , k}.
We will show in Lemma 1 that: Let G 1 be the set of ground terms built from

q (6) A ---------→ * T (6,3) A ∪P (3,0) t 0 ← --------- * T (9,4) A ∪P (4,0) q (9) A
F 0 ∪ F 1 ∪ F 6 ∪ F 7 .
Definition 3.

(

) Let --→ * R (s) = {t | s --→ * R t}. For a subset C ⊆ {0, • • • , 12} 1
, let G C be the intersection of G 1 and the set of ground terms built from e and colored function symbols in

∪ i∈C (Σ (i) ∪ ∆ (i) ∪ Q (i) A ∪ Q (i) B ).
(2) The index of an i-colored term built from ∆ (i) ∪ {e} is a string of integers defined as follows: index(e) = ε, and index( n, a, a (i) (t)) = n index(t).

This Lemma 1 will be useful in the proof of the following Lemma 2.

Lemma 1. Assume that q (6)

A --→ * R0 t 0 and q (9) (0) . Then, the following properties hold:

A --→ * R0 t 0 where t 0 = ((u i1 ⊗ v i1 ) • • • (u im ⊗ v im )(e))
(1) q (6) A ---------→ * T (6,3) A ∪P (3,0) t 0 (2) q (9) A ---------→ * T (9,4) A ∪P (4,0) t 0 Proof ¡ ¢ £ ¤ ¡ ¦¥ § © ¥ ¡ ¦¤ ¡ ¡ ¡ Π 1 T A T A T A T A T B T B S S P P Π 2 T A Fig. 1.
Graph of the reduction of colors for R1.

(1) By definition of R 0 , q

A --------------→ * T (6,3) A ∪P (3,0) ∪Ξ (3,1) 1 t 0 where Ξ (3,1) 1 (6)
is the subset of

Π (3,1) 1
defined by:

Ξ (3,1) 1 = { n, _, a (3) (x) → x | n ∈ {2, • • • , l P }, a ∈ Σ ∪ {_}}. Note that index(t 0 ) = (1 • • • l P ) m .
In this rewrite sequence, if there is at least one application of some rule of Ξ

, index(t 0 ) = (1 • • • l P ) m does not hold, since if we applied a rule n, _, a (3) (x) → x, then at most m -1 symbols of n would be included in index(t 0 ) whereas exactly m symbols of 1 in index(t 0 ) (since any symbol of form 1, a, a (3) can not be deleted). Thus, the proposition holds.

(2) Similar to (1).

Lemma 2. 0 --→ * R1 1 iff the PCP P has a solution.

Proof

Only if part: by definition of R 1 , we have:

0 --→ R1 f(q (6)
A , q

A , q

A , q

A , q

B , q

(11) B ) ----→ R0 >ε * f(t 3 , t 3 , t 4 , t 4 , t 5 , t 5 ) --→ R1 g(t 3 , t 3 , t 4 , t 4 , t 5 , t 5 , q (12)
A ) ----→ R0 >ε * g(t 0 , t 1 , t 2 , t 0 , t 1 , t 2 , t 0 ) --→ R1 1
By definition of R 0 :

--→ * R0 (q

(6) A ) ⊆ G {0,1,3,6} , --→ * R0 (q (7) A ) ⊆ G {0,1,3,7} , --→ * R0 (q (8) A ) ⊆ G {0,2,4,8} , --→ * R0 (q (9) A ) ⊆ G {0,2,4,9} , --→ * R0 (q (10) B ) ⊆ G {1,2,5,10} , --→ * R0 (q (11)
B ) ⊆ G {1,2,5,11} We first show that the following condition (I) holds:

t i ∈ G {i} ∀i ∈ {0, • • • , 5} (I) Note that t 3 ∈ G {0,1,3} holds, since t 3 ∈--→ * R0 (q (6) A )∩ --→ * R0 (q (7)
A ). Similarly, t 4 ∈ G {0,2,4} and t 5 ∈ G {1,2,5} . Since t 3 --→ * R0 t 0 and t 4 --→ * R0 t 0 , we have

t 0 ∈ G {0,1,3} ∩ G {0,2,4} = G {0} . Similarly, t 1 ∈ G {0,1,3} ∩ G {1,2,5} = G {1} and t 2 ∈ G {0,2,4} ∩ G {1,2,5} = G {2} .
Hence, the condition (I) holds for i ∈ {0, 1, 2}.

Since t 3 --→ * R0 t 0 ∈ G {0} and t 3 --→ * R0 t 1 ∈ G {1} , t 3 can not contain any symbol in G {0,1} , hence t 3 ∈ G {3} holds. Similarly, t 4 ∈ G {4} holds because t 4 --→ * R0 t 2 ∈ G {2} and t 4 --→ * R0 t 0 ∈ G {0} , and t 5 ∈ G {5} holds because t 5 --→ * R0 t 1 ∈ G {1} and t 5 --→ * R0 t 2 ∈ G {2}
. Hence, (I) holds for i ∈ {3, 4, 5}, as claimed.

By (I), we have: (3) and (1) , and since t 4 ----→ * (2) . Finally, t 1 ← ----S (5,1) t 5 ----→ * S (5,2) t 2 , hence t 5 = (u i1 • • • u im (e)) (5) = (v i1 • • • v im (e)) (5) . It means that the PCP P has a solution.

t 3 ----→ * Π (3,1) 1 t 1 ← ---- * S (5,1) t 5 and t 4 ----→ * Π (4,2) 2 t 2 ← ---- * S (5,2) t 5 . Since q (12) A --→ * R0 t 0 , t 0 = ((u i1 ⊗ v i1 ) • • • (u im ⊗ v im )(e)) (0) for some i 1 , • • • , i m ∈ {1, • • • , k}. We have m > 0 because the initial state q A is not final. By Lemma 1, t 3 ----→ * P (3,0) t 0 ← ---- * P (4,0) t 4 . Thus, t 3 = ((u i1 ⊗ v i1 ) • • • (u im ⊗ v im )(e))
t 4 = ((u i1 ⊗ v i1 ) • • • (u im ⊗ v im )(e)) (4) . Since t 3 ----→ * Π (3,1) 1 t 1 , t 1 = (u i1 • • • u im (e))
Π (4,2) 2 t 2 , t 2 = (v i1 • • • v im (e))
If part: let i 1 • • • i m be a solution of the PCP P , and let:

s = (u i1 ⊗ v i1 ) • • • (u im ⊗ v im )(e) and t = u i1 • • • u im (e) Then, t = v i1 • • • v im (e)
holds. By definition of R 1 , we have:

0 → f(q (6) A , q (7)
A , q

A , q

A , q

(10) B , q (11)
B ) -→ * f(s (3) , s (3) , s (4) , s (4) , t (5) , t (5) ) → g(s (3) , s (3) , s (4) , s (4) , t (5) , t (5) , q

A ) -→ * g(s (0) , t (1) , t (2) , s (0) , t (1) , t (2) , s (0) ) → 1.

Hence, 0 --→ * R1 1
As a consequence of Lemma 2, we have the following main theorem of this section.

Theorem 1. Reachability is undecidable for flat TRSs.

Since 1 is a normal form, 0 --→ * R1 1 iff 0 ↓ R1 1. Thus, the following corollary holds. Corollary 1. Joinability is undecidable for flat TRSs.

Compared to the construction in [START_REF] Jacquemard | Reachability and confluence are undecidable for flat term rewriting systems[END_REF] for Lemma 2, on the one hand, the above TRS R 1 is simpler and on the other hand, some rules have been added in order to permit the reduction q (12)

A -----→ * T (12,0) A t 0 . This appeared to be necessary in order to fix a bug [START_REF] Jacquemard | Reachability and confluence are undecidable for flat term rewriting systems[END_REF] where a reduction 0 -→ * 1 was possible with the TRS associated to the PCP { aa, a , a, ab } whereas it has no solution. The main reason for this counter-example is for lack of some consideration such as Lemma 1 above (derived from the existence of q (0) and the definition of operator ⊗).

(12) A -→ * ((u i1 ⊗ v i1 ) • • • (u im ⊗ v im )(e))

Confluence for flat TRSs

We show that confluence for flat TRSs is undecidable by reduction of the reachability problem which has been shown undecidable in the previous section. We introduce some technical definitions in Sections 4.1.

Mapping lemma

A mapping φ from T to T can be extended to TRSs as follows:

φ(R) = {φ(α) → φ(β) | α → β ∈ R} \ {t → t | t ∈ T }
Such a mapping φ can also be extended to substitutions by φ(θ) = {x → φ(xθ) | x in the domain of θ}. The following lemma gives a characterization of confluence for a TRS R using φ(R). Lemma 3. A TRS R is confluent iff there exists a mapping φ : T → T that satisfies the following conditions (1)-( 4).

(1

) If s --→ R t then φ(s) ----→ * φ(R) φ(t) (2) ----→ φ(R) ⊆--→ * R (3) t --→ * R φ(t) (4) φ(R) is confluent
Proof Only if part: let φ be the identity mapping.

If part: assume that s ← --

* R r --→ * R t. By Condition (1), φ(s) ← ---- * φ(R) φ(r) ----→ * φ(R) φ(t). By Condition (4), φ(s) ↓ φ(R) φ(t). By Condition (2), φ(s) ↓ R φ(t). By Condition (3), s --→ * R φ(s) and t --→ * R φ(t). Thus, s ↓ R t.
This lemma is used in Section 4.2.

Proof of undecidability

Let us introduce new function symbols Θ 012 2 = {d 2 | d ∈ Θ 012 }, where each d 2 has arity 2. We add the following rules to the TRS R 1 of Section 3:

R 2 = R 1 ∪ {e → 0} ∪ {d(x) → d 2 (0, x), d 2 (1, x) → x | d ∈ Θ 012 }
Note that the TRS R 2 is flat. Let G 2 be the set of ground terms built from

F 0 ∪ F 1 ∪ F 6 ∪ F 7 ∪ Θ 012 2 . First, we show that 0 --→ * R2 1 iff 0 --→ * R1 1.
For this purpose, we will introduce another reduction mapping φ and another TRS R 2 and show a technical lemma.

Let ψ be the mapping over G 2 defined as follows.

ψ(h(t 1 , • • • , t n )) = e (if h ∈ {0, 1, f, g}) ψ(d 2 (t 1 , t 2 )) = d(ψ(t 2 )) (if d ∈ Θ 012 ) ψ(h(t 1 , • • • , t n )) = h(ψ(t 1 ), • • • , ψ(t n )) (otherwise) Let R 2 = R 1 ∪ {e → 0} ∪ {d(x) → d 2 (0, x) | d ∈ Θ 012 }. Lemma 4. For any s ∈ G 2 , if s --→ R 2 t then ψ(s) --→ = R1 ψ(t).
Proof We prove this lemma by induction on the structure of s.

Base case:

if s ∈ Q then s = ψ(s) --→ R1 ψ(t) = t. If s ∈ {e, 0} then ψ(s) = ψ(t) = e.
Induction step: Case of s = d 2 (s 1 , s 2 ) where d ∈ Θ 012 : in this case, t = d 2 (t 1 , t 2 ) holds for some t 1 , t 2 and either s

Case of s ∈ {f(s 1 , • • • , s 6 ), g(s 1 , • • • , s 7 )}: in this case, ψ(s) = ψ(t) = e. Case of s = d(s 1 ) where d ∈ Θ 345 : if t = d(t 1 ) and s 1 --→ R 2 t 1 then ψ(s) = d(ψ(s 1 )) --→ =
1 --→ R 2 t 1 and s 2 = t 2 or s 2 --→ R 2 t 2 and s 1 = t 1 , hence ψ(s) = d(ψ(s 2 )) --→ = R1 d(ψ(t 2 )) = ψ(t) by the induction hypothesis. Lemma 5. 0 --→ * R2 1 iff 0 --→ * R1 1.
Proof The if part is obvious. For the only if part, by definition of R 2 , if 0 --→ * R2 1 then there exists a shortest sequence γ that satisfies:

γ : 0 --→ R1 f(q (6) A , q (7)
A , q

A , q

A , q

B , q

(11) B ) ----→ R2 >ε * f(t 3 , t 3 , t 4 , t 4 , t 5 , t 5 ) --→ R1 g(t 3 , t 3 , t 4 , t 4 , t 5 , t 5 , q (12) A ) ----→ R2 >ε * g(t 0 , t 1 , t 2 , t 0 , t 1 , t 2 , t 0 ) --→ R1 1.
Note that d 2 (1, x) → x can not be applied in γ. Indeed, if d 2 (1, x) → x is applied in γ, then γ must contain a subsequence 0 --→ * R2 1 since 1 appears only in the right-hand side of the rule g(x 0 , x 1 , x 2 , x 0 , x 1 , x 2 , x 0 ) → 1, g is only generated by the rule f(x 3 , x 3 , x 4 , x 4 , x 5 , x 5 ) → g(x 3 , x 3 , x 4 , x 4 , x 5 , x 5 , q

A ), and f is only generated by the rule 0 → f(q

(6) A , q (7) A , q (8)
A , q

A , q

(10) B , q (11)
B ). This contradicts the hypothesis that γ is a shortest sequence. Thus,

f(q (6) A , q (7)
A , q

A , q

A , q

B , q

(11) B ) ----→ R 2 >ε * f(t 3 ,
A ) ----→ R 2 >ε * g(t 0 , t 1 , t 2 , t 0 , t 1 , t 2 , t 0 ) (12)
By Lemma 4 (for sake of readability, we shall write below x instead of ψ(x)):

f q (6)
A , q

A , q

A , q

A , q

B , q

(11) B --→ * R1 f t 3 , t 3 ,
A --→ * R1 g t 0 , t 1 , t 2 , t 0 , t 1 , t 2 , t 0 Since ψ(q) = q for every q ∈ Q, 0 --→ R1 f q (12)
A , q

A , q

A , q

A , q

B , q

.

By definition of R 1 , f t 3 , t 3 , t 4 , t 4 , t 5 , t 5 --→ R1 g t 3 , t 3 , t 4 , t 4 , t 5 , t 5 , q

A

and g t 0 , t 1 , t 2 , t 0 , t 1 , t 2 , t 0 --→ R1 1. Altogether 0 --→ * R1 1.
We shall show next that R 2 is confluent iff 0 --→ * R2 1 by using Lemma 3. We need the following lemma for that purpose.

Lemma 6. If 0 --→ * R2 1 then t --→ * R2 1 for any t ∈ G 2 .
Proof First, we note that for any q ∈ Q, there exists s ∈ G 2 which does not contain any function symbol in Q such that q --→ * R2 s. Since both of the automata A and B are clean, there exists u ∈ ∆ (3) * ∪ ∆ (4) * ∪ Σ (5) * ∪ ∆ (0) * such that q --→ * R0 u(e). Thus, it suffices to show that for any t ∈ G 2 which does not contain any function symbol in Q, t --→ * R2 1. We show this proposition by induction on the structure of t:

Base case: by e --→ R2 0 --→ * R2 1.

Induction step: let t = h(t 1 , • • • , t n )
where n > 0 and h ∈ Θ 012 ∪Θ 345 ∪{f, g}∪ Θ 012 2 . By the induction hypothesis,

h(t 1 , • • • , t n ) --→ * R2 h(1, • • • , 1). For every d ∈ Θ 345 , d(1) --→ R1 d (1) for some d ∈ Θ 012 or d(1) --→ R1 1. For every d ∈ Θ 012 , d (1) --→ R2 d 2 (0, 1) --→ * R2 d 2 (1, 1). For every d 2 ∈ Θ 012 2 , d 2 (1, 1) --→ R2 1. Moreover, f(1, • • • , 1) --→ R1 g(1, • • • , 1, q (12) A ) --→ * R1 g(1, • • • , 1, u(e)) --→ * R2 g(1, • • • , 1, 1) --→ R1 1 where u ∈ ∆ (0) *
Let φ(t) be the term obtained from t by replacing every maximal ground subterm (w.r.t. ≥ sub ) by 1. Note that:

φ(R 0 ) = P (3,0) ∪ Π (3,1) 1 ∪ Π (4,2) 2
∪ P (4,0) ∪ S (5,1) ∪ S (5,2) φ(R 1 ) = φ(R 0 ) ∪ f(x 3 , x 3 , x 4 , x 4 , x 5 , x 5 ) → g(x 3 , x 3 , x 4 , x 4 , x 5 , x 5 , 1), g(

x 0 , x 1 , x 2 , x 0 , x 1 , x 2 , x 0 ) → 1 φ(R 2 ) = φ(R 1 ) ∪ {d(x) → d 2 (1, x), d 2 (1, x) → x | d ∈ Θ 012 }.
Note also that the rules of T A and T B vanish in φ(R 0 ). The following technical lemma is used in the proof of Lemma 8.

Lemma 7. For any non-constant function symbol

h ∈ Θ 012 ∪Θ 345 ∪{f, g}∪Θ 012 2 , h(1, • • • , 1) ----→ * φ(R2) 1. Proof For every d ∈ Θ 345 , d(1) ----→ φ(R1) d (1) for some d ∈ Θ 012 or d(1) ----→ φ(R1) 1. For every d ∈ Θ 012 , d (1) ----→ φ(R2) d 2 (1, 1). For every d 2 ∈ Θ 012 2 , d 2 (1, 1) ----→ φ(R2) 1. Moreover, f(1, • • • , 1) ----→ φ(R1) g(1, • • • , 1) ----→ φ(R1) 1.
Thus, the lemma holds.

We show now how the hypotheses of Lemma 3 hold for R 2 and φ.

Lemma 8. If 0 --→ * R2 1 then the following properties hold. (1) If s --→ R2 t then φ(s) ----→ * φ(R2) φ(t). (2) ----→ φ(R2) ⊆ --→ * R2 . (3) t --→ * R2 φ(t). (4) φ(R 2 ) is confluent.

Proof

(1) By induction on the structure of s. If s is a ground term then φ(s) = φ(t) = 1.

Thus, we assume that s is not ground. Let s --→ p R2 t.

If p = ε then s = αθ → βθ = t where α → β ∈ R 2 . Let s = h(s 1 , • • • , s n ) for some h ∈ Θ 012 ∪ Θ 345 ∪ {f, g} ∪ Θ 012 2 and s 1 , • • • , s n , and α = h(a 1 , • • • , a n ). Since R 2 is flat, a 1 • • • a n ∈ X ∪ F 0 . If a i is a variable then φ(a i θ) = a i φ(θ). If a i is a constant then φ(s i ) = φ(a i ) = 1. Thus, φ(s) = φ(α)φ(θ). Similarly, φ(t) = φ(β)φ(θ), so φ(s) ----→ φ(R2) φ(t) holds. If p = ε then s = h(s 1 , • • • , s i , • • • , s n ), t = h(s 1 , • • • , t i , • • • , s n ), and s i --→ R2 t i where i ∈ {1, • • • , n}. Since s is not ground, φ(s) = h(φ(s 1 ), • • • , φ(s i ), • • • , φ(s n )).

By the induction hypothesis, φ(s

i ) ----→ * φ(R2) φ(t i ). If t is not ground then h(φ(s 1 ), • • • , φ(t i ), • • • , φ(s n )) = φ(t). If t is ground then h(φ(s 1 ), • • • , φ(t i ), • • • , φ(s n )) = h(1, • • • , 1). By Lemma 7, h(1, • • • , 1) ----→ * φ(R2) 1 = φ(t). Thus, φ(s) ----→ * φ(R2) φ(t) holds. (2) Since φ(R 2 ) \ d(x) → d 2 (1, x) | d ∈ Θ 012 ∪ f(x 3 , x 3 , x 4 , x 4 , x 5 , x 5 ) → g(x 3 , x 3 , x 4 , x 4 , x 5 , x 5 , 1) ⊆ R 2 , it suffices to show that: d(xθ) --→ * R2 d 2 (1, xθ) and f(x 3 θ, x 3 θ, x 4 θ, x 4 θ, x 5 θ, x 5 θ) --→ * R2 g(x 3 θ, x 3 θ, x 4 θ, x 4 θ, x 5 θ, x 5 θ, 1) We have that: d(xθ) --→ R2 d 2 (0, xθ) --→ * R2 d 2 (1, xθ)
. By Lemma 6: f(x 3 θ, x 3 θ, x 4 θ, x 4 θ, x 5 θ, x 5 θ) --→ R1 g x 3 θ, x 3 θ, x 4 θ, x 4 θ, x 5 θ, x 5 θ, q (12) A --→ * R2 g(x 3 θ, x 3 θ, x 4 θ, x 4 θ, x 5 θ, x 5 θ, 1) (3) By Lemma 6. (4) We can easily show that φ(R 2 ) is terminating by using a lexicographic path order induced by a precedence > that satisfies the following conditions: for any

d ∈ Θ 345 , d ∈ Θ 012 , d ∈ Θ 012 2 , d > d > d > 1 and f > g > 1.
Thus, it suffices to show that every critical peak of φ(R 2 ) is joinable.

For every a, a ∈ Σ, n, a, a (0) (x) ← n, a, a (3) (x) → a (1) (x) is joinable by: n, a, a (0) (x) → n, a, a

(0) 2 (1, x) → x ← a (1) 2 (1, x) ← a (1) (x). For every a ∈ Σ, n, _, a (0) (x) ← n, _, a (3) (x) → x is joinable by: n, _, a (0) (x) → n, _, a (0)
2 (1, x) → x. For every a, a ∈ Σ, n, a, a (0) (x) ← n, a, a (4)

(x) → a (2) (x) is joinable by: n, a, a (0) (x) → n, a, a (0) 2 (1, x) → x ← a (2) 2 (1, x) ← a (2) (x). For every a ∈ Σ, n, a, _ (0) (x) ← n, a, _ (4) (x) → x is joinable by: n, a, _ (0) (x) → n, a, _ (0)
2 (1, x) → x. For every a ∈ Σ, a (1) (x) ← a (5)

(x) → a (2) (x) is joinable by: a (1) (x) → a (1) 2 (1, x) → x ← a (2) 2 (1, x) ← a (2) (x). Lemma 9. R 2 is confluent iff 0 --→ * R2 1.
Proof The if part follows from Lemmata 3 and 8. For the only if part, by n, _, a (0) (x)← ----

P (3,0) n, _, a (3) (x)----→ Π (3,1) 1
x, the confluence ensures that n, _, a (0) (x) ↓ R2 x. Since x is a normal form, n, _, a (0) (x) --→ * R2 x. Thus, there exists a sequence:

n, _, a (0) (x) --→ R2 n, _, a (0) 2 (0, x) --→ * R2 n, _, a (0) 2 (1, x) --→ R2 x
It follows that 0 --→ * R2 1 holds. By Lemmata 2, 5, 9, the following theorem holds.

Theorem 2. Confluence is undecidable for flat TRSs.

The above TRS R 2 differs from the analogous one of [START_REF] Jacquemard | Reachability and confluence are undecidable for flat term rewriting systems[END_REF]. Indeed, in some cases, with the TRS of [START_REF] Jacquemard | Reachability and confluence are undecidable for flat term rewriting systems[END_REF] we may have 0 --→ * R2 1 whereas 0 --→ * R1 1 does not hold, which is a problem for the correctness of the reduction. This error was corrected in [START_REF] Jacquemard | Erratum to the paper: Reachability and confluence are undecidable for flat term rewriting system[END_REF], but Lemma 9 does not hold for the TRS of this report. Therefore, the above TRS R 2 and the above proof differ from the ones of [START_REF] Jacquemard | Erratum to the paper: Reachability and confluence are undecidable for flat term rewriting system[END_REF].

Concluding remarks

We have shown that the properties of reachability, joinability and confluence are undecidable for flat TRSs. These results are negative solutions to the open problems posed in [START_REF] Godoy | On the confluence of linear shallow term rewrite systems[END_REF], and striking compared with the results that the word and unification problems for shallow TRSs are decidable [START_REF] Comon | Syntacticness, cycle-syntacticness and shallow theories[END_REF]. The undecidability of reachability is shown by a reduction of the Post's Correspondence Problem and the case of joinability and confluence are treated both by a reduction of reachability (with a non trivial reduction in the case of confluence).

The proof techniques involved in our constructions, namely term coloring in Section 3, the criteria for confluence of Lemma 3 and the ground term mapping of Section 4 appeared to be very useful in this context and we believe that they could be of benefit to other decision problems.

Note that the only rules not linear in our TRS are f(x 3 , x 3 , x 4 , x 4 , x 5 , x 5 ) → g(x 3 , x 3 , x 4 , x 4 , x 5 , x 5 , q

A ) and g(x 0 , x 1 , x 2 , x 0 , x 1 , x 2 , x 0 ) → 1 (both left and right members of the first rule are non-linear and they share variables, which is crucial in our reduction). Hence, we have narrowed dramatically the gap between known decidable and undecidable cases of confluence, reachability and joinability of TRS. All three properties are indeed decidable for TRSs whose left members of rules are flat and right members are flat and linear [START_REF] Tiwari | Deciding confluence of certain term rewriting systems in polynomial time[END_REF][START_REF] Nagaya | Decidability for left-linear growing term rewriting systems[END_REF][START_REF] Takai | Right-linear finite path overlapping term rewriting systems effectively preserve recognizability[END_REF].

It will be a next step to find non-right-linear subclasses of flat (or shallow) TRSs with the decidable property for some of these decision problems. For example, what about the class of flat and semi-constructor TRSs? Here, a semi-constructor TRS is such a TRS that all defined symbols appearing in the right-hand side of each rewrite rule occur only in its ground subterms.

Another interesting question is: does there exist a subclass of TRSs such that exactly one of reachability and confluence is decidable? For the related question about whether there exists a subclass such that exactly one of reachability and joinability is decidable, the existence of such a confluent subclass has been shown in [START_REF] Mitsuhashi | The joinability and related decision problems for semi-constructor TRSs[END_REF][START_REF] Mitsuhashi | The reachability and related decision problems for monadic and semi-constructor TRSs[END_REF].

Figure 1

 1 Figure1shows how colors are changed by the rules of R 1 .Let G 1 be the set of ground terms built fromF 0 ∪ F 1 ∪ F 6 ∪ F 7 .

R1d

  (ψ(t 1 )) = ψ(t) by the induction hypothesis. Otherwise either t = d (s 1 ) with d ∈ Θ 012 and ψ(s) = d(ψ(s 1 )) --→ R1 d (ψ(s 1 )) = ψ(t) or t = s 1 and ψ(s) = d(ψ(s 1 )) --→ R1 ψ(s 1 ) = ψ(t). Case of s = d(s 1 ) where d ∈ Θ 012 : if t = d(t 1 ) and s 1 --→ R 2 t 1 then ψ(s) = d(ψ(s 1 )) --→ = R1 d(ψ(t 1 )) = ψ(t) by the induction hypothesis. Otherwise t = d 2 (0, s 1 ) and ψ(s) = ψ(t) = d(ψ(s 1 )).

  t 3 , t 4 , t 4 , t 5 , t 5 ) and g(t 3 , t 3 , t 4 , t 4 , t 5 , t 5 , q

  t 4 , t 4 , t 5 , t 5 and g t 3 , t 3 , t 4 , t 4 , t 5 , t 5 , q

Acknowledgements

We would like to thank Professor Masahiko Sakai of Nagoya University for his helpful comments. This work was supported in part by Grant-in-Aid for Scientific Research 15500009 from Japan Society for the Promotion of Science.