Thomas Genet
email: thomas.genet@irisa.fr

Yann Salmon
email: yann.salmon@irisa.fr

Reachability Analysis of Innermost Rewriting

Approximating the set of terms reachable by rewriting finds more and more applications ranging from termination proofs of term rewriting systems, cryptographic protocol verification to static analysis of programs. However, since approximation techniques do not take rewriting strategies into account, they build very coarse approximations when rewriting is constrained by a specific strategy. In this work, we propose to adapt the Tree Automata Completion algorithm to accurately approximate the set of terms reachable by rewriting under the innermost strategy. We prove that the proposed technique is sound and precise w.r.t. innermost rewriting. The proposed algorithm has been implemented in the Timbuk reachability tool. Experiments shows that it noticeably improves the accuracy of static analysis for functional programs using the call-by-value evaluation strategy. In particular, for some functional programs needing lazy evaluation to terminate, the computed approximations are precise enough to prove the absence of innermost normal forms, i.e. prove non termination of the program with call-by-value.

Introduction

For a Term Rewriting System (TRS) R and a set of terms L 0 ⊆ T (Σ), the set of reachable terms is R * (L 0 ) = t ∈ T (Σ) ∃s ∈ L 0 , s → * R t . This set can be computed for specific classes of R but, in general, it has to be approximated. Applications of the approximation of R * (L 0 ) are ranging from cryptographic protocol verification [GK00, ABB + 05], to static analysis of various programming languages [START_REF] Boichut | Rewriting Approximations for Fast Prototyping of Static Analyzers[END_REF][START_REF] Kochems | Improved Functional Flow and Reachability Analyses Using Indexed Linear Tree Grammars[END_REF] or to TRS termination proofs [START_REF] Middeldorp | Approximations for strategies and termination[END_REF][START_REF] Geser | On tree automata that certify termination of left-linear term rewriting systems[END_REF]. Most of the techniques compute such approximations using tree automata as the core formalism to represent or approximate the (possibly) infinite set of terms R * (L 0 ). Most of them also rely on a Knuth-Bendix completion-like algorithm to produce an automaton A * recognising exactly, or over-approximating, the set of reachable terms. As a result, these techniques can be refered as tree automata completion techniques [Gen98, TKS00, Tak04, FGVTT04, BCHK09, GR10, Lis12].

Surprisingly, very little effort has been paid to computing or over-approximating R * strat (L 0 ), i.e. set of reachable terms when R is applied with a strategy strat. To the best of our knowledge, Pierre Réty and Julie Vuotto's work [START_REF] Réty | Regular Sets of Descendants by some Rewrite Strategies[END_REF] is the first one to have tackled this goal. They give some sufficient conditions on L 0 and R for R * strat (L 0 ) to be recognised by a tree automaton A * , where strat can be the innermost or the outermost strategy. Innermost reachability for shallow TRSs was studied in [START_REF] Gascon | Closure of Tree Automata Languages under Innermost Rewriting[END_REF]. However, in both cases, those restrictions on R are strong and generally incompatible with programs seen as TRS. Moreover, the proposed techniques are not able to over-approximate reachable terms when the TRS are outside of this class.

In this paper, we define a tree automata completion algorithm over-approximating the set R * in (L 0 ) for all left-linear TRSs R and all regular set of input terms L 0 . As the completion algorithm of [START_REF] Genet | Equational tree automata completion[END_REF], it is parameterised by a set of term equations E defining the precision of the approximation. We prove the soundness of the algorithm: for all set of equation E, if completion terminates then the resulting automaton A * recognises an over-approximation of R * in (L 0 ). Then, we prove a precision theorem: A * recognises no more terms that the set of terms reachable by innermost rewriting with R modulo equations of E. Finally, we show on a simple example that the precision of this innermost completion can improve a lot the accuracy of the analysis for functional programs.

This paper is organised as follows. Section 2 recalls some basic notions about TRSs and tree automata. Section 3 defines tree automata completion. Section 4 explains how to adapt completion so as to take innermost strategy into account. Section 5 states and proves the soundness of this method. Section 6 demonstrates how our new technique can effectively give more precise results on functional programs thanks to the tool TimbukSTRAT, an implementation of our method in the Timbuk reachability tool [START_REF]Timbuk -reachability analysis and Tree Automata Calculations[END_REF]. Section 7 states a precision theorem.

Basic notions and notations

Terms Definition 1 (Signature).

A signature is a set whose elements are called function symbols. Each function symbol has an arity, which is a natural integer. Function symbols of arity 0 are called constants. Given a signature Σ and k ∈ N, the set of its function symbols of arity k is noted Σ k .

1 Definition 2 (Term, ground term, linearity).

Given a signature Σ and a set X whose elements are called variables and such that Σ ∩X = ∅, we define the set of terms over Σ and X , T (Σ, X ), as the smallest set such that :

1. X ⊆ T (Σ, X ) and 2. ∀k ∈ N, ∀f ∈ Σ k , ∀t 1 , . . . , t k ∈ T (Σ, X ), f (t 1 , . . . , t k ) ∈ T (Σ, X ).

Terms in which no variable appears, i.e. terms in T (Σ, ∅), are called ground; the set of ground terms is noted T (Σ).

Terms in which any variable appears at most once are called linear. 1 2 Definition 3 (Substitution).

A substitution over T (Σ, X ) is an application from X to T (Σ, X ). Any substitution is inductively extended to T (Σ, X ) by σ (f (t 1 , . . . , t k )) = f (σ (t 1 ), . . . , σ (t k )). Given a substitution σ and a term t, we note tσ instead of σ (t).

Definition 4 (Context).

A context over T (Σ, X ) is a term in T (Σ ∪ X , { }) in which the variable appears exactly once. A ground context over T (Σ, X ) is a context over T (Σ). The smallest possible context, , is called the trivial context. Given a context C and a term t, we note C[t] the term Cσ t , where σ t : → t.

4

Definition 5 (Position).

Positions are finite words over the alphabet N. The set of positions of term t, Pos(t), is defined by induction over t:

1. for all constant c and all variable X, Pos(c) = Pos(X) = {Λ} and 2. Pos(f (t 1 , . . . , t k )) = {Λ} ∪ k i=1 {i}. Pos(t i ).

5 Definition 6 (Subterm-at-position, replacement-at-position).

The position of the hole in context C, Pos (C), is defined by induction on C:

1. Pos ( ) = Λ 2. Pos (f (C 1 , . . . , C k )) = i. Pos (C i )
, where i is the unique integer in 1 ; k such that C i is a context.

Given a term u and p ∈ Pos(u), there is a unique context C and a unique term v such that Pos (C) = p and u = C [v]. The term v is noted u |p , and, given another term t, we note u [t]

p = C[t].

Rewriting

Definition 7 (Rewriting rule, term rewriting system).

A rewriting rule over (Σ, X ) is a couple ( , r) ∈ T (Σ, X ) × T (Σ, X ), that we note → r, such that any variable appearing in r also appears in . A term rewriting system (TRS) over (Σ, X ) is a set of rewriting rules over (Σ, X ).

7

Definition 8 (Rewriting step, redex, reducible term, normal form).

Given a signature (Σ, X ), a TRS R over it and two terms s, t ∈ T (Σ), we say that s can be rewritten into t by R, and we note s → R t if there exist a rule → r ∈ R, a ground context C over T (Σ) and a substitution σ over T (Σ, X ) such that s = C[ σ ] and t = C [rσ ].

In this situation, the term s is said to be reducible by R and the subterm σ is called a redex of s. A term s that is not reducible by R is a normal form of R. The set of normal forms of R is noted Irr(R).

We note → * R the reflexive and transitive closure of → R .

8

Definition 9 (Set of reachable terms). Given a signature (Σ, X ), a TRS R over it and a set of terms L ⊆ T (Σ), we note

R(L) = {t ∈ T (Σ) | ∃s ∈ L, s → R t} and R * (L) = t ∈ T (Σ) ∃s ∈ L, s → * R t . 9
Definition 10 (Left-linearity).

A TRS R is said to be left-linear if for each rule → r of R, the term is linear.

Definition 11 (Constructors and defined symbols, sufficient completeness). Given a TRS R over (Σ, X ), there is a partition (C, D) of Σ such that all symbols occurring at the root position of left-hand sides of rules of R are in D. D is the set of defined symbols of R, C is the set of constructors. Terms in T (C) are called data-terms. A TRS R over (Σ, X ) is sufficiently complete if for all s ∈ T (Σ), R * ({s}) ∩ T (C) ∅. A binary relation over some set S is an equivalence relation if it is reflexive, symmetric and transitive.

An equivalence relation

≡ over T (Σ) is a congruence if for all k ∈ N, for all f ∈ Σ k , for all t 1 , . . . , t k , s 1 , . . . , s k ∈ T (Σ) such that ∀i ∈ 1 ; k , t i ≡ s i , we have f (t 1 , . . . , t k ) ≡ f (s 1 , . . . , s k ).
12 Definition 13 (Equation, ≡ E ).

An equation over (Σ, X ) is a pair of terms (s, t) ∈ T (Σ, X ) × T (Σ, X ), that we note s = t. A set E of equations over (Σ, X ) induces a congruence ≡ E over T (Σ) which is the smallest congruence over T (Σ) such that for all s = t ∈ E and for all substitution θ : X → T (Σ), sθ ≡ E tθ. The classes of equivalence of ≡ E are noted with [•] E . 13 Definition 14 (Rewriting modulo E).

Given a TRS R and a set of equations E both over (Σ, X ), we define the

R modulo E rewriting relation, → R/E , as follows. For any u, v ∈ T (Σ), u → R/E v if and only if there exist u , v ∈ T (Σ) such that u ≡ E u, v ≡ E v and u → R v .
We define → * R/E , (R/E)(L) and (R/E) * (L) for L ⊆ T (Σ) as in Definitions 8 and 9.

14

Tree automata

Definition 15 (Tree automaton, delta-transition, epsilon-transition, new state).

An automaton over Σ is some A = (Σ, Q, Q F , ∆) where Q is a finite set of states, Q F is a subset of Q whose elements are called final states and ∆ a finite set of transitions. A delta-transition is of the form f (q 1 , . . . , q k ) q where f ∈ Σ k and q 1 , . . . , q k , q ∈ Q. An epsilon-transition is of the form q q where q, q ∈ Q. A configuration of A is a term in T (Σ, Q). A state q ∈ Q that appears nowhere in ∆ is called a new state. A configuration is elementary if each of its subconfigurations at depth 1 (if any) is a state. A configuration is trivial if it is just a state.

15

Remark. We simply write A to denote an automaton, write Q A for the set of states of A. We assimilate an automaton with its set of transitions. When taking a "new state", we silently expand Q A if needed. We are only rarely interested in Q F , the set of final states.

Definition 16.

Let A = (Σ, Q, Q F , ∆) be an automaton and let c, c be configurations of A. We say that A recognises c into c in one step, and note c

∈ Q, L (A, q) = t ∈ T (Σ) t * A
q . We extend this definition to subsets of

Q and note L (A) = L (A, Q F ). 16 4
Example 17.

Let Σ be defined with Σ 0 = {n, 0}, Σ 1 = {s, a, f }, Σ 2 = {c} where 0 is meant to represent integer zero, s the successor operation on integers, a the predecessor ("antecessor") operation, n the empty list, c the constructor of lists of integers and f intended to be the function on lists that filters out integer zero.

Let R = {f (n) → n, f (c(s(X), Y )) → c(s(X), f (Y )), f (c(a(X), Y )) → c(a(X), f (Y )), f (c(0, Y )) → f (Y ), a(s(X)) → X, s(a(X)) → X}. Let A 0 = {n
q n , 0 q 0 , s(q 0 ) q s , a(q s ) q a , c(q a , q n ) q c , f (q c ) q f }. We have

L (A 0 , q f ) = {f (c(a(s(0)), n))} and R(L (A 0 , q f )) = {f (c(0, n)), c(a(s(0)), f (n))}.
Definition 18 (Determinism, Completeness, Accessibility).

An automaton is deterministic if it has no epsilon-transition and for all delta-transitions τ ρ and τ ρ , if τ = τ then ρ = ρ . An automaton is complete if each of its non-trivial configurations is the left-hand side of some of its transitions. A state q of automaton A is accessible if L (A, q) ∅. An automaton is accessible if all of its states are.

18

Remark. Transitions may have "colours", like R for transition q R q . We will use colours R and E.

Definition 19.

Given an automaton A and a colour R, we denote by A R the automaton obtained from A by removing all transitions coloured with R.

19

Definition 20.

Given two states q, q of some automaton A and a colour E, we note q E A q when we have both q

E A q and q E A q. 20 Remark. q E, * A q is stronger than (q E, * A q ∧ q E, * A q). E, * A is an equivalence relation over Q A .
This relation is extended to a congruence relation over T (Σ, Q). The equivalence classes are noted with [•] E .

Definition 21.

Let A = (Σ, Q, Q F , ∆) be an automaton and E a colour. We note A/E the automaton over Σ whose set of states is Q/E, whose set of final states if Q F /E and whose set of transitions is We now give notations used for pair automata, the archetype of which is the product of two automata.

f ([q 1 ] E , . . . , [q k ] E ) q E f (q 1 , . . . , q k ) q ∈ ∆ ∪ [q] E q E q q ∈ ∆ ∧ [q] E q E .

Definition 22 (Pair automaton).

An automaton A = (Σ, Q, Q F , ∆) is said to be a pair automata if there exists some sets Q 1 and

Q 2 such that Q = Q 1 × Q 2 .

Definition 23 (Product automaton).

Let A = (Σ, Q, Q F , ∆ A ) and B = (Σ, P , P F , ∆ B ) be two automata. The product automaton of A and B is A × B = (Σ, Q × P , Q F × P F , ∆) where

∆ = f ( q 1 , p 1 , . . . , q k , p k ) q , p f (q 1 , . . . , q k ) q ∈ ∆ A ∧ f (p 1 , . . . , p k ) p ∈ ∆ B
∪ q, p q , p q q ∈ ∆ A ∪ q, p q, p p p ∈ ∆ B .

23

Definition 24 (Projections).

Let A = (Σ, Q, Q F , ∆) be a pair automaton, let τ ρ be one of its transitions and q, p be one of its states. We define Π 1 ( q, p ) = q and extend Π 1 (•) to configurations inductively:

Π 1 (f (γ 1 , . . . , γ k )) = f (Π 1 (γ 1 ) , . . . , Π 1 (γ k )). We define Π 1 (τ ρ) = Π 1 (τ) Π 1 (ρ). We define Π 1 (A) = (Σ, Π 1 (Q) , Π 1 (Q F ) , Π 1 (∆)). Π 2 (•)
is defined on all these objects in the same way for the right components.

24

Remark. Using Π 1 (A) amounts to forgetting the precision given by the right components of the states. As a result, L (Π 1 (A) , q) ⊇ L (A, q, p ).

Innermost strategies

In general, a strategy over a TRS R is a set of (computable) criteria to describe a certain subrelation of → R . In this paper, we will be interested in innermost strategies. In these strategies, commonly used to execute functional programs ("call-by-value"), terms are rewritten by always contracting one of the lowest reducible subterms.

Definition 25 (Innermost strategy).

Given a TRS R and two terms s, t, we say that s can be rewritten into t by R with an innermost strategy, and we note s → R in t, if s → R t and each strict subterm of the redex in s is a R-normal form. We define → * R in , R in (L) and R * in (L) as in Definitions 8 and 9.

25

Example 26.

Let us go on with Example 17: R in (L (A 0 , q f )) = {f (c(0, n))}.

26

Remark. It is in fact sufficient to check whether subterms of s at depth 1 are in normal form to decide whether s can be rewritten with an innermost strategy.

To deal with innermost strategies, we will have to discriminate normal forms. This is possible within the tree automaton framework when R is left-linear.

Theorem 27 ([CR87]).

Let R be a left-linear TRS. There is a deterministic and complete tree automaton IRR(R) whose states are all final except one, noted p red and such that L (IRR(R)) = Irr(R) and L (IRR(R), p red ) = T (Σ) Irr(R).

27

Remark. From determinism and the property of p red follows that for any state p different from p red , L (IRR(R), p) ⊆ Irr(R).

Remark. If a term is reducible, any term built upon it is also reducible. Thus any transition of IRR(R) where p red appears in the left-hand side will necessarily have p red as its right-hand side. Therefore, for brevity, these transitions will always be left implicit when describing the automaton IRR(R) for some TRS R.

Example 28.

In Example 17, IRR(R) needs, in addition to p red , a state p list to recognise lists of integers, a state p a for terms of the form a(. . . ), a state p s for s(. . . ), a state p 0 for 0 and a state p var to recognise terms that are not subterms of lhs of R, but may participate in building a reducible term by being instances of variables in a lhs. We note P = {p list , p 0 , p a , p s , p var } and P int = {p 0 , p a , p s }.

Classical equational completion

Equational completion of [START_REF] Genet | Equational tree automata completion[END_REF] is an iterative process on automata that is not guaranteed to terminate. Each iteration comprises two parts: (exact) completion itself, then equational merging. The former tends to incorporate descendants by R of already recognised terms into the recognised language; this leads to the creation of new states. The latter tends to merge states in order to ease termination of the overall process, at the cost of precision of the computed result. Some transition added by equational completion will have colours R or E; it is assumed that the transitions of the input automaton A 0 do not have any colour and that A 0 does not have any epsilon-transition.

Exact completion

Exact completion is about resolving critical pairs. A critical pair represents a situation where some term is recognised by the current automaton, but not its descendants by R. Its resolution consists in adding transitions to let the descendants be recognised as well. This process can create new critical pairs.

Definition 29 (Critical pair).

A pair ( → r, σ , q) where → r ∈ R, σ :

X → Q A and q ∈ Q A is critical if (see Figure 1(a)) 1. σ * A q and 2. rσ ¡ ¡ ¡ * A q. 29 σ rσ q q R A * A * A R (a) A critical pair sθ tθ q 1 q 2 E A * A * E A (b) Situation of ap- plication
Figure 1: A critical pair and a situation of application of an equation 7

We will want to close the square of Figure 2, that is to add transitions rσ q and q q . However, doing the former is not generally possible in one step, as rσ might be a nonelementary configuration. We will have to take steps and maybe introduce new states: this is what normalisation does. Given an automaton A, a configuration c of A and a new state q, we note Norm A (c, q) the set of transitions (with new states) that we add to A to ensure that c is recognised into q. The formal definition of normalisation is presented in Appendix A.

Example 30.

With a suitable signature, suppose that automaton A consists of the transitions c q 1 and f (q 1 ) q 2 and we want to normalise f (g(q 2 , c)) to the new state q N . We first have to normalise under g: q 2 is already a state, so it does not need to be normalised; c has to be normalised to a state: since A already has transition c q 1 , we add nothing and it remains to normalise g(q 2 , q 1 ). Since A does not contain a transition for this configuration, we must add a new state q and the transition g(q 2 , q 1 ) q . Finally, we add f (q ) q N . 30

Definition 31 (Completion of a critical pair).

A critical pair CP = ( → r, σ , q) in automaton A is completed by first computing N = Norm A¡ R (rσ , q ) where q is a new state, then adding to A the new states and the transitions appearing in N as well as the transition q R q. If rσ is a trivial configuration (ie. r is just a variable), only transition rσ R q is added.

31

Definition 32 (Step of completion).

Let P C be the set of all critical pairs of A i . For pc ∈ P C, let N pc be the set of new states and transitions needed under Definition 31 to complete pc.

Then A i+1 = A i ∪ pc∈P C N pc . 32
Example 33.

Let Σ be defined with Σ 0 = {n, 0}, Σ 1 = {s, a, f }, Σ 2 = {c} where 0 is meant to represent integer zero, s the successor operation on integers, a the predecessor ("antecessor") operation, n the empty list, c the constructor of lists of integers and f intended by some unwise person to be the function on lists that filters out integer zero.

Let R = {f (n) → n, f (c(s(X), Y )) → c(s(X), f (Y )), f (c(a(X), Y )) → c(a(X), f (Y )), f (c(0, Y )) → f (Y ), a(s(X)) → X, s(a(X)) → X}. Let A 0 = {n q n , 0 q 0 , s(q 0 ) q s , a(q s ) q a , c(q a , q n ) q c , f (q c ) q f }. We have L (A 0 , q f ) = {f (c(a(s(0)), n))} and R(L (A 0 , q f )) = {f (c(0, n)), c(a(s(0)), f (n))}.
There is a critical pair CP 1 in A 0 with the rule f (c(a(X), Y )) → c(a(X), f (Y )), the substitution σ 1 = {X → q s , Y → q n } and the state q f . It is resolved by adding transitions to recognise c(a(q s ), f (q n )) into q f . Normalisation finds and reuses the transition a(q s ) q a . It has to create a new state q N 1 such that f (q n ) q N 1 , and q N 2 such that c(q a , q N 1 ) q N 2 . We then add q N 2 R q f , and have produced J

(P C 1 ) R (A 0 ). Another critical pair is CP 2 in A 0 with the rule a(s(X)) → X, the substitution σ 2 = {X → q 0 }
and the state q a . It is resolved by adding to J

(P C 1 ) R (A 0 ) the transition q 0 R q a , producing J (P C 1 ,P C 2 ) R (A 0 ).
There is no more critical pair in

A 0 : thus C R (A 0 ) = J (P C 1 ,P C 2 ) R (A 0 ). There is a new critical pair in C R (A 0 ) with f (n) → n,
the empty substitution and state q N 1 . 33

Equational merging

Since completion of a critical pair can create new critical pairs, the process fuels itself, which is problematic for obtaining a fix-point. Equational merging is a way of countering this phenomenon at the cost of precision that is parametrised by equations over T (Σ).

Definition 34 (Situation of application of an equation).

Given an equation s = t, an automaton A, a θ : X → Q A and states q 1 and q 2 , we say that (s = t, θ, q 1 , q 2 ) is a situation of application in A if (see Figure 1(b))

1. sθ * A q 1 , 2. tθ * A q 2 and 3. q 1 ¡ ¡ ¡ E A q 2 .
34 Definition 35 (Application of an equation).

Given (s = t, θ, q 1 , q 2 ) a situation of application in A, applying the underlying equation in it consists in adding transitions q 1 E q 2 and q 2 E q 1 to A. This produces a new automaton A and we note A ; E A .

35

Remark. In [START_REF] Genet | Equational tree automata completion[END_REF], q 1 and q 2 were merged by "renaming" q 2 into q 1 , ie. removing q 2 from Q A and replacing every occurrence of q 2 by q 1 in the transitions of A. This is equivalent to applying our method, then considering automaton A/E (see definition 21) and finally choosing a representative (here q 1 for the class {q 1 , q 2 }) of each equivalence class of states.

Definition 36 (Simplified automaton).

Given an automaton A and a set of equations E, we call simplified automaton of A by E and note S E (A) the automaton resulting from the successive application of all applicable equations in A.

36

Remark (; E is confluent). Indeed, there is a unique automaton A ! that differs from A only by its E-transitions and is such A R ; * E (A ! ) R and there is no more situation of application of equations in (A ! ) R .

Definition 37 (Step of equational completion).

A step of equational completion is the composition of a step of exact completion, then equational simplification:

CE R,E (A) = S E (C R (A)). 37
The following notion is part of an easier discourse about the R/E-coherence notion of [START_REF] Genet | Equational tree automata completion[END_REF].

Definition 38 (Coherent automaton).

Let A 0 = (Σ, Q, Q F , ∆) be a tree automaton and E a set of equations. The automaton A 0 is said to be E-coherent if for all q ∈ Q, there exists s ∈ L (A 0 , q) such that L (A 0 , q) ⊆ [s] E .

Known results

We now recall the two main theorems of [START_REF] Genet | Equational tree automata completion[END_REF].

Theorem 39 (Correctness).

Let A 0 be some automaton. Assume the equational completion procedure defined above terminates when applied to A 0 . Let A * be the resulting fix-point automaton. If R is left-linear, then the calculated over-approximation is correct, that is

L (A * ) ⊇ R * (L (A 0 )). 39
We will make usage of E-coherence for the precision theorem.

Lemma 40.

Let A 0 be a E-coherent automaton, R a left-linear TRS and A be an automaton obtained from A 0 after several steps of equational completion with R, E. Then A R is E-coherent and moreover, for all state q of A, there exists s ∈ L (A R , q) such that L (A, q) ⊆ (R/E) * (s).

40 Such an automaton is said to be R/E-coherent. The intuition behind this is the following: in the tree automaton, R-transitions represent rewriting steps and transitions of A R recognise E-equivalence classes. More precisely, in a R/E-coherent tree automaton, if two terms s, t are recognised into the same state q in A R then they belong to the same E-equivalence class. Otherwise, if at least one R-transition is necessary to recognise, say, t into q then at least one step of rewriting was necessary to obtain t from s. In [START_REF] Genet | Equational tree automata completion[END_REF], the following theorem made an assumption of R/E-coherence for A 0 , but, given that A 0 does not have any R-transition

, A 0 is R/E-coherent if and only if it is E-coherent.
Theorem 41 (Upper bound).

Let E be a set of equations, A 0 a E-coherent tree automaton and R a left-linear TRS. If A is an automaton produced from A 0 after several steps of equational completion with R, E, then

L (A) ⊆ (R/E) * (L (A 0 )) 41

Adaptation to innermost strategies

Introduction

Our first contribution is an adaptation of the classical equational completion of [START_REF] Genet | Equational tree automata completion[END_REF]. The classical equational completion procedure with a left-linear TRS R produces a correct over-approximaton of R * (L 0 ) whenever it terminates. As R * in (L 0 ) ⊆ R * (L 0 ), this is a correct over-approximation of R * in (L 0 ) as well. Still, we would like to refine this procedure to deal more precisely with R in . Indeed, there are some critical pairs that we would not want to complete because they do not correspond to any innermost rewriting situation.

Example 42.

Let us look at Example 33. The rewriting of f (c(a(s(0)), n)) into c(a(s(0)), f (n)) does not conform to innermost strategy because a(s(0)) is not a normal form. We would like to abstain from completing CP 1 of Example 33.

Due to the definition of innermost rewriting, we will need to discriminate between normal forms and terms reducible by R. To do so is possible using the automaton IRR(R) (see Theorem 27). It is possible to build a product between A and IRR(R), the tree automaton recognising the normal forms of R. Let A • be an automaton recognising the initial language. Completion will start with A 0 = A • × IRR(R). This automaton enjoys the following property, which we will be useful to prove correctness.

Definition 43 (Consistency with IRR(R)).

A pair automaton A is said to be consistent with IRR(R) if, for any configuration c and any state q, p of A, Π 2 (c) is a configuration and p is a state of IRR(R), and if c * A q, p then

Π 2 (c) * IRR(R)
p.

43

In the next subsections, we will restate the definitions used by equational completion to adapt them to our new framework of pair automata. The TRS R is always supposed left-linear. Some parts of them might look tricky, and they are indeed tricks to preserve the property of consistency with IRR(R).

Exact completion Definition 44 (Innermost critical pair).

A pair ( → r, σ , q, p ) where

→ r ∈ R, σ : X → Q A and q, p ∈ Q A is critical if 1. σ * A q, p ,
2. there is no p such that rσ * A q, p and 3. for each subconfiguration γ at depth 1 of σ , the state q γ , p γ such that γ * A q γ , p γ in the recognition path of condition 1 is with p γ p red .

44

Remark. Because a critical pair denotes a rewriting situation, the p of definition 44 is necessarily p red as long as A is consistent with IRR(R).

Example 45.

In the situation of Examples 17-28, consider the rule f (c(a(X), Y )) → c(a(X), f (Y )), the substitution σ 1 = {X → q s , p s , Y → q n , p n } and the state q f , p red : this is not an innermost critical pair because the recognition path is f (c(a( q s , p s ), q n , p n ))

f (c( q a , p red , q n , p n )) f ( q c , p red ) q f , p red and so there is a p red at depth 1. But there is an innermost critical in A 0 with the rule a(s(X)) → X, the substitution σ 2 = {X → q 0 , p 0 } and the state q a , p red . 45 Normalisation is like in the classical case, except we deal with pairs q, p instead of just q. Note that whenever we add a new transition c q , p , only the q is arbitrary: the p is always the state of IRR(R) such that projdroitec

IRR(R)
p . Again, the formal definition presented in Appendix A, as it is technical and the details are not relevant to understanding the tree automata completion process. With a suitable signature, suppose that automaton A consists of the transitions c q 1 , p c and f ( q 1 , p c ) q 2 , p f (c) and we want to normalise f (g( q 2 , p f (c) , c)) to the new state q N , p f (g(f (c),c)) . We first have to normalise under g: q 2 , p f (c) is already a state, so it does not need to be normalised; c has to be normalised to a state: since A already has transition c q 1 , p c , we add nothing and it remains to normalise g( q 2 , p f (c) , q 1 , p c ). Since A does not contain a transition for this configuration, we must add a new state q , p g(f (c),c) and the transition g( q 2 , p f (c) , q 1 , p c ) q , p g(f (c),c) . Finally, we add f ( q , p g(f (c),c) ) q N , p f (g(f (c),c)) . Note that whenever we add a new transition c q , p , only the q is arbitrary: the p is always the state of IRR(R) such that projdroitec

σ rσ f (q 1 , . . . , q k ) q q R A * A A * A R (a) Classical σ rσ f ( q 1 , p 1 , . . . , q k , p k ) q, p red q , p rσ q, p rσ R in A * A p 1 , . . . , p k p red A * A R (b) Innermost
IRR(R) p . 46
The following definition comprises two parts. The first set of operation formalises "closing the square"; the supplementary operations ensure that any context that was recognised after q, p red will have a corresponding recognition path starting from q, p rσ .

Definition 47 (Completion of an innermost critical pair).

A critical pair ( → r, σ , q, p ) in automaton A is completed by first computing N = Norm A¡ R (rσ , q , p rσ ) where q is a new state and Π 2 (rσ ) * IRR(R)

p rσ , then adding to A the new states and the transitions appearing in N as well as the transition q , p rσ R q, p rσ . If rσ is a trivial configuration (ie. r is just a variable), only transition rσ R q, Π 2 (rσ ) is added. Afterwards, we execute the following supplementary operations. For any transition f (. . . , q, p red , . . . ) q , p , we add (if it is not present) a transition f (. . . , q, p rσ , . . . ) q , p with f (. . . , p rσ , . . . )

IRR(R)
p . These new transitions are in turn recursively considered for the supplementary operations.2

Definition 48 (Step of exact completion). This is the same definition as Definition 32, but using Definition 47 instead of Definition 31 for each critical pair. Given an equation s = t, an automaton A, a θ : X → Q A and states q 1 , p 1 and q 2 , p 2 , we say that (s = t, θ, q 1 , p 1 , q 2 , p 2 ) is a situation of application in Given (s = t, θ, q 1 , p 1 , q 2 , p 1 ) a situation of application in A, applying the underlying equation in it consists in adding transitions q 1 , p 1 E q 2 , p 1 and q 2 , p 1 E q 1 , p 1 to A.

A if 1. sθ * A q 1 , p 1 , 2. tθ * A q 2 , p 2 , 3. q 1 , p 1 ¡ ¡ ¡ E A q 2 , p
We also add the supplementary transitions q 1 , p 1 E q 2 , p 1 and q 2 , p 1 E q 1 , p 1 where q 1 , p 1 and q 2 , p 1 are variants that occur in the automaton.

50

Lemma 51.

Applying an equation preserves consistency with IRR(R).

51

Proof.

Let A be a consistent with IRR(R) automaton whose set of states is Q, let B result from the adjunction of transition q 1 , p 1 q 2 , p 1 to A due to the application of some equation. Notice that this is sufficient because of the symmetry between q 1 and q 2 . We proceed by induction on k, the number of times the transition q 1 , p 1 q 2 , p 1 occurs in the path c * B q, p where c is a configuration and q, p is a state of B. If there is no occurrence, then c * A q, p and by

consistency of A, Π 2 (c) * IRR(R) p.
Suppose the property is true for some k and there is a context

C on T (Σ, Q) such that c * A C[ q 1 , p 1 ] B C[ q 2 , p 1 ] * B
q, p with the last part of the path using less than k times the new transition. First, there is a configuration c 1 such that c = C[c 1 ] and c 1 * A q 1 , p 1 , and therefore Π 2 (c 1 ) * IRR(R)

p 1 . Second, by induction hypothesis, Π 2 (C[p 1 ]) * IRR(R) p. Finally, Π 2 (c) * IRR(R) Π 2 (C[p 1 ]) * IRR(R) p.
Remark. The condition 4 (p 1 = p 2 ) of definition 49 is obviously necessary for this lemma.

Here is why consistency is important and what would happen if we allowed equations to be applied without regard for condition 4 of Definition 49. Take R = {f (a) → w, g(f (b)) → c}, E = {a = b} and A • = {a q a , b q b , f (q a ) q f a , g(q f a ) q gf a }. We have

IRR(R) = {a p a , b p b , c p c , w p c , f (p a ) p red , f (p b ) p f b , f (p c ) p c , g(p f b ) p red , g(p c ) p c }
We omit the transitions whose left-hand side contains p red : they always have p red as a righthand side.

Remark that c ∈ R in (g(f (b))). However, g(f (b)) is not recognised by A • into any state and thus not by A • × IRR(R) either, so we are not interested in its successors. But let us apply the equation a = b without taking condition 4 of definition 49 into account: in particular, we add the transition q b , p b q a , p a . Therefore we now have g(f (b))

g(f ( q b , p b )) g(f ( q a , p a ))
g( q f a , p red ) q gf a , p red . We have g(f (b)) ∈ L (A, q gf a , p red ) and are thus now interested in its successors: we would like to have some critical pair involving g(f (b)) and c. But we do not, because the only recognition path of g(f (b)), the one we just created, does not fulfil condition 3 of definition 44.

Correctness Lemma 52.

Let A be an automaton obtained from some A • × IRR(R) after some steps of innermost completion. A is consistent with IRR(R).

52

Proof.

A • × IRR(R) is consistent with IRR(R) by construction. Lemma 51 shows that applying an equation preserves this. It remains to show that a step of exact completion does so as well.

The first steps of normalisation are preserving because the new q i , p i are precisely chosen such that Π 2 d |ξ i * IRR(R) p i . The last step of normalisation is preserving too, as well as the remaining operations of the completion of a critical pair, because, again, we choose p such that rσ * IRR(R)

p .

The same goes for the supplementary operations.

Lemma 53.

Let A be an automaton consistent with IRR(R), ( → r, σ , q, p ) a critical pair in A, let p rσ be the state of IRR(R) such that rσ * IRR(R)

p rσ and B be the automaton resulting from the completion of this critical pair. Let C be a context on T (Σ) and q 1 , p 1 a state of A such that C[ q, p ] * A q 1 , p 1 . Then there exists a state p 2 of IRR(R) such that C[ q, p rσ ] * B q 1 , p 2 .

53

Proof.

Note that we have p = p 1 = p red . We have to show that all the transitions used in the path C[ q, p red ] * A q 1 , p red have some counterpart starting from C[ q, p rσ ]. First, observe that all transitions used to recognise subterms at positions of C that are parallel to the position of the hole can remain unchanged. It remains to be shown that the transitions involving positions in the branch of the completion of the considered critical pair also have their counterpart: they exist thanks to the supplementary operations of definition 47.

Remark. The supplementary operations are necessary for this lemma. Indeed, take

R = {g(f (b)) → g(f (a)), f (a) → c}, A • = {b q b , f (q b ) q f b , g(q f b ) q gf b }. We have IRR(R) = {a p a , b p b , c p c , f (p a ) p red , g(p a ) p c , f (p b ) p f b , g(p f b ) p red , f (p c ) p c , g(p c ) p c }.
There is a critical pair P C 1 = (g(f (b)) → g(f (a)), ∅, q gf b , p red ) in A • ×IRR(R), which is resolved by adding transitions a q N 1 , p a , f ( q N 1 , p a ) q N 2 , p red , g( q N 2 , p red ) q N 3 , p red and q N 3 , p red q gf b , p red , thereby producing automaton A 1 . The supplementary operations do not create any new transition here.

There is a critical pair P C 2 = (f (a) → c, ∅, q N 2 , p red ) in A 1 , which is resolved by adding transitions c q N 4 , p c and q N 2 , p c , thereby producing automaton A 2 . The supplementary operations are detailed further down and produce automaton A 2 . Now consider that g(c) ∈ R in (g(f (a))) and g(f (a)) ∈ L (A 2 , q gf b , p red ) because we completed P C 1 . But all what we have is g(c)

A 2 g( q N 4 , p c ) A 2
g( q N 2 , p c ), this last configuration being not productive. As a result, g(c) L (A 2 , q gf b , p ) for any p .

The supplementary operations are made after completion of P C 2 . Since there is a transition g( q N 2 , p red ) q N 3 , p red , we add a transition g( q N 2 , p c ) q N 3 , p c . Then, since q N 3 A • either, and there is a q N 3 , p red q gf b , p red , we add q N 3 , p c q gf b , p c . No further transition needs to be added. These transitions allow g(c) ∈ L (A 2 , q gf b , p c ).

Definition 54 (Correct automaton).

An automaton A is correct wrt. R in if for all state q, p red of A, for all u ∈ L (A, q, p red ) and for all v ∈ R in (u), either there is a state p of IRR(R) such that v ∈ L (A, q, p ) or there is a critical pair ( → r, σ , q 0 , p 0 ) in A for some q 0 , p 0 and a context C on T (Σ) such that Any automaton produced by innermost completion starting from some A • ×IRR(R) is correct wrt. R in .

55

Proof.

Let A be such an automaton; it is consistent with IRR(R). Let q, p red be a state of A, u ∈ L (A, q, p red ) and v ∈ R in (u). By definition of innermost rewriting, there is a rule → r of R, a substitution µ : X → T (Σ) and a context C such that u = C[ µ], v = C[rµ] and each strict subterm of u is a normal form. Let u 0 = µ and v 0 = rµ. There is a q 0 , p red such that u 0 ∈ L (A, q 0 , p red ) and C[ q 0 , p red ] * A q, p red .

Since is linear, there is a σ :

X → Q A such that µ * A σ * A q 0 , p red and rµ * A rσ . This entails that u * A C[ σ ] * A C[ q 0 , p red ] * A q, p red and v * A C[rσ ].
Assume that there is no p 0 such that v 0 ∈ L (A, q 0 , p 0 ) and show that ( → r, σ , q 0 , p red ) is a critical pair in A. First, by assumption, there is no p such that rσ * A q 0 , p . Conditions 1 and 2 of definition 44 are thus met. Suppose = f (γ 1 , . . . , γ k ) and show that condition 3 of definition 44 holds. 3 For each i ∈ 1 ; k , let q i , p i be the state of A such that γ i µ * A γ i σ * A q i , p i in the path of recognition of σ . Then, by consistency with IRR(R), for each i ∈ 1 ; k , γ i µ * IRR(R) p i . Since strict subterms of µ are strict subterms of u as well, they are normal forms, thus p i p red , which validates condition 3 of definition 44.

Assume now that v 0 ∈ L (A, q 0 , p 0 ) and show that there is a p such that v ∈ L (A, q, p ). This is obvious at the initial step A • × IRR(R), and this property is conserved by completion as shown by lemma 53.

Theorem 56 (Correctness).

Assuming R is left-linear, the innermost equational completion procedure defined above produces a correct result whenever it terminates and produces some fixpoint A in * :

L (A in * ) ⊇ R * in (L (A • × IRR(R))).

56

Proof.

Let A in * be the calculated fixpoint automaton. By lemma 52, A in * is consistent with IRR(R), and therefore, by lemma 55, A in * is correct wrt. R in . Since this automaton is a fixpoint, the case of definition 54 where there remains a critical pair cannot occur, and therefore, for all state q, p red of A, for all u ∈ L (A in * , q, p red ) and for all v ∈ R in (u), there is a p such that v ∈ L (A in * , q, p ). Thus, A in * is R in -closed: R in (L (A in * )) ⊆ L (A in * ). Since the completion process only adds transitions, L (A in * ) ⊇ L (A • × IRR(R)), which concludes the proof.

Using innermost completion to improve accuracy of static analysis

We made an alpha implementation of innermost completion. This new version of Timbuk, named TimbukSTRAT, is available at [START_REF]Timbuk -reachability analysis and Tree Automata Calculations[END_REF] along with several examples. On those examples, innermost completion run within milliseconds. Sets of approximation equations, when needed, are systematically defined [START_REF] Genet | Tree Automata Completion for Static Analysis of Functional Programs[END_REF].

We now explain two of those examples add and sumlist1 showing that this tool can improve the accuracy of static analysis techniques. TRSs, and similar formalisms, have been shown to be a convenient model for static analysis of functional programs [START_REF] Jones | Flow analysis of lazy higher-order functional programs[END_REF][START_REF] Kochems | Improved Functional Flow and Reachability Analyses Using Indexed Linear Tree Grammars[END_REF] and Java programs [START_REF] Boichut | Rewriting Approximations for Fast Prototyping of Static Analyzers[END_REF]. In this setting, the static analysis tool itself only builds approximations of terms reachable with the TRS encoding the semantics of the program.

More relevant analysis for TRSs encoding the Java semantics

In the Java semantics, the add bytecode performs an addition of two integers x and y of a stack. Here is a simplified version of what should be the TRS encoding the effect of the add Java bytecode on a stack of integers:

plus(0, X) → X plus(s(X), Y ) → s(plus(X, Y )) add(stack(X, stack(Y , Z))) → stack(plus(X, Y ), Z)
However, to be coherent with Java semantics, this TRS should ensure that the addition x+y has been normalized before storing its result on the same stack. Since the tools building the approximations of reachable terms are not strategy-aware, they build rough approximations containing stacks of non-reduced integer additions, which are not reachable w.r.t. the Java semantics. In [START_REF] Boichut | Rewriting Approximations for Fast Prototyping of Static Analyzers[END_REF], the TRS representing the semantics of a Java programs had to be transformed so as to encode, in the TRS, the call-by-value of Java. Furthermore, a similar transformation is necessary for many of the Java bytecode operations, leading to an unnecessarily complicated TRS. This is also the case with methods commonly used to encode the innermost strategy into the program itself, such as continuation-passing-style transformations [START_REF] Plotkin | Call-by-name, call-by-value and the lambda-calculus[END_REF][START_REF] Danvy | Representing control: A study of the CPS transformation[END_REF].

Using innermost completion can totally avoid this problem. On the above TRS, the set of descendants computed by Timbuk STRAT with file add does not contain stacks of non-reduced integer additions.

Improving static analysis of functional programs

There is a recent and renewed interest for Data flow analysis of higher-order functional programs [OR11, KO11, KI13] that was initiated by [START_REF] Jones | Flow analysis of lazy higher-order functional programs[END_REF]. On examples taken from [START_REF] Ong | Verifying higher-order functional programs with patternmatching algebraic data types[END_REF], we showed in [START_REF] Genet | Tree Automata Completion for Static Analysis of Functional Programs[END_REF] that completion can compete with those techniques. None of those techniques is strategy-aware: on Example 17, they all consider the term c(a(s(0)), f (n)) as reachable, though it is not with innermost strategy. Example 17 also shows that this is not the case with innermost completion.

Accuracy of innermost completion can benefit to static analysis of functional programs. To illustrate this, we choose to show that approximations built with TimbukSTRAT are precise enough to prove non-termination of functions using call-by-value evaluation strategy. First, we recall how to prove non-termination using an approximation of reachable terms [START_REF] Genet | Decidable approximations of sets of descendants and sets of normal forms[END_REF]. Consider the following OCaml program, which can be represented as a TRS R: It is faulty: the recursive call should be (hd l)::delete(e, tl l). Any call delete(e, l) will not terminate if l is not empty and hd l is not e. Since the language of such calls to delete with l not empty is regular, completion can compute an automaton over-approximating of the set of reachable terms from this language. Besides, we can compute the automaton IRR(R) recognizing normal forms of R5 . Then, computing the intersection between the two automata, we obtain the automaton recognizing the set of reachable terms in normal form6 : this set is empty. This reflects the fact that the delete function does not compute any result, i.e. it is not terminating. Now, we perform the same kind of non-termination proof on a program which is terminating with call-by-name but not with call-by-value strategy. 7 The OCaml program sum x computes transition nth( q 0 , p i , q 2 , p red ) q 3 , p red . However, this cannot happen because q 2 does not recognise any irreducible term. Furthermore, during all the following completion steps, terms recognised by q 2 will all be reducible. We can illustrate this on the second completion step which only solves one critical pair: sumList( q 0 , p i , q 0 , p i ) cons( q 0 , p i + q 0 , p i , sumList( q 0 , p i + q 0 , p i , s( q 0 , p i )))

q 2 , p red q 6 , p red R A 1 * A 2 * A 2 R
Normalisation of the corresponding transition results in the following set of new transitions to be added to A 1 : cons( q 4 , p red , q 5 , p red ) q 6 , p red , q 0 , p i + q 0 , p i q 4 , p red , sumList( q 4 , p red , q 0 , p i ) q 5 , p red and q 6 , p red R q 2 , p red . Note that right-hand side of this critical pair is recognised by the state q 6 , p red . In fact, as explained above, all terms rooted by a sumList symbol will necessarily be recognised by p red . As a consequence, we will never be able to perform an innermost completion step on the transition nth( q 0 , p i , q 2 , p red ) q 3 , p red because the state q 2 , p red and all its successors will only contain terms having sumList symbols and thus being reducible. Using equations, it is possible to guarantee the termination of the completion (see [START_REF] Genet | Tree Automata Completion for Static Analysis of Functional Programs[END_REF]). On this example, having a set of equations containing at least equations s(s(X)) = s(X) and add(0, X) = X is enough to have a terminating completion. Rule (3) produces infinite lists with infinite sums of the form (((0+1)+3)+6)+. . .. The equations are used to merge together all the integers. Completion with TimbukSTRAT terminates on an automaton (see section B) where the only product state labelled by q 1 is q 1 , p red . This means that terms of the form sum(s * (0)) have no innermost normal form. Thus, this proves that the function sum is not terminating in OCaml, which uses a call-by-value strategy.

On the same example, all aforementioned techniques [OR11, KO11, KI13, Jon87], as well as all completion techniques [Tak04, GR10, Lis12], give a more coarse approximation and are unable to prove non-termination with call-by-value. Indeed, those techniques approximate all reachable terms, independently of the rewriting strategy. Their approximation will, in particular, contain the integer results that are reachable by a call-by-need evaluation strategy.

Precision theorem

We showed that accuracy of the approximation has a great impact on the quality of the static analysis. Now we formally quantify this accuracy w.r.t. rewriting modulo E. For this, we need the hypothesis that the initial automaton does not mix different equivalence classes into the same state.

Definition 57 (Separation of E-classes).

The pair automaton A separates the classes of E if for any q ∈ Π 1 (Q A ), there is a term s such that for all p ∈ Π 2 (Q A ), L (A, q, p ) ⊆ [s] E .

57

The following definitions are internal to the proof. We first give a notation for the common class of the terms recognised into a given state and extend this for configurations of the automaton.

Definition 58 (Equivalence class of a configuration).

Let A be an automaton that separates the classes of E. Let q be a left-component of a state (q ∈ Π 1 (A)). If there is a p ∈ Π 2 (A) such that L (A, q, p ) ∅, then the common E-class of all terms recognised by A into states of the form q, • is noted [q] A E . If there is no such p, we note [q] A E = ⊥. We extend this notation to configurations of A as follows. First, we note [ q, p ] A

E = [q] A E . Then, let c = f (c 1 , . . . , c k ) be a configuration of A. If there is an i ∈ 1 ; k such that [c i ] A E = ⊥, then let [c] A E = ⊥. Else, for each i ∈ 1 ; k , let t i ∈ L (Π 1 (A) , Π 1 (c i )). We note [c] A E = [f (t 1 , . . . , t n )] E . 58
Definition 59 (Total separation of classes).

Let A be an automaton separating the classes of E. We say that this separation is total if for any configuration

c of A, [c] A E ⊥.
59 Now, some purely technical remarks to make the proof more readable.

Definition 60 (Reflexivity equations).

For a signature (Σ, X ), the set of its reflexivity equations is

E r = {f (x 1 , . . . , x k ) = f (x 1 , . . . , x k ) | k ∈ N ∧ f ∈ Σ k ∧ x 1 , . . . , x k are distinct} . 60 Remark.
To ease the formulation of the proof, we will use a normalisation procedure that does not reuse already existing states, thus always normalising to new states. To compensate for this, we will add to E the set E r of reflexivity equations: equational simplification will merge the superfluous states that were created by this modified normalisation procedure. On the other hand, the equivalence classes of ≡ E are the same as those of ≡ E∪E r and equational simplification makes recognised languages bigger, so this way of doing is valid.

Here follows the property that will be passed on to each completed automaton A 1 , etc.

Definition 61 (R in /E-coherence).

An automaton A is R in /E-coherent if 1. A R totally separates the classes of E, 2.
A is accessible, and 3. for any state q, p of A,

L (A, q, p ) ⊆ (R in /E) * [q] A¡ R E .
61

The following two simple lemmas show that we do equational simplification or completion "for a reason". Lemma 62.

Let A be an automaton that totally separates the classes of E. Let (s = t, θ, q 1 , p , q 2 , p ) be a situation of application of an equation of

E in A. Then [q 1 ] A E = [q 2 ] A E . 62
Proof.

It suffices to prove that [sθ]

A E = [tθ] A E .
Since the separation of the classes by A is total, for each x in the domain of θ, there is a term xµ ∈ L (Π 1 (A) , xθ). This builds an instance sµ ≡ E tµ of the considered equation. But

[sθ] A E = [sµ] E and [tθ] A E = [tµ] E .
Lemma 63.

Let A be a R in /E-coherent automaton that is consistent with IRR(R), let ( → r, σ , q, p red ) be a critical pair that is to be completed by adding transition q , p rσ R q, p rσ . We suppose that the normalisation steps have just been performed and still note A the resulting automaton.

We have

L (A, rσ ) ⊆ (R in /E) * [q] A¡ R E . 63 Proof. let t ∈ T (Σ) such that t * A rσ * A¡ R
q , p rσ . For each variable x of r, let xµ be the subterm of t at the position where x occurs in r: we have thus t = rµ. For each variable y appearing in but not in r, let yµ be any term in L (A, yσ ). Since A is consistent with IRR(R) and the critical pair fulfils Condition 3 of Definition 44, each strict subterm of µ is a normal form. So t = rµ ∈ R in ( µ).

Moreover, µ ∈ L (A, q, p red ) and

A is R in /E-coherent, so t ∈ (R in /E) * [q] A¡ R E .
This is the main theorem of preservation.

Theorem 64.

Equational simplification preserves R in /E-coherence.

64

Proof.

Let (s = t, θ, q 1 , p 0 , q 2 , p 0 ) be a situation of application of an equation of E in A and let B be the automaton resulting from the merger of q1, p 0 and q 2 , p 0 . Let q, p be a state.

Show that L (B R , q, p ) ⊆ [q] A¡ R E . Consider u = C[u 0 ] * A¡ R C[ q 1 , p 0 ] E C[ q 2 , p 0 ] * A¡ R q, p .
We have

u 0 ∈ [q 1 ] A¡ R E , thus, by Lemma 62, u 0 ∈ [q 2 ] A¡ R E . Therefore u ∈ C[[q 2 ] A¡ R E ], which is just [q] A¡ R E .
Other cases are either trivial, symmetrical or reducible to this one. Next, show that L (B, q, p )

⊆ (R in /E) * [q] A¡ R E . Consider u = C[u 0 ] * A C[ q 1 , p 0 ] E C[ q 2 , p 0 ] * A q, p . We have u 0 ∈ (R in /E) * [q 1 ] A¡ R E , i.e. u 0 ∈ (R in /E) * [q 2 ] A¡ R E . Thus u ∈ (R in /E) * C[[q 2 ] A¡ R E ] . First, assume that C[ q 2 , p 0 ] * A¡ R q, p . Then C[[q 2 ] A¡ R E ] = [q] A¡ R E , therefore u ∈ (R in /E) * [q] A¡ R E .
Second, assume that C[ q 2 , p 0 ] * A q, p with just one R-transition, that is

C[ q 2 , p 0 ] * A¡ R D[rσ ] * A¡ R D[ q 3 , p 3 ] R D[ q 3 , p 3 ] * A¡ R
q, p . There is a corresponding critical pair ( → r, σ , q 3 , p red ) and, by Lemma 63, L (A, rσ

) ⊆ (R in /E) * [q 3 ] A¡ R E . On the other hand, D[[q 3 ] A¡ R E ] = [q] A¡ R E , so L (A, D[rσ ]) ⊆ (R in /E) * [q] A¡ R E .
Since (R in /E) * is an operator that deals with equivalence classes, every term equivalent to one of

L (A, D[rσ ]) is also a descendant of [q] A¡ R E by R in /E. Since C[[q 2 ] A¡ R E ] = D[[rσ ] A¡ R E ], u is a descendant of such a term, so u ∈ (R in /E) * [q] A¡ R E .
Finally, in the paragraph above, it suffices that D

[[q 3 ] A¡ R E ] ⊆ (R in /E) * [q] A¡ R E (we had D[[q 3 ] A¡ R E ] =
[q] A¡ R E ): this allows us to reuse this case as an induction step over the number of R-transitions present in the path C[ q 2 , p 0 ] * A q, p .

Dealing with reachable terms and strategies was first addressed in [START_REF] Réty | Regular Sets of Descendants by some Rewrite Strategies[END_REF] in the exact case for innermost and outermost strategies but only for some restricted classes of TRSs, and also in [START_REF] Gascon | Closure of Tree Automata Languages under Innermost Rewriting[END_REF]. As far as we know, the technique we propose is the first to over-approximate terms reachable by innermost rewriting for any left-linear TRSs. For instance, the Examples 17 and of Section 6 are in the scope of innermost completion but are outside of the classes of [START_REF] Réty | Regular Sets of Descendants by some Rewrite Strategies[END_REF][START_REF] Gascon | Closure of Tree Automata Languages under Innermost Rewriting[END_REF]. It is due to the fact that a right-hand side of a rule has two nested defined symbols and is not shallow.

Data flow analysis of higher-order functional programs is a long standing research topic [KI13, OR11, KO11, Jon87]. Used techniques ranges from tree grammars to specific formalisms: HORS, PMRS of ILTGs and can deal with higher-order functions. Higher-order functions are not in the scope of the work presented here, though it is possible with tree automata completion in general [START_REF] Genet | Tree Automata Completion for Static Analysis of Functional Programs[END_REF]. None of [KI13, OR11, KO11, Jon87], takes evaluation strategies into account and analysis results are thus coarse when program execution rely on a specific strategy.

Conclusion

In this paper, we have proposed a sound and precise algorithm over-approximating the set of terms reachable by innermost rewriting. As far as we know this is the first algorithm solving this problem for any left linear TRS and any regular initial set of terms. It is based on tree automata completion and equational abstractions with a set E of approximation equations. The algorithm also minimises the set of added transitions by completing the product automaton (between A • and IRR(R)). We proposed TimbukSTRAT [Tim14], a prototype implementation of this method.

The precision of the approximations have been shown on a theoretical and a practical point of view. On a theoretical point of view, we have shown that the approximation automaton recognises no more terms than those effectively reachable by innermost rewriting modulo the approximation E. On the practical side, unlike other techniques used to statically analyse functional programs [KI13, OR11, KO11, Jon87], completion can take the call-by-value strategy into account. As a result, for programs whose semantics highly depend on the evaluation strategy, innermost completion yields more accurate approximations. This should open new ways to statically analyse functional programs by taking evaluation strategies into account.

Approximations of sets of ancestors or descendants can improve existing termination techniques [START_REF] Geser | On tree automata that certify termination of left-linear term rewriting systems[END_REF][START_REF] Middeldorp | Approximations for strategies and termination[END_REF]. In the dependency pairs setting, such approximations can remove edges in a dependency graph by showing that there is no rewrite derivation from a pair to another. Besides, it has been shown that dependency pairs can prove innermost termination [START_REF] Giesl | Mechanizing and improving dependency pairs[END_REF]. In this case, innermost completion can more strongly prune the dependency graph: it can show that there is no innermost derivation from a pair to another. For instance, on the TRS: choice(x, y) → x choice(x, y) → y eq(s(x), s(y)) → eq(x, y) eq(0, 0) → tt eq(s(x), 0) → f f eq(0, s(y

)) → f f g(0, x) → eq(x, x) g(s(x), y) → g(x, y) f (f f , x, y) → f (g(x, choice(x, y)), x, y)
We can prove that any term of the form f (g(t 1 , choice(t 2 , t 3 )), t 4 , t 5 ) cannot be rewritten (innermost) to a term of the form f (f f , t 6 , t 7 ) (for all terms t i ∈ T (Σ), i = 1 . . . 7). This proves that, in the dependency graph, there is no cycle on this pair. This makes the termination proof of this TRS simpler than what AProVE [APr] does: it needs more complex techniques, including proofs by induction. Simplification of termination proofs using innermost completion should be investigated more deeply.

For further work, we want to improve and expand our implementation of innermost completion in order to design a strategy-aware and higher-order-able static analyser for OCaml. We also want to study if the innermost completion covers the decidable classes of [START_REF] Réty | Regular Sets of Descendants by some Rewrite Strategies[END_REF], like standard completion does for many decidable classes [START_REF] Feuillade | Reachability Analysis over Term Rewriting Systems[END_REF]. Another objective is to define a completion for the outermost strategy and thus deal with the call-by-need evaluation strategy, used in Haskell8 .

A. Normalisation

Here, we describe an algorithmic way to browse a configuration in order to normalise it, that is to create all the necessary intermediate transitions and the required new states. The discourse is quite fastidious and not unique, but this is not really important. Indeed, we either reuse existing transitions, and thus do not change the behaviour of the automaton, or create new states whose sole purpose is to recognise some subconfiguration of c. By definitions, these new states only appear in the new transitions that we add, they do not influence the previous behaviour of the automaton. The order in which they are added is therefore not important.

Definition 69 (Norm A (c, q, p )).

Let A be an automaton, c be a non-trivial configuration and q, p be any state. Let Ξ = (ξ 1 , . . . , ξ K ) be a postfix traversal of c (ξ K is the root position). With ∆ the set of transitions of A, let us use an auxiliary function:

Norm A (c, q, p ) = NormAux Ξ,1 ∆ (c, q, p ). (1)
Now let us define NormAux Ξ,i • . For i ranging from 1 to K -1, for any set of transitions ∆ and any configuration d such that d |ξ i is an elementary configuration, let NormAux Ξ,i ∆ (d, q, p ) = {d |ξ i q , p } ∪ NormAux Ξ,i+1 ∆∪{d |ξ i q ,p } (d q , p ξ i , q, p )

where q , p is such that d |ξ i q , p in ∆/E (or, if there is no such state, q is a new state, distinct from q, and p is the state such that Π 2 d |ξ i * IRR(R) p ). Also, for any set of transitions ∆ and any elementary configuration d, let

NormAux Ξ,K ∆ (d, q, p ) = {d q, p }.

(3)

Remark. It is necessary to consider equivalence by E when searching for an already existing transition. Suppose we work with some f (q 1 ) and have q 1 E ∆ q 2 and f (q 2 ) ∆ q : we do not want to create a new state here, but reuse q and set f (q 1 ) q .

B. Completed automaton for the sum function

Let R be the TRS:

(

1) 0 + X → X (2) s(X) + Y → s(X + Y ) (3) sumList(X, Y ) → cons(X + Y , sumList(X + Y , s(Y ))) (4) nth(0, cons(X, Y )) → X (5) nth(s(X), cons(Y , Z)) → nth(X, Z) (6) sum(X) → nth(X, sumList(0, 0))
and E = {cons(x, cons(y, z)) = cons(y, z), (x+y)+z = x+y}. Starting from the product automaton having transitions: 0 q 0 , p i , s( q 0 , p i ) q 0 , p i , sum( q 0 , p i ) q 1 , p red . We successively solve the following critical pairs.

B.1. First completion step

The first completion step solves only one critical pair which is: sum( q 0 , p i ) nth( q 0 , p i , sumList(0, 0))

q 1 , p red q 3 , p red R A 0 * A 1 * A 1 R
The set of transitions added to A 0 to obtain A 1 consists of nth( q 0 , p i , q 2 , p red ) q 3 , p red , sumList( q 0 , p i , q 0 , p i ) q 2 , p red , and q 3 , p red R q 1 , p red .

B.2. Second completion step

The second completion step solves one critical pair:

sumList( q 0 , p i , q 0 , p i ) cons( q 0 , p i + q 0 , p i , sumList( q 0 , p i + q 0 , p i , s( q 0 , p i )))

q 2 , p red q 6 , p red R A 1 * A 2 * A 2 R
Normalisation of the corresponding transition results in the following set of new transitions to be added to A 1 : cons( q 4 , p red , q 5 , p red ) q 6 , p red , q 0 , p i + q 0 , p i q 4 , p red , sumList( q 4 , p red , q 0 , p i ) q 5 , p red and q 6 , p red R q 2 , p red .

B.3. Third completion step

The third completion step solves two critical pairs. The first critical pairs are: 0 + q 0 , p i q 0 , p i q 4 , p red

q 4 , p i R A 2 * A 3 R s( q 0 , p i ) + q 0 , p i s( q 0 , p i + q 0 , p i ) q 4 , p red q 7 , p red R A 2 * A 3 * A 3 R
For solving the second critical pair, since the transition q 0 , p i + q 0 , p i q 4 , p red already belong to A 2 , it is enough to add the transitions: s( q 4 , p red ) q 7 , p red and q 7 , p red R q 4 , p red . For solving the first critical pair, it is enough to add the transition q 0 , p i R q 4 , p i and to add supplementary transitions, as mentioned in Definition 47. Because of the separation between states q 4 , p red and q 4 , p i , it is necessary to add a copy of all transitions with a state q 4 , p red in their left-hand side where we replace it by state q 4 , p i to . We thus add the transitions: cons( q 4 , p i , q 5 , p red ) q 6 , p red , sumList( q 4 , p i , q 0 , p i ) q 5 , p red and s( q 4 , p i ) q 7 , p i .

B.4. Fourth critical pair

The fourth completion step solves one critical pair and applies two equations. The critical pair is:

sumList( q 4 , p i , q 0 , p i ) cons( q 4 , p i + q 0 , p i , sumList( q 4 , p i + q 0 , p i , s( q 0 , p i ))) q 5 , p red q 8 , p red R

A 3 * A 4 * A 4 R
The transitions added to A 3 are thus: q 4 , p i + q 0 , p i q 9 , p red , sumList( q 9 , p red , q 0 , p i ) q 10 , p red , cons( q 9 , p red , q 10 , p red ) q 8 , p red and q 8 , p red R q 5 , p red . Now, with equation (x + y) + z = x + y of E, we can find a first equational simplification position: ( q 0 , p i + q 0 , p i ) + q 0 , p i q 0 , p i + q 0 , p i q 9 , p red q 4 , p red

E A * A * E E
This results in the addition of transitions q 9 , p E q 4 , p for all state p. Similarly the equation cons(x, cons(y, z)) = cons(y, z) of E finds an equational simplification position: 28 cons( q 4 , p red , cons( q 9 , p red , q 10 , p red )) cons( q 9 , p red , q 10 , p red ) q 6 , p red q 8 , p red E A * A * E E This results in the addition of transitions q 6 , p E q 8 , p for all state p.

B.5. Fith completion step

Now all critical pairs on rules (1) and (2) are joinable: 0 + q 0 , p i q 0 , p i q 9 , p red q 4 , p red q 9 , p i R

A 4 * A 4 R A 4
E s( q 0 , p i ) + q 0 , p i s( q 0 , p i + q 0 , p i ) q 9 , p red q 4 , p i q 7 , p red R

A 4 * A 4 * A 4 R A 4 E
There remains a last critical pair which is:

sumList( q 9 , p i , q 0 , p i ) cons( q 9 , p i + q 0 , p i , sumList( q 9 , p i + q 0 , p i , s( q 0 , p i ))) q 10 , p red q 8 , p red R A 4 * A 5 * A 5 R However, using transitions of A 4 the right-hand side of the critical pair can be recognised into state q 6 , p red . More in details, the subterm q 9 , p i + q 0 , p i can be normalised into q 4 , p red and the subterm sumList( q 9 , p i , s( q 0 , p i )) can be normalised into q 5 , p red . Finally cons( q 4 , p i , q 5 , p red ) q 8 , p red belongs to transitions of A 4 . Furthermore, q 6 , p red E q 8 , p red . Finally the only transition to add is thus q 8 , p red R q 10 , p red . Since no new transition is added on symbol sumList, this ends the completion. All remaining critical pairs are joinable, in particular: 29 sumList( q 9 , p i , q 0 , p i ) cons( q 9 , p i + q 0 , p i , sumList( q 9 , p i + q 0 , p i , s( q 0 , p i ))) q 10 , p red q 8 , p red R

A 4 * A 4 * A 4 R
The transitions of the completed automaton are: 0 q 0 , p i s( q 0 , p i ) q 0 , p i sum( q 0 , p i ) q 1 , p red nth( q 0 , p i , q 2 , p red ) q 3 , p red sumList( q 0 , p i , q 0 , p i ) q 2 , p red q 3 , p red R q 1 , p red cons( q 4 , p red , q 5 , p red ) q 6 , p red q 0 , p i + q 0 , p i q 4 , p red sumList( q 4 , p red , q 0 , p i ) q 5 , p red q 6 , p red R q 2 , p red s( q 4 , p red ) q 7 , p red q 7 , p red R q 4 , p red q 0 , p i R q 4 , p i cons( q 4 , p i , q 5 , p red ) q 6 , p red sumList( q 4 , p i , q 0 , p i ) q 5 , p red s( q 4 , p i ) q 7 , p i q 4 , p i + q 0 , p i q 9 , p red sumList( q 9 , p red , q 0 , p i ) q 10 , p red sumList( q 9 , p i , q 0 , p i ) q 10 , p red cons( q 9 , p red , q 10 , p red ) q 8 , p red q 8 , p red R q 5 , p red q 9 , p E q 4 , p for all p q 6 , p E q 8 , p for all p q 8 , p red R q 10 , p red Note that this completed automaton recognises, in particular, all infinite list of natural number, i.e. terms of the form cons(a, cons(b, cons(c, . . . sumList(d, e)))) where a, b, c, d, e are any natural numbers. For instance, the term cons(0, cons(0, cons(0, cons(0, sumList(0, 0))))) is recognised in the following way: cons(0, cons(0, cons(0, cons(0, sumList(0, 0)))))

* cons( q 0 , p i , cons( q 0 , p i , cons( q 0 , p i , cons( q 0 , p i , sumList( q 0 , p i , q 0 , p i )))))

R cons( q 0 , p i , cons( q 0 , p i , cons( q 0 , p i , cons( q 0 , p i , sumList( q 4 , p i , q 0 , p i )))))

R cons( q 0 , p i , cons( q 0 , p i , cons( q 0 , p i , cons( q 0 , p i , sumList( q 4 , p i , q 0 , p i )))))

E cons( q 0 , p i , cons( q 0 , p i , cons( q 0 , p i , cons( q 0 , p i , sumList( q 9 , p i , q 0 , p i ))))) cons( q 0 , p i , cons( q 0 , p i , cons( q 0 , p i , cons( q 0 , p i , q 10 , p red )))) cons( q 0 , p i , cons( q 0 , p i , cons( q 0 , p i , cons( q 0 , p i , q 10 , p red ))))

R cons( q 0 , p i , cons( q 0 , p i , cons( q 0 , p i , cons( q 4 , p i , q 10 , p red ))))

E cons( q 0 , p i , cons( q 0 , p i , cons( q 0 , p i , cons( q 9 , p i , q 10 , p red )))) cons( q 0 , p i , cons( q 0 , p i , cons( q 0 , p i , q 8 , p red )))

R cons( q 0 , p i , cons( q 0 , p i , cons( q 0 , p i , q 5 , p red )))

R cons( q 0 , p i , cons( q 0 , p i , cons( q 4 , p i , q 5 , p red )))

R cons( q 0 , p i , cons( q 0 , p i , q 6 , p red ))

E cons( q 0 , p i , cons( q 0 , p i , q 8 , p red ))

R cons( q 0 , p i , cons( q 0 , p i , q 5 , p red ))

R cons( q 0 , p i , cons( q 4 , p i , q 5 , p red ))

R cons( q 0 , p i , q 6 , p red ) E cons( q 0 , p i , q 8 , p red ) R cons( q 0 , p i , q 5 , p red ) R cons( q 4 , p i , q 5 , p red ) q 6 , p red R q 2 , p red

  6

  Definition 12 (Equivalence relation, congruence).

Ac

  if there a transition τ ρ in A and a context C over T (Σ, Q) such that c = C[τ] and c = C[ρ]. We note * A the reflexive and transitive closure of A and, for any q

21Remark.

  For any configurations c, c of A, we have c * A c if and only if [c] E * A/E c E . So the languages recognised by A and A/E are the same.

Figure 2 :

 2 Figure 2: Comparison of classical and innermost critical pairs

  48 4.3. Equational simplification Definition 49 (Situation of application of an equation).

  2 and 4. p 1 = p 2 . 49 Definition 50 (Application of an equation).

4 1

 4 let hd = function x :: _ -> x ;; 2 let tl = function _ :: l -> l ;; 3 let rec delete (e , l )= 4 if ( l =[]) then [] 5 else if ( hd l = e ) then tl l else ( hd l ):: delete (e , l );;

 1 In particular, any ground term is linear.

We add no new state in these supplementary operations, so this necessarily terminates.

If is a constant, then condition 3 is vacuously true.

See file nonTerm1 under TimbukSTRAT at[START_REF]Timbuk -reachability analysis and Tree Automata Calculations[END_REF].

For functional programs, computing IRR(R) can be easier than for general TRS: it can consist of the simple automaton recognising constructor terms[START_REF] Genet | Tree Automata Completion for Static Analysis of Functional Programs[END_REF].

Computing IRR(R) and the intersection can be done using Timbuk.

See file sumlist1.txt.

Note that in tree automata completion every computation is done only once, associated to a state and shared in the tree automaton, as in call-by-need.

Acknowledgements The authors thank René Thiemann for providing the example of innermost terminating TRS submitted to AProVE, and Prof. Luke Ong, Jonathan Kochems and Robin Neatherway for their remarks.

the sum of the x first natural numbers. It does not terminate because of OCaml's call-by-value evaluation. Strategy-unaware methods cannot show this: there are (outermost) reachable terms that are in normal forms: the integer results obtained with a call-by-need or lazy evaluation.

1 let rec sumList (x , y )= 2 ( x + y ):: sumList ( x +y , y +1);; 3 let rec nth i ( x :: l )= 4 if i <=0 then x else nth (i -1) l ;; 5 let sum x = nth x ( sumList (0 ,0));;

1 Ops sum :1 nth :2 sumList :2 cons :2 nil :0 zero :0 s :

Assume that we want to over-approximate the set of results of the function sum for all natural number i. Thus, our aim is to compute the automaton recognising the set of innermost reachable terms from the initial regular language {sum(s * (0

q 0 , s(q 0 ) q 0 , sum(q0) q 1 } be an automaton recognising this language. Timbuk [Tim14] can compute the automaton IRR(R), whose description is then appended to the definition of the TRS in sumlist1.txt. In this automaton, all transitions with top symbol sum are mapped to p red . This is not surprising since the rule sum(X) → nth(X, sumList(0, 0)) rewrites any term rooted by sumList, i.e. they are all reducible. This is the same for all transitions rooted by the sumList symbol.

On the opposite, terms built only on symbols s and 0 are all irreducible. Let us denote by p i the state recognising them in IRR(R). Let us denote by A 0 , A 1 , . . . the tree automata obtained by innermost completion. Let A 0 = A • × IRR(R) be the initial product automaton whose set of transitions is: 0 q 0 , p i , s( q 0 , p i ) q 0 , p i , sum( q 0 , p i ) q 1 , p red . The first completion step solves only one critical pair which is: sum( q 0 , p i ) nth( q 0 , p i , sumList(0, 0))

During the normalisation of the new transition nth( q 0 , p i , sumList(0, 0)) q 3 , p red , the subterm 0 is normalised using the transition 0 q 0 , p i of A 0 and the subterm sumList( q 0 , p i , q 0 , p i ) is normalised using a new state q 2 , p red . Thus, according to Definition 47, the set of transitions added to A 0 to obtain A 1 is nth( q 0 , p i , q 2 , p red ) q 3 , p red , sumList( q 0 , p i , q 0 , p i ) q 2 , p red , and q 3 , p red R q 1 , p red . Since no other critical pair with symbol sum will never be solved, the language of reachable terms from sum(s * (0)) is recognised by q 1 and thus by q 3 . For q 3 to recognise irreducible terms, it necessary to discard the nth symbol by applying either rule (4) or (5) of R, i.e. have an innermost critical pair between rules (4) or (5) and the Because we decided to always use fresh states for normalisation, the step about completion of a critical pair is simpler.

Lemma 65.

Normalisation preserves R in /E-coherence. So do the supplementary operations performed after completing a critical pair. 65 Lemma 66.

Completion of a critical pair preserves R in /E-coherence.

66

Proof.

Let ( → r, σ , q, p red ) be a critical pair and let it be completed by normalisation and adding transition q , p R q, p . Let B be the resulting automaton. It is enough to show that

Remember that we use a modified version of normalisation that never reuses existing states, so L (B, q , p ) = L (A, rσ ). We conclude thanks to Lemma 63.

Theorem 64 and Lemma 66 can be summed as follows.

Theorem 67.

Innermost equational completion preserves R in /E-coherence.

67

This shows that under the assumption that A 0 separates the classes of E, innermost completion will never add to the computed approximation a term that is not a descendant of L (A 0 ) through R modulo E rewriting.

Theorem 68 (Precision).

Let E be a set of equations. Let A 0 A • × IRR(R), where A • has designated final states. We prune A 0 of its non-accessible states. Suppose A 0 separates the classes of E. Let R be any leftlinear TRS. Let A be obtained from A 0 after some steps of innermost equational completion. Then L (A) ⊆ (R in /E) * (L (A • × IRR(R))).

68

Proof.

Since A 0 does not contain any R-marked transition, A R 0 = A 0 . Thus, the third condition of (R in /E)-coherence is trivial for A 0 assuming the two first are met (for any TRS R). Plus, A 0 separates the classes of E and is accessible, so it totally separates the classes of E, so A 0 is indeed (R in /E)-coherent. Theorem 67 show that this property is passed to A, which yields the result.

Related work

All tree automata completion-like techniques [Gen98, TKS00, Tak04, FGVTT04, BCHK09, GR10, Lis12] do not take evaluation strategies into account. They compute over-approximations of all reachable terms. Our contribution here is to propose the first algorithm computing over-approximations restricted to innermost reachable terms. Furthermore, the accuracy of the approximation w.r.t. innermost rewriting has been shown on a practical and theoretical point of view.