1 Introduction↩︎

Semantic labelling is a transformation technique for rewrite systems, introduced by Zantema [1], [2]. Given a rewrite system, the goal is to find a labelled version for which termination is easier to prove than for the original system. For the transformation to be correct, it must preserve both termination and nontermination. Since the labelled system typically has a larger alphabet, interpretations and other termination methods gain more freedom as they can assign different meanings to the same original symbol, now distinguished by labels. Each semantic labelling is parameterized by an algebra—hence the name—and is correct if that algebra is a model of the rewrite system. Algebras with larger domains yield larger alphabets for the transformed system—as desired—but automating semantic labelling becomes increasingly difficult, due to the combinatorially large number of algebras.

In this paper, we compare different model-finding strategies: exhaustive enumeration for bounded domain sizes within restricted search spaces, and semantic context-closure for fixed algebras. We report on experiments with our tools Matchbox [3]¹ and MultumNonMulta (MnM) [4]².

Definitions and examples in this paper refer to string rewriting, but all approaches discussed can be directly applied to term rewriting as well. All examples in the directories SRS_Standard and SRS_Relative are taken from the Termination Problems Database³, and we occasionally refer to results of the annual Termination Competition (TC)⁴, where tools are evaluated on benchmark problems.

Following the seminal work of Zantema [1], numerous extensions and applications of semantic labelling have been proposed. Among these, we mention self-labelling [5]; labelling for rewriting modulo equations [6]; predictive labelling [7], [8], restricting the model property to usable rules, and predictive labelling for innermost termination [9]; root-labelling [10]; modularity results and certification for labelling and unlabelling [11]; SAT-encoding of constraints for labelling, among other proof methods [12], [13]. Various termination tools include implementations of semantic labelling, including Torpa [2], TPA [14], Teparla, Jambox, AProVE [15], and TcT [16].

We mostly use standard notations from rewriting, formal languages and algebra, as in [17]–[19]. For a a set \(R\) of strict rules (denoted by \(\to\)) and a set \(S\) of nonstrict rules (denoted by \(\mathrel{\to^=}\)), we say that \(R \cup S\) is terminating if \(R\) is terminating relative to \(S\). Let \([0, n) = \{0, \dots, n-1\}\) for \(n \in \mathbb{N}\).

2 Semantic Labelling↩︎

Semantic labelling is parameterized by a fixed algebra whose domain serves as the set of labels. Since labels propagate right-to-left in strings (and bottom-up in terms), the labelling is not a homomorphic interpretation. This right-context sensitivity, together with the increasing alphabet, constitutes the main strength of the transformation.

For an alphabet \(\Sigma\), a \(\Sigma\)-algebra \(A\) consists of a nonempty domain \(D\) and an interpretation function \(A : \Sigma \to D^D\) that is homomorphically extended to \(A : \Sigma^* \to D^D\) by \(A(\epsilon) = \textsf{id}_D\) for the empty string \(\epsilon\) and the identity \(\textsf{id}_D\) on \(D\), and \(A(x \cdot y) = A(x) \circ A(y)\) for \(x, y \in \Sigma^*\).⁵ Thus, the interpretation of strings in a given algebra is a homomorphic interpretation into the function space \(D^D\), i.e., a homomorphism from \((\Sigma^*, {\cdot})\) into \((D^D, {\circ})\), where \(\cdot\) is concatentation of strings, and \(\circ\) is function composition. Note that, when letters are viewed as unary symbols of a term signature, this definition coincides with those based on term evaluation. In this paper all alphabets and domains are finite; without loss of generality, let \(D = [0, n)\) for some natural number \(n > 0\). We further identify \(A : \Sigma^* \to D^D\) with its uncurried form \(A: \Sigma^* \times D \to D\) and write \(A(x, d)\) for \(A(x)(d)\) accordingly.

As an immediate consequence, \(\lambda_A(x \cdot y, d) = \lambda_A(x, A(y, d)) \cdot \lambda_A(y, d)\) for \(x,y \in \Sigma^*\). We say that \(a\) is labelled by \(d\) in \((a, d)\). For readability, we abbreviate \((a, d)\) as \(a_d\) in examples.

Define \(\lambda_A(R) = \{ \lambda_A(\ell, d) \to \lambda_A(r, d) \mid (\ell \to r) \in R,\, d \in D\}\).

By unlabelling [2] (cf. [11]), i.e., by the homomorphism \(u : (a, d) \mapsto a\), we arrive at the reverse implication.⁶ Note that \(u(\lambda_A(R)) = R\).

The following result is an immediate consequence of Lemmas 2 and 3.

Rewrite systems \(R\) and \(S\) over the same alphabet \(\Sigma\) are called isomorphic if there exists a bijection \(f : \Sigma \to \Sigma\) such that \(f(R) = S\).⁸ In particular, any (non)termination proof for a rewrite system carries over to every isomorphic system.

3 Restricting the Search Space↩︎

Finding a model for a given rewrite system by enumerating algebras is feasible only if the search space is sufficiently small, and if the subsequent proof attempt for each algebra is sufficiently fast. In this section, we describe two approaches for reducing the search space: the use of restricted growth algebras as an approximation of a full isomorphism check, and the use of strongly connected algebras to eliminate a different source of redundancy. In experiments, we consider only weight orderings as subsequent proof attempts (see Footnote 7), since the existence of a compatible weight ordering can be checked efficiently using current constraint solvers; our tools use GLPK⁹ for that purpose.

3.1 Restricted Growth Algebras↩︎

Restricted growth sequences are a well-established combinatorial concept and have been used in various variants for enumerating and counting discrete structures; see, e.g., [20] and [21].

Without loss of generality, let \(\Sigma = [0, s)\) for some \(s \in \mathbb{N}\). For algebra \(A\) with domain \(D = [0, n)\) let \(A : a \mapsto \{0 \mapsto a_0, 1 \mapsto a_1, ..., n-1 \mapsto a_{n-1}\}\), where \(a \in \Sigma\) and \(a_i \in D\). Let \(\textsf{vals}(a) = (a_0, \dots, a_{n-1})\) be the list of values of \(A(a)\), and let \((k_1, \dots, k_{s \cdot n})\) be the concatenation of \(\textsf{vals}(0), \dots, \textsf{vals}(s-1)\). Define Algebra \(A\) to be a restricted growth algebra, or RG-algebra for short, if \((k_1, \dots, k_{s \cdot n})\) is a restricted growth sequence, i.e., if \(k_1 \leq 1\) and \(k_i \leq \max\{ k_0, \dots, k_{i-1}\} + 1\) for \(1 < i \leq s \cdot n\). Note that in contrast to the standard definition, we also allow \(k_1 = 1\) in a restricted growth sequence.¹⁰

An algebra \(A\) is a model of a rewrite system \(R\) if and only if every algebra isomorphic to \(A\) is a model of \(R\). Hence, without loss of generality, we may restrict our search for models of \(R\) to RG-algebras. Note that RG-algebras are not necessarily unique in their respective isomorphism class, as the next example shows.

3.2 Strongly Connected Algebras↩︎

A different way to restrict the search space is by excluding algebras that are not strongly connected, cf. Remark [useless]. For \(d, d' \in D\), we say that \(d'\) is reachable from \(d \in D\) if \(A(x, d) = d'\) for some \(x \in \Sigma^*\). This corresponds to reachability in the automaton from Remark [automaton]. An algebra \(A\) is said to be strongly connected, or an SC-algebra for short, if every element of \(D\) is reachable from every other element of \(D\). In particular, every algebra isomorphic to a strongly connected algebra is strongly connected. We use the term strongly connected component (SCC) in the standard graph-theoretic sense. An SCC is called a sink if it has no outgoing edges in the corresponding condensation DAG.

We generalize the labelling of rules to subsets of the domain \(\bar{D} \subseteq D\) by \(\lambda_A(R, \bar{D}) = \{ \lambda_A(\ell, d) \to \lambda_A(r, d) \mid (\ell \to r) \in R,\, d \in \bar{D}\}\), thus \(\lambda_A(R) = \lambda_A(R, D)\).

Again, the search for models can be restricted to SC-algebras, and even to algebras that are both RG- and SC-algebras (RG-SC-algebras for short), assuming that smaller domains are considered before larger ones in the enumeration.

3.3 Counting Restricted Algebras↩︎

Table 1 compares the number of \(\Sigma\)-algebras with domain size \(n\) against the cardinality of the restricted classes discussed above. The number of all algebras is \(n^{n |\Sigma|}\), the number of all RG-algebras can explicitely be given using Stirling numbers of the second kind, and for the number of all SC-algebras see Table 1 in [23].

4 Context-Closure↩︎

Example 4 illustrates that the class of models for systems with projection rules (i.e., rules with empty right-hand sides) is strongly restricted. Similar restrictions frequently arise in practice for a variety of systems. In such cases, an appropriate contex-closure may turn the system into one that admits a model, enabling subsequent proof steps to succeed.

We use the following notations for concatenation on languages, rewrite rules and systems. For \(x \in \Sigma\) and \(X, Y \subseteq \Sigma^*\) let \(xY = \{xy \mid y \in Y\}\) and \(XY = \bigcup_{x \in X}xY\). For a rewrite rule \(\ell \to r\) let \(x(\ell \to r) = (x\ell \to xr)\) be its context-closure with left-context \(x\), further let \(X(\ell \to r) = \bigcup_{x \in X}(x\ell \to xr)\), and the system \(XR = \bigcup_{p \in R}Xp\) is the context-closure of \(R\) with left-contexts \(X\); closure under right-contexts is defined analogously. For \(n, m \in \mathbb{N}\), let \(\textsf{cc}(n, R, m)\) denote \(\Sigma^n R \Sigma^m\), abbreviated as \(\textsf{cc}(n, m)\) when \(R\) is clear from the context.

For an arbitrary context-closure \(R'\) of \(R\), termination of \(R\) implies termination of \(R'\), since \({\to_{R'}} \subseteq {\to_R}\), but the converse does not hold in general.

Nontermination is preserved, however, if we additionally require the context-closure to be complete. For \(x, y \in \Sigma^*\) we write \(y \geq x\) if \(x\) is a suffix of \(y\), i.e., if \(y \in \Sigma^*x\). A set \(X \subseteq \Sigma^*\) is a complete set of suffixes, if \(\Sigma^* = Z \cup \Sigma^* X\) for \(Z = \{z \mid \exists x \in X : x \geq z\}\), i.e, each string is the suffix of some string in \(X\), or has a suffix in \(X\).

In what follows, we restrict ourselves to left-contexts.

Conversely, a context-closure may establish the model property, turning a non-model into a model: Even if \(A(\ell) \neq A(r)\), we can have \(A(x \ell) = A(x r)\) in case \(A(x)\) is not injective.

4.1 Full Context-Closure↩︎

This approach proceeds by successively searching for models of increasingly large context-closures of \(R\), i.e., of \(\Sigma^i R\) for \(i \geq 0\). Cleary, each \(\Sigma^i R\) is a complete context-closure of \(R\).

4.2 Semantic Context-Closure↩︎

Here, we fix an algebra \(A\) and test whether it is a model of increasingly large context-closures of \(R\). Completeness of these context-closures is ensured by expanding context-closures for single rules by single letters in all possible ways. This is done for those rules that violate the model property.

More formally, define the relation \(\mathrel{\vcenter{\vdash}}_A\) on rewrite systems by \(R \cup \{p\} \mathrel{\vcenter{\vdash}}_A R \cup \Sigma p\), where \(p\) is a rule with \(A \mathrel{\vcenter{\nvDash}}p\). We start with \(R_0 = R\) and compute a sequence \(R_0 \mathrel{\vcenter{\vdash}}_A R_1 \mathrel{\vcenter{\vdash}}_A R_2 \cdots\). This process need not terminate, but if it does, the result is uniquely determined, as the relation \(\mathrel{\vcenter{\vdash}}_A\) is confluent. Further, the corresponding set of suffixes is complete, because \(\{\epsilon\}\) is complete (note that \(R = \{\epsilon\}R\)) and completeness is preserved by \(\mathrel{\vcenter{\vdash}}_A\) (cf. Remark [expand]).

Finally, we present a class of algebras for which semantic context closure is guaranteed to terminate. For \(n > 0\) and nonempty \(\Gamma \subseteq \Sigma\) let \(I_{n,\Gamma}\) be the \(\Sigma\)-algebra with domain \([0,n)\), \(I_{n,\Gamma}(a,d) = \min\{d+1, n-1\}\) for \(a \in \Gamma\) (saturating increment), and \(I_{n,\Gamma}(a,d) = 0\) otherwise (reset). Note that \(I_{n,\Gamma}\) is a strongly connected restricted growth algebra.

Example 16 (Example 14 cont’d). Consider again \(R = \{ a a \to \epsilon, b b b \to \epsilon, a \mathrel{\to^=}a b b a \}\) over \(\Sigma = \{a,b\}\), and choose \(A = I_{5,\Gamma}\) for \(\Gamma = \{b\}\). Algebra \(A\) already is a model of the third rule, since both its left- and right-hand side start with letter \(a\). The expansion process thus adds contexts for the two remaining (projection) rules. For instance, \(R_0 = R \setminus \{a \mathrel{\to^=}a b b a \} \mathrel{\vcenter{\vdash}}_A R_1 = R_0 \setminus \{aa \to \epsilon\} \cup \{aaa \to a,\, baa \to b\} \mathrel{\vcenter{\vdash}}_A R_1 \setminus \{baa \to b\} \cup \{abaa \to ab,\, bbaa \to bb\} \mathrel{\vcenter{\vdash}}_A \cdots \mathrel{\vcenter{\vdash}}_A S R_0\) for the resulting complete set of suffixes \(S = \{ a b^n \mid 0 \leq n \leq 3 \} \cup \{ b^4 \}\). The labelled system has 50 strict and 5 nonstrict rules over an alphabet of size 10. A weight ordering finally establishes termination. Figure 1 illustates the expansion of suffixes. In this example, for both projection rules the resulting sets of suffixes happen to coincide.

For an arbitrary rule \(\ell \to r\), semantic context closure with \(A = I_{n,\Gamma}\) always terminates: We have \(A \mathrel{\vcenter{\vDash}}x(\ell \to r)\) for every \(x \in \Sigma^{n-1}\) (\(\ast\)), therefore semantic context-closure stops with some subset of suffixes of \(\Sigma^{n-1}\). In order to prove (\(\ast\)), let \(\bar{\Gamma} = \Sigma \setminus \Gamma\) and consider two cases: If \(x = yz\) for some \(z \in \bar{\Gamma}\Sigma^*\), then \(A \mathrel{\vcenter{\vDash}}z(\ell \to r)\), since \(A(z\ell, d) = 0 = A(zr, d)\) for \(d \in D\), thus \(A \mathrel{\vcenter{\vDash}}yz(\ell \to r)\) by Remark [preserve-model]. Otherwise we have \(x \in \Gamma^*\), and \(A \mathrel{\vcenter{\vDash}}x(\ell \to r)\), since \(A(x \ell, d) = n - 1 = A(x r, d)\) for \(d \in D\). Note that this proof also shows that the resulting suffix set is always a subset of \(\bar{\Gamma} \Gamma^* \cup \Gamma^*\).

5 Future Work↩︎

All constructions presented in this paper extend to quasi-models [1]. Continuing the approach from Section 4.2, a natural direction is to investigate semantic context-closure for other families of algebras, or to show that the family of algebras considered here is in some sense canonical. Finally, it may be worth exploring the relation between finite models and interpretations with almost linear weight functions over an infinite domain [25].

References↩︎