Claudia Chan Yone

Jean-Louis Milan

Jean-Marie Rossi

Jean-François Witz

Mathias Brieu

Patrick Chabrand

Homogenization and µCT analysis for the trabecular bone remodeling

Introduction

Osteoporosis is a bone disease characterized by low bone mass but also a degradation of cancellous bone micro-architecture. Bone weakness can generate fracture, that is why tools have been developed to assess probability of fracture. The clinical device DEXA, is a quantitative measure of bone mineral density (result is a T-score), while FRAX R (1) is a questionary based on statistical analysis including criteria like age, bone mass index and lifestyle. Although those informations are essential in fracture assessment, one in two person undeclared osteoporotic according to WHO definition (T-score < -2.5) will have a fracture (2; 3; 4; 5). That is why bone quantity, or statistical analysis are unsufficient to predict bone weakness, but bone quality i.e bone micro-structure should be considered.

Many numerical models have been developed in purpose to predict bone alteration and so fracture assessment. Bone alteration is due to an imbalance in the bone remodeling process : quantity of new deposited tissue is smaller than the removal old matrix tissue. Furthermore, bone is well known to adapt its morphology to the mechanical environment. From those observations many researchers developed numerical models based on biological and/or mechanical criteria (6; 7; 8; 9; 10; 11; 12; 13). Among those theoritical approachs, some authors worked on real cancellous bone micro-architecture alteration (14; 15; 16; 17; 18). They have simulated 1 trabecular plate perforation, decrease of bone volume fraction and loss of mechanical properties which can lead to bone fracture. Those approachs are interesting because they used real human bone, and predicted realistic altered cancellous micro-structure due to aging or disease.

Those models used micro-finite element analysis (µFEA) based on 3-D reconstruction from micro-computed tomography acquisition (µCT). Voxels are directly convert in finite elements, as a consequence models are composed of several millions of elements (until 20 millions). The quantity of degree of freedom is not compatible with an iterative process in order to consider biological or mechanical stimuli changes. That is why alteration was randomly distributed over trabeculae and consider not any mechanical criteria. However mechanical environment play a crucial role in activation [START_REF] Klein-Nulend | Sensitivity of osteocytes to biomechanical stress in vitro[END_REF] and localization of bone remodeling : indeed damage and cracks are generally used as precusors of bone remodeling (20; 21; 22; 23).

In this study we will present a method to build µFE model from µCT acquisition reducing degree of freedom in order to simulate bone degradation with an iterative process, so that to integrate mechanical stimuli variations (bed-ridden case), or biological modifications (medical treatment). We will study what is the influence of reducing model complexity in term of mechanical global and local behaviour. Furthermore we will investigate if material heterogenities, like hypermineralized bone, influence repartition of areas which are over or under-constrained among the structure. Indeed, hypermineralized bone is a privileged place of cracks accumulation [START_REF] Vajda | Age-related hypermineralization in the female proximal human femur[END_REF], and can play an important role in ordre to identify remodeling sites.

Materials and methods

Trabecular bone sample and µCT imaging

Studied bone is a human femoral head collected behind a femoral neck fracture. The willing donor, was a woman aged of 87 years old, her bone mass index was 19.8 (limit underweight ≤ 18.5) and was prone to bone weakness because she fractured her shoulder in the past.

A cubic specimen was harvested (10x10x10mm) from femoral head and prepared removing marrow with a water bath (37 • C) containing a stirring rod. Remaining marrow was extracted with compressed air. Sample was scanned by a µCT system (model Skyscan 1172) at 20µm resolution. Cross-section images were stored in 16-bit format (format tif) with 1000x1000 pixels in size. Phantoms of cortical and trabecular bone were placed under the sample with respectively a density of hydroxyapatite of 1750 and 800mg/cm 3 , i.e a physical density of 2.17 and 1.53g/cm 3 . These latters gave us a grayscale reference to identify material component and so mechanical properties. Some morphologic datas were computed directly after acqusition by the sofware SKYSCAN CTANalyser (table 1).

BV/TV (%) BS/BV (mm -1 ) SMI Tb,Th (mm) Tb,N (mm

Thresholding and mass computation

Repartition of gray-value of whole volume was plotted (figure 3). Two significant peaks were identified : the highest correspond to the background gray-value (remaining marrow and artefacts), although the smallest correspond to the bone tissue gray-value. Thresholding between background and bone tissue was determined as the middle point between these two peaks. As the black dash-line is cortical phantom gray-value, this graph puts forward the hypermineralized bone : around 70% of bone elements are hypermineralized.

Initial bone mass noted M 0 was computed supposing that element bone mass was linearly correlated to the gray-value element. For coarsened geometry, mass was computed from mass density and also, cortical and trabecular phantom gray-value : each bone mass element was computed and added to get total bone mass. Thresholding was made as sample bone mass was in best agreement with M 0 , so as

|M -M 0 | M 0 ≤ 0.1%.

Material heterogeneous method

Finite element model were generated directly from converting voxels to equally sized eightnode brick elements. All elements are considered elastic linear isotropic. Poisson's ratio was set to 0.3 and Young Modulus value was calculated with the formula ( 25) :

E element = E max (GV element ) γ (1)
where GV element is the normalized gray-value of the element, γ a constant set to 1.5, and E max is the maximal elastic modulus according to maximal gray-value considered and is determined with the equation 2:

E max = exp log(E cort ) -γlog GV cort GV max (2)
where E cort is cortical bone elastic modulus defined by nano-indentation and set to 19GPa

(27; 28), GV cort is cortical phantom gray-value, and GV max is maximum gray-value of coarsened volume. E cort was considered as treshold between mineralized and hypermineralized bone because at microscopic scale cancellous and cortical bone elastic modulus are similar [START_REF] Turner | The elastic properties of trabecular and cortical bone tissues are similar: results from two microscopic measurement techniques[END_REF].

More than 99.9% of bone elements have a Young modulus between 13 and 40GPa, with a maximum at 23GPa (figure 4).

Binarization method

As previous method, finite element model were generated directly from converting voxels to a Poisson's ratio was set to 0.3 and Young Modulus set to 19GPa.

Computation and post-processing

Marrow and isolated elements were removed from the finite element analysis. Three static compression tests were simulated with an uniaxial displacement so that global mean strain was equal to -0.3%. Loading was imposed on one face of the sample, on the opposite face displacement along the loading was constrained, furthermore one node was encastred (to avoid part sliding). Reaction force was computed to determine apparent Young modulus of the structure and also strain energy density (directly computed with post-processing Abaqus software).

Influence of homogenization

As far as global mechanical behaviour is concerned, apparent Young modulus was computed in 3 principal directions -→ x , -→ y and -→ z which correspond to normal sample faces, for different coarsen voxel size. Apparent Young modulus were sorted as

E 3 > E 2 > E 1 , with E 3 = E z , E 2 = E x and E y = E 1 .
Results are plotted in figure 6 As far as local mechanical behaviour is concerned, we compared distribution of strain energy density between initial and coarsen model. Bone tissue where strain exceeds 3000µε, which can correpond from a biological point of view to remodeling sites, were identified. Indeed, when strain stimulus is over 3000µε new bone tissue is apposed [START_REF] Frost | On our age-related bone loss: Insights from a new paradigm[END_REF], that is why we focused on hyper-stimulated bone, where strain energy density is over w max defined by : remodeling sites is around two voxels, and relative resorbable volume error is low (table 3).

w max = 1 2 E bone ε 2

Influence of binarization

Binarized model, generally used in literature, was computed in order to compare influence of material heterogeneities on mechanical behaviour. Mean relative error on apparent Young modulus due to difference of mineralization is 7.5%, which is in agreement with literature [START_REF] Zebaze | Differences in the degree of bone tissue mineralization account for little of the differences in tissue elastic properties[END_REF].

Furthermore relative mean strain energy density error is less than 10 % (table 4). 8). Material heterogeneities do not influence the global mechanical behaviour, nevertheless its influence volume of remodeling sites.

Heterogeneous model

Influence of thresholding

After µCT acquisition, thresolding was made to distinguish background to bone tissue. This step is essential for the rest of the numerical study. Indeed a threshold variation result in variation in bone volume fraction and maximal stiffness [START_REF] Hara | The influence of microcomputed tomography threshold variations on the assessment of structural and mechanical trabecular bone properties[END_REF].

Treshold value was chosen as the middle point between the two significant peaks on grayscale distribution (figure 3), nevertheless a variation of 5% in tresholding was possible and results in a variation of 5% on bone volume fraction. Higher is coarsen voxel size, higher is the difference in bone volume fraction because voxel volume increases while coarsening (table 5). Moreover many tresholding were made on coarsen models, and a linear relationship was established between apparent Young modulus versus gray-value tresholding (figure 9). Decreasing grayvalue treshold consiste in considering thicker trabeculaes and so micro-structure becomes stiffer. Coarsening method is a relevant method to get mechanical cancellous bone properties, nevertheless, as trabeculae are relatively thin, voxel size is limited in order to keep connectivity and realistic bone morphology. Indeed a trabeculae should be composed of 4 or 5 voxels to be relevant in term of mechanical behaviour [START_REF] Charras | Improving the local solution accuracy of large-scale digital image-based finite element analyses[END_REF]. A numerical study with a voxel size upper than 80µm is not conceivable in order to simulate realistic case.

As a conclusion, it is now possible to compute cancellous bone mechanical properties of realistic sample (8x8x8mm) with directly coarsened voxel while reducing the computational cost.

However, a remodeling process can be planned in order to simulate a physiological case : bone alertation due to a low-loading case (bed-ridden case, microgravity), or bone adaptation due to an overloading case (sport). Lastly, as hypermineralized bone is a privileged place of cracks

8 Figure 1 :Figure 2 :

 812 Figure 1: Principle of coarsening in two dimensions : n m contain m x m voxels of 20µm

Figure 3 :

 3 Figure 3: Grayscale of whole reference volume (without coarsening), black solid line is tresholding void/bone and black dotted line is tresholding bone/hypermineralized bone

Figure 4 :

 4 Figure 4: Young modulus distribution taking account of hypermineralized bone for initial voxel size (without coarsening)

Figure 5 :

 5 Figure 5: Schematization of method : from micro-tomography acquisition to post-processing of FEA

Figure 6 :

 6 Figure 6: Relative apparent Young modulus error (a) and relative mean strain energy error (b) computed for coarsened model

  max with E bone = 19GP a, and ε max = 3000µε (3) sites, mean distance between remodeling sites was calculated in coarsen model and compared 112 with initial model. Smaller is this value, better is the accuracy of coarsen model. Moreover 113 volume remodeling sites, that is to say bone tissue where strain density exceed 3000µε were 114 compared. As a results, remodeling sites are located in the same place on both coarsen and 115 initial model (figure 7 (a) and (b)). For coarsen voxel of 60 µm, mean distance between 116

Figure 7 :

 7 Figure 7: Comparaison of strain energy distribution on initial (a) and coarsen model (b) -Localization of remodeling sites on initial (c) and coarsen model (d)

Figure 8 :

 8 Figure 8: Localization of remodeling sites on heterogeneous and binarized model : sites are located on same place, but more expanded in heterogeneous case which correspond to hypermineralized bone tissue (Young modulus¿19GPa)

Table 1 :

 1 -1 ) Tb,Sp (mm) DA Morphometric parameters computed after µCT acquisition

	29.87	10.18	0.69	0.343	0.869	0.769	0.677
	BV/TV : Bone Volume/ Total Volume; BS/BV : Bone Surface/Bone Volume; SMI : Structure Model Index
	Tb,Th : Trabeculae Thickness; Tb,N : Trabeculae Number; Tb,Sp : Trabeculae Space; DA : Degree of Anisotropy
	Homogenization/Coarsening method
	For the numerical study a central cubical sub-volume equivalent to 4x4x4mm (200x200x200
	voxels) was extracted. A coarsening method (25; 26) was applied on the whole volume contain-
	ing both marrow and bone tissue elements : figure 1 describe the principle in two dimensions

: initial voxels of 20x20µm 2 were grouped to new voxels of 40x40µm 2 until 100x100x100µm 2 . Initial micro-structure is showed in 3 dimensions without marrow voxels in figure

2

(a), and figure 2(c) to figure 2(f) illustrate different case of coarsened voxel. This method allows to simulate degradation of system acquisition, but also to reduce numbers of voxels contained in studied volume.

Table 2 :

 2 Number of bone element in finite element analysis and computation time

	distance remodeling relative resorbable volume	error sites (µm) (%)	--	29 0.1	62 1.4	199 22.1	153 27.4
	maximal Von relative error mean	Mises stress (MPa) strain energy density (%)	488.8 0	298.5 2.8	185.1 4.2	184.3 18.3	162.7 29.2
	voxel size	(µm)	20	40	60	80	100

Table 3 :

 3 Maximal von mises stress and strain energy density for different degree of coarsening

Table 4 :

 4 Apparent young modulus and mean strain energy density on heterogeneous and bina-

	Binarized model

Table 5 :

 5 Difference in bone volume fraction and apparent Young modulus for a variation of 5% , we have numerically built new voxels whose gray-value correspond to an average of initial gray-values. This methods allows to increase numerically voxel size, which decrease number of considered elements and degree of freedom for the finite element analysis. From a biomechanical point a view, if we are interested in bone remodeling we should compare the agreement of remodeling sites between coarsen and initial model. If we focus on sites where strain exceeds 3000µε, which correspond to the treshold of activation of new bone tissue deposit, we have seen that over-constrained areas in coarsen and initial model one voxel size away, for a coarsen voxel of 60µm. This difference of localization is negligible at osteoclast scale because during remodeling process, several osteoclasts, which measure until 100µm of diameter, come on trabeculae surface and dig a channel on hundred micrometers on trabeculae bone surface. So a variation of 60µm on remodeling site localization is insignificant.Compared to binarization method which is largely used in the literature, it was put forward that in a hypermineralized bone tissue, volume of bone where strain energy density is over 3000µε is under estimated at 19% in a binarized model. Nevertheless binarization give an accurate global mechanical behaviour until coarsen voxel of 60µm. Cancellous bone mechanical properties are more dictated by the micro-structure than local material heterogeneities.

		1900
	apparent Young modulus (MPa)	1400 1500 1600 1700 1800	40um 60um 80um 100um
		1.35 1300	1.4	1.45	1.5	1.55	1.6	1.65
			gray-value treshold (Hounsfield Unit)	x 10 4
	Figure 9: Linear relationship between apparent Young modulus (E3) and gray-value treshold
	voxel size Difference in bone Difference in apparent
	(µm)	volume fraction (%)	Young modulus (%)
	20		3.5				X
	40		3.5				6.3
	60		4.1				8.6
	80		10.3				8.2
	100		13.7				9
	in tresholding
	4 Discussion
	Mechanical cancellous bone properties is a decisive parameter in bone fracture. Numerical
	simulations allow to quantify elastic bone properties during disease or aging (16; 18; 14). Nev-
	ertheless those methods use millions of elements and models are not suitable for simulation of
	iterative process like bone remodeling. So mechanical consideration, like stress concentration,
	or local mechanical stimulus (inside tissue bone) are not available due to computational cost.

In this paper we studied the influence of coarsening voxel size in term of global mechanical behaviour, but also in term of local mechanical behaviour. From micro-tomography acquisi-tion

 [START_REF] Müller | Long-term prediction of three-dimensional bone architecture in simulations of pre-, peri-and post-menopausal microstructural bone remodeling[END_REF]


Payet Étienne
email: etienne.payet@univ-reunion.fr

Lim

Guided Unfoldings for Finding Loops in Standard Term Rewriting

Keywords: term rewrite systems, dependency pairs, non-termination, loop, unfolding

In this paper, we reconsider the unfolding-based technique that we have introduced previously for detecting loops in standard term rewriting. We modify it by guiding the unfolding process, using disagreement pairs in rewrite rules. This results in a partial computation of the unfoldings, whereas the original technique consists of a thorough computation followed by a mechanism for eliminating some rules. We have implemented this new approach in our tool NTI and conducted successful experiments on a large set of term rewrite systems.

Introduction

In [START_REF] Payet | Loop detection in term rewriting using the eliminating unfoldings[END_REF], we have introduced a technique for finding loops (a periodic, special form of non-termination) in standard term rewriting. It consists of unfolding the term rewrite system (TRS) R under analysis and of performing a semi-unification [START_REF] Lankford | A finite termination criterion[END_REF] test on the unfolded rules for detecting loops. The unfolding operator U R which is applied processes both forwards and backwards and considers every subterm of the rules to unfold, including variable subterms.

Example 1. Let R be the TRS consisting of the following rules (x is a variable):

R 1 = f(s(0), s(1), x) l → f(x, x, x) r R 2 = h → 0 R 3 = h → 1 .
Note that R is a variation of a well-known example by Toyama [START_REF] Toyama | Counterexamples to the termination for the direct sum of term rewriting systems[END_REF]. Unfolding the subterm 0 of l backwards with the rule R 2 , we get the unfolded rule U 1 = f(s(h), s(1), x) → f(x, x, x). Unfolding the subterm x (a variable) of l backwards with R 2 , we get U 2 = f(s(0), s(1), h) → f(0, 0, 0). Unfolding the first (from the left) occurrence of x in r forwards with R 2 , we get U 3 = f(s(0), s(1), h) → f(0, h, h). We have {U 1 , U 2 , U 3 } ⊆ U R (R). Now, if we unfold the subterm 1 of U 1 backwards with R 3 , we get f(s(h), s(h), x) → f(x, x, x), which is an element of U R (U R (R)).

The left-hand side l 1 of this rule semi-unifies with its right-hand side r 1 i.e., l 1 θ 1 θ 2 = r 1 θ 1 for the substitutions θ 1 = {x/s(h)} and θ 2 = {}. Therefore, lθ 1 = f(s(h), s(h), s(h)) loops with respect to R because it can be rewritten to itself using the rules of R (the redex is underlined at each step):

f(s(h), s(h), s(h)) → R2 f(s(0), s(h), s(h)) → R3 f(s(0), s(1), s(h)) → R1 f(s(h), s(h), s(h)) .

Iterative applications of the operator U R result in a combinatorial explosion which significantly limits the approach. In order to reduce it, a mechanism is introduced in [START_REF] Payet | Loop detection in term rewriting using the eliminating unfoldings[END_REF] for eliminating unfolded rules which are estimated as useless for detecting loops. Moreover, in practice, three analyses are run in parallel (in different threads): one with forward unfoldings only, one with backward unfoldings only and one with forward and backward unfoldings together.

So, the technique of [START_REF] Payet | Loop detection in term rewriting using the eliminating unfoldings[END_REF] roughly consists in computing all the rules of U R (R), U R (U R (R)), . . . and removing some useless ones, until the semi-unification test succeeds on an unfolded rule or a time limit is reached. Therefore, this approach corresponds to a breadth-first search for a loop, as the successive iterations of U R are computed thoroughly, one after the other. However, it is not always necessary to compute all the elements of each iteration of U R . For instance, in Ex. 1 above, U 2 and U 3 do not lead to an unfolded rule satisfying the semiunification criterion. This is detected by the eliminating mechanism of [START_REF] Payet | Loop detection in term rewriting using the eliminating unfoldings[END_REF], but only after these two rules are generated. In order to avoid the generation of these useless rules, one can notice that l and r differ at the first argument of f: in l, the first argument is s(0) while in r it is x. We say that s(0), x is a disagreement pair of l and r. Hence, one can first concentrate on resolving this disagreement, unfolding this pair only, and then, once this is resolved, apply the same process to another disagreement pair.

Example 2 (Ex. 1 continued). There are two ways to resolve the disagreement pair s(0), x of l and r (i.e., make it disappear).

The first way consists in unifying s(0) and x, i.e., in computing R 1 θ where θ is the substitution {x/s(0)}, which gives V 0 = f(s(0), s(1), s(0)) → f(s(0), s(0), s(0)). The left-hand side of V 0 does not semi-unify with its right-hand side.

The other way is to unfold s(0) or x. We decide not to unfold variable subterms, hence we select s(0). As it occurs in the left-hand side of R 1 , we unfold it backwards. The only possibility is to use R 2 , which results in

V 1 = f(s(h), s(1), x) → f(x, x, x) .
Note that this approach only generates two rules (V 0 and V 1 ) at the first iteration of the unfolding operator. In comparison, the approach of [START_REF] Payet | Loop detection in term rewriting using the eliminating unfoldings[END_REF] produces 14 rules (before elimination), as all the subterms of R 1 are considered for unfolding.

Hence, the disagreement pair s(0), x has been replaced with the disagreement pair s(h),

x in V 1 . Unifying s(h) and x i.e., computing V 1 θ where θ is the substitution {x/s(h)}, we get V 1 = f(s(h), s(1), s(h)) → f(s(h), s(h), s(h)). So,
the disagreement s(0), x is solved: it has been replaced with s(h), s(h) . Now, 1, h is a disagreement pair in V 1 (here we mean the second occurrence of h in the right-hand side of V 1 ). Unfolding 1 backwards with R 3 , we get W = f(s(h), s(h), s(h)) → f(s(h), s(h), s(h)) and unfolding h forwards with R 3 , we get

W = f(s(h), s(1), s(h)) → f(s(h), s (1)
, s(h)). The semi-unification test succeeds on both rules: we get the looping terms f(s(h), s(h), s(h)) and f(s(h), s(1), s(h)) from W and W , respectively.

In the approach sketched in Ex. 2, the iterations of U R are not thoroughly computed because only some selected disagreement pairs are considered for unfolding, unlike in our previous approach [START_REF] Payet | Loop detection in term rewriting using the eliminating unfoldings[END_REF] which tries to unfold all the subterms in rules. Hence, now the unfoldings are guided by disagreement pairs. In this paper, we formally describe the intuitions presented above (Sect. [START_REF] Arts | Termination of term rewriting using dependency pairs[END_REF][START_REF] Baader | Term Rewriting and All That[END_REF][START_REF] Giesl | Analyzing program termination and complexity automatically with AProVE[END_REF]. We also report experiments on a large set of rewrite systems from the TPBD [START_REF]Termination Problems Data Base[END_REF] (Sect 6). The results we get in practice with the new approach are better than those obtained with the approach of [START_REF] Payet | Loop detection in term rewriting using the eliminating unfoldings[END_REF] and we do not need to perform several analyses in parallel, nor to unfold variable subterms, unlike [START_REF] Payet | Loop detection in term rewriting using the eliminating unfoldings[END_REF].

Preliminaries

If Y is an operator from a set E to itself, then for any e ∈ E we let

(Y ↑ 0)(e) = e and ∀n ∈ N : (Y ↑ n + 1)(e) = Y (Y ↑ n)(e) .
We refer to [START_REF] Baader | Term Rewriting and All That[END_REF] for the basics of rewriting. From now on, we fix a finite signature F together with an infinite countable set V of variables with F ∩V = ∅. Elements of F (symbols) are denoted by f, g, h, 0, 1, . . . and elements of V by x, y, z, . . . The set of terms over F ∪ V is denoted by T (F, V). For any t ∈ T (F, V), we let root(t) denote the root symbol of t:

root(t) = f if t = f(t 1 , . . . , t m ) and root(t) = ⊥ if t ∈ V,
where ⊥ is a new symbol not occurring in F and V. We let Var (t) denote the set of variables occurring in t and Pos(t) the set of positions of t. For any p ∈ Pos(t), we write t| p to denote the subterm of t at position p and t[p ← s] to denote the term obtained from t by replacing t| p with a term s. For any p, q ∈ Pos(t), we write p ≤ q iff p is a prefix of q and we write p < q iff p ≤ q and p = q. We also define the set of non-variable positions of t which either are a prefix of p or include p as a prefix:

NPos(t, p) = {q ∈ Pos(t) | q ≤ p ∨ p ≤ q, t| q ∈ V} .
A disagreement position of terms s and t is a position p ∈ Pos(s) ∩ Pos(t) such that root(s| p ) = root(t| p ) and, for every q < p, root(s| q ) = root(t| q ). The set of disagreement positions of s and t is denoted as DPos(s, t). A disagreement pair of s and t is an ordered pair s| p , t| p where p ∈ DPos(s, t).

Example 3. Let s = f(s(0), s(1), y), t = f(x, x, x), p 1 = 1, p 2 = 2 and p 3 = 3. Then, {p 1 , p 2 } ⊆ DPos(s, t) and s| p1 , t| p1 = s(0), x and s| p2 , t| p2 = s(1), x are disagreement pairs of s and t. However, p 3 ∈ DPos(s, t) because s| p3 , t| p3 = y, x and root(y) = root(x) = ⊥.

We write substitutions as sets of the form {x 1 /t 1 , . . . , x n /t n } denoting that for each 1 ≤ i ≤ n, variable x i is mapped to term t i (note that x i may occur in t i ). The empty substitution (identity) is denoted by id . The application of a substitution θ to a syntactic object o is denoted by oθ. We let mgu(s, t) denote the (up to variable renaming) most general unifier of terms s and t. We say that s semi-unifies with t when sθ 1 θ 2 = tθ 1 for some substitutions θ 1 and θ 2 .

A rewrite rule (or rule) over F ∪ V has the form l → r with l, r ∈ T (F, V), l ∈ V and Var (r) ⊆ Var (l). A term rewriting system (TRS) over F ∪ V is a finite set of rewrite rules over F ∪ V. Given a TRS R and some terms s and t, we write s → R t if there is a rewrite rule l → r in R, a substitution θ and p ∈ Pos(s) such that s| p = lθ and t = s[p ← rθ]. We let

+ → R (resp. * → R ) denote
the transitive (resp. reflexive and transitive) closure of → R . We say that a term t is non-terminating with respect to (w.r.t.) R when there exist infinitely many terms t 1 , t 2 , . . . The unfolding operators that we define in Sect. 3 of this paper use narrowing. We say that a term s narrows forwards (resp. backwards) to a term t w.r.t. a TRS R when there exists a non-variable position p of s and a rule l → r of R renamed with new variables not previously met such that t

such that t → R t 1 → R t 2 → R • • • . We say that
= s[p ← r]θ (resp. t = s[p ← l]θ) where θ = mgu(s| p , l) (resp. θ = mgu(s| p , r)).
We refer to [START_REF] Arts | Termination of term rewriting using dependency pairs[END_REF] for details on dependency pairs. The defined symbols of a TRS R over F ∪ V are D R = {root(l) | l → r ∈ R}. For every f ∈ F we let f # be a fresh tuple symbol with the same arity as f. The set of tuple symbols is denoted as F # . The notations and definitions above with terms over F ∪ V are naturally extended to terms over (F ∪F # )∪V. Elements of F ∪F # are denoted as f, g, . . . If t = f(t 1 , . . . , t m ) ∈ T (F, V), we let t # denote the term f # (t 1 , . . . , t m ), and we call t # an F # -term. An F # -rule is a rule whose left-hand and right-hand sides are F # -terms. The set of dependency pairs of R is

{l # → t # | l → r ∈ R, t is a subterm of r, root(t) ∈ D R } .
A sequence s 1 → t 1 , . . . , s n → t n of dependency pairs of R is an R-chain if there exists a substitution σ such that t i σ * → R s i+1 σ holds for every two consecutive pairs s i → t i and s i+1 → t i+1 in the sequence.

Theorem 1 ([3]

). R is non-terminating iff there exists an infinite R-chain.

The dependency graph of R is the graph whose nodes are the dependency pairs of R and there is an arc from

s → t to u → v iff s → t, u → v is an R-chain.
This graph is not computable in general since it is undecidable whether two dependency pairs of R form an R-chain. Hence, for automation, one constructs an estimated graph containing all the arcs of the real graph. This is done by computing connectable terms, which form a superset of those terms s, t where sσ * → R tσ holds for some substitution σ. The approximation uses the transformations cap and ren where, for any t ∈ T (F ∪ F # , V), cap(t) (resp. ren(t)) results from replacing all subterms of t with defined root symbol (resp. all variable occurrences in t) by different new variables not previously met. More formally:

cap(x) = x if x ∈ V cap(f (t 1 , . . . , t m )) = a new variable not previously met if f ∈ D R f (cap(t 1 ), . . . , cap(t m )) if f ∈ D R ren(x) = a new variable not previously met if x is an occurrence of a variable ren(f (t 1 , . . . , t m )) = f (ren(t 1 ), . . . , ren(t m )) A term s is connectable to a term t if ren(cap(s)) unifies with t. An F # -rule l → r is connectable to an F # -rule s → t if r is connectable to s.
The estimated dependency graph of R is denoted as DG(R). Its nodes are the dependency pairs of R and there is an arc from N to N iff N is connectable to N . We let SCC (R) denote the set of strongly connected components of DG(R) that contain at least one arc. Hence, a strongly connected component consisting of a unique node is in SCC (R) only if there is an arc from the node to itself.

Example 4. Let R be the TRS of Ex. 1. We have

SCC (R) = {C} where C consists of the node N = f # (s(0), s(1), x) → f # (x, x, x) and of the arc (N, N ). Example 5. Let R = {f(0) → f(1), f(2) → f(0), 1 → 0}. We have SCC (R ) = {C } where C consists of the nodes N 1 = f # (0) → f # (1) and N 2 = f # (2) → f # (0) and of the arcs {N 1 , N 2 } × {N 1 , N 2 } \ {(N 2 , N 2 )}.
The strongly connected component of DG(R ) which consists of the unique node f # (0) → 1 # does not belong to SCC (R ) because it has no arc.

Finite sequences are written as [e 1 , . . . , e n ]. We let :: denote the concatenation operator over finite sequences. A path in DG(R) is a finite sequence [N 1 , N 2 , . . . , N n ] of nodes where, for each 1 ≤ i < n, there is an arc from N i to N i+1 . When there is also an arc from N n to N 1 , the path is called a cycle. It is called a simple cycle if, moreover, there is no repetition of nodes (modulo variable renaming).

Guided unfoldings

In the sequel of this paper, we let R denote a TRS over F ∪ V.

While the method sketched in Ex. 2 can be applied directly to the TRS R under analysis, we use a refinement based on the estimated dependency graph of R. The cycles in DG(R) are over-approximations of the infinite R-chains i.e., any infinite R-chain corresponds to a cycle in the graph but some cycles in the graph may not correspond to any R-chain. Moreover, by Theorem 1, if we find an infinite R-chain then we have proved that R is non-terminating. Hence, we concentrate on the cycles in DG(R). We try to solve them, i.e., to find out if they correspond to any infinite R-chain. This is done by iteratively unfolding the F # -rules of the cycles. If the semi-unification test succeeds on one of the generated unfolded rules, then we have found a loop.

Definition 1 (Syntactic loop). A syntactic loop in R is a finite sequence [N 1 , . . . , N n ] of distinct (modulo variable renaming) F # -rules where, for each 1 ≤ i < n, N i is connectable to N i+1 and N n is connectable to N 1 . We identify syntactic loops consisting of the same (modulo variable renaming) elements, not necessarily in the same order.

Note that the simple cycles in DG(R) are syntactic loops. For any C ∈ SCC (R), we let s-cycles(C) denote the set of simple cycles in C. We also let

s-cycles(R) = ∪ C∈SCC (R) s-cycles(C)
be the set of simple cycles in R. The rules of any simple cycle in R are assumed to be pairwise variable disjoint.

Example 6 (Ex. 4 and 5 continued). We have

s-cycles(R) = {[N ]} and s-cycles(R ) = {[N 1 ], [N 1 , N 2 ]} with, in s-cycles(R ), [N 1 , N 2 ] = [N 2 , N 1 ].
The operators we use for unfolding an F # -rule R at a disagreement position p are defined as follows. They are guided by a given term u and they only work on the non-variable subterms of R. They unify a subterm of R with a subterm of u, see (1) in Def. 2-3. This corresponds to what we did in Ex. 2 for generating V 1 from V 1 , but in the definitions below we do not only consider p, we consider all its prefixes. The operators also unfold R using narrowing, see [START_REF]AProVE Web site[END_REF] in Def. 2-3: there, l → r R means that l → r is a new occurrence of a rule of R that contains new variables not previously met. This corresponds to what we did in Ex. 2 for generating V 1 from R 1 . In contrast to [START_REF] Alpuente | Safe folding/unfolding with conditional narrowing[END_REF], the positions that are greater than p are also considered in (2); for instance in Ex. 2, we unfolded the inner subterm 0 of the disagreement pair component s(0). Definition 2 (Forward guided unfoldings). Let l → r be an F # -rule, s be an F # -term and p ∈ DPos(r, s). The forward unfoldings of l → r at position p, guided by s and w.r.t. R are

F R (l → r, s, p) = U q ∈ NPos(r, p), q ≤ p θ = mgu(r| q , s| q ), U = (l → r)θ (1)
∪ U q ∈ NPos(r, p), l → r R θ = mgu(r| q , l ), U = (l → r[q ← r ])θ (2)
. Definition 3 (Backward guided unfoldings). Let s → t be an F # -rule, r be an F # -term and p ∈ DPos(r, s). The backward unfoldings of s → t at position p, guided by r and w.r.t. R are B R (s → t, r, p) = U q ∈ NPos(s, p), q ≤ p θ = mgu(r| q , s| q ), U = (s → t)θ

(1)

∪ U q ∈ NPos(s, p), l → r R θ = mgu(s| q , r ), U = (s[q ← l ] → t)θ (2)
.

Example 7 (Ex. 4 and 6 continued).

[N ] is a simple cycle in R with

N = f # (s(0), s(1), x) s → f # (x, x, x) t .
Let r = t. Then p = 1 ∈ DPos(r, s). Moreover, q = 1.1 ∈ NPos(s, p) because p ≤ q and s| q = 0 is not a variable. Let l → r = h → 0 ∈ R. We have id = mgu(s| q , r ). Hence, by [START_REF]AProVE Web site[END_REF] in Def. 3, we have [START_REF]AProVE Web site[END_REF] in Def. 3, we have

U 1 = f # (s(h), s(1), x) s1 → f # (x, x, x) t1 ∈ B R (N, r, p) . Let r 1 = t 1 . Then, p = 1 ∈ DPos(r 1 , s 1 ). Moreover, p ∈ NPos(s 1 , p) with s 1 | p = s(h), p ≤ p and r 1 | p = x. As {x/s(h)} = mgu(r 1 | p , s 1 | p ), by (1) in Def. 3 we have U 1 = f # (s(h), s(1), s(h)) s 1 → f # (s(h), s(h), s(h)) t 1 ∈ B R (U 1 , r 1 , p) . Let r 1 = t 1 . Then, p = 2.1 ∈ DPos(r 1 , s 1 ) with p ∈ NPos(s 1 , p ). Let l → r = h → 1 ∈ R. We have id = mgu(s 1 | p , r ). Hence, by
U 1 = f # (s(h), s(h), s(h)) → f # (s(h), s(h), s(h)) ∈ B R (U 1 , r 1 , p ) .
Our approach consists of iteratively unfolding syntactic loops using the following operator.

Definition 4 (Guided unfoldings). Let X be a set of syntactic loops of R. The guided unfoldings of X w.r.t. R are defined as

GU R (X) = L ::[U ] :: L L ::[l → r, s → t] :: L ∈ X, θ = mgu(r, s) U = (l → t)θ, L ::[U ] :: L is a syntactic loop (1) ∪    L ::[U, s → t] :: L L ::[l → r, s → t] :: L ∈ X p ∈ DPos(r, s), U ∈ F R (l → r, s, p) L ::[U, s → t] :: L is a syntactic loop    (2) ∪    L ::[l → r, U ] :: L L ::[l → r, s → t] :: L ∈ X p ∈ DPos(r, s), U ∈ B R (s → t, r, p) L ::[l → r, U ] :: L is a syntactic loop    (3) ∪    [U ] [l → r] ∈ X, p ∈ DPos(r, l) U ∈ F R (l → r, l, p) ∪ B R (l → r, r, p) [U ] is a syntactic loop    (4)
.

The general idea is to compress the syntactic loops into singletons by iterated applications of this operator. The semi-unification criterion can then be applied to these singletons, see Theorem 2 below. Compression takes place in case (1) of Def. 4: when the right-hand side of a rule unifies with the left-hand side of its successor, then both rules are merged. When merging two successive rules is not possible yet, the operators F R and B R are applied to try to transform the rules into mergeable ones, see cases ( 2) and (3). Once a syntactic loop has been compressed to a singleton, we keep on unfolding (case (4)) to try reaching a compressed form satisfying the semi-unification criterion. Note that after an unfolding step, we might get a sequence which is not a syntactic loop: the newly generated rule U might be identical to another rule in the sequence or it might not be connectable to its predecessor or successor. So, ( 1)-( 4) require that the generated sequence is a syntactic loop. The guided unfolding semantics is defined as follows, in the style of [START_REF] Alpuente | Safe folding/unfolding with conditional narrowing[END_REF][START_REF] Payet | Loop detection in term rewriting using the eliminating unfoldings[END_REF].

Definition 5 (Guided unfolding semantics). The guided unfolding semantics of R is the limit of the unfolding process described in Def. 4, starting from the simple cycles in R:

gunf (R) = ∪ n∈N gunf (R, n) where, for all n ∈ N, gunf (R, n) = (GU R ↑ n)(s-cycles(R)) .
This semantics is very similar to the overlap closure [START_REF] Guttag | On proving uniform termination and restricted termination of rewriting systems[END_REF] of R (denoted by OC(R)). A difference is that for computing gunf (R) one starts from dependency pairs of R (s-cycles(R)), whereas for computing OC(R) one starts directly from the rules of R. In case (1) of Def. 4, we merge two unfolded rules. Similarly, for computing OC(R) one overlaps closures with closures. However, in cases ( 2)-( 4) the operators F R and B R narrow an unfolded rule with a rule of R, not with another unfolded rule, unlike in the computation of OC(R).

(R) = {[N 1 , N 2 ]}. As id = mgu(g # (1), g # (1)) and (f # (0) → f # (0))id = f # (0) → f # (0), by (1) in Def. 4 we have [f # (0) → f # (0)] ∈ gunf (R, 1). Proposition 1. For any n ∈ N and [s # → t # ] ∈ gunf (R, n) there exists some context C such that s + → R C[t].
Proof. For some context C, we have s → C[t] ∈ unf (R) where unf (R) is the unfolding semantics defined in [START_REF] Payet | Loop detection in term rewriting using the eliminating unfoldings[END_REF]. So, by Prop. 3.12 of [START_REF] Payet | Loop detection in term rewriting using the eliminating unfoldings[END_REF], s

+ → R C[t].

Inferring terms that loop

As in [START_REF] Payet | Loop detection in term rewriting using the eliminating unfoldings[END_REF], we use semi-unification [START_REF] Lankford | A finite termination criterion[END_REF] for detecting loops. Semi-unification encompasses both matching and unification, and a polynomial-time algorithm for it can be found in [START_REF] Kapur | Semi-unification[END_REF].

Theorem 2. For any n ∈ N, if there exist [s # → t # ] ∈ gunf (R, n) and some substitutions θ 1 and θ 2 such that sθ 1 θ 2 = tθ 1 , then the term sθ 1 loops w.r.t. R.

Proof. By Prop. 1, s

+ → R C[t] for some context C. Since → R is stable, we have sθ 1 + → R C[t]θ 1 i.e., sθ 1 + → R Cθ 1 [tθ 1 ] i.e., sθ 1 + → R Cθ 1 [sθ 1 θ 2 ] .
Hence, sθ 1 loops w.r.t. R.

Example 10 (Ex. 8 continued). We have

[f # (s(h), s(h), s(h)) → f # (s(h), s(h), s(h)) U 1 ] ∈ gunf (R, 3) with f(s(h), s(h), s(h))θ 1 θ 2 = f(s(h), s(h), s(h))θ 1 for θ 1 = θ 2 = id . Consequently, f(s(h), s(h), s(h))θ 1 = f(s(h), s(h), s(h)) loops w.r.t. R.
Example 11 (Ex. 9 continued).

[f # (0) → f # (0)] ∈ gunf (R, 1) with f(0)θ 1 θ 2 = f(0)θ 1 for θ 1 = θ 2 = id . Hence, f(0)θ 1 = f(0) loops w.r.t. R.
The substitutions θ 1 and θ 2 that we use in the next example are more sophisticated than in Ex. 10 and Ex. 11.

Example 12. Let R = {f(g(x, 0), y) → f(g(0, x), h(y))}. Then, SCC (R) = {C} where C consists of the node N = f # (g(x, 0), y) → f # (g(0, x), h(y)) and of the arc (N, N ). Moreover, s-cycles(R) = {[N ]} hence [N ] ∈ gunf (R, 0). Therefore, as f(g(x, 0), y)θ 1 θ 2 = f(g(0,
x), h(y))θ 1 for θ 1 = {x/0} and θ 2 = {y/h(y)}, by Theorem 2 we have that f(g(x, 0), y)θ 1 = f(g(0, 0), y) loops w.r.t. R.

We do not have an example where semi-unification is necessary for detecting a loop. In every example that we have considered, matching or unification were enough. However, semi-unification sometimes allows us to detect loops earlier in the unfolding process than with matching and unification. This is important in practice, because the number of unfolded rules can grow rapidly from iteration to iteration.

Example 13 (Ex. 12 continued). Semi-unification allows us to detect a loop at iteration 0 of GU R . But a loop can also be detected at iteration 1 using matching. Indeed, we have

N = f # (g(x, 0), y) l → f # (g(0, x), h(y)) r with p = 1.1 ∈ DPos(r, l). Hence, U = f # (g(0, 0), y) s # → f # (g(0, 0), h(y)) t # ∈ F R (l → r, l, p) .
So, by (4) in Def. 4, we have [U ] ∈ gunf (R, 1). Notice that sθ = t for θ = {y/h(y)}, so s matches t. Moreover, by Theorem 2, s = f(g(0, 0), y) loops w.r.t. R (take θ 1 = id and θ 2 = θ).

5 Further comparisons with the approach of [START_REF] Payet | Loop detection in term rewriting using the eliminating unfoldings[END_REF] The approach that we have presented in [START_REF] Payet | Loop detection in term rewriting using the eliminating unfoldings[END_REF] relies on an unfolding operator U R (where R is the TRS under analysis) which is also based on forward and backward narrowing (as F R and B R herein). But, unlike the technique that we have presented above, it directly unfolds the rules (not the dependency pairs) of R and it does not compute any SCC. Moreover, it consists of a thorough computation of the iterations of U R followed by a mechanism for eliminating rules that cannot be further unfolded to a rule l → r where l semi-unifies with r. Such rules are said to be root-useless. The set of root-useless rules is an overapproximation of the set of useless rules (rules that cannot contribute to detecting a loop), hence the elimination technique of [START_REF] Payet | Loop detection in term rewriting using the eliminating unfoldings[END_REF] may remove some rules which are actually useful for detecting a loop. Our non-termination analyser which is based on [START_REF] Payet | Loop detection in term rewriting using the eliminating unfoldings[END_REF] uses a time limit. It stops whenever it has detected a loop within the limit (then it answers NO, standing for No, this TRS does not terminate as in the Termination Competition [START_REF]The Annual International Termination[END_REF]) or when the limit has been reached (then it answers TIME OUT) or when no more unfolded rule could be generated at some point within the limit ((U R ↑ n)(R) = ∅ for some n). In the last situation, either the TRS under analysis is not looping (it is terminating or non-looping non-terminating) or it is looping but a loop for it cannot be captured by the approach (for instance, the elimination mechanism has removed all the useful rules). In such a situation, our analyser answers DON'T KNOW.

Example 14. Consider the terminating TRS R = {0 → 1}. As the left-hand (resp. right-hand) side of the rule of R cannot be narrowed backwards (resp. forwards) with R then we have

(U R ↑ 1)(R) = ∅.
In contrast, the approach that we have presented in Sect. 3-4 above avoids the generation of some rules by only unfolding disagreement pairs. Currently, in terms of loop detection power, we do not have any theoretical comparison between this new technique and that of [START_REF] Payet | Loop detection in term rewriting using the eliminating unfoldings[END_REF]. Our new non-termination analyser also uses a time limit and answers NO, TIME OUT or DON'T KNOW when no more unfolded rules are generated at some point (gunf (R, n) = ∅ for some n, as in Ex. 14). Moreover, it allows the user to fix a selection strategy of disagreement pairs: in Def. 4, the conditions p ∈ DPos(r, s) (cases (2)-( 3)) and p ∈ DPos(r, l) (case (4)) are replaced with p ∈ select R (l → r, s → t) and p ∈ select R (l → r, l → r) respectively, where select R can be one of the following functions.

Selection of all the pairs: select all R (l → r, s → t) = DPos(r, s).

Leftmost selection: if DPos(r, s) = ∅ then select lm R (l → r, s → t) = ∅, oth- erwise select lm R (l → r, s → t) = {p}
where p is the leftmost disagreement position of r and s. Leftmost selection with non-empty unfoldings:

select lmne R (l → r, s → t) = {p}
where p is the leftmost disagreement position of r and s such that

F R (l → r, s, p) ∪ B R (s → t, r, p) = ∅ .
If such a position p does not exist then select lmne R (l → r, s → t) = ∅.

Example 15. Let R = {f(s(0), s(1), z) → f(x, y, z)} and l = f # (s(0), s(1), z) and r = f # (x, y, z). Then, we have select all R (l → r, l → r) = DPos(r, l) = {1, 2}. Moreover, 1 is the leftmost disagreement position of r and l because r| 1 = x occurs to the left of r| 2 = y in r and l| 1 = s(0) occurs to the left of l| 2 = s(1) in l. Therefore, we have select lm R (l → r, l → r) = {1}.

Example 16. Let R = {f(x, x) → f(g(x), h(x)), h(x) → g(x)}. Then, SCC (R) = {C} where C consists of the node N = l → r = f # (x, x) → f # (g(x), h(x)) and of the arc (N, N ). Then, DPos(r, l) = {1, 2} and select lm R (N, N ) = {1}. As F R (N, l, 1) ∪ B R (N, r, 1) = ∅ and F R (N, l, 2) ∪ B R (N, r, 2) = ∅ (for instance, f # (x, x) → f # (g(x), g(x)) ∈ F R (N, l, 2) is obtained from narrowing r| 2 = h(x) forwards with h(x) → g(x)), then select lmne R (N, N ) = {2}.
As the approach of [START_REF] Payet | Loop detection in term rewriting using the eliminating unfoldings[END_REF], and depending on the strategy used for selecting disagreement pairs, our new technique is not complete in the sense that it may miss some loop witnesses.

Example 17 (Ex. 16 continued). We have gunf (R, 0) = s-cycles(R) = {[N ]}. As l does not semi-unify with r, no loop is detected from gunf (R, 0), so we go on and compute gunf (R, 1). Only case (4) of Def. 4 is applicable to [N ]. First, suppose that select R = select lm R . Then, select R (N, N ) = {1} and, as F R (N, l, 1) ∪ B R (N, r, 1) = ∅, case (4) does not produce any rule. Consequently, we have gunf (R, 1) = ∅, hence no loop is detected for R. Now, suppose that select R = select lmne R . Then, select R (N, N ) = {2}. Narrowing r| 2 = h(x) forwards with h(x) → g(x), we get the rule N = f # (x, x) → f # (g(x), g(x)) which is an element of F R (N, l, 2). Hence, [N ] ∈ gunf (R, 1). As in N we have that f(x, x) semi-unifies with f(g(x), g(x)) (take θ 1 = id and θ 2 = {x/g(x)}), then f(x, x) loops w.r.t. R. This loop is also detected by the approach of [START_REF] Payet | Loop detection in term rewriting using the eliminating unfoldings[END_REF].

Experiments

We have implemented the technique of this paper in our analyser NTI1 (Non-Termination Inference). For our experiments, we have extracted from the directory TRS_Standard of the TPBD [START_REF]Termination Problems Data Base[END_REF] all the valid rewrite systems2 that were either proved looping or unproved3 during the Termination Competition 2017 (TC'17) [START_REF]The Annual International Termination[END_REF]. Otherwise stated, we removed from TRS_Standard all the nonvalid TRSs and all the TRSs that were proved terminating or non-looping nonterminating by a tool participating in the competition. We ended up with a set S of 333 rewrite systems. We let L (resp. U) be the subset of S consisting of all the systems that were proved looping (resp. that were unproved) during TC'17. Some characteristics of L and U are reported in Table 1. Note that the complete set of simple cycles of a TRS may be really huge, hence NTI only computes a subset of it. The simple cycle characteristics given in Table 1

2.27

Table 1. Some characteristics of the analysed TRSs. Sizes are in number of rules. In square brackets, we report the number of TRSs with the corresponding min or max.

We have run our new approach (NTI '18) and that of [START_REF] Payet | Loop detection in term rewriting using the eliminating unfoldings[END_REF] (NTI'08) on the TRSs of S. The results are reported in Table 2 and Table 3. We used an Intel 2-core i5 at 2 GHz with 8 GB of RAM and the time limit fixed for a proof was 120s. For every selection strategy, NTI'18 issues more successful proofs (NO) and generates less unfolded rules than NTI'08. Moreover, as it avoids the generation of some rules instead of computing all the unfolding and then eliminating some rules (as NTI'08 does), its times are better. At the bottom of the tables, we give the numbers of TRSs proved looping by both approaches and by one approach only. NTI'18 succeeds on all the TRSs of L on which NTI'08 succeeds, but it fails on one TRS of U on which NTI'08 succeeds. This is due to our simplified computation of the set of simple cycles: our algorithm does not generate the cycle that would allow NTI'18 to succeed and NTI'18 times out, trying to unfold syntactic loops from which it cannot detect anything. Another point to note is that the implementation of the new approach does not need to run several analyses in parallel to achieve the results presented in Table 2 andTable 3. One single thread of computation is enough. On the contrary, for the approach of [START_REF] Payet | Loop detection in term rewriting using the eliminating unfoldings[END_REF], 3 parallel threads are necessary: one with forward unfoldings only, one with backward unfoldings only and one with forward and backward unfoldings together. The results get worse if NTI'08 only runs one thread performing forward and backward unfoldings together. In Table 2 Four tools participated in the category TRS Standard of TC'17: AProVE [2, 5], MU-TERM [START_REF]MU-TERM Web site[END_REF], NaTT [START_REF]NaTT -The Nagoya Termination Tool[END_REF] and WANDA [START_REF] Kop | WANDA -A higher-order termination tool[END_REF]. The numbers of TRSs proved looping by each of them during the competition is reported in Table 4. An important point to note here is that the time limit fixed in TC'17 was 300s, whereas in our experiments with NTI'18 and NTI'08 it was 120s. Moreover, the machine we used (an Intel 2-core i5 at 2 GHz with 8 GB of RAM) is much less powerful than the machine used during TC'17 (the StarExec platform [START_REF]StarExec -A cross-community solver execution and benchmark library service[END_REF] running on an Intel Xeon E5-2609 at 2.4 GHz with 129 GB of RAM). All the tools of TC'17 failed on all the rewrite systems of U. In contrast, NTI'18 (resp. NTI'08) finds a loop for 6 (resp. 4) of them. Regarding L, AProVE was able to prove loopingness of 172 out of 173 TRSs. The only TRS of L on which AProVE failed 4 was proved looping by NaTT. In comparison, our approach succeeds on 158 systems of L, less than AProVE but more than the other tools of TC'17. Similarly to our approach, AProVE handles the SCCs of the estimated dependency graph independently, but it first performs a termination analysis. The non-termination analysis is then only applied to those SCCs that could not be proved terminating. On the contrary, NTI only performs non-termination proofs. If an SCC is terminating, it cannot prove it and keeps on trying a non-termination proof, unnecessarily generating unfolded rules at the expense of the analysis of the other SCCs. The loop detection techniques implemented in AProVE and NTI'18 are based on the idea of searching for loops by forward and backward narrowing of dependency pairs and by using semi-unification to detect potential loops. This idea has been presented in [START_REF] Giesl | Proving and disproving termination of higher-order functions[END_REF] where heuristics are used to select forward or backward narrowing. Note that in constrast, the technique that we present herein does not use any heuristics and proceeds both forwards and backwards.

Conclusion

We have reconsidered and modified the unfolding-based technique of [START_REF] Payet | Loop detection in term rewriting using the eliminating unfoldings[END_REF] for detecting loops in standard term rewriting. The new approach uses disagreement pairs for guiding the unfoldings, which now are only partially computed, whereas the technique of [START_REF] Payet | Loop detection in term rewriting using the eliminating unfoldings[END_REF] consists of a thorough computation followed by a mechanism for eliminating some rules. Two theoretical questions remain open: in terms of loop detection, is an approach more powerful than the other and does semiunification subsume matching and unification?

We have implemented the new approach in our tool NTI and compared it to [START_REF] Payet | Loop detection in term rewriting using the eliminating unfoldings[END_REF] on a set of 333 rewrite systems. The new results are better (better times, more successful proofs, less unfolded rules). Moreover, the approach compares well to the tools that participated in TC'17. However, the number of generated rules is still important. In an attempt to reduce it, during our experiments we added the elimination mechanism of [START_REF] Payet | Loop detection in term rewriting using the eliminating unfoldings[END_REF] to the new approach, but the results we recorded were not satisfactory (an equivalent, slightly smaller, number of generated rules but, due to the computational overhead, bigger times and less successes); hence, we removed it. Termination analysis may help to reduce the number of unfolded rules by detecting terminating SCCs in the estimated dependency graph i.e., SCCs on which it is useless to try a non-termination proof. In other words, we could use termination analysis as an elimination mechanism. Several efficient and powerful termination analysers have been implemented so far [START_REF]Termination Portal -An (incomplete) overview of existing tools for termination analysis[END_REF] and one of them could be called by NTI. A final idea to improve our approach would be to consider more sophisticated strategies for selecting disagreement pairs.

Example 8 .Example 9 .

 89 By Ex. 7 and (4) in Def. 4, we have [U 1 ] ∈ gunf (R, 3). Let R = {f(0) → g(1), g(1) → f(0)}. Then, SCC (R) = {C} where C consists of the nodes N 1 = f # (0) → g # (1) and N 2 = g # (1) → f # (0) and of the arcs (N 1 , N 2 ) and (N 2 , N 1 ). Moreover, s-cycles

  R is non-terminating if there exists a non-terminating term w.r.t. it. A term t loops w.r.t. R when t We say that R is looping when it admits a loop. If a term loops w.r.t. R then it is non-terminating w.r.t. R.

	+ → R	C[tθ] for some context C and substitution θ. Then t	+ → R	C[tθ] is called a loop
	for R.

  relate to the subsets computed by NTI.

	S = L U (333 TRSs)	L (173 TRSs) Min Max Average Min Max Average U (160 TRSs)
	TRS size	1 [17] 104 [1]	11.08 1 [9] 837 [1]	64.78
	Number of SCCs	1 [101] 12 [1]	1.95 1 [70] 130 [1]	6.14
	SCC size	1 [96] 192 [1]	4.44 1 [54] 473 [1]	10.79
	Number of simple cycles 1 [47] 185 [1]	8.55 2 [15] 1,176 [1]	69.02
	Simple cycle size	1 [157] 9 [2]	2.23 1 [157]	9 [4]	2.21
	Number of symbols	1 [4] 66 [1]	9.09 2 [7] 259 [1]	24.14
	Symbol arity	0 [153] 5 [2]	1.07 0 [150]	12 [2]	1.94
	Number of defined symbols 1 [28] 58 [1]	5.21 1 [15] 132 [2]	17.19
	Defined symbol arity	0 [74] 5 [2]	1.38 0 [28]	12 [2]

Table 2 .

 2 and Table3, we report in square brackets the number of successes of NTI'08 when it only runs one thread performing both forward and backward unfoldings. Analysis results on the TRSs of L.

	L (173 TRSs)	NTI'08	NTI'18 select all select lm select lmne
	NO	152 [149]	157	157	158
	DON'T KNOW	0	0	1	0
	TIME OUT	21	16	15	15
	Time	2,966s	2,194s	1,890s	1,889s
	Generated rules 11,167,976 9,030,962 8,857,421 8,860,560
	NO(NTI'08) ∩ NO(NTI'18)	152	151	152
	NO(NTI'08) \ NO(NTI'18)	0	1	0
	NO(NTI'18) \ NO(NTI'08)	5	6	6
	U (160 TRSs)	NTI'08	NTI'18 select all select lm select lmne
	NO	4 [3]	6	6	6
	DON'T KNOW	0	0	1	0
	TIME OUT	156	154	153	154
	Time	18,742s	18,563s	18,414s	18,534s
	Generated rules 64,011,002 53,134,334 61,245,705 63,300,604
	NO(NTI'08) ∩ NO(NTI'18)	3	3	3
	NO(NTI'08) \ NO(NTI'18)	1	1	1
	NO(NTI'18) \ NO(NTI'08)	3	3	3

Table 3 .

 3 Analysis results on the TRSs of U.

Table 4 .

 4 Number of successes (NO) on L and U obtained during TC'17 and those obtained by NTI during our experiments.

	S = L U (333 TRSs)	TC'17 (time limit = 300s) AProVE MU-TERM NaTT WANDA NTI'08 NTI'18 (select lmne) (time limit = 120s)
	L (173 TRSs)	172	81 109	0	152	158
	U (160 TRSs)	0	0	0	0	4	6

http://lim.univ-reunion.fr/staff/epayet/Research/NTI/NTI.html

Surprisingly, the subdirectory Transformed CSR 04 contains 60 files where a pair l → r with Var (r) ⊆ Var (l) occurs. These pairs are not valid rewrite rules.

By unproved we mean that no tool succeeded in proving that these TRSs were terminating or non-terminating (all the tools failed on these TRSs).

Ex6 15 AEL02 FR.xml in the directory TRS Standard/Transformed CSR 04

Acknowledgements

The author thanks the anonymous reviewers for their many helpful comments and constructive criticisms. He also thanks Fred Mesnard for presenting the paper at the symposium.