{'fraction_non_alphanumeric': 0.05800707593017379, 'fraction_numerical': 0.010924925158430854, 'mean_word_length': 3.8468061051441493, 'pattern_counts': {'":': 0, '<': 0, '<?xml version=': 0, '>': 2, 'https://': 0, 'lorem ipsum': 0, 'www.': 0, 'xml': 0}, 'pii_count': 0, 'substrings_counts': 0, 'word_list_counts': {'cursed_substrings.json': 30, 'profanity_word_list.json': 0, 'sexual_word_list.json': 0, 'zh_pornsignals.json': 0}}
A Semantic Approach to the Analysis of Rewriting-Based Systems

Properties expressed as the provability of a first-order sentence can be disproved by just finding a model of the negation of the sentence. This fact, however, is meaningful in restricted cases only, depending on the shape of the sentence and the class of systems at stake. In this paper we show that a number of interesting properties of rewriting-based systems can be investigated in this way, including infeasibility and non-joinability of critical pairs in (conditional) rewriting, non-loopingness of conditional rewrite systems, or the secure access to protected pages of a web site modeled as an order-sorted rewrite theory. Interestingly, this uniform, semantic approach succeeds when specific techniques developed to deal with the aforementioned problems fail.


Introduction
First-Order Logic is an appropriate language to express the semantics of computational systems and also the (claimed) properties of such computational systems [5]. In this paper we explore the use of first-order logic in the analysis of rewriting-based systems, including Term Rewriting Systems (TRSs, [2]), Conditional TRSs (CTRSs, [3,11,30]), Membership Equational Programs [12,28], and more general rewriting-based formalisms [4,16,29]. The insertion of a 'rewritingbased system' R into First-Order Logic is made as (the specification of) a Horn theory, i.e., a set of sentences R which are universally quantified implications A 1 ∧ · · · ∧ A n ⇒ B for some n ≥ 0 where A i , 1 ≤ i ≤ n and B are atoms corresponding to predicate symbols →, → * , etc. Such a Horn theory is usually obtained from the operational semantics of the system usually given by means of some inference rules. Example 1. Consider the following CTRS R: Its associated Horn theory R (using predicate symbols → and → * ) is: Sentence (3) corresponds to reflexivity of the many-step rewrite relation → * and (4) is usually called transitivity, although it actually says how the one-step rewrite relation → and the many-step relation are related. Finally, (5) and (6) describe the CTRS at stake.
In this setting, our approach goes back to Floyd, Hoare, and Manna's early work on proving program properties using first-order logic: we can use logical formulas to describe the execution of a program and then other formulas describe the property of interest [5,Chapter 10]. However, the natural idea of using the notion of logical consequence R |= ϕ (i.e., that ϕ is satisfied in every model of R) as a formal definition of "system R has property ϕ" may fail to work.
Example 2. (Continuing Example 1) Note that a does not rewrite into b because the conditional part of rule (2) cannot be satisfied: c cannot be rewritten into b.
Following the aforementioned 'natural approach', we are tempted to formalize this as follows: R |= ¬(a → b) holds, i.e., every model of R satisfies ¬(a → b).
However, an interpretation of the constant symbols a and b as 0, with → and → * interpreted as the equality satisfies (3) − (6) (i.e., it is a model of R), but ¬(a → b) does not hold. Thus, R |= ¬(a → b) does not hold! This 'mismatch' between the expressivity of pure first-order logic and the intended meaning of logic sentences referred to the computational logic describing a given computational system is usually avoided by the assumption that sentences expressing program properties should be checked with respect to a given canonical model only [6,Chapter 4]. For instance, the problem in Example 2 disappears if we assume that ¬(a → b) must hold in the least Herbrand model H R of R only. In H R , → and → * are interpreted precisely as the sets (→) HR and (→ * ) HR of pairs (s, t) of ground terms s and t such that s → R t and s → * R t, respectively. Then, we indeed have H R |= ¬(a → b), which is agreed to be the intended meaning of the logic expression ¬(a → b).
In general, the (standard) least Herbrand model H of a Horn theory is not computable 1 . Thus, the practical verification of properties ϕ as satisfiability in H, i.e., H |= ϕ, is not possible, in general. In this paper we show that the class of properties ϕ which can be written as the existential closure of a positive boolean combination of atoms can be disproved (with regard to the least Herbrand model of a Horn theory S) by showing the satisfiability of ¬ϕ in an arbitrary model A of S, i.e., by proving A |= ¬ϕ. When this approach is applied to rewritingbased systems R and the associated Horn theory R, a number of interesting properties (some of them already considered in the literature) can be expressed and disproved in this way. Some examples are given in Figure 1, where s and t denote ground terms, s 1 , . . . , s n , t 1 , . . . , t n denote arbitrary terms with variables in x (in the feasibility property, see [20]) and ☎ is the subterm relation.
After some preliminaries, Section 3 presents the main result of the paper which is formulated in a standard first-order logic framework [27]. Section 5 explains its use in a rewriting setting. By lack of space we mainly focus on CTRSs but other computational systems could be treated in this way. Section 6 discusses some related work. Section 7 concludes.

Preliminaries
A signature with predicates 2 Ω is a pair Ω = (F , Π), where F is a set of function symbols F = {f, g, . . .} and Π is a set of predicate symbols Π = {P, Q, . . .} with F ∩ Π = ∅. An arity mapping ar : F ∪ Π → N fixes the number of arguments for each symbol. First-order terms t and formulas ϕ are built from these symbols (and an infinite set X of variable symbols X = {x, y, z, . . .}, which is disjoint from F ∪ Π) in the usual way. Equations s = t for terms s and t can also be used as atoms if necessary, even without any equality symbol in Π. The set of terms is denoted as T (F , X ) (the set of ground terms, i.e., terms without variables, is denoted as T (F ). The set of (first-order) formulas is denoted as Form F ,Π .
An Ω-structure A for a signature with predicates Ω is an interpretation of the function and predicate symbols in Ω as mappings f A , g A , . . . and relations P A , Q A , . . . on a given set (carrier) dom(A), often denoted A as well. The equality symbol has a fixed interpretation as the identity relation {(a, a) | a ∈ A} on A. An Ω-homomorphism between Ω-structures A and A ′ is a mapping h : dom(A) → dom(A ′ ) such that (i) for each k-ary symbols f ∈ F , and a 1 , . . . , a k ∈ dom(A), h(f A (a 1 , . . . , a k )) = f A ′ (h(a 1 ), . . . , h(a k )) and (ii) for each n-ary predicate symbols P ∈ Π and a 1 , . . . , a n ∈ dom(A), if (a 1 , . . . , a n ) ∈ P A , then (h(a 1 ), . . . , h(a n )) ∈ P A ′ [18, Section 1.2]. Given a valuation mapping α : A model for a theory S, i.e., a set of sentences (which are formulas whose variables are all quantified ), is just a structure that makes them all true, written A |= S, see [18]. Let Mod (S) be the class of structures A which are models of S. A sentence ϕ is a logical consequence of a theory S (written S |= ϕ) if for all A ∈ Mod (S), A |= ϕ. If ϕ can be proved from S by using an appropriate calculus (e.g., the axiomatic calculus by Hilbert [27, Section 2.3], or Gentzen's natural deduction, see [31]), we write S ⊢ ϕ.

Existentially Closed Boolean Combinations of Atoms
Every set S of ground atoms has an initial model. Let Ω be a first-order signature and S be a set of ground atoms. Then, there is a structure I S such that 1. I S |= S, 2. every element of dom(I S ) is of the form t IS for some ground term t, 3. if A is an Ω-structure and A |= S, then there is a unique homomorphism h : Actually, the initial structure I S (or just I, if S is understood from the context) which is mentioned in Theorem 1, and also in some of the results below, consists of the usual Herbrand Domain of ground terms modulo the equivalence ∼ generated by the equations in S [18, Lemma 1.5.1]: For each ground term t ∈ T (F ), let t ∼ be the equivalence class of t under ∼. Then, 3. For each predicate symbol P ∈ Ω of arity n, define P I as the set If S contains no equation, then I is the Least Herbrand Model of S [18]. A positive boolean combination of atoms is a formula where m ≥ 0, n i ≥ 0 for all 1 ≤ i ≤ m, and A ij are atoms for all 1 ≤ i ≤ m and 1 ≤ j ≤ n i (cf. [18,Section 2.4]). Satisfiability of the existential closure of formulas (7), i.e., formulas of the form for some atoms A ij with variables in x 1 , . . . , x k for some k ≥ 0, is preserved under homomorphism, i.e., the following holds: Let Ω be a signature with predicates and A ij be atoms for all 1 ≤ i ≤ m and 1 ≤ j ≤ n i with variables x 1 , . . . , x k . Let A and A ′ be Ω-structures such that there is an Ω-homomorphism from A to A ′ . Then, Our main result is just a combination of the two previous results. If S is (logically equivalent to) a set of ground atoms, then it is satisfiable in the initial model I S of S (i.e., I S |= S holds) and for all models A of S there is a homomorphism h : I S → A (Theorem 1). By Theorem 2, if I S satisfies a formula ϕ of the form (8), then for all such models A of S (for which we have a homomorphism h : Thus, ϕ is a logical consequence of S: S |= ϕ.

Corollary 1.
Let Ω be a first-order signature, S be a set of ground atoms, and A ij be atoms for all 1 ≤ i ≤ m and 1 ≤ j ≤ n i with variables x 1 , . . . , x k . Then,  Remark 1 (Application to Horn theories). If the (possibly infinite) set of atoms S is viewed as generated by a finite subset S 0 of (non-necessarily atomic) Horn sentences, then the interpretation of each predicate symbol P by I consists of the set of atomic consequences of the form P (t 1 , . . . , t n ) of S for ground terms t 1 , . . . , t n , i.e., the set of ground atoms P (t 1 , . . . , t n ) such that S 0 ⊢ P (t 1 , . . . , t n ) [13]. In order to obtain a non-empty set of ground atoms associated to a Horn theory S 0 , the set of ground terms cannot be empty, i.e., the signature must contain at least a constant symbol.
The following consequence of Corollary 1 is the basis of the practical applications discussed in the following sections.
Corollary 2 (Semantic criterion). Let S be a Horn theory with a non-empty set of ground atomic consequences, ϕ be the existential closure of a positive boolean combination of atoms, and A be a model of S, i.e., A |= S. If A |= ¬ϕ, then I S |= ¬ϕ.
Models A to be used in Corollary 2 can be automatically generated from the Horn theory S and sentence ϕ at stake by using a tool like AGES [17]. Actually, we generate a model A of S ∪{¬ϕ} as described in [21]. Corollaries 1 and 2 easily generalize to many-sorted signatures: as usual (see [38]), we just need to treat sorted variables x i : s i using atoms S i (x i ) which are added as a new conjunction k i=1 S i (x i ) to the matrix formula (7). In Section 5.6 we use this without further formalization (but see [16]).

Conditional Rewrite Systems as Horn Theories
A CTRS is a pair R = (F , R) where F is a signature of function symbols and R is a set of conditional rules ℓ → r ⇐ c where ℓ and r are terms and c is the conditional part of the rule consisting of sequences s 1 ≈ t 1 , . . . , s n ≈ t n of expressions s i ≈ t i , usually interpreted as reachability or joinability problems after an appropriate instantiation with a substitution σ, i.e., for all i, for the joinability semantics) [3,11,30]. In the following we focus on the reachability semantics for CTRSs 3 . We write s → * R t for terms s and t iff there is a proof tree for s → * t using R in the inference system of Figure 2 where each rewriting s1 → * t1 · · · sn → * tn ℓ → r for ℓ → r ⇐ s1 → t1, . . . , sn → tn ∈ R Fig. 2. Inference rules for conditional rewriting with a CTRS R with signature F step s → R t also requires a proof of the goal s → t before it can be considered part of the one-step rewriting relation associated to R (see Figure 2) [22].

Remark 2.
All rules in the inference system in Figure 2 are schematic in the sense that each inference rule B1 ··· Bn A can be used for any instance σ(B1) ··· σ(Bn) σ(A) of the rule by a substitution σ [33]. For instance, (Rp) actually establishes that, for every rule ℓ → r ⇐ s 1 → t 1 , . . . , s n → t n in the CTRS R, every instance σ(ℓ) by a substitution σ rewrites into σ(r) provided that, for each s i → t i , with 1 ≤ i ≤ n, the reachability condition σ(s i ) → * σ(t i ) can be proved.
In the logic of CTRSs, with binary predicates → and → * , the Horn theory R for a CTRS R is obtained from the inference rules in Figure 2 (for the reachability semantics of conditions) by specializing (C ) f,i for each f ∈ F and i, 1 ≤ i ≤ ar(f ) and (Rp) ρ for all ρ : ℓ → r ⇐ c ∈ R. Inference rules B1 ··· Bn A become universally quantified implications B 1 ∧ · · · ∧ B n ⇒ A [23, Section 2].  Figure 3 shows its Horn theory R.

Application to (Conditional) Term Tewriting
Note that all sentences in Figure 1 are particular cases of (8) when the language of the logic of CTRSs is used. Some of the problems represented by these formulas have been investigated in the literature. In the following, we consider them and show that our results are useful to improve or complement the already developed proof methods for these analysis problems.

Infeasible Conditional Critical Pairs (ϕ Feas )
In the literature about confluence of conditional rewriting, the so-called infeasible Conditional Critical Pairs (CCPs) for a CTRS R are those critical pairs s ↓ t ⇐ c whose conditional parts c are infeasible, i.e., there is no substitution σ such that for all i, 1 ≤ i ≤ n, we have σ(s i ) → * R σ(t i ) (for the rewriting semantics; or σ(s i ) ↓ R σ(t i ) for the joinability semantics) [30, Definition 7.1.8]. Detecting infeasible CCPs is important in proofs of confluence of CTRSs [3,30,35,36].
has the following conditional critical pair: The domain of A is the set of natural numbers N. Function symbols are interpreted as follows: Predicate symbols → and → * are interpreted as follows: has a conditional critical pair f(x, f(a, b). The following structure A over the finite domain {0, 1}: (a, b). Thus, the critical pair is infeasible. In [36,Example 23] this is proved by using unification tests together with a transformation. It is discussed that the the alternative tree automata techniques investigated in the paper do not work for this example.

Infeasible Rules (ϕ Feas )
The infeasibility of the conditional part of a conditional rule with respect to a given CTRS is also important to prove other computational properties of such systems. In particular, proving the infeasibility of the conditional dependency pairs which are used to characterize termination properties of CTRSs [24] is useful in (automated) proofs of such termination properties [26].

Example 8.
A CTRS R is operationally terminating iff no term t has an infinite proof tree using the inference system in Figure 2 [22]. According to [24,26], a formal proof of operational termination of R in Example 5 is easily obtained if the following conditional dependency pair (which is just a conditional rule): (where G is a new function symbol) is proved infeasible with respect to reductions with R. The following structure A over N − {0}: Figure 3 and ϕ Feas is (∃x) f(x) → * x. Thus, rule (24) is proved R-infeasible and R operationally terminating.
The following structure A over N: (27) is proved R-infeasible. In [36,Example 17] this is proved by using tree automata techniques. It is also shown that the alternative technique investigated in the paper (the use of unification tests) does not work in this case.

Non-Joinability of Critical Pairs (ϕ Join )
The analysis of confluence often relies on checking for joinability of the components s and t of a critical pair s ↓ t obtained from the rules of the (C)TRS R, i.e., we look for a term u such that s → * R u and t → * R u. The problem of disproving joinability of ground terms has been investigated for TRSs, as an interesting contribution to the development of methods for (automatically) proving non-confluence of TRSs [1].
Actually, proving non-joinability of (ground) terms can be seen as a particular case of infeasibility: given ground terms s and t, we prove that (∃x)(s → * x∧t → * x) does not hold. In this way, we use our technique to check non-joinability of ground terms in CTRSs, something which is also considered in [36].
has a conditional critical pair a ↓ b ⇐ x → a, x → b. This critical pair is both non-joinable and infeasible: 1. For non-joinability, consider the structure A over {0, 1}: Thus, the critical pair is non-joinable. In [36,Example 3] this is proved by an unification test. 2. For infeasibility, consider the structure A over N: Thus, the critical pair is infeasible. In [36, Example 3] this is not actually proved but the authors argue that the unification test does not work.

Irreducible Terms (ϕ Red )
It is well-known that, in sharp contrast to unconditional rewriting, for CTRSs R it is not decidable whether a given term t is (one-step) reducible. In Example 3, we already exemplified the use of our technique to check whether a given reduction step s → t for ground terms s and t is not possible. In general, with ϕ Red , i.e., (∃x) t → x, and Corollary 2 we can prove that a given ground term t is irreducible. In the following example we show an interesting variant.
Example 11. Consider the following CTRS R [25, Example 13]: Note that every term f(t) is irreducible at the root. We can prove this claim with a slight variant of ϕ Red : (∃x, y) f(x) Λ → y, which claims for the existence of a where reductions with Λ → R are not propagated below the root of terms: for each rule ℓ → r ⇐ s 1 → t 1 , . . . , s n → t n , we have a sentence: in H Λ

→R
(where x 1 , . . . , x k are the variables occurring in the rule) and nothing else. Note that the conditions in the rules are evaluated with → * R rather than with Λ −→ * R . For this reason, no definition of the reflexive and transitive closure of Λ → is given. Thus, the Horn theory R ∪ H Λ →R we have to deal with is This proves that for all ground terms t, f(t) is irreducible at the root.

Cycling/Looping Terms and Systems (ϕ Cycl /ϕ Loop )
A term t loops (with respect to a CTRS R) if there is a rewrite sequence t = t 1 → R · · · → R t n for some n > 1 such that t is a (non-necessarily strict) subterm of t n , written t n ☎ t (cf., [10,Definition 3]). We say that a CTRS is non-looping if no term loops. We can check loopingness of terms t or CTRSs R by using ϕ Loopt and ϕ Loop in Figure 1 together with Corollary 2 if the considered Horn theory is the union of R and the Horn theory H ☎ describing the subterm relation ☎: where (46) is given for each k-ary function symbol f ∈ F and argument i, Example 12. Consider the TRS We can prove a non-looping. The Horn theory R ∪ H ☎ is the following The following structure over N ∪ {−1}: Therefore, a is non-looping. On the other hand, although b is a looping term, we can also prove that it is non-cycling. Actually, we can prove that R itself is non-cycling with the following structure over N ∪ {−1}

Secure Access to Web sites
The specification in Figure 4 provides a partial representation of the structure and connectivity of the site of the  [19]. As in [19], web pages are modeled as terms p(u) where u represents the user browsing the site. Transitions among web pages are modeled as rewrite rules. In contrast to [19], we use an order-sorted specification and the sort of u is used to allow/disallow the access to some web pages. For this reason, the specification is given as a Maude module whose syntax is hopefully self-explanatory [7].
We want to guarantee a secure access to web pages: browsing is allowed for registered users only. Regular and secure pages are terms of sort WebPage and SecureWebPage, respectively. SecureWebPage is subsort of WebPage. Registered and eventual users are given sorts RegUser and EventualUser, respectively. Both are subsorts of User. Browsing the web site is modeled as rewriting in the OS-TRS above. Our goal is verifying that no eventual user can reach the submission page. Thus, we formulate the property we want to avoid : Indeed, this is a particular case of ϕ Feas but including information about sorts is crucial. The following structure A with (i) domains and (iii) predicate symbols → * , → ∈ Π WebPage WebPage both interpreted as ≥ is a model of R ∪ {¬(∃u : EventualUser) wwv05(u) → * submit(u)}, thus proving the desired security property. Note that this crucially depends on the type RegUser of variable R controling the 'identity' of any user reaching the web page submit. If a rank submit : User -> SecureWebPage is used instead of the current one but variable R in the rule for submit is of type RegUser, the property still holds. However, if R is of type User, then no model is obtained.

Related Work
The so-called first-order theory of rewriting (FOThR in the following) uses a restricted first-order language (without constant or function symbols, and with only two predicate symbols → and → * ). The predicate symbols are by definition interpreted on an intended model that, for a given TRS R, gives meaning to → and → * as the one-step and many-step rewrite relations → R and → * R for R on ground terms, respectively [9]. Note that this is just the least Herbrand model H R associated to the Horn theory R of R! FOThR is often used to express and verify properties of TRSs. For instance, confluence can be expressed as follows: Given a TRS R and a formula ϕ in the language of FOThR, H R |= ϕ (i.e., the satisfiability of ϕ in H R ) actually means that the property expressed by ϕ holds for the TRS R. For instance H R |= (58) means 'R is ground confluent'. And ¬(H R |= (58)), which is equivalent to H R |= ¬(58) means 'R is not ground confluent'. Decision algorithms for these properties exist for restricted classes of TRSs R like left-linear right-ground TRSs, where variables are allowed in the left-hand side of the rules (without repeated occurrences of the same variable) but disallowed in the right-hand side [32]. However, a simple fragment of FOThR like the First-Order Theory of One-Step Rewriting, where only a single predicate symbol → representing one-step rewritings with R is allowed, has been proved undecidable even for linear TRSs [37]. In contrast, we use the full expressive power of first-order logic to represent sophisticated rewrite theories where sorts, conditional rules and equations, membership predicates, etc., are allowed. We do not impose any restriction on the class of rewrite systems we can deal with. In contrast to FOThR, where function symbols are not allowed in formulas, we can use arbitrary sentences involving arbitrary terms. Also in contrast to FOThR, with a single allowed model H R , we permit the arbitrary interpretation of the underlying first-order logic language for proving properties. As a consequence of this, though, we also need to impose restrictions to the shape of first-order sentences we can deal with meaningfully. The application of this approach to well-known problems in rewriting leads to new methods which show their usefulness with regard to existing methods. In contrast to FOThR, though, sentences like (58) do not fit format (8) considered in this paper (but most sentences in Figure 1 cannot be expressed in FOThR either, as they involve specific terms with or without variables).
Other approaches like the ITP tool, a theorem prover that can be used to prove properties of membership equational specifications [8] work similarly: the tool can be used to verify such properties with respect to ITP-models which are actually special versions of the Herbrand model of the underlying theory. Then, one may have similar decidability problems as discussed for FOThR.

Conclusions and future work
We have presented a semantic approach to prove properties of computational systems whose semantics can be given as a Horn theory S. Provided that a program property can be expressed as a first-order sentence ϕ which is the existential closure of a positive boolean combination of atoms, the satisfaction of the negation ¬ϕ of this sentence by an arbitrary model A of S implies that ¬ϕ holds in the standard Herbrand model of S. As usual, we can think of this fact as S actually missing the property expressed by ϕ.
We have explained how to apply this simple technique to deal with rewritingbased computational systems, in particular with (possibly sorted) conditional rewrite systems. We have considered a number of properties that have been investigated in the literature (infeasibility of conditional critical pairs and rules, non-joinability of ground terms, non-loopingness, nonreachability, etc.). Quite surprisingly, we could handle many specific examples coming from papers developing specific techniques to deal with these problems with our semantic approach (Corollary 2). In particular, we could deal with all the examples solved in [35,36] (some of them reported in our examples above; note that these papers explore several alternative methods and, as reported by the authors, some of them fail in specific examples which then require a different approach). We also dealt with all Aoto's examples in [1] in combination with his usable rules refinement (see also [20]). Furthermore, these examples were all handled by using our tool AGES for the automatic generation of models of Order-Sorted First-Order Theories.
In the future, we plan to improve the ability of our methods to deal with more general properties. In particular, a better use of sorts when modeling computational systems looks promising (as suggested in Section 5.6), in a similar way as type introduction improves the ability to prove properties of TRSs [39].