An Isabelle/HOL Formalization of Semi-Thue and Conditional Semi-Thue Systems

Kim, Dohan

doi:10.4230/LIPIcs.ITP.2025.10

An Isabelle/HOL Formalization of Semi-Thue and Conditional Semi-Thue Systems

Dohan Kim

Department of Computer Science, University of Innsbruck, Austria

Abstract

We present a formalized framework for semi-Thue and conditional semi-Thue systems for studying monoids and their word problem using the Isabelle/HOL proof assistant. We provide a formalized decision procedure for the word problem of monoids if they are finitely presented by complete semi-Thue systems. In particular, we present a new formalized method for checking confluence using (conditional) critical pairs for certain conditional semi-Thue systems. We propose and formalize an inference system for generating conditional equational theories and Thue congruences using conditional semi-Thue systems. Then we provide a new formalized decision procedure for the word problem of monoids which have finite complete (reductive) conditional presentations.

Keywords and phrases:

semi-Thue systems, conditional semi-Thue systems, conditional string rewriting, monoids, word problem

Copyright and License:

2012 ACM Subject Classification:

Theory of computation

\rightarrow

Logic and verification ; Theory of computation

\rightarrow

Equational logic and rewriting

Supplementary Material:

Software (Source Code): http://cl-informatik.uibk.ac.at/experiments/ITP2025/material.zip

Acknowledgements:

The author would like to thank René Thiemann for his valuable comments on this paper. The author also would like to thank the anonymous reviewers for their valuable comments to improve the presentation of this paper.

Funding:

This research was funded by the Austrian Science Fund (FWF) project I 5943-N.

DOI:

10.4230/LIPIcs.ITP.2025.10

Event:

16th International Conference on Interactive Theorem Proving (ITP 2025)

Editors:

Yannick Forster and Chantal Keller

Series and Publisher:

Leibniz International Proceedings in Informatics, Schloss Dagstuhl – Leibniz-Zentrum für Informatik

1 Introduction

It is generally accepted that semi-Thue systems, also known as string rewriting systems, were first introduced by Axel Thue in 1910’s in order to solve the word problem of semigroups and monoids [39]. They can also be viewed as presentations of monoids, where monoids are fundamental algebraic structures widely used in mathematics and computer science. In particular, they serve as a well-known framework for solving the word problem for monoids and groups. The word problem of monoids (or groups) is undecidable in general but it is decidable if they are presented by finite complete (i.e., terminating and confluent) semi-Thue systems over finite alphabets. If a finite semi-Thue system is terminating, then the critical pair lemma provides a decision procedure for confluence. If a monoid is presented by a finite terminating semi-Thue system $S$ but it is not confluent, then one may attempt to construct a finite complete semi-Thue system $S^{\prime}$ equivalent to $S$ using a completion procedure.

Semi-Thue systems can also be considered as a special case of term rewriting systems (TRSs), where term rewriting systems play an important role in programming languages (e.g., functional programming) [26], software engineering (e.g., equationally specified abstract data types) [37], computer algebra [29], and automated theorem proving [20]. For example, a semi-Thue system $S$ on $\Sigma^{*}$ can be associated with a term rewriting system (TRS) $\mathcal{R}_{S}$ in such a way that $\mathcal{R}_{S}:=\{\ell(x)\to r(x)\,|\,\ell\to r\in S\}$ [7], where each letter from an alphabet $\Sigma$ is interpreted as a unary function symbol. Here, variables in $\mathcal{R}_{S}$ are renamed whenever necessary.

The formalization¹¹1In this paper, by “formalization”, we mean a computer-assisted formalization using a proof assistant. of TRSs has been done extensively via Isabelle/HOL (e.g., IsaFoR [44]) and Coq (e.g., [8, 9]), and word problems of algebraic structures using TRSs were also discussed in early systems, such as the RRL [25] and the REVE system [31]. However, they are not directly suited for monoid and group presentations.

Our Isabelle/HOL formalization of semi-Thue systems and their related results is based on the simple string matching methods instead of using the more complex term structures. It also uses the simple shortlex order (i.e. length-lexicographic order) [7] on strings, which is simpler than the usual term orderings, such as the lexicographic path order (LPO) [22], the Knuth–Bendix order (KBO) [29] and the weighted path order (WPO) [45]. Some results of semi-Thue systems were also formalized, for example, in Lean [15] and Coq [17].

Meanwhile, conditional semi-Thue systems are extensions of semi-Thue systems, where each of their rules has the form $\ell\to r\Leftarrow s_{1}\approx t_{1},\ldots,s_{n}\approx t_{n}$ for strings $\ell,r,s_{1},t_{1},\ldots,s_{n},t_{n}$ . (Here, $\ell\to r$ can also be denoted as an ordered pair $(\ell,r)$ .) A finitely generated monoid with decidable word problem may not admit a finite complete (unconditional) presentation, but it may admit a finite complete conditional presentation [11]. For example, the monoid presented by $\mathcal{R}=\{aba\to ba\}$ on $\Sigma=\{a,b\}$ does not admit a finite complete (unconditional) presentation by a semi-Thue system but admits a finite complete conditional presentation by a conditional semi-Thue system.

The equality symbol $\approx$ in conditional string rewriting rules of conditional semi-Thue systems can be interpreted in different ways, yielding different types of conditional semi-Thue systems. Note that some conditional semi-Thue systems, such as right conditional semi-Thue systems, can be associated with conditional term rewriting systems (CTRSs) [23], but this is not the case for all types of conditional semi-Thue systems, for example, left-right conditional semi-Thue systems. We classify and formalize different types of conditional semi-Thue systems, which extend the classification of conditional semi-Thue systems discussed in [11].

We also formalize conditional equational theories and Thue congruences using conditional semi-Thue systems for the associated monoids and their word problem. In particular, we provide a formalized method for checking confluence using (conditional) critical pairs for certain types of conditional semi-Thue systems, which provides a decision procedure for confluence if they are reductive w.r.t. the shortlex order.

Our Isabelle/HOL formalization of semi-Thue and conditional semi-Thue systems along with their related results is built on IsaFoR (Isabelle/HOL Formalization of Rewriting) [44], where Isabelle/HOL [36] is a generic proof assistant and a theorem prover allowing the users to express concepts in mathematics and computer science and to prove properties about them. It also relies on the “A Case Study in Basic Algebra” AFP (archive of formal proofs) entry [4] for a formalization of monoids and groups, and the “Abstract Rewriting” AFP entry [42] for a formalization of the abstract rewriting systems (ARSs) [1] and their related properties, such as the Church-Rosser (CR) and the strong normalization (SN) property.

To the best of our knowledge, conditional semi-Thue systems and their related results have not been formalized in any proof assistant. Our formalization may provide a formalized framework for string rewriting and conditional string rewriting along with their wide variety of applications. The relevant Isabelle/HOL theory files²²2http://cl-informatik.uibk.ac.at/experiments/ITP2025/material.zip. inside IsaFoR under the directory thys/Conditional_Semi_Thue_Systems are as follows:

Semi_Thue_Systems.thy	Conditional_Semi_Thue_Systems.thy
String_Rewriting	Conditional_String_Rewriting.thy
ShortLex.thy	STS_Completion.thy
Conditional_Equational_Theories.thy	STS_Critical_Pairs.thy
CSTS_P_Critical_Pairs.thy	CSTS_R_Critical_Pairs.thy.thy

In the remainder of this paper, we use hyperlinks marked by for providing an HTML rendering for our formalized proofs in Isabelle/HOL.

2 Preliminaries

The definitions and results in this section can be found, for example, in [13, 7, 14, 19, 40].

Let $\Sigma$ be a finite alphabet, $>$ be a strict order on $\Sigma$ (i.e. a precedence on $\Sigma$ ), and $\Sigma^{*}$ be the set of all finite (possibly empty) strings from $\Sigma$ .

The shortlex order (or length-lexicographic order) $\succ_{sl}$ on $\Sigma^{*}$ induced by > is defined as follows: $s=s_{1}\cdots s_{i}\succ_{sl}t_{1}\cdots t_{j}=t$ if $i>j$ , or they have the same length (i.e., $i=j$ ) and $s_{1}\cdots s_{i}$ comes before $t_{1}\cdots t_{i}$ lexicographically using a precedence $>$ on $\Sigma$ . Here, $s_{1}\cdots s_{i}$ comes before $t_{1}\cdots t_{i}$ lexicographically using a precedence $>$ on $\Sigma$ if there is a $k$ such that $s_{1}\cdots s_{k-1}=t_{1}\cdots t_{k-1}$ and $s_{k}>t_{k}$ . If $\ell\succ_{sl}r$ , then $u\ell v\succ_{sl}urv$ for all $u,v\in\Sigma^{*}$ .

A monoid is a set equipped with an associative binary operation and a (two-sided) identity element. Note that a monoid cannot be empty because of an identity element. For example, $\Sigma^{*}$ is a (free) monoid generated by $\Sigma$ under the operation of concatenation as an associative binary operation with the empty string $\varepsilon$ as an identity element. A homomorphism between two monoids $(M,\cdot)$ and $(M^{\prime},\cdot^{\prime}$ ) is a function $\phi:M\to M^{\prime}$ such that $\phi(x\cdot y)=\phi(x)\cdot^{\prime}\phi(y)$ for all $x,y\in M$ and $\phi(1)=1^{\prime}$ , where $1$ and $1^{\prime}$ are the identities of $M$ and $M^{\prime}$ , respectively. A bijective monoid homomorphism is called a monoid isomorphism. Two monoids are said to be isomorphic if there is a monoid isomorphism between them. An element $a$ of a monoid $(M,\cdot)$ is invertible if there is an element $b\in M$ such that $a\cdot b=b\cdot a=1$ , where 1 is an identity element of $M$ . A group is a monoid in which every element is invertible.

The reflexive and transitive closure of a binary relation $\to$ is denoted by $\stackrel{{\scriptstyle*}}{{\to}}$ , and the reflexive, symmetric and transitive closure of $\to$ is denoted by $\stackrel{{\scriptstyle*}}{{\leftrightarrow}}$ called conversion.

A derivation for a binary relation $\to$ is a sequence of form $t_{0}\to t_{1}\to t_{2}\cdots$ . A binary relation $\to$ is terminating (or strongly normalizing) if there are no infinite derivations $t_{0}\to t_{1}\to t_{2}\cdots$ . An element $s$ is reducible (w.r.t. a given binary relation $\to$ ) if there is an element $u$ such that $s\to u$ ; otherwise, $s$ is irreducible. We say that $u$ is an $\to$ -normal form of $s$ if $s\stackrel{{\scriptstyle*}}{{\rightarrow}}u$ and $u$ is irreducible via $\to$ . A binary relation $\to$ is confluent if there is an element $w$ such that $u\stackrel{{\scriptstyle*}}{{\rightarrow}}w$ and $v\stackrel{{\scriptstyle*}}{{\rightarrow}}w$ whenever $s\stackrel{{\scriptstyle*}}{{\rightarrow}}u$ and $s\stackrel{{\scriptstyle*}}{{\rightarrow}}v$ . A binary relation $\to$ is locally confluent if there is an element $w$ such that $u\stackrel{{\scriptstyle*}}{{\rightarrow}}w$ and $v\stackrel{{\scriptstyle*}}{{\rightarrow}}w$ whenever $s\rightarrow u$ and $s\rightarrow v$ . A binary relation $\to$ is Church-Rosser if there is an element $w$ such that $u\stackrel{{\scriptstyle*}}{{\rightarrow}}w$ and $v\stackrel{{\scriptstyle*}}{{\rightarrow}}w$ whenever $u\stackrel{{\scriptstyle*}}{{\leftrightarrow}}v$ . Here, $\to$ is Church-Rosser iff it is confluent. Two elements $u$ and $v$ are joinable w.r.t. a binary relation $\to$ , denoted by $u\downarrow v$ , if there is an element $w$ such that $u\stackrel{{\scriptstyle*}}{{\to}}w\stackrel{{\scriptstyle*}}{{\leftarrow}}v$ (i.e., $u\stackrel{{\scriptstyle*}}{{\to}}w$ and $v\stackrel{{\scriptstyle*}}{{\to}}w$ ). A binary relation $\to$ is complete if it is both terminating and confluent. If $\to$ is terminating, then it is confluent iff it is locally confluent (see Newman’s lemma [35, 1]).

3 Semi-Thue Systems

A semi-Thue system (STS) $\mathcal{R}$ [7] over a finite alphabet $\Sigma$ is a subset of $\Sigma^{*}\times\Sigma^{*}$ . If $\mathcal{R}$ is an STS over a finite alphabet $\Sigma$ , then the single-step string rewriting relation on $\Sigma^{*}$ induced by $\mathcal{R}$ is defined as follows: for any $u,v\in\Sigma^{*}$ , $u\rightarrow_{\mathcal{R}}v$ iff there exists $(\ell,r)\in\mathcal{R}$ such that for some $x,y\in\Sigma^{*}$ , $u=x\ell y$ and $v=xry$ . Also, $\rightarrow_{\mathcal{R}}^{*}$ denotes the reflexive, transitive closure of $\rightarrow_{\mathcal{R}}$ . By extension, the terms “terminating”, “confluent”, etc., used in Section 2 are also applied to an STS $\mathcal{R}$ whose single-step string rewriting relation $\to_{\mathcal{R}}$ has those properties. In the remainder of this paper, unless otherwise stated, we denote by $\Sigma$ a finite alphabet and assume that a total precedence $>$ on $\Sigma$ is always given so that the shortlext order $\succ_{sl}$ is a well-founded total order on $\Sigma^{*}$ .

An STS $\mathcal{R}$ with the property that $(\ell,r)\in\mathcal{R}$ implies $(r,\ell)\in\mathcal{R}$ is called a Thue system. The Thue congruence induced by $\mathcal{R}$ is the relation $\stackrel{{\scriptstyle*}}{{\leftrightarrow}}_{\mathcal{R}}$ . Two strings $u,v\in\Sigma^{*}$ are congruent (modulo $\mathcal{R}$ ) if $u\stackrel{{\scriptstyle*}}{{\leftrightarrow}}_{\mathcal{R}}v$ . The congruence class $[w]_{\mathcal{R}}$ of a word $w\in\Sigma^{*}$ is defined as $[w]_{\mathcal{R}}:=\{v\in\Sigma^{*}\,|\,w\stackrel{{\scriptstyle*}}{{% \leftrightarrow}}_{\mathcal{R}}v\}$ . The set $\{[w]_{\mathcal{R}}\,|\,w\in\Sigma^{*}\}$ of congruence classes (modulo $\mathcal{R}$ ) is denoted by $\mathcal{M}_{\mathcal{R}}$ . In this section, we refer to [7, 21, 18] for the definitions and results related to STSs, monoids, and completion.

Lemma 1.

The set $\mathcal{M}_{\mathcal{R}}$ is a monoid under the operation $[u]_{\mathcal{R}}\cdot[v]_{\mathcal{R}}:=[uv]_{\mathcal{R}}$ with identity $[\varepsilon]_{\mathcal{R}}$ .

In fact, $\mathcal{M}_{\mathcal{R}}$ is the factor monoid of the free monoid $\Sigma^{*}$ modulo the congruence $\stackrel{{\scriptstyle*}}{{\leftrightarrow}}_{\mathcal{R}}$ , i.e., $\mathcal{M}_{\mathcal{R}}=\Sigma^{*}/\stackrel{{\scriptstyle*}}{{% \leftrightarrow}}_{\mathcal{R}}$ .

Definition 2.

(i)

Let $\mathcal{R}$ be an STS over $\Sigma$ . If a monoid $\mathcal{M}$ is isomorphic to the factor monoid $\mathcal{M}_{\mathcal{R}}$ ( $\mathcal{M}\cong\mathcal{M}_{\mathcal{R}}$ ), then the ordered pair ( $\Sigma;\mathcal{R}$ ) is a presentation of $\mathcal{M}$ , and simply write $\mathcal{M}=(\Sigma;\mathcal{R})$ . If $\to_{\mathcal{R}}$ is complete, then ( $\Sigma;\mathcal{R}$ ) is a complete presentation of $\mathcal{M}$ .
(ii)

The monoid $\mathcal{M}=(\Sigma;\mathcal{R})$ is finitely presented if both $\Sigma$ and $\mathcal{R}$ are finite.
(iii)

The word problem of the monoid $\mathcal{M}=(\Sigma;\mathcal{R})$ is the following decision problem: Given two words $u,v\in\Sigma^{*}$ , decide if $u=v$ in $\mathcal{M}$ .

Our formalization of STSs and their associated monoids is based on the following Isabelle’s locale, where a locale [3] is a named context for fixed parameters with assumptions.

locale semi_Thue $=$

fixes $R : :$ $s t s$ and $T : :$ $s t s$ and $S : :$ " $char\;set$ "

assumes " $T=\textup{(}ststep\;R\textup{)}^{\leftrightarrow^{*}}$ " and " $finite\;S$ " and " $S\neq\{\}$ " and " $finite\;R$ " and " $\textup{(}ststep\;R\textup{)}^{*}\subseteq S^{\star}\times S^{\star}$ "

begin

$\ldots$

Above, $R$ denotes a finite STS over a finite non-empty alphabet $S$ , while $T$ denotes the Thue congruence induced by $R$ . The sts type for $R$ and $T$ is declared as follows:

type_synonym sts $=$ "srule set"

where the type srule is declared simply as string $\times$ string. (Alternatively, instead of using the Isabelle’s dedicated string type (i.e., char list type), one can use the ’a list type, which is suitable for more general STSs.) Also, $(ststep\;R)^{*}\subseteq S^{\star}\times S^{\star}$ represents the assumption ${\to}_{\mathcal{R}}^{*}\,\subseteq\,\Sigma^{*}\times\Sigma^{*}$ , which also implies $\to_{\mathcal{R}}\,\subseteq\,\Sigma^{*}\times\Sigma^{*}$ . Our formalization of Lemma 1 also uses the locale monoid in the AFP entry [4]. It is instantiated as a sublocale using the following parameters, where $S^{\star}/T$ represents the factor monoid $\mathcal{M}_{\mathcal{R}}$ with identity $[\varepsilon]_{\mathcal{R}}$ .

sublocale $monoid\;$ " $S^{\star}/T$ " " $\textup{(}[\cdot]\textup{)}$ " " $eq.Class\;\varepsilon$ "

We also use the locale group in the same AFP entry, which extends the locale monoid by adding the assumption that every element of a monoid is invertible. This can be further refined as in the following lemma.

Lemma 3.

The monoid $\mathcal{M}_{\mathcal{R}}$ is a group if for all $u\in\Sigma$ , there is some $v\in\Sigma^{*}$ such that $uv\stackrel{{\scriptstyle*}}{{\leftrightarrow}}_{\mathcal{R}}\varepsilon$ and $vu\stackrel{{\scriptstyle*}}{{\leftrightarrow}}_{\mathcal{R}}\varepsilon$ .

If an STS $\mathcal{R}$ is complete, then each congruence class contains a unique irreducible word only, which can be chosen as a normal form for this congruence class. Therefore, if $\mathcal{R}$ is finite and complete, then the word problem of the monoid $M=(\Sigma;\mathcal{R})$ can be solved using string rewriting, that is, given two strings $u,v\in\Sigma^{*}$ , reduce $u$ and $v$ by $\mathcal{R}$ to their respective $\mathcal{R}$ -normal forms $\bar{u}$ and $\bar{v}$ and simply compare them. Now, if one can show that ( $\Sigma;\mathcal{R}$ ) is a finite complete presentation, then one can decide the word problem of the monoid ( $\Sigma;\mathcal{R}$ ). First, in order to show that $\mathcal{R}$ is terminating, there is an easy sufficient condition for it.

Lemma 4.

If $\ell\succ_{sl}r$ for each $(\ell,r)\in\mathcal{R}$ , then $\rightarrow_{\mathcal{R}}$ is terminating.

Lemma 5.

If $\rightarrow_{\mathcal{R}}$ is terminating, then $\rightarrow_{\mathcal{R}}$ is confluent iff $\rightarrow_{\mathcal{R}}$ is locally confluent.

In Lemma 4, the shortlex order $\succ_{sl}$ is formalized as follows:

fun shortlex:: " $string\Rightarrow string\Rightarrow bool$ " where

" $shortlex\;str1\;str2=\textup{(}if\;lenorder\;str1\;str2\;then\;True\;else\;if% \;lenorder\;str2\;str1\;then\;False$

$\quad\quad else\;lexorder\;str1\;str2\textup{)}$

where the lenorder function is used for comparing the lengths of two strings and the lexorder function is used for comparing two strings of the same length via the lexicographic order (see below).

fun lenorder:: " $string\Rightarrow string\Rightarrow bool$ " where

" $lenorder\;s\;t=\textup{(}length\;s\,>\,length\;t\textup{)}$ "

fun lexorder:: " $string\Rightarrow string\Rightarrow bool$ " where

" $lexorder\;s\;t=\textup{(}\exists u1\;u2\;u3\;ch1\;ch2\,.\,s=u1\,@\,[ch1]\,@\,u% 2\wedge t=u1\,@\,[ch2]\,@\,u3\wedge ch1\succ_{p}ch2\textup{)}$ "

Above, “@” denotes the list append function in Isabelle/HOL. Here, the list append function “@” serves as the string concatenation function. Accordingly, both $ch1$ and $ch2$ are characters, where $ch1\succ_{p}ch2$ denotes that $ch1$ has a higher precedence than $ch2$ . It is also the case that $s$ is greater than $t$ w.r.t. the lexicographic order if $t$ is a strict prefix of $s$ (see [14]). We omit this case because this case is not necessary for the shortlex order. The shortlex order using the shortlex function is abbreviated as $\succ_{sl}$ .

abbreviation shortlex_s (infix " $\succ_{sl}$ " 50) where " $s\succ_{sl}t\equiv shortlex\;s\;t$ "

abbreviation shortlex_ns (infix " $\succeq_{sl}$ " 50) where " $s\succeq_{sl}t\equiv shortlex\;s\;t\vee s=t$ "

Definition 6.

(i)

For each pair of not necessarily distinct string rewriting rules from $\mathcal{R}$ , say $(u_{0},v_{0})$ and $(u_{0}^{\prime},v_{0}^{\prime})$ , the set of critical pairs, denoted by $CP(\mathcal{R})$ , corresponding to this pair is $\{(v_{0}y,xv_{0}^{\prime})\,|\,\text{there are }x,y\in\Sigma^{*}\text{ such % that }u_{0}y=xu_{0}^{\prime}\text{ and }|x|<|u_{0}|\}\cup\{(v_{0},xv_{0}^{% \prime}y)\,|\,\text{there are }x,y\in\Sigma^{*}\text{ such that }u_{0}=xu_{0}^% {\prime}y\}$ .
(ii)

A critical pair $(z_{1},z_{2})$ is joinable if $z_{1}\downarrow_{\mathcal{R}}z_{2}$ .

Lemma 7.

If $t\mathrel{{}_{\mathcal{R}}{\mathrel{\leftarrow}}}s\to_{\mathcal{R}}u$ , then $t\downarrow_{\mathcal{R}}u$ or $t\leftrightarrow_{CP(\mathcal{R})}u$ .

Lemma 8.

$\rightarrow_{\mathcal{R}}$ is locally confluent iff all its critical pairs are joinable.

By using Definition 6(i), the set of critical pairs for an STS $\mathcal{R}$ is formalized as follows:

definition sts_critical_pairs where

" $sts\_critical\_pairs\;R=\{\textup{(}v\,@\,y,x\,@\,v^{\prime}\textup{)}\,|\,x\,% y\,u\,v\,u^{\prime}\,v^{\prime}.\textup{(}u,v\textup{)}\in R\,\wedge\textup{(}% u^{\prime},v^{\prime}\textup{)}\in R\;\wedge\;u\,@\,y=x\,@\,u^{\prime}\;\wedge\;$

$\quad length\;x<length\;u\}\;\cup\;\{\textup{(}v,x\,@\,v^{\prime}\,@\,y\textup% {)}\,|\,x\,y\,u\,v\,u^{\prime}\,v^{\prime}.\textup{(}u,v\textup{)}\in R\wedge% \textup{(}u^{\prime},v^{\prime}\textup{)}\in R\wedge u=x\,@\,u^{\prime}\,@\,y\}$ "

lemma sts_critical_pair_lemma:

" $WCR\,\textup{(}ststep\;R\textup{)}\longleftrightarrow\textup{(}\forall\textup{% (}s,t\textup{)}\in sts\_critical\_pairs\;R\;.\;\textup{(}s,t\textup{)}\in% \textup{(}ststep\;R\textup{)}^{\downarrow}\textup{)}$ "

Our formalization of Lemma 8 is as above. Here, WCR [42] is the existing formalized definition of the Weak Church-Rosser property, where $WCR\,(ststep\;R)$ denotes that $\to_{\mathcal{R}}$ is locally confluent.

Theorem 9.

If $\rightarrow_{\mathcal{R}}$ is terminating, then $\rightarrow_{\mathcal{R}}$ is confluent iff all its critical pairs are joinable.

The following theorem and its proof provide a decision procedure for the word problem of a monoid if it is presented by a finite complete STS.

Theorem 10.

Let $\mathcal{R}$ be a finite STS on $\Sigma^{*}$ . If $\rightarrow_{\mathcal{R}}$ is complete, then we can decide whether $s$ and $t$ in $\Sigma^{*}$ are the same element in the monoid $\mathcal{M}_{\mathcal{R}}$ .

Proof.

Observe that if $s\stackrel{{\scriptstyle*}}{{\leftrightarrow}}_{\mathcal{R}}t$ , then $s$ and $t$ are the same element in $\mathcal{M}_{\mathcal{R}}:=\Sigma^{*}/\stackrel{{\scriptstyle*}}{{% \leftrightarrow}}_{\mathcal{R}}$ ; otherwise, they are the different elements in $\mathcal{M}_{\mathcal{R}}$ . Since $\rightarrow_{\mathcal{R}}$ is finite and complete, we can decide whether $s\stackrel{{\scriptstyle*}}{{\leftrightarrow}}_{\mathcal{R}}t$ by comparing the normal forms of $s$ and $t$ w.r.t. $\rightarrow_{\mathcal{R}}$ , that is, if the normal forms of $s$ and $t$ w.r.t. $\rightarrow_{\mathcal{R}}$ are the same, then they are the same element in $\mathcal{M}_{\mathcal{R}}$ (i.e., $[s]_{\mathcal{R}}=[t]_{\mathcal{R}}$ ); otherwise, they are the different elements in $\mathcal{M}_{\mathcal{R}}$ (i.e., $[s]_{\mathcal{R}}\neq[t]_{\mathcal{R}}$ ). $\hfill\blacktriangleleft$

Figure 1: Inference rules for completion of a semi-Thue system

\mathcal{R}

on

\Sigma^{*}

.

$\blacktriangleright$ Remark 11.

Thus far, this section has been concerned with the word problem of monoids and its decision procedure if they are presented by finite complete STSs. Our formalization can also be used for the word problem for finitely presented groups. Group presentations can be converted into monoid presentations (see [19, 40]). (Recall that groups are also monoids.) Let $S$ be a set of generators of a group $G$ , $R$ be a set of relations of $G$ , and $S_{\alpha}=\{s^{\alpha}\,|\,s\in S,\alpha\in\{1,-1\}\}$ . Then the group defined by the presentation $<S\,|\,R>$ is equivalent to the monoid defined by the presentation $(\Sigma;\mathcal{R})$ , where $\Sigma=S_{\alpha}$ and $\mathcal{R}$ is an STS orienting the equations in $\{ss^{-1}\approx 1\,|\,s\in S_{\alpha}\}\cup R$ using the total shortlex order on $S_{\alpha}^{*}$ . (Here, if $u=v^{-1}\in S_{\alpha}$ , then $u^{-1}$ is defined to be equal to $v$ .) Therefore, Theorem 10 can also be used for the word problem of a group if its group presentation yields the monoid presentation $(\Sigma;\mathcal{R})$ such that $\mathcal{R}$ is a finite complete STS on $\Sigma^{*}$ .

Completion [1, 29, 18] attempts to transform a set of equations (or string rewriting rules in equational form) on $\Sigma^{*}$ into an equivalent complete string rewriting system. It basically converts non-joinable critical pairs into string rewriting rules so that they are joinable. It uses a reduction order [19] (e.g. the shortlex order) to orient equations on $\Sigma^{*}$ , and also uses string rewriting for simplification. (Here, an equation is an unordered pair $(s,t)$ of strings on $\Sigma^{*}$ , written as $s\approx t$ .) The inference rules, which are given in Figure 1, operate on pairs $(\mathcal{E},\mathcal{R})$ , where $\mathcal{E}$ is a set of equations and $\mathcal{R}$ is a set of string rewriting rules on $\Sigma^{*}$ . Intuitively speaking, $\mathcal{E}$ is a set of input equations or critical pairs that have not yet been transformed (i.e., oriented) into string rewriting rules, while $\mathcal{R}$ is a terminating set of string rewriting rules.

Definition 12.

We write $(\mathcal{E},\mathcal{R})\vdash_{SR}(\mathcal{E}^{\prime},\mathcal{R}^{\prime})$ if $(\mathcal{E}^{\prime},\mathcal{R}^{\prime})$ can be obtained from $(\mathcal{E},\mathcal{R})$ by applying one of the inference rules in Figure 1.

Definition 13.

(i)

A (finite) run for an initial set of equations $\mathcal{E}$ is a finite sequence $(\mathcal{E}_{0},\mathcal{R}_{0})\vdash_{SR}(\mathcal{E}_{1},\mathcal{R}_{1})% \vdash_{SR}\cdots\vdash_{SR}(\mathcal{E}_{n},\mathcal{R}_{n})$ , where $\mathcal{E}_{0}=\mathcal{E}$ and $\mathcal{R}_{0}=\emptyset$ .
(ii)

A run $(\mathcal{E}_{0},\mathcal{R}_{0})\vdash_{SR}(\mathcal{E}_{1},\mathcal{R}_{1})% \vdash_{SR}\cdots\vdash_{SR}(\mathcal{E}_{n},\mathcal{R}_{n})$ fails if $\mathcal{E}_{n}\neq\emptyset$ .
(iii)

A run $(\mathcal{E}_{0},\mathcal{R}_{0})\vdash_{SR}(\mathcal{E}_{1},\mathcal{R}_{1})% \vdash_{SR}\cdots\vdash_{SR}(\mathcal{E}_{n},\mathcal{R}_{n})$ is fair if $CP(\mathcal{R}_{n})\subseteq\bigcup_{i=0}^{n}\leftrightarrow_{\mathcal{E}_{i}}$ .

Lemma 14.

For every non-failing run $(\mathcal{E}_{0},\mathcal{R}_{0})\vdash_{SR}(\mathcal{E}_{1},\mathcal{R}_{1})% \vdash_{SR}\cdots\vdash_{SR}(\mathcal{E}_{n},\mathcal{R}_{n})$ , $\stackrel{{\scriptstyle*}}{{\leftrightarrow}}_{\mathcal{E}_{0}}\;=\;\stackrel{% {\scriptstyle*}}{{\leftrightarrow}}_{\mathcal{R}_{n}}$ .

Definition 15 (cf. [18]).

Let $\mathcal{R}$ be an STS on $\Sigma^{*}$ and $M$ be a finite multiset of strings on $\Sigma^{*}$ . We write (the labeled string rewriting) $s\xrightarrow[\mathcal{R}]{M}t$ if $s\to_{\mathcal{R}}t$ and there are some $s^{\prime},t^{\prime}\in M$ such that $s^{\prime}\succeq_{sl}s$ and $t^{\prime}\succeq_{sl}t$ . Here, $\succeq_{sl}$ denotes the reflexive closure of $\succ_{sl}$ .

Lemma 16.

Let $(\mathcal{E},\mathcal{R})\vdash_{SR}(\mathcal{E}^{\prime},\mathcal{R}^{\prime})$ . If $\smash{t\mathrel{\smash{\xleftrightarrow[\mathcal{E}\hskip 0.85358pt\cup\hskip 0% .85358pt\mathcal{R}]{M}}^{*}\vphantom{\xleftrightarrow[\mathcal{E}\hskip 0.853% 58pt\cup\hskip 0.85358pt\mathcal{R}]{M}}}u}$ and $\mathcal{R}^{\prime}\subseteq{\succ_{sl}}$ , then $\smash{t\mathrel{\smash{\xleftrightarrow[\mathcal{E}^{\prime}\hskip 0.85358pt% \cup\hskip 0.85358pt\mathcal{R}^{\prime}]{M}}^{*}\vphantom{\xleftrightarrow[% \mathcal{E}^{\prime}\hskip 0.85358pt\cup\hskip 0.85358pt\mathcal{R}^{\prime}]{% M}}}u}$ .

The following definition is due to [43, 18].

Definition 17.

(i)

An abstract rewrite system (ARS) $\mathcal{A}$ is a set $A$ equipped with a binary relation $\to$ . We also write an ARS $\mathcal{A}$ as $\langle A,\{\to_{\alpha}\}_{\alpha\in I}\rangle$ where we denote by $\to_{\alpha}$ the part of the binary relation $\to$ with label $\alpha$ indexed by $I$ so that ${\to}=\bigcup\nobreak\ \{\to_{\alpha}\mid\alpha\in I\}$ .
(ii)

An ARS $\mathcal{A}=\langle A,\{\to_{\alpha}\}_{\alpha\in I}\rangle$ is peak decreasing if there exists a well-founded order $>$ on $I$ such that for all $\alpha,\beta\in I$ the inclusion

${\mathrel{{}_{\alpha}{\mathrel{\leftarrow}}}\cdot\to_{\beta}}\nobreak\ % \subseteq\nobreak\ {\xleftrightarrow[\,\vee\alpha\beta\nobreak\ ]{*}}$

holds. Here, ${\vee\alpha\beta}$ denotes the set $\{\gamma\in I\mid\text{$\alpha>\gamma$ or $\beta>\gamma$}\}$ and if $J\subseteq I$ then $\xleftrightarrow[J]{*}$ denotes a conversion consisting of ${\to}_{J}=\bigcup\nobreak\ \{\to_{\gamma}\mid\gamma\in J\}$ steps.

See [18] for the proof of the following lemma and its Isabelle/HOL formalization.

Lemma 18.

Every peak decreasing ARS is confluent.

Theorem 19 (cf. [18]).

For every fair non-failing run $(\mathcal{E}_{0},\mathcal{R}_{0})\vdash_{SR}(\mathcal{E}_{1},\mathcal{R}_{1})% \vdash_{SR}\cdots\vdash_{SR}(\mathcal{E}_{n},\mathcal{R}_{n})$ , $\rightarrow_{\mathcal{R}_{n}}$ is a complete STS for an initial finite set of equations $\mathcal{E}=\mathcal{E}_{0}$ on $\Sigma^{*}$ .

Sketch of the proof.

We first show that $\rightarrow_{\mathcal{R}_{n}}$ is terminating. If $(\mathcal{E},\mathcal{R})\vdash_{SR}(\mathcal{E}^{\prime},\mathcal{R}^{\prime})$ and $\mathcal{R}\subseteq\,\succ_{sl}$ , then $\mathcal{R}^{\prime}\subseteq\,\succ_{sl}$ by the case analysis of each inference rule in Figure 1. We leave the straightforward induction proof to our formalization for showing $\mathcal{R}_{n}\subseteq\,\succ_{sl}$ , which in turn shows that $\mathcal{R}_{n}$ is terminating. Now, we let $t\xleftarrow[\mathcal{R}_{n}]{M_{1}}s\xrightarrow[\mathcal{R}_{n}]{M_{2}}u$ be a labeled local peak in $\mathcal{R}_{n}$ and show that $\mathcal{R}_{n}$ is peak decreasing. By Lemma 7, we have $t\downarrow_{\mathcal{R}_{n}}u$ or $t\leftrightarrow_{CP(\mathcal{R}_{n})}u$ , and thus $t\downarrow_{\mathcal{R}_{n}}u$ or $(t,u)\in\bigcup_{i=0}^{n}{\xleftrightarrow{}_{\mathcal{E}_{i}}}$ by fairness and Definition 13(iii). Here, we only consider the case where $(t,u)\in\bigcup_{i=0}^{n}{\xleftrightarrow{}_{\mathcal{E}_{i}}}$ and leave the proof of the other case to our formalization. Since $(t,u)\in\bigcup_{i=0}^{n}{\xleftrightarrow{}_{\mathcal{E}_{i}}}$ , there is some $k$ such that $(t,u)\in{\xleftrightarrow{}_{\mathcal{E}_{k}}}$ . Now, let $M:=\{t,u\}$ . Then, we have $(t,u)\in\,\xleftrightarrow[\mathcal{E}_{k}]{M}$ , and thus $(t,u)\in\smash{\mathrel{\smash{\xleftrightarrow[\mathcal{E}_{k}\hskip 0.85358% pt\cup\hskip 0.85358pt\mathcal{R}_{k}]{M}}^{*}\vphantom{\xleftrightarrow[% \mathcal{E}_{k}\hskip 0.85358pt\cup\hskip 0.85358pt\mathcal{R}_{k}]{M}}}}$ . By repeated applications of Lemma 16, we have $(t,u)\in\smash{\mathrel{\smash{\xleftrightarrow[\mathcal{R}_{n}]{M}}^{*}% \vphantom{\xleftrightarrow[\mathcal{R}_{n}]{M}}}}$ . This means that there is a conversion between $t$ and $u$ , where each step in the conversion is labeled by $M$ . Let $\succ_{sl}^{mul}$ denote the multiset extension of $\succ_{sl}$ . Then, $\succ_{sl}^{mul}$ is well-founded because $\succ_{sl}$ is well-founded. Since $M_{1}\succ_{sl}^{mul}M$ and $M_{2}\succ_{sl}^{mul}M$ , $\rightarrow_{\mathcal{R}_{n}}$ is peak decreasing, and thus confluent by Lemma 18. $\hfill\blacktriangleleft$

Our formalization of the inference rules in Figure 1 for a completion step uses the “inductively defined predicates” in Isabelle/HOL.

inductive $sts\_compl\_step$ :: " $sts\times sts\Rightarrow sts\times sts\Rightarrow bool$ " (infix " $\,\vdash_{SR}$ " 55) where

$d e d u c e$ : " $\textup{(}E,R\textup{)}\,\vdash_{SR}\,\textup{(}E\cup\{\textup{(}s\,@\,u3,u1\,% @\,t\textup{)}\},R\textup{)}$ "

if " $\textup{(}u1\,@\,u2,s\textup{)}\in R$ " and " $\textup{(}u2\,@\,u3,t\textup{)}\in R$ " and " $u2\neq[]$ "

$|$ $s i m p l i f y l$ : " $\textup{(}E\cup\{\textup{(}u1\,@\,u2\,@\,u3,s\textup{)}\},R\textup{)}\,\vdash_% {SR}\,\textup{(}E\cup\{\textup{(}u1\,@\,t\,@\,u3,s\textup{)}\},R\textup{)}$ "

if " $\textup{(}u2,t\textup{)}\in R$ "

$|$ $s i m p l i f y r$ : " $\textup{(}E\cup\{\textup{(}s,u1\,@\,u2\,@\,u3\textup{)}\},R\textup{)}\,\vdash_% {SR}\,\textup{(}E\cup\{\textup{(}s,u1\,@\,t\,@\,u3\textup{)}\},R\textup{)}$ "

if " $\textup{(}u2,t\textup{)}\in R$ "

$|$ $o r i e n t l$ : " $\textup{(}E\cup\{\textup{(}s,t\textup{)}\},R\textup{)}\,\vdash_{SR}\,\textup{(% }E,\{R\cup\{\textup{(}s,t\textup{)}\}\textup{)}$ " if " $s\succ_{sl}t$ "

$|$ $o r i e n t r$ : " $\textup{(}E\cup\{\textup{(}s,t\textup{)}\},R\textup{)}\,\vdash_{SR}\,\textup{(% }E,\{R\cup\{\textup{(}t,s\textup{)}\}\textup{)}$ " if " $t\succ_{sl}s$ "

$|$ $c o l l a p s e$ : " $\textup{(}E,R\cup\{\textup{(}u1\,@\,u2\,@\,u3,s\textup{)}\}\textup{)}\vdash_{% SR}\textup{(}E\cup\{\textup{(}u1\,@\,t\,@\,u3,s\textup{)}\},R\textup{)}$ " if " $\textup{(}u2,t\textup{)}\in R$ "

$|$ $c o m p o s e$ : " $\textup{(}E,R\cup\{\textup{(}s,u1\,@\,u2\,@\,u3\textup{)}\}\textup{)}\vdash_{% SR}\textup{(}E,R\cup\{\textup{(}s,u1\,@\,t\,@\,u3\textup{)}\}\textup{)}$ " if " $\textup{(}u2,t\textup{)}\in R$ "

$|$ $d e l e t e$ : " $\textup{(}E\cup\{\textup{(}s,s\textup{)}\},R\textup{)}\,\vdash_{SR}\,\textup{(% }E,R\textup{)}$ "

Note that in Figure 1, $\mathcal{E}$ consists of unordered pairs (i.e., equations). In our formalization above, it consists of ordered pairs for technical convenience, so we use $s i m p l i f y l$ and $s i m p l i f y r$ for the simplify rule and $o r i e n t l$ and $o r i e i n t r$ for the orient rule in Figure 1.

Now, Theorem 19 is formalized as follows, where the assumptions describe a fair non-failing run $(\mathcal{E}_{0},\mathcal{R}_{0})\vdash_{SR}(\mathcal{E}_{1},\mathcal{R}_{1})% \vdash_{SR}\cdots\vdash_{SR}(\mathcal{E}_{n},\mathcal{R}_{n})$ in Theorem 19.

theorem $sts\_finite\_fair\_run\_complete$ : assumes $R\;0=\{\}$ and $E\;n=\{\}$

and " $\forall i<n\,.\,\textup{(}E\;i,R\;i\textup{)}\vdash_{SR}\textup{(}E\,\textup{(% }Suc\;i\textup{)},R\,\textup{(}Suc\;i\textup{)}\textup{)}$ "

and " $sts\_critical\_pairs\;\textup{(}R\;n\textup{)}\subseteq\textup{(}\bigcup i\leq n% \,.\,\textup{(}ststep\;\textup{(}E\;i\textup{)}\textup{)}^{\leftrightarrow}% \textup{)}$ "

shows " $complete\,\textup{(}ststep\;\textup{(}R\;n\textup{)}\textup{)}$ "

$\blacktriangleright$ Remark 20.

Using an inference system for a completion procedure is known to be simple and efficient, and it is easy to apply simplification rules [1]. An inference system-based completion procedure for TRSs was already discussed in the literature [2, 18, 1]. Our inference system in Figure 1 is adapted from the existing Knuth-Bendix completion procedures for STSs [24, 7] that do not use an inference system. (There are also inference systems for equational reasoning over strings, such as [27, 28], but they are not directly applicable to a completion procedure for STSs.) Regarding a completion procedure for finitely presented monoids and groups, one may attempt to use an inference system discussed in abstract completion [18, 2] by converting STSs into TRSs as discussed in Section 1. This is not tailored toward a completion procedure for finitely presented monoids and groups. In particular, we use the simple string matching method and the simple shortlex order on strings in Figure 1 rather than using more complex term structures for unification/matching and ordering. Note that given a fixed signature with its precedence, it takes only linear time to compare two finite strings w.r.t. the shortlex order. It takes also linear time to match two finite strings using, for example, the Knuth–Morris–Pratt (KMP) algorithm [30].

4 Conditional Semi-Thue Systems

Conditional semi-Thue systems (CSTSs) [11] are extensions of STSs in the sense that their rules may admit non-empty conditions. A CSTS on $\Sigma^{*}$ [11] is defined to be a set of conditional string rewriting rules, where each rule has the form $(\ell,r)\Leftarrow\phi$ (also denoted as $\ell\to r\Leftarrow\phi$ ) consisting of strings $\ell,r\in\Sigma^{*}$ and a sequence $\phi$ of unordered pairs of strings on $\Sigma^{*}$ . Here, $\phi$ can be thought of as a conjunction of conditions for the rule $(\ell,r)\Leftarrow\phi$ . In the following, let $\mathcal{R}$ be a CSTS on $\Sigma^{*}$ .

Definition 21.

We write $\mathcal{R}\vdash_{lr}s\approx t$ if the equation $s\approx t$ is derivable from the inference rules in Figure 2, and say that $s\approx t$ belongs to the left-right conditional equational theory induced by $\mathcal{R}$ .

Figure 2: Inference rules for yielding a left-right conditional equational theory induced by a conditional semi-Thue system

\mathcal{R}

on

\Sigma^{*}

.

We may also consider other types of conditional equational theories depending on how contexts are used for the conditions in each conditional string rewriting rule (cf. [11]).

Above, each condition is considered with a right context $u\in\Sigma^{*}$ and this context is also used for the conclusion.

Definition 22.

We write $\mathcal{R}\vdash_{r}s\approx t$ if the equation $s\approx t$ is derivable from the inference rules in Figure 2 substituting the above “Replacement (R)” rule for the “Replacement (LR)” rule. If $\mathcal{R}\vdash_{r}s\approx t$ , then we say that $s\approx t$ belongs to the right conditional equational theory induced by $\mathcal{R}$ .

Above, no additional context is used for each condition and the conclusion.

Definition 23.

We write $\mathcal{R}\vdash_{p}s\approx t$ if the equation $s\approx t$ is derivable from the inference rules in Figure 2 substituting the above “Replacement (P)” rule for the “Replacement (LR)” rule. If $\mathcal{R}\vdash_{p}s\approx t$ , then we say that $s\approx t$ belongs to the pure conditional equational theory induced by $\mathcal{R}$ .

Our formalization of the inference rules in Figure 2 for the left-right conditional equational theory induced by $\mathcal{R}$ also uses the “inductively defined predicates” in Isabelle/HOL.

inductive $cond\_eq\_lr\_theory$ :: " $csts\Rightarrow string\times string\Rightarrow bool$ " (infix " $\,\vdash_{celr}$ " 55) where

$r e f l$ : " $R\,\vdash_{celr}\,\textup{(}s,s\textup{)}$ "

$|$ $s y m m e t r y$ : " $R\,\vdash_{celr}\,\textup{(}s,t\textup{)}$ " if " $R\,\vdash_{celr}\,\textup{(}t,s\textup{)}$ "

$|$ $t r a n s i t i v e$ : " $R\,\vdash_{celr}\,\textup{(}s,u\textup{)}$ " if " $R\,\vdash_{celr}\,\textup{(}s,t\textup{)}\wedge R\,\vdash_{celr}\,\textup{(}t,% u\textup{)}$ "

$|$ $c o n g r u e n c e$ : " $R\,\vdash_{celr}\,\textup{(}u\,@\,s\,@\,v,u\,@\,t\,@\,v\textup{)}$ " if " $R\,\vdash_{celr}\,\textup{(}s,t\textup{)}$ "

$|$ $r e p l a c e m e n t$ : " $R\,\vdash_{celr}\,\textup{(}u\,@\,l\,@\,w,u\,@\,r\,@\,w\textup{)}$ "

if " $\textup{(}\textup{(}l,r\textup{)},cs\textup{)}\in R\wedge\textup{(}\forall% \textup{(}s_{i},t_{i}\textup{)}\in set\;cs.\;R\,\vdash_{celr}\,\textup{(}u\,@% \,s_{i}\,@\,w,u\,@\,t_{i}\,@\,w\textup{)}\textup{)}$ "

Above, $R\,\vdash_{celr}\,(s,t)$ denotes that $s\approx t$ belongs to the left-right conditional equational theory induced by $\mathcal{R}$ . The right (resp. pure) conditional equational theory induced by $\mathcal{R}$ can be formalized in a similar way, where $\vdash_{cer}$ (resp. $\vdash_{cep}$ ) is used for inductively defined predicate for the right (resp. pure) conditional equational theory induced by $\mathcal{R}$ . They are only different from the replacement part (see below):

$r e p l a c e m e n t$ : " $R\,\vdash_{cer}\,\textup{(}l\,@\,w,r\,@\,w\textup{)}$ "

if " $\textup{(}\textup{(}l,r\textup{)},cs\textup{)}\in R\wedge\textup{(}\forall% \textup{(}s_{i},t_{i}\textup{)}\in set\;cs.\;R\,\vdash_{celr}\,\textup{(}s_{i}% \,@\,w,t_{i}\,@\,w\textup{)}\textup{)}$ "

$r e p l a c e m e n t$ : " $R\,\vdash_{cep}\,\textup{(}l,r\textup{)}$ "

if " $\textup{(}\textup{(}l,r\textup{)},cs\textup{)}\in R\wedge\textup{(}\forall% \textup{(}s_{i},t_{i}\textup{)}\in set\;cs.\;R\,\vdash_{celr}\,\textup{(}s_{i}% ,t_{i}\textup{)}\textup{)}$ "

Meanwhile, the types of CSTSs depend on the string rewriting relations induced by CSTSs. More specifically, the types of CSTSs depend on how conditions are evaluated in the conditional parts of their conditional string rewriting rules (cf. [5, 46]). The induced string rewriting relations from CSTSs are structured into levels (cf. [41, 46]).

Definition 24.

The string rewriting relation $\to_{\mathcal{R},lr,s}$ for a left-right-semi-equational CSTS $\mathcal{R}$ on $\Sigma^{*}$ is defined as follows: $t_{1}\to_{\mathcal{R},lr,s}t_{2}$ iff $t_{1}\to_{\mathcal{R}_{n}}t_{2}$ for some $n\geq 0$ . Here, the unconditional STS $\mathcal{R}_{n}$ are inductively defined as follows:

\begin{cases}\mathcal{R}_{0}:=\emptyset\\ \mathcal{R}_{n+1}:=\{(u\ell v,urv)\,|\,(\ell,r)\Leftarrow\phi\in\mathcal{R},% \text{ and }usv\stackrel{{\scriptstyle*}}{{\leftrightarrow}}_{\mathcal{R}_{n}}% utv\text{ for\,all\,}s\approx t\in\phi\text{ and }u,v\in\Sigma^{*}\}\end{cases}

The string rewriting relation $\to_{\mathcal{R},lr,j}$ for a left-right-join CSTS $\mathcal{R}$ on $\Sigma^{*}$ is defined as: $t_{1}\to_{\mathcal{R},lr,j}t_{2}$ iff $t_{1}\to_{\mathcal{R}^{\prime}_{n}}t_{2}$ for some $n\geq 0$ , where $\mathcal{R}^{\prime}_{n}$ are inductively defined as follows:

\begin{cases}\mathcal{R}^{\prime}_{0}:=\emptyset\\ \mathcal{R}^{\prime}_{n+1}:=\{(u\ell v,urv)\,|\,(\ell,r)\Leftarrow\phi\in% \mathcal{R},\text{ and }usv\downarrow_{\mathcal{R}^{\prime}_{n}}utv\text{ for % all }s\approx t\in\phi\text{ and }u,v\in\Sigma^{*}\}\end{cases}

Definition 25.

The string rewriting relation $\to_{\mathcal{R},r,s}$ for a right-semi-equational CSTS $\mathcal{R}$ on $\Sigma^{*}$ is defined as follows: $t_{1}\to_{\mathcal{R},r,s}t_{2}$ iff $t_{1}\to_{\mathcal{R}_{n}}t_{2}$ for some $n\geq 0$ . Here, the unconditional STS $\mathcal{R}_{n}$ are inductively defined as follows:

\begin{cases}\mathcal{R}_{0}:=\emptyset\\ \mathcal{R}_{n+1}:=\{(\ell v,rv)\,|\,(\ell,r)\Leftarrow\phi\in\mathcal{R},% \text{ and }sv\stackrel{{\scriptstyle*}}{{\leftrightarrow}}_{\mathcal{R}_{n}}% tv\text{ for all }s\approx t\in\phi\text{ and }v\in\Sigma^{*}\}\end{cases}

The string rewriting relation $\to_{\mathcal{R},r,j}$ for a right-join CSTS $\mathcal{R}$ on $\Sigma^{*}$ is defined as: $t_{1}\to_{\mathcal{R},r,j}t_{2}$ iff $t_{1}\to_{\mathcal{R}^{\prime}_{n}}t_{2}$ for some $n\geq 0$ , where $\mathcal{R}^{\prime}_{n}$ are inductively defined as follows:

\begin{cases}\mathcal{R}^{\prime}_{0}:=\emptyset\\ \mathcal{R}^{\prime}_{n+1}:=\{(\ell v,rv)\,|\,(\ell,r)\Leftarrow\phi\in% \mathcal{R},\text{ and }sv\downarrow_{\mathcal{R}^{\prime}_{n}}tv\text{ for % all }s\approx t\in\phi\text{ and }v\in\Sigma^{*}\}\end{cases}

Definition 26.

The string rewriting relation $\to_{\mathcal{R},p,s}$ for a pure-semi-equational CSTS $\mathcal{R}$ on $\Sigma^{*}$ is defined as follows: $t_{1}\to_{\mathcal{R},p,s}t_{2}$ iff $t_{1}\to_{\mathcal{R}_{n}}t_{2}$ for some $n\geq 0$ . Here, the unconditional STS $\mathcal{R}_{n}$ are inductively defined as follows:

\begin{cases}\mathcal{R}_{0}:=\emptyset\\ \mathcal{R}_{n+1}:=\{(\ell,r)\,|\,(\ell,r)\Leftarrow\phi\in\mathcal{R},\text{ % and }s\stackrel{{\scriptstyle*}}{{\leftrightarrow}}_{\mathcal{R}_{n}}t\text{ % for all }s\approx t\in\phi\}\end{cases}

The string rewriting relation $\to_{\mathcal{R},p,j}$ for a pure-join CSTS $\mathcal{R}$ on $\Sigma^{*}$ is defined as: $t_{1}\to_{\mathcal{R},p,j}t_{2}$ iff $t_{1}\to_{\mathcal{R}^{\prime}_{n}}t_{2}$ for some $n\geq 0$ , where $\mathcal{R}^{\prime}_{n}$ are inductively defined as follows:

\begin{cases}\mathcal{R}^{\prime}_{0}:=\emptyset\\ \mathcal{R}^{\prime}_{n+1}:=\{(\ell,r)\,|\,(\ell,r)\Leftarrow\phi\in\mathcal{R% },\text{ and }s\downarrow_{\mathcal{R}^{\prime}_{n}}t\text{ for all }s\approx t% \in\phi\}\end{cases}

The following lemma says that our inference system for yielding the left-right, right, and pure conditional equational theories is sound w.r.t. the Thue congruences induced by the string rewriting relations associated with the left-right-semi-equational, right-semi-equational, and pure-semi-equational CSTSs, respectively.

Lemma 27.

Let $\mathcal{R}$ be a CSTS on $\Sigma^{*}$ and $t_{1},t_{2}\in\Sigma^{*}$ .

(i)

$t_{1}\stackrel{{\scriptstyle*}}{{\leftrightarrow}}_{\mathcal{R},lr,s}t_{2}$ iff $\mathcal{R}\vdash_{lr}t_{1}\approx t_{2}$ .
(ii)

$t_{1}\stackrel{{\scriptstyle*}}{{\leftrightarrow}}_{\mathcal{R},r,s}t_{2}$ iff $\mathcal{R}\vdash_{r}t_{1}\approx t_{2}$ .
(iii)

$t_{1}\stackrel{{\scriptstyle*}}{{\leftrightarrow}}_{\mathcal{R},p,s}t_{2}$ iff $\mathcal{R}\vdash_{p}t_{1}\approx t_{2}$ .

The bidirectional use of the string rewriting relations for evaluating the conditions in semi-equational CSTSs is both inefficient and unnatural (cf. [46]). We can use the join CSTSs instead of the semi-equational CSTSs if they have the confluence property.

Lemma 28.

Let $\mathcal{R}$ be a CSTS on $\Sigma^{*}$ .

(i)

If $\rightarrow_{\mathcal{R},lr,j}$ is confluent, then $\to_{\mathcal{R},lr,s}\;=\;\to_{\mathcal{R},lr,j}$ .
(ii)

If $\rightarrow_{\mathcal{R},r,j}$ is confluent, then $\to_{\mathcal{R},r,s}\;=\;\to_{\mathcal{R},r,j}$ .
(iii)

If $\rightarrow_{\mathcal{R},p,j}$ is confluent, then $\to_{\mathcal{R},p,s}\;=\;\to_{\mathcal{R},p,j}$ .

$\blacktriangleright$ Remark 29.

Recall that an STS $S$ on $\Sigma^{*}$ can be associated with a TRS $\mathcal{R}_{S}$ , where each letter from $\Sigma$ is interpreted as a unary function symbol. Similarly, a right-join CSTS $S^{\prime}$ on $\Sigma^{*}$ can be associated with a join CTRS $\mathcal{R}_{S^{\prime}}$ in such a way that $\mathcal{R}_{S^{\prime}}:=\{\ell(x)\to r(x)\Leftarrow s_{1}(x)\approx t_{1}(x)% ,\ldots,s_{n}(x)\approx t_{n}(x)\,|\,\ell\to r\Leftarrow s_{1}\approx t_{1},% \ldots,s_{n}\approx t_{n}\in S^{\prime}\}$ [11]. (Here, variables in $\mathcal{R}_{S^{\prime}}$ are renamed whenever necessary.) However, this is not the case for left-right-join CSTSs.

Example 30.

Consider $\mathcal{R}=\{a\ell\to b\ell,\ell am\to\ell bm,c\to d\Leftarrow a\approx b\}$ , where $\Sigma=\{a,b,c,d,\ell,m\}$ with $a>b>c>d>\ell>m$ . If $\mathcal{R}$ is a pure-join CSTS, then neither $c\ell\to_{\mathcal{R},p,j}d\ell$ nor $\ell cm\to_{\mathcal{R},p,j}\ell dm$ holds. If $\mathcal{R}$ is a right-join CSTS, then $c\ell\to_{\mathcal{R},r,j}d\ell$ holds, but $\ell cm\to_{\mathcal{R},r,j}\ell dm$ does not hold. If $\mathcal{R}$ is a left-right-join CSTS, then both $c\ell\to_{\mathcal{R},rl,j}d\ell$ and $\ell cm\to_{\mathcal{R},rl,j}\ell dm$ hold.

Now, we discuss our formalization of right-join and pure-join CSTSs. (Our formalization of left-right-join CSTSs is similar and is omitted.) First, the string rewriting relation $\to_{\mathcal{R},r,j}$ associated with a right-join CSTS is formalized as follows:

definition "csr_r_join_step $\mathcal{R}=\textup{(}\bigcup n.\;csr\_r\_join\_step\_n\;\mathcal{R}\;n\textup% {)}$ "

fun csr_r_join_step_n:: " $csts\Rightarrow nat\Rightarrow string\;rel$ " where

" $csr\_r\_join\_step\_n\;\mathcal{R}\;0=\;\{\}$ " $|$

" $csr\_r\_join\_step\_n\;\mathcal{R}\;\textup{(}Suc\;n\textup{)}=$

$\{\textup{(}C\mathopen{\hbox{\set@color${\langle}$}\kern-1.7986pt\hbox{% \set@color${\langle}$}}\ell\,@\,w\mathclose{\hbox{\set@color${\rangle}$}\kern-% 1.7986pt\hbox{\set@color${\rangle}$}},\,C\mathopen{\hbox{\set@color${\langle}$% }\kern-1.7986pt\hbox{\set@color${\langle}$}}r\,@\,w\mathclose{\hbox{\set@color% ${\rangle}$}\kern-1.7986pt\hbox{\set@color${\rangle}$}}\mathclose{\hbox{% \set@color${\rangle}$}\kern-1.7986pt\hbox{\set@color${\rangle}$}}\textup{)}\;|% \;C\;\ell\;r\;cs\;w.\;\textup{(}\textup{(}\ell,r\textup{)},\;cs\textup{)}\in% \mathcal{R}\;\wedge\;$

$\quad\quad\textup{(}\forall\textup{(}s_{i},\,t_{i}\textup{)}\in set\,cs.\,% \textup{(}s_{i}\,@\,w,\,t_{i}\,@\,w\textup{)}\in\textup{(}csr\_r\_join\_step\_% n\;\mathcal{R}\;n\textup{)}^{\downarrow}\textup{)}\}"$

In the csr_r_join_step_n function, $C$ is a (string) context and $C\mathopen{\hbox{\set@color${\langle}$}\kern-1.94444pt\hbox{\set@color${% \langle}$}}\ell@w\mathclose{\hbox{\set@color${\rangle}$}\kern-1.94444pt\hbox{% \set@color${\rangle}$}}$ (resp. $C\mathopen{\hbox{\set@color${\langle}$}\kern-1.94444pt\hbox{\set@color${% \langle}$}}r@w\mathclose{\hbox{\set@color${\rangle}$}\kern-1.94444pt\hbox{% \set@color${\rangle}$}}$ ) denotes the application of the context $C$ to the string $\ell w$ (resp. $r w$ ). We formalize a context for strings based on the existing formalization of contexts for terms in IsaFoR.

datatype sctxt $=$ Hole " $\textup{(}\bigcirc\textup{)}$ " $|$ More "string" "sctxt" "string"

fun sctxt_apply_string :: " $sctxt\Rightarrow string\Rightarrow string$ " ("_ $\mathopen{\hbox{\set@color${\langle}$}\kern-1.7986pt\hbox{\set@color${\langle}% $}}\_\mathclose{\hbox{\set@color${\rangle}$}\kern-1.7986pt\hbox{\set@color${% \rangle}$}}$ " [900, 0] 900) where

" $\bigcirc\mathopen{\hbox{\set@color${\langle}$}\kern-1.7986pt\hbox{\set@color${% \langle}$}}s\mathclose{\hbox{\set@color${\rangle}$}\kern-1.7986pt\hbox{% \set@color${\rangle}$}}=s$ " $|$

"(More ss1 $C$ ss2) $\mathopen{\hbox{\set@color${\langle}$}\kern-1.7986pt\hbox{\set@color${\langle}% $}}s\mathclose{\hbox{\set@color${\rangle}$}\kern-1.7986pt\hbox{\set@color${% \rangle}$}}=\textup{(}ss1\,@\,\textup{(}C\mathopen{\hbox{\set@color${\langle}$% }\kern-1.7986pt\hbox{\set@color${\langle}$}}s\mathclose{\hbox{\set@color${% \rangle}$}\kern-1.7986pt\hbox{\set@color${\rangle}$}}\textup{)}\,@\,ss2\textup% {)}$ "

Using the above function, $C\mathopen{\hbox{\set@color${\langle}$}\kern-1.94444pt\hbox{\set@color${% \langle}$}}s\mathclose{\hbox{\set@color${\rangle}$}\kern-1.94444pt\hbox{% \set@color${\rangle}$}}$ denotes $u s v$ for some (possibly empty) strings $u$ and $v$ . In the csr_r_join_step_n function, we consider all possible contexts $C$ because $\to_{\mathcal{R},r,j}$ is a string rewriting relation, i.e., $\ell\to_{\mathcal{R},r,j}r$ implies $u\ell v\to_{\mathcal{R},r,j}urv$ for all (possibly empty) strings $u$ and $v$ . Next, the string rewriting relation $\to_{\mathcal{R},p,j}$ associated with a pure-join CSTS is formalized as follows. Here, no additional string is appended for evaluating each condition.

definition "csr_p_join_step $\mathcal{R}=\textup{(}\bigcup n.\;csr\_p\_join\_step\_n\;\mathcal{R}\;n\textup% {)}$ "

fun csr_p_join_step_n:: " $csts\Rightarrow nat\Rightarrow string\;rel$ " where

" $csr\_p\_join\_step\_n\;\mathcal{R}\;0=\;\{\}$ " $|$

" $csr\_p\_join\_step\_n\;\mathcal{R}\;\textup{(}Suc\;n\textup{)}=$

$\{\textup{(}C\mathopen{\hbox{\set@color${\langle}$}\kern-1.7986pt\hbox{% \set@color${\langle}$}}\ell\mathclose{\hbox{\set@color${\rangle}$}\kern-1.7986% pt\hbox{\set@color${\rangle}$}},\,C\mathopen{\hbox{\set@color${\langle}$}\kern% -1.7986pt\hbox{\set@color${\langle}$}}r\mathclose{\hbox{\set@color${\rangle}$}% \kern-1.7986pt\hbox{\set@color${\rangle}$}}\textup{)}\;|\;C\;\ell\;r\;cs.\;% \textup{(}\textup{(}\ell,r\textup{)},\;cs\textup{)}\in\mathcal{R}\;\wedge\;% \textup{(}\forall\textup{(}s_{i},\;t_{i}\textup{)}\in$

$\quad\quad set\;cs.\;\textup{(}s_{i},\;t_{i}\textup{)}\in\textup{(}csr\_p\_% join\_step\_n\;\mathcal{R}\;n\textup{)}^{\downarrow}\textup{)}\}"$

Our formalization of CSTSs and their associated monoids relies on the following locale.

locale conditional_semi_Thue $=$

fixes $R : :$ $c s t s$ and $S : :$ " $char\;set$ "

assumes " $finite\;S$ " and " $S\neq\{\}$ " and " $finite\;R$ "

For example, the locale for right-join CSTSs extends the above locale and is described as:

locale conditional_r_join_semi_Thue $=$ $reductive\_r\_join$ $+$ $conditional\_semi\_Thue\;R\;S$

for $R : : c s t s$ and $S : :$ " $char\;set$ " $+$

fixes $Thue\_R\_Congruence::$ $s t s$

assumes " $Thue\_R\_Congruence=\textup{(}csr\_r\_join\_step\;R\textup{)}^{\leftrightarrow% ^{*}}$ " and " $Thue\_R\_Congruence\subseteq S^{*}\times S^{*}$ "

begin

$\ldots$

Since the locale conditional_r_join_semi_Thue extends the locale conditional_semi_Thue, the alphabet denoted by $S$ is assumed to be finite and non-empty. The assumptions in the locale conditional_r_join_semi_Thue also represent the assumption $\stackrel{{\scriptstyle*}}{{\leftrightarrow}}_{\mathcal{R},r,j}\,\subseteq\,% \Sigma^{*}\times\Sigma^{*}$ , which also implies the assumption $\to_{\mathcal{R},r,j}\,\subseteq\,\Sigma^{*}\times\Sigma^{*}$ .

Definition 31.

(i)

We call a CSTS $\mathcal{R}$ reductive if for all $(\ell,r)\Leftarrow\phi\in\mathcal{R}$ , $\ell\succ_{sl}r$ , $\ell\succ_{sl}s_{i}$ , and $\ell\succ_{sl}t_{i}$ for all $(s_{i},t_{i})\in\phi$ (cf. decreasingness [12] in CTRSs).
(ii)

Two STSs $\mathcal{R}_{1}$ and $\mathcal{R}_{2}$ on $\Sigma^{*}$ are equivalent if $\stackrel{{\scriptstyle*}}{{\leftrightarrow}}_{\mathcal{R}_{1}}\;=\;\stackrel{% {\scriptstyle*}}{{\leftrightarrow}}_{\mathcal{R}_{2}}$ , that is, they present the same monoid.
(iii)

An STS $\mathcal{R}_{1}$ and a reductive right-join (resp. a pure-join) CSTS $\mathcal{R}_{2}$ on $\Sigma^{*}$ are equivalent if $\stackrel{{\scriptstyle*}}{{\leftrightarrow}}_{\mathcal{R}_{1}}\;=\;\stackrel{% {\scriptstyle*}}{{\leftrightarrow}}_{\mathcal{R}_{2},r,j}$ (resp. $\stackrel{{\scriptstyle*}}{{\leftrightarrow}}_{\mathcal{R}_{1}}\;=\;\stackrel{% {\scriptstyle*}}{{\leftrightarrow}}_{\mathcal{R}_{2},p,j})$ .

Example 32 (see [11]).

The monoid $\mathcal{M}=(\Sigma;\mathcal{R})$ , where $\Sigma=\{a,b\}$ and $\mathcal{R}=\{aba\to ba\}$ , is finitely presented and have decidable word problem, but does not admit an equivalent monoid presentation with $(\Sigma;\mathcal{R}^{\prime})$ , where $\mathcal{R}^{\prime}$ is a finite complete STS. More specifically, a completion procedure for $\mathcal{R}$ may only yield an infinite complete semi-Thue system $\{ab^{n}a\to b^{n}a\,|\,n\geq 1\}$ . However, $\mathcal{R}$ admits an equivalent finite complete (reductive) right-join CSTS $\mathcal{R}^{\prime\prime}=\{aba\to ba,abb\to bb\Leftarrow ab\approx b\}$ . (Here, $(\Sigma;\mathcal{R}^{\prime\prime})$ is a finite complete (reductive) conditional presentation of $\mathcal{M}$ , which will be discussed later in this section.)

Unlike the string rewriting relations induced by semi-Thue systems, $\to_{\mathcal{R},r,j}$ is not necessarily decidable even if it is terminating (cf. [37]).

Lemma 33.

(i)

If $\mathcal{R}$ is a finite reductive right-join CSTS, then $\to_{\mathcal{R},r,j}$ is terminating and the set $\Delta_{R,r,j,s}^{*}=\{t\,|\,s\to_{\mathcal{R},r,j}^{*}t\}$ is finite for all $s\in\Sigma^{*}$ .
(ii)

If $\mathcal{R}$ is a finite reductive pure-join CSTS, then $\to_{\mathcal{R},p,j}$ is terminating and the set $\Delta_{R,p,j,s}^{*}=\{t\,|\,s\to_{\mathcal{R},p,j}^{*}t\}$ is finite for all $s\in\Sigma^{*}$ .

In the above lemma, if $\mathcal{R}$ is finite and reductive and $\to_{\mathcal{R},r,j}$ (resp. $\to_{\mathcal{R},p,j}$ ) is terminating, then we may simulate the decidability of $\to_{\mathcal{R},r,j}$ (resp. $\to_{\mathcal{R},p,j}$ ) using the finiteness of the set of descendants $\Delta_{R,r,j,s}^{*}$ (resp. $\Delta_{R,p,j,s}^{*}$ ) for all $s\in\Sigma^{*}$ . Here, the set $\Delta_{R,r,j,s}^{*}$ (resp. $\Delta_{R,p,j,s}^{*}$ ) can be shown to be computable for all $s\in\Sigma^{*}$ using the well-founded induction on $\succ_{sl}$ if $\mathcal{R}$ is finite and reductive (cf. Theorem 7.2.9 in [37]).

Definition 34.

(i)

Let $\mathcal{R}$ be a right-join CSTS. For each pair of not necessarily distinct conditional string rewriting rules from $\mathcal{R}$ , say $(u_{0},v_{0})\Leftarrow\forall_{i=1}^{m}u_{i}\approx v_{i}$ and $(u_{0}^{\prime},v_{0}^{\prime})\Leftarrow\forall_{i=1}^{n}u_{i}^{\prime}% \approx v_{i}^{\prime}$ , the set of critical pairs w.r.t. $\to_{\mathcal{R},r,j}$ corresponding to this pair is $\{(v_{0}y,xv_{0}^{\prime})\Leftarrow\forall_{i=1}^{m}u_{i}y\approx v_{i}y% \wedge\forall_{i=1}^{n}u_{i}^{\prime}\approx v_{i}^{\prime}\,|\,\text{there % are }x,y\in\Sigma^{*}\text{ such that }u_{0}y=xu_{0}^{\prime}\text{ and }|x|<|% u_{0}|\}\cup\{(v_{0},xv_{0}^{\prime}y)\Leftarrow\forall_{i=1}^{m}u_{i}\approx v% _{i}\wedge\forall_{i=1}^{n}u_{i}^{\prime}y\approx v_{i}^{\prime}y\,|\,\text{% there are }x,y\in\Sigma^{*}\text{ such that }u_{0}=xu_{0}^{\prime}y\}$ .
(ii)

A critical pair $(s_{0},t_{0})\Leftarrow\forall_{i=1}^{n}s_{i}\approx t_{i}$ is joinable w.r.t. $\to_{\mathcal{R},r,j}$ if for any $y\in\Sigma^{*}$ , $s_{i}y\downarrow_{\mathcal{R},r,j}t_{i}y$ for all $1\leq i\leq n$ implies $s_{0}y\downarrow_{\mathcal{R},r,j}t_{0}y$ .
(iii)

Let $\mathcal{R}$ be a pure-join CSTS. For each pair of not necessarily distinct conditional string rewriting rules from $\mathcal{R}$ , say $(u_{0},v_{0})\Leftarrow\forall_{i=1}^{m}u_{i}\approx v_{i}$ and $(u_{0}^{\prime},v_{0}^{\prime})\Leftarrow\forall_{i=1}^{n}u_{i}^{\prime}% \approx v_{i}^{\prime}$ , the set of critical pairs w.r.t. $\to_{\mathcal{R},p,j}$ corresponding to this pair is $\{(v_{0}y,xv_{0}^{\prime})\Leftarrow\forall_{i=1}^{m}u_{i}\approx v_{i}\wedge% \forall_{i=1}^{n}u_{i}^{\prime}\approx v_{i}^{\prime}\,|\,\text{there are }x,y% \in\Sigma^{*}\text{ such that }u_{0}y=xu_{0}^{\prime}\text{ and }|x|<|u_{0}|\}% \cup\{(v_{0},xv_{0}^{\prime}y)\Leftarrow\forall_{i=1}^{m}u_{i}\approx v_{i}% \wedge\forall_{i=1}^{n}u_{i}^{\prime}\approx v_{i}^{\prime}\,|\,\text{there % are }x,y\in\Sigma^{*}\text{ such that }u_{0}=xu_{0}^{\prime}y\}$ .
(iv)

A critical pair $(s_{0},t_{0})\Leftarrow\forall_{i=1}^{n}s_{i}\approx t_{i}$ is joinable w.r.t. $\to_{\mathcal{R},p,j}$ if $s_{i}\downarrow_{\mathcal{R},p,j}t_{i}$ for all $1\leq i\leq n$ implies $s_{0}\downarrow_{\mathcal{R},p,j}t_{0}$ .

Now, we discuss our formalization of Definition 34. First, the set of critical pairs for a right-join CSTS $\mathcal{R}$ is formalized as follows:

definition csts_r_critical_pairs where

" $csts\_r\_critical\_pairs\;R=\{\textup{(}\textup{(}v\,@\,y,x\,@\,v^{\prime}% \textup{)},cs^{\prime}\,@\,map\textup{(}\lambda\textup{(}lhs,rhs\textup{)}\;.% \;\textup{(}lhs\,@\,y,rhs\,@\,y\textup{)}\textup{)}\;cs\textup{)}\,|$

$\quad x\,y\,u\,v\,u^{\prime}\,v^{\prime}\,cs\,cs^{\prime}\;.\;\,\textup{(}% \textup{(}u,v\textup{)},cs\textup{)}\in R\wedge\textup{(}\textup{(}u^{\prime},% v^{\prime}\textup{)},cs^{\prime}\textup{)}\in R\wedge u\,@\,y=x\,@\,u^{\prime}% \wedge length\;x<length\;u\}\;\cup\;$

$\quad\{\textup{(}\textup{(}v,x\,@\,v^{\prime}\,@\,y\textup{)},cs\,@\,map% \textup{(}\lambda\textup{(}lhs,rhs\textup{)}\;.\;\textup{(}lhs\,@\,y,rhs\,@\,y% \textup{)}\textup{)}\;cs^{\prime}\textup{)}\,|\,x\,y\,u\,v\,u^{\prime}\,v^{% \prime}\,cs\,cs^{\prime}\;.\;\textup{(}\textup{(}u,v\textup{)},cs\textup{)}$

$\quad\in R\wedge\textup{(}\textup{(}u^{\prime},v^{\prime}\textup{)},cs^{\prime% }\textup{)}\in R\wedge u=x\,@\,u^{\prime}\,@\,y\}$ "

Above, if $c s$ is of the form $\forall_{i=1}^{m}u_{i}\approx v_{i}$ , then $map(\lambda(lhs,rhs)\;.\;(lhs\,@\,y,rhs\,@\,y))\;cs$ is $\forall_{i=1}^{m}u_{i}y\approx v_{i}y$ . Also, $((\ell,r),cs)$ denotes the conditional string rewriting rule $(\ell,r)\Leftarrow cs$ , where $c s$ is the list type for technical convenience. Based on Definition 34(ii), the statement that all critical pairs of $\mathcal{R}$ are joinable w.r.t. $\to_{\mathcal{R},r,j}$ is formalized as follows:

definition all_ccps_r_joinable where

" $all\_ccps\_r\_joinable\;R=\textup{(}\forall s\;t\;cs\;.\;\textup{(}\textup{(}s% ,t\textup{)},cs\textup{)}\in csts\_r\_critical\_pairs\;R\to$

$\quad\textup{(}\forall y\,.\,csts\_conds\_r\_sat\;R\;cs\;y\to\textup{(}s\,@\,y% ,t\,@\,y\textup{)}\in\textup{(}csr\_r\_join\_step\;R\textup{)}^{\downarrow}% \textup{)}\textup{)}$ "

where the definition of csts_conds_r_sat is formalized as follows:

definition csts_conds_r_sat where

" $csts\_conds\_r\_sat\;R\;cs\;y\longleftrightarrow\textup{(}\forall\textup{(}s_{% i},t_{i}\textup{)}\in set\;cs\;.\;\textup{(}s_{i}\,@\,y,t_{i}\,@\,y\textup{)}% \in\textup{(}csr\_r\_join\_step\;R\textup{)}^{\downarrow}\textup{)}$ "

Meanwhile, the set of critical pairs for a pure-join CSTS $\mathcal{R}$ is formalized as follows:

definition csts_p_critical_pairs where

" $csts\_p\_critical\_pairs\;R=\{\textup{(}\textup{(}v\,@\,y,x\,@\,v^{\prime}% \textup{)},cs^{\prime}\,@\,cs\textup{)}\,|\,x\,y\,u\,v\,u^{\prime}\,v^{\prime}% \,cs\,cs^{\prime}\;.\;\,\textup{(}\textup{(}u,v\textup{)},cs\textup{)}\in R\,\wedge$

$\quad\textup{(}\textup{(}u^{\prime},v^{\prime}\textup{)},cs^{\prime}\textup{)}% \in R\;\wedge\;u\,@\,y=x\,@\,u^{\prime}\;\wedge\;length\;x<length\;u\}\;\cup\;% \{\textup{(}\textup{(}v,x\,@\,v^{\prime}\,@\,y\textup{)},cs\,@\,cs^{\prime}\,|\,$

$\quad x\,y\,u\,v\,u^{\prime}\,v^{\prime}\,cs\,cs^{\prime}\;.\;\textup{(}% \textup{(}u,v\textup{)},cs\textup{)}\in R\wedge\textup{(}\textup{(}u^{\prime},% v^{\prime}\textup{)},cs^{\prime}\textup{)}\in R\wedge u=x\,@\,u^{\prime}\,@\,y\}$ "

Note that conditions are evaluated without using any context in the above formalization. The statement that all critical pairs of $\mathcal{R}$ are joinable w.r.t. $\to_{\mathcal{R},p,j}$ is formalized as follows:

definition all_ccps_p_joinable where

" $all\_ccps\_p\_joinable\;R=\textup{(}\forall s\;t\;cs\;.\;\textup{(}\textup{(}s% ,t\textup{)},cs\textup{)}\in csts\_p\_critical\_pairs\;R\to$

$\quad csts\_conds\_p\_sat\;R\;cs\to\textup{(}s,t\textup{)}\in csr\_p\_join\_% step\;R\textup{)}^{\downarrow}\textup{)}$ "

where the definition of csts_conds_p_sat is simply formalized as follows:

definition csts_conds_p_sat where

" $csts\_conds\_p\_sat\;R\;cs\longleftrightarrow\textup{(}\forall\textup{(}s_{i},% t_{i}\textup{)}\in set\;cs\;.\;\textup{(}s_{i},t_{i}\textup{)}\in\textup{(}csr% \_p\_join\_step\;R\textup{)}^{\downarrow}\textup{)}$ "

Lemma 35 (see [11]).

Let $\mathcal{R}$ be a finite reductive right-join CSTS. Then, $\to_{\mathcal{R},r,j}$ is confluent if and only if all critical pairs of $\mathcal{R}$ are joinable w.r.t. $\to_{\mathcal{R},r,j}$ .

Lemma 36.

Let $\mathcal{R}$ be a finite reductive pure-join CSTS. Then, $\to_{\mathcal{R},p,j}$ is confluent if and only if all critical pairs of $\mathcal{R}$ are joinable w.r.t. $\to_{\mathcal{R},p,j}$ .

Proof.

Since the “only if” direction is straightforward, we only show the “if” direction. Suppose that all critical pairs of $\mathcal{R}$ are joinable w.r.t. $\to_{\mathcal{R},p,j}$ . Since $\mathcal{R}$ is finite and reductive, $\to_{\mathcal{R},p,j}$ is terminating and decidable by Lemma 33(ii), so by Newman’s Lemma, it suffices to show that $\to_{\mathcal{R},p,j}$ is locally confluent. Let $s\to_{\mathcal{R},p,j}t$ and $s\to_{\mathcal{R},p,j}u$ , and let $(\ell,r)\Leftarrow\forall_{i=1}^{m}s_{i}\approx t_{i}$ and $(\ell^{\prime},r^{\prime})\Leftarrow\forall_{i=1}^{n}s_{i}^{\prime}\approx t_{% i}^{\prime}$ be two rules to reduce $s$ to $t$ and $u$ , respectively. We show that $t\downarrow_{\mathcal{R},p,j}u$ by considering the following three cases according to the positions of $\ell$ and $\ell^{\prime}$ in $s$ .

1.

$\ell$ and $\ell^{\prime}$ do not overlap, i.e., $s=x\ell y\ell^{\prime}z$ and $t=xry\ell^{\prime}z\mathrel{\prescript{}{\mathcal{R},p,j}{\mathrel{\leftarrow}% }}x\ell y\ell^{\prime}z\to_{\mathcal{R},p,j}x\ell yr^{\prime}z=u$ using the rules $(\ell,r)\Leftarrow\forall_{i=1}^{m}s_{i}\approx t_{i}$ and $(\ell^{\prime},r^{\prime})\Leftarrow\forall_{i=1}^{n}s_{i}^{\prime}\approx t_{% i}^{\prime}$ , where $x,y,z\in\Sigma^{*}$ . Since $\forall_{i=1}^{m}s_{i}\downarrow_{\mathcal{R},p,j}t_{i}$ and $\forall_{i=1}^{n}s^{\prime}_{i}\downarrow_{\mathcal{R},p,j}t^{\prime}_{i}$ , we have $t=xry\ell^{\prime}z\to_{\mathcal{R},p,j}xryr^{\prime}z\mathrel{\prescript{}{% \mathcal{R},p,j}{\mathrel{\leftarrow}}}x\ell yr^{\prime}z=u$ . Therefore, $t$ and $u$ are joinable w.r.t. $\to_{\mathcal{R},p,j}$ .
2.

$\ell^{\prime}$ is a substring of $\ell$ , i.e., $s=x\ell y=xu\ell^{\prime}vy$ and $t=xry\mathrel{\prescript{}{\mathcal{R},p,j}{\mathrel{\leftarrow}}}x\ell y=xu% \ell^{\prime}vy\to_{\mathcal{R},p,j}xur^{\prime}vy=u$ using the rules $(\ell,r)\Leftarrow\forall_{i=1}^{m}s_{i}\approx t_{i}$ and $(\ell^{\prime},r^{\prime})\Leftarrow\forall_{i=1}^{n}s_{i}^{\prime}\approx t_{% i}^{\prime}$ , where $x,y,u,v\in\Sigma^{*}$ . Since $\ell=u\ell^{\prime}v$ , we have a critical pair $(r,ur^{\prime}v)\Leftarrow\forall_{i=1}^{m}s_{i}\approx t_{i}\wedge\forall_{i=% 1}^{n}s_{i}^{\prime}\approx t_{i}^{\prime}$ . This critical pair is joinable w.r.t. $\to_{\mathcal{R},p,j}$ by hypothesis with $\forall_{i=1}^{m}s_{i}\downarrow_{\mathcal{R},p,j}t_{i}$ and $\forall_{i=1}^{n}s^{\prime}_{i}\downarrow_{\mathcal{R},p,j}t^{\prime}_{i}$ , so there is some $w$ such that $r\to_{\mathcal{R},p,j}^{*}w$ and $ur^{\prime}v\to_{\mathcal{R},p,j}^{*}w$ . Since $xry\to_{\mathcal{R},p,j}^{*}xwy$ and $xur^{\prime}vy\to_{\mathcal{R},p,j}^{*}xwy$ , we have $xry\downarrow_{\mathcal{R},p,j}xur^{\prime}vy$ , and thus $t$ and $u$ are joinable w.r.t. $\to_{\mathcal{R},p,j}$ .
3.

$\ell$ and $\ell^{\prime}$ have an overlap in such a way that $s=x\ell uy=xv\ell^{\prime}y$ and $t=xruy\mathrel{\prescript{}{\mathcal{R},p,j}{\mathrel{\leftarrow}}}x\ell uy=xv% \ell^{\prime}y\to_{\mathcal{R},p,j}xvr^{\prime}y=u$ using the rules $(\ell,r)\Leftarrow\forall_{i=1}^{m}s_{i}\approx t_{i}$ and $(\ell^{\prime},r^{\prime})\Leftarrow\forall_{i=1}^{n}s_{i}^{\prime}\approx t_{% i}^{\prime}$ , where $|v|<|\ell|$ and $x,y,u,v\in\Sigma^{*}$ . Since $\ell u=v\ell^{\prime}$ with $|v|<|\ell|$ , we have a critical pair $(ru,vr^{\prime})\Leftarrow\forall_{i=1}^{m}s_{i}\approx t_{i}\wedge\forall_{i=% 1}^{n}s_{i}^{\prime}\approx t_{i}^{\prime}$ . This critical pair is also joinable w.r.t. $\to_{\mathcal{R},p,j}$ by hypothesis with $\forall_{i=1}^{m}s_{i}\downarrow_{\mathcal{R},p,j}t_{i}$ and $\forall_{i=1}^{n}s^{\prime}_{i}\downarrow_{\mathcal{R},p,j}t^{\prime}_{i}$ , so there is some $w$ such that $ru\to_{\mathcal{R},p,j}^{*}w$ and $vr^{\prime}\to_{\mathcal{R},p,j}^{*}w$ . Since $xruy\to_{\mathcal{R},p,j}^{*}xwy$ and $xvr^{\prime}y\to_{\mathcal{R},p,j}^{*}xwy$ , we have $xruy\downarrow_{\mathcal{R},p,j}xvr^{\prime}y$ , and thus $t$ and $u$ are joinable w.r.t. $\to_{\mathcal{R},p,j}$ .

This shows that $t\downarrow_{\mathcal{R},p,j}u$ , and thus $\to_{\mathcal{R},p,j}$ is locally confluent. $\hfill\blacktriangleleft$

Lemmas 35 and 36 are simply formalized respectively as follows:

lemma csts_r_critical_pair_lemma: assumes " $reductive\;R$ "

" $CR\,\textup{(}csr\_r\_join\_step\;R\textup{)}\longleftrightarrow all\_ccps\_r% \_joinable\;R$ "

lemma csts_p_critical_pair_lemma: assumes " $reductive\;R$ "

" $CR\,\textup{(}csr\_p\_join\_step\;R\textup{)}\longleftrightarrow all\_ccps\_p% \_joinable\;R$ "

For reductive right-join (or pure-join) CSTSs, joinability of critical pairs suffices to show confluence by Lemma 35 (resp. Lemma 36). However, this is not the case for reductive left-right-join CSTSs. In particular, unlike reductive right-join or pure-join CSTSs, non-overlap may not be joinable for reductive left-right-join CSTSs as shown in the following example.

Example 37.

Consider the left-right-join CSTS $\mathcal{R}=\{b\to u\Leftarrow i\approx j,c\to v\Leftarrow l\approx m,aic\to ajc% ,bld\to bmd\}$ over $\Sigma=\{a,b,c,d,i,j,l,m,u,v\}$ . Using the shortlex ordering $\succ_{sl}$ induced by the precedence $a>b>c>d>i>j>l>m>u>v$ , we see that $\mathcal{R}$ is reductive. Now, consider a non-overlap $aucd\mathrel{\prescript{}{\mathcal{R},rl,j}{\mathrel{\leftarrow}}}abcd\to_{% \mathcal{R},rl,j}abvd$ . Here, the step $abcd\to_{\mathcal{R},rl,j}aucd$ uses the rules $b\to u\Leftarrow i\approx j$ and $aic\to ajc$ , and the step $abcd\to_{\mathcal{R},rl,j}abvd$ uses the rules $c\to v\Leftarrow l\approx m$ and $bld\to bmd$ . However, it is not the case that $aucd\downarrow_{\mathcal{R},rl,j}abvd$ .

Now, we discuss the monoids defined by certain congruence relations induced by the string rewriting relations $\to_{\mathcal{R},r,j}$ and $\to_{\mathcal{R},p,j}$ .

Definition 38.

Let $\mathcal{R}$ be a reductive right-join (resp. a pure-join) CSTS on $\Sigma^{*}$ . The Thue congruence induced by $\to_{\mathcal{R},r,j}$ (resp. $\to_{\mathcal{R},p,j}$ ) is the relation $\stackrel{{\scriptstyle*}}{{\leftrightarrow}}_{\mathcal{R},r,j}$ (resp. $\stackrel{{\scriptstyle*}}{{\leftrightarrow}}_{\mathcal{R},p,j}$ ). Two strings $u,v\in\Sigma^{*}$ are congruent w.r.t. $\to_{\mathcal{R},r,j}$ (resp. $\to_{\mathcal{R},p,j}$ ) if $u\stackrel{{\scriptstyle*}}{{\leftrightarrow}}_{\mathcal{R},r,j}v$ (resp. $u\stackrel{{\scriptstyle*}}{{\leftrightarrow}}_{\mathcal{R},p,j}v$ ). The congruence class $[w]_{\mathcal{R},r,j}$ (resp. $[w]_{\mathcal{R},p,j}$ ) of a word $w\in\Sigma^{*}$ is defined as $[w]_{\mathcal{R},r,j}:=\{v\in\Sigma^{*}\,|\,w\stackrel{{\scriptstyle*}}{{% \leftrightarrow}}_{\mathcal{R},r,j}v\}$ (resp. $[w]_{\mathcal{R},p,j}:=\{v\in\Sigma^{*}\,|\,w\stackrel{{\scriptstyle*}}{{% \leftrightarrow}}_{\mathcal{R},p,j}v\}$ ). The set $\{[w]_{\mathcal{R},r,j}\,|\,w\in\Sigma^{*}\}$ (resp. $\{[w]_{\mathcal{R},p,j}\,|\,w\in\Sigma^{*}\}$ ) of congruence classes w.r.t. $\to_{\mathcal{R},r,j}$ (resp. $\to_{\mathcal{R},p,j}$ ) is denoted by $\mathcal{M}_{\mathcal{R},r,j}$ (resp. $\mathcal{M}_{\mathcal{R},p,j}$ ).

$\blacktriangleright$ Remark 39.

In Definition 38, one can alternatively define $\mathcal{M}_{\mathcal{R},r,j}$ (resp. $\mathcal{M}_{\mathcal{R},p,j}$ ) only if $\to_{\mathcal{R},r,j}$ (resp. $\to_{\mathcal{R},p,j}$ ) is confluent so that $\stackrel{{\scriptstyle*}}{{\leftrightarrow}}_{\mathcal{R},r,j}$ ( $\stackrel{{\scriptstyle*}}{{\leftrightarrow}}_{\mathcal{R},p,j}$ ) is the same as the right (resp. pure) conditional equational theory induced by $\mathcal{R}$ (see Lemmas 27 and 28). In this case, $\mathcal{M}_{\mathcal{R},r,j}$ (resp. $\mathcal{M}_{\mathcal{R},p,j}$ ) can be directly associated with the right (resp. pure) conditional equational theory induced by $\mathcal{R}$ . We use the simpler definition of $\mathcal{M}_{\mathcal{R},r,j}$ (resp. $\mathcal{M}_{\mathcal{R},p,j}$ ) as in Definition 38 instead of adding the restriction that $\to_{\mathcal{R},r,j}$ (resp. $\to_{\mathcal{R},p,j}$ ) is confluent (cf. Theorem 42).

Lemma 40.

(i)

The set $\mathcal{M}_{\mathcal{R},r,j}$ is a monoid under the operation $[u]_{\mathcal{R},r,j}\cdot[v]_{\mathcal{R},r,j}:=[uv]_{\mathcal{R},r,j}$ with the identity element $[\varepsilon]_{\mathcal{R},r,j}$ .
(ii)

The set $\mathcal{M}_{\mathcal{R},p,j}$ is a monoid under the operation $[u]_{\mathcal{R},p,j}\cdot[v]_{\mathcal{R},p,j}:=[uv]_{\mathcal{R},p,j}$ with the identity element $[\varepsilon]_{\mathcal{R},p,j}$ .

Definition 41.

Let $\mathcal{R}$ be a reductive right-join (resp. a pure-join) CSTS over $\Sigma$ . The ordered pair ( $\Sigma;\mathcal{R}$ ) is a (reductive) conditional presentation of the monoid $\mathcal{M}_{\mathcal{R},r,j}$ (resp. $\mathcal{M}_{\mathcal{R},p,j}$ ). The monoid $\mathcal{M}_{\mathcal{R},r,j}$ (resp. $\mathcal{M}_{\mathcal{R},p,j}$ ) is finitely presented if both $\Sigma$ and $\mathcal{R}$ are finite in ( $\Sigma;\mathcal{R}$ ). The ordered pair ( $\Sigma;\mathcal{R}$ ) is a complete (reductive) conditional presentation of the monoid $\mathcal{M}_{\mathcal{R},r,j}$ (resp. $\mathcal{M}_{\mathcal{R},p,j}$ ) if $\to_{\mathcal{R},r,j}$ (resp. $\to_{\mathcal{R},p,j}$ ) is complete.

The following theorem and its proof provide a decision procedure for the word problem of monoids with finite complete (reductive) conditional presentations.

Theorem 42.

(i)

Let $\mathcal{R}$ be a finite reductive right-join CSTS on $\Sigma^{*}$ . If $\to_{\mathcal{R},r,j}$ is confluent, then we can decide whether $s$ and $t$ on $\Sigma^{*}$ are the same element in the monoid $\mathcal{M}_{\mathcal{R},r,j}:=\Sigma^{*}/\stackrel{{\scriptstyle*}}{{% \leftrightarrow}}_{\mathcal{R},r,j}$ .
(ii)

Let $\mathcal{R}$ be a finite reductive pure-join CSTS on $\Sigma^{*}$ . If $\to_{\mathcal{R},p,j}$ is confluent, then we can decide whether $s$ and $t$ on $\Sigma^{*}$ are the same element in the monoid $\mathcal{M}_{\mathcal{R},p,j}:=\Sigma^{*}/\stackrel{{\scriptstyle*}}{{% \leftrightarrow}}_{\mathcal{R},p,j}$ .

Proof.

For the proof of (i), if $s\stackrel{{\scriptstyle*}}{{\leftrightarrow}}_{\mathcal{R},r,j}t$ , then $s$ and $t$ are the same element in $\mathcal{M}_{\mathcal{R},r,j}$ . Otherwise, $s$ and $t$ are the different elements in $\mathcal{M}_{\mathcal{R},r,j}$ . Since $\mathcal{R}$ is finite and reductive, $\to_{\mathcal{R},r,j}$ is terminating and decidable. Furthermore, $\to_{\mathcal{R},r,j}$ is confluent by hypothesis, so we can decide whether $s\stackrel{{\scriptstyle*}}{{\leftrightarrow}}_{\mathcal{R},r,j}t$ by comparing the normal forms of $s$ and $t$ w.r.t. $\rightarrow_{\mathcal{R},r,j}$ . In other words, if the normal forms of $s$ and $t$ w.r.t. $\rightarrow_{\mathcal{R},r,j}$ are the same, then they are the same element in $\mathcal{M}_{\mathcal{R},r,j}$ , and they are the different elements in $\mathcal{M}_{\mathcal{R},r,j}$ , otherwise. We omit the proof of (ii) because it is similar to the proof of (i). $\hfill\blacktriangleleft$

Our formalization of Theorem 42 is an extension of the formalization of Theorem 10 discussed in Section 3 in conditional setting, where the locale monoid is instantiated using the different parameters for $\mathcal{M}_{\mathcal{R},r,j}$ and $\mathcal{M}_{\mathcal{R},p,j}$ , respectively:

$monoid\;$ " $S^{\star}/Thue\_R\_Congruence$ " " $\textup{(}[\cdot]_{r}\textup{)}$ " " $equiv\_r.Class\;\varepsilon$ "

$monoid\;$ " $S^{\star}/Thue\_P\_Congruence$ " " $\textup{(}[\cdot]_{p}\textup{)}$ " " $equiv\_p.Class\;\varepsilon$ "

Above, $Thue\_R\_Congruence$ and $Thue\_P\_Congruence$ are (csr_r_join_step $\;R)^{\leftrightarrow^{*}}$ and (csr_p_join_step $\;R)^{\leftrightarrow^{*}}$ , respectively. They correspond to the Thue congruence relations induced by $\rightarrow_{\mathcal{R},r,j}$ and $\rightarrow_{\mathcal{R},p,j}$ , respectively. Also, $[\cdot]_{r}$ (resp. $[\cdot]_{p}$ ) represents an associative binary operator for the monoid $\mathcal{M}_{\mathcal{R},r,j}$ (resp. $\mathcal{M}_{\mathcal{R},p,j}$ ) in such a way that $[u]_{\mathcal{R},r,j}\,[\cdot]_{r}\,[v]_{\mathcal{R},r,j}=[uv]_{\mathcal{R},r,j}$ (resp. $[u]_{\mathcal{R},p,j}\,[\cdot]_{p}\,[v]_{\mathcal{R},p,j}=[uv]_{\mathcal{R},p,j}$ ) for all $u,v\in\Sigma^{*}$ , where $\Sigma$ is represented by $S$ in the above. Finally, $equiv\_r.Class$ $\;\varepsilon$ (resp. $equiv\_p.Class\;\varepsilon$ ) represents the congruence class $[\varepsilon]_{\mathcal{R},r,j}$ (resp. $[\varepsilon]_{\mathcal{R},p,j}$ ) corresponding to the identity element in $\mathcal{M}_{\mathcal{R},r,j}$ (resp. $\mathcal{M}_{\mathcal{R},p,j}$ ).

5 Conclusion

Semi-Thue and certain types of conditional semi-Thue systems can be viewed as presentations of monoids because they define a quotient of the free monoid modulo the Thue congruence that they induce. We have presented an Isabelle/HOL formalization of semi-Thue and conditional semi-Thue systems along with a decision procedure for the word problem of monoids with finite complete unconditional or reductive conditional presentations. Also, our formalized framework for semi-Thue and Thue systems can provide formalized building blocks for different kinds applications because there is a wide variety of applications of semi-Thue and Thue systems, such as formal language theory [7, 38], group theory [10, 33, 19, 40], and algebraic protocols [7, 6].

The main contributions of this paper are as follows: (i) We have presented the first (computer-aided) formalization of conditional semi-Thue systems (using a proof assistant). In particular, we have provided a new formalized method for checking confluence using (conditional) critical pairs for finite reductive right-join and pure-join conditional semi-Thue systems. (ii) The existing classification of conditional semi-Thue systems basically consists only of left-right-join and right-join conditional semi-Thue systems (see [11]). We have extended this classification depending on how conditions are evaluated in the conditional parts of their rules, and provided a formalized framework for the different types of conditional semi-Thue systems. (For the classification of conditional term rewriting systems, see [46].) Furthermore, we have proposed and formalized a new inference system for generating different conditional equational theories and Thue congruences for the associated monoids along with their word problem. (iii) We have presented and formalized an inference system for a completion procedure of semi-Thue systems, which is adapted from the existing Knuth-completion procedure [24, 7] of semi-Thue systems and an abstract completion procedure [18, 2] of term rewriting systems. When attempting to construct a finite complete presentation of a monoid or a group, our inference-system based completion procedure is straightforward and easy to use (in comparison to algorithm-based completion procedures [24, 7]) by means of simple string matching. We have also provided the formalized proof of its correctness.

Yet, much work still remains ahead. Unlike semi-Thue systems, conditional semi-Thue systems have not been well researched. For example, effective/operation termination [32, 37], confluence, and the reachability analysis [16] of the different types of conditional semi-Thue systems along with their formalization are possible future research directions. Another possible future research direction is to classify and formalize the different types of conditional string rewriting in terms of the expressive power [34] of string rewriting.

References

[1] Franz Baader and Tobias Nipkow. Term Rewriting and All That. Cambridge University Press, Cambridge, UK, 1998. doi:10.1017/CBO9781139172752.
[2] Leo Bachmair, Nachum Dershowitz, and Jieh Hsiang. Orderings for Equational Proofs. In Proceedings of the Symposium on Logic in Computer Science (LICS ’86), Cambridge, Massachusetts, USA, June 16-18, 1986, pages 346–357. IEEE Computer Society, 1986.
[3] Clemens Ballarin. Tutorial to Locales and Locale Interpretation, 2010. URL: http://isabelle.in.tum.de/doc/locales.pdf.
[4] Clemens Ballarin. A Case Study in Basic Algebra. Arch. Formal Proofs, 2019. URL: https://www.isa-afp.org/entries/Jacobson_Basic_Algebra.html.
[5] Jan A. Bergstra and Jan Willem Klop. Conditional Rewrite Rules: Confluence and Termination. J. Comput. Syst. Sci., 32(3):323–362, 1986. doi:10.1016/0022-0000(86)90033-4.
[6] Ronald V. Book and Friedrich Otto. On the Verifiability of Two-Party Algebraic Protocols. Theor. Comput. Sci., 40:101–130, 1985. doi:10.1016/0304-3975(85)90161-6.
[7] Ronald V. Book and Friedrich Otto. String-Rewriting Systems. Springer, New York, NY, 1993. doi:10.1007/978-1-4613-9771-7.
[8] Thomas Braibant and Damien Pous. Tactics for Reasoning Modulo AC in Coq. In Jean-Pierre Jouannaud and Zhong Shao, editors, Certified Programs and Proofs - First International Conference, CPP 2011, Kenting, Taiwan, December 7-9, 2011. Proceedings, volume 7086 of Lecture Notes in Computer Science, pages 167–182. Springer, 2011. doi:10.1007/978-3-642-25379-9_14.
[9] Jacek Chrzaszcz and Daria Walukiewicz-Chrzaszcz. Towards Rewriting in Coq. In Hubert Comon-Lundh, Claude Kirchner, and Hélène Kirchner, editors, Rewriting, Computation and Proof, Essays Dedicated to Jean-Pierre Jouannaud on the Occasion of His 60th Birthday, volume 4600 of Lecture Notes in Computer Science, pages 113–131. Springer, 2007. doi:10.1007/978-3-540-73147-4_6.
[10] Daniel E. Cohen. String Rewriting – A Survey for Group Theorists. In Graham A. Niblo and Martin A. Roller, editors, Geometric Group Theory, London Mathematical Society Lecture Note Series, pages 37–47. Cambridge University Press, 1993.
[11] Thomas Deiß. Conditional Semi-Thue systems for Presenting Monoids. Technical report, Universität Kaiserslautern, 1992. SEKI Report SR-92-12 available at https://agent.informatik.uni-kl.de/seki/1992/Deiss.SR-92-12.english.ps.Z. A shorter version of the paper was presented at Annual Symposium on Theoretical Aspects of Computer Science in 1992 (STACS 92) with the same title.
[12] Nachum Dershowitz, Mitsuhiro Okada, and G. Sivakumar. Confluence of Conditional Rewrite Systems. In Stéphane Kaplan and Jean-Pierre Jouannaud, editors, Conditional Term Rewriting Systems, 1st International Workshop, Orsay, France, July 8-10, 1987, Proceedings, volume 308 of LNCS, pages 31–44. Springer, 1987. doi:10.1007/3-540-19242-5_3.
[13] Nachum Dershowitz and David A. Plaisted. Rewriting. In John Alan Robinson and Andrei Voronkov, editors, Handbook of Automated Reasoning (in 2 volumes), pages 535–610. Elsevier and MIT Press, 2001. doi:10.1016/B978-044450813-3/50011-4.
[14] Patrick Baxter Dragon, Oscar I. Hernandez, Joe Sawada, Aaron Williams, and Dennis Wong. Constructing de Bruijn sequences with co-lexicographic order: The k-ary Grandmama sequence. Eur. J. Comb., 72:1–11, 2018. doi:10.1016/J.EJC.2018.03.006.
[15] Hannah Fechtner. Braids in Lean. Master’s thesis, Carnegie Mellon University, PA, USA, 2024.
[16] Guillaume Feuillade, Thomas Genet, and Valérie Viet Triem Tong. Reachability Analysis over Term Rewriting Systems. J. Autom. Reason., 33(3-4):341–383, 2004. doi:10.1007/S10817-004-6246-0.
[17] Yannick Forster, Dominique Larchey-Wendling, Andrej Dudenhefner, Edith Heiter, Dominik Kirst, Fabian Kunze, Gert Smolka, Simon Spies, Dominik Wehr, and Maximilian Wuttke. A Coq Library of Undecidable Problems. In CoqPL 2020 The Sixth International Workshop on Coq for Programming Languages, New Orleans, USA, 2020. URL: https://hal.science/hal-02944217.
[18] Nao Hirokawa, Aart Middeldorp, Christian Sternagel, and Sarah Winkler. Abstract Completion, Formalized. Log. Methods Comput. Sci., 15(3), 2019. doi:10.23638/LMCS-15(3:19)2019.
[19] D. F. Holt, B. Eick, and E. A. O’Brien. Handbook of computational group theory. CRC Press, Boca Raton, FL, 2005.
[20] Jieh Hsiang, Hélène Kirchner, Pierre Lescanne, and Michaël Rusinowitch. The Term Rewriting Approach to Automated Theorem Proving. J. Log. Program., 14(1&2):71–99, 1992. doi:10.1016/0743-1066(92)90047-7.
[21] Nathan Jacobson. Basic algebra I. Dover Publications, Inc., Mineola, NY, 2nd edition, 2009.
[22] Sam Kamin and Jean-Jacques Levy. Two generalizations of the recursive path ordering. Technical report, Dept. of Computer Science, Univ. of Illinois at Urbana-Champaign, 1980.
[23] Stéphane Kaplan. Conditional Rewrite Rules. Theor. Comput. Sci., 33:175–193, 1984. doi:10.1016/0304-3975(84)90087-2.
[24] Deepak Kapur and Paliath Narendran. The Knuth-Bendix Completion Procedure and Thue Systems. SIAM J. Comput., 14(4):1052–1072, 1985. doi:10.1137/0214073.
[25] Deepak Kapur and G. Sivakumar. RRL: theorem proving environment based on rewriting techniques. SIGSOFT Softw. Eng. Notes, 10(4):67–68, 1985. doi:10.1145/1012497.1012522.
[26] Yutaka Kikuchi and Takuya Katayama. An Application of Term Rewriting Systems for Functional Programming. In Yutaka Ohno and Toshiko Matsuda, editors, Distributed Environments: Software Paradigms and Workstations, pages 79–106. Springer Japan, 1991. doi:10.1007/978-4-431-68144-1_7.
[27] Dohan Kim. Equational theorem proving for clauses over strings. Mathematical Structures in Computer Science, 34(10):1055–1078, 2024. doi:10.1017/S0960129524000112.
[28] Dohan Kim. Congruence Closure Modulo Groups. Logical Methods in Computer Science, Volume 21, Issue 1, 2025. doi:10.46298/lmcs-21(1:20)2025.
[29] D. E. Knuth and P. B. Bendix. Simple Word Problems in Universal Algebras. In Jörg H. Siekmann and Graham Wrightson, editors, Automation of Reasoning: 2: Classical Papers on Computational Logic 1967–1970, pages 342–376. Springer Berlin Heidelberg, 1983. doi:10.1007/978-3-642-81955-1.
[30] Donald E. Knuth, James H. Morris Jr., and Vaughan R. Pratt. Fast Pattern Matching in Strings. SIAM J. Comput., 6(2):323–350, 1977. doi:10.1137/0206024.
[31] Pierre Lescanne. Computer experiments with the REVE term rewriting system generator. In Proceedings of the 10th ACM SIGACT-SIGPLAN Symposium on Principles of Programming Languages, POPL ’83, pages 99–108, 1983. doi:10.1145/567067.567078.
[32] Salvador Lucas, Claude Marché, and José Meseguer. Operational termination of conditional term rewriting systems. Inf. Process. Lett., 95(4):446–453, 2005. doi:10.1016/J.IPL.2005.05.002.
[33] Klaus Madlener and Friedrich Otto. Using String-Rewriting for Solving the Word Problem for Finitely Presented Groups. Inf. Process. Lett., 24(5):281–284, 1987. doi:10.1016/0020-0190(87)90149-9.
[34] Massimo Marchiori. On the Expressive Power of Rewriting. In S. Ramesh and G. Sivakumar, editors, Foundations of Software Technology and Theoretical Computer Science, 17th Conference, Kharagpur, India, December 18-20, 1997, Proceedings, volume 1346 of Lecture Notes in Computer Science, pages 88–102. Springer, 1997. doi:10.1007/BFB0058025.
[35] M. H. A. Newman. On Theories with a Combinatorial Definition of “Equivalence”. Annals of Mathematics, 43(2):223–243, 1942. doi:10.2307/1968867.
[36] Tobias Nipkow, Lawrence C. Paulson, and Markus Wenzel. Isabelle/HOL - A Proof Assistant for Higher-Order Logic, volume 2283 of Lecture Notes in Computer Science. Springer, 2002. doi:10.1007/3-540-45949-9.
[37] Enno Ohlebusch. Advanced topics in term rewriting. Springer Science & Business Media, Berlin/Heidelberg, Germany, 2002.
[38] Friedrich Otto. On the Connections between Rewriting and Formal Language Theory. In Paliath Narendran and Michaël Rusinowitch, editors, Rewriting Techniques and Applications, 10th International Conference, RTA-99, Trento, Italy, July 2-4, 1999, Proceedings, volume 1631 of LNCS, pages 332–355. Springer, 1999. doi:10.1007/3-540-48685-2_27.
[39] James F Power. Thue’s 1914 paper: a translation. arXiv preprint arXiv:1308.5858, 2013. doi:10.48550/arXiv.1308.5858.
[40] C. C. Sims. Computation with finitely presented groups. Cambridge University Press, New York, NY, 1994.
[41] Christian Sternagel and Thomas Sternagel. Certifying Confluence of Quasi-Decreasing Strongly Deterministic Conditional Term Rewrite Systems. In Leonardo de Moura, editor, Automated Deduction - CADE 26 - 26th International Conference on Automated Deduction, Gothenburg, Sweden, August 6-11, 2017, Proceedings, volume 10395 of Lecture Notes in Computer Science, pages 413–431. Springer, 2017. doi:10.1007/978-3-319-63046-5_26.
[42] Christian Sternagel and René Thiemann. Abstract Rewriting. Arch. Formal Proofs, 2010, 2010. URL: https://www.isa-afp.org/entries/Abstract-Rewriting.shtml.
[43] Terese. Term Rewriting Systems, volume 55 of Cambridge Tracts in Theoretical Computer Science. Cambridge University Press, 2003.
[44] René Thiemann and Christian Sternagel. Certification of Termination Proofs Using CeTA. In Stefan Berghofer, Tobias Nipkow, Christian Urban, and Makarius Wenzel, editors, Theorem Proving in Higher Order Logics, 22nd International Conference, TPHOLs 2009, Munich, Germany, August 17-20, 2009. Proceedings, volume 5674 of Lecture Notes in Computer Science, pages 452–468. Springer, 2009. doi:10.1007/978-3-642-03359-9_31.
[45] Akihisa Yamada, Keiichirou Kusakari, and Toshiki Sakabe. A unified ordering for termination proving. Sci. Comput. Program., 111:110–134, 2015. doi:10.1016/J.SCICO.2014.07.009.
[46] Toshiyuki Yamada, Jürgen Avenhaus, Carlos Loría-Sáenz, and Aart Middeldorp. Logicality of conditional rewrite systems. Theor. Comput. Sci., 236(1-2):209–232, 2000. doi:10.1016/S0304-3975(99)00210-8.

[bib.bib1] [1] Franz Baader and Tobias Nipkow. Term Rewriting and All That. Cambridge University Press, Cambridge, UK, 1998. doi:10.1017/CBO9781139172752.

[bib.bib2] [2] Leo Bachmair, Nachum Dershowitz, and Jieh Hsiang. Orderings for Equational Proofs. In Proceedings of the Symposium on Logic in Computer Science (LICS ’86), Cambridge, Massachusetts, USA, June 16-18, 1986, pages 346–357. IEEE Computer Society, 1986.

[bib.bib3] [3] Clemens Ballarin. Tutorial to Locales and Locale Interpretation, 2010. URL: http://isabelle.in.tum.de/doc/locales.pdf.

[bib.bib4] [4] Clemens Ballarin. A Case Study in Basic Algebra. Arch. Formal Proofs, 2019. URL: https://www.isa-afp.org/entries/Jacobson_Basic_Algebra.html.

[bib.bib5] [5] Jan A. Bergstra and Jan Willem Klop. Conditional Rewrite Rules: Confluence and Termination. J. Comput. Syst. Sci., 32(3):323–362, 1986. doi:10.1016/0022-0000(86)90033-4.

[bib.bib6] [6] Ronald V. Book and Friedrich Otto. On the Verifiability of Two-Party Algebraic Protocols. Theor. Comput. Sci., 40:101–130, 1985. doi:10.1016/0304-3975(85)90161-6.

[bib.bib7] [7] Ronald V. Book and Friedrich Otto. String-Rewriting Systems. Springer, New York, NY, 1993. doi:10.1007/978-1-4613-9771-7.

[bib.bib8] [8] Thomas Braibant and Damien Pous. Tactics for Reasoning Modulo AC in Coq. In Jean-Pierre Jouannaud and Zhong Shao, editors, Certified Programs and Proofs - First International Conference, CPP 2011, Kenting, Taiwan, December 7-9, 2011. Proceedings, volume 7086 of Lecture Notes in Computer Science, pages 167–182. Springer, 2011. doi:10.1007/978-3-642-25379-9_14.

[bib.bib9] [9] Jacek Chrzaszcz and Daria Walukiewicz-Chrzaszcz. Towards Rewriting in Coq. In Hubert Comon-Lundh, Claude Kirchner, and Hélène Kirchner, editors, Rewriting, Computation and Proof, Essays Dedicated to Jean-Pierre Jouannaud on the Occasion of His 60th Birthday, volume 4600 of Lecture Notes in Computer Science, pages 113–131. Springer, 2007. doi:10.1007/978-3-540-73147-4_6.

[bib.bib10] [10] Daniel E. Cohen. String Rewriting – A Survey for Group Theorists. In Graham A. Niblo and Martin A. Roller, editors, Geometric Group Theory, London Mathematical Society Lecture Note Series, pages 37–47. Cambridge University Press, 1993.

[bib.bib11] [11] Thomas Deiß. Conditional Semi-Thue systems for Presenting Monoids. Technical report, Universität Kaiserslautern, 1992. SEKI Report SR-92-12 available at https://agent.informatik.uni-kl.de/seki/1992/Deiss.SR-92-12.english.ps.Z. A shorter version of the paper was presented at Annual Symposium on Theoretical Aspects of Computer Science in 1992 (STACS 92) with the same title.

[bib.bib12] [12] Nachum Dershowitz, Mitsuhiro Okada, and G. Sivakumar. Confluence of Conditional Rewrite Systems. In Stéphane Kaplan and Jean-Pierre Jouannaud, editors, Conditional Term Rewriting Systems, 1st International Workshop, Orsay, France, July 8-10, 1987, Proceedings, volume 308 of LNCS, pages 31–44. Springer, 1987. doi:10.1007/3-540-19242-5_3.

[bib.bib13] [13] Nachum Dershowitz and David A. Plaisted. Rewriting. In John Alan Robinson and Andrei Voronkov, editors, Handbook of Automated Reasoning (in 2 volumes), pages 535–610. Elsevier and MIT Press, 2001. doi:10.1016/B978-044450813-3/50011-4.

[bib.bib14] [14] Patrick Baxter Dragon, Oscar I. Hernandez, Joe Sawada, Aaron Williams, and Dennis Wong. Constructing de Bruijn sequences with co-lexicographic order: The k-ary Grandmama sequence. Eur. J. Comb., 72:1–11, 2018. doi:10.1016/J.EJC.2018.03.006.

[bib.bib15] [15] Hannah Fechtner. Braids in Lean. Master’s thesis, Carnegie Mellon University, PA, USA, 2024.

[bib.bib16] [16] Guillaume Feuillade, Thomas Genet, and Valérie Viet Triem Tong. Reachability Analysis over Term Rewriting Systems. J. Autom. Reason., 33(3-4):341–383, 2004. doi:10.1007/S10817-004-6246-0.

[bib.bib17] [17] Yannick Forster, Dominique Larchey-Wendling, Andrej Dudenhefner, Edith Heiter, Dominik Kirst, Fabian Kunze, Gert Smolka, Simon Spies, Dominik Wehr, and Maximilian Wuttke. A Coq Library of Undecidable Problems. In CoqPL 2020 The Sixth International Workshop on Coq for Programming Languages, New Orleans, USA, 2020. URL: https://hal.science/hal-02944217.

[bib.bib18] [18] Nao Hirokawa, Aart Middeldorp, Christian Sternagel, and Sarah Winkler. Abstract Completion, Formalized. Log. Methods Comput. Sci., 15(3), 2019. doi:10.23638/LMCS-15(3:19)2019.

[bib.bib19] [19] D. F. Holt, B. Eick, and E. A. O’Brien. Handbook of computational group theory. CRC Press, Boca Raton, FL, 2005.

[bib.bib20] [20] Jieh Hsiang, Hélène Kirchner, Pierre Lescanne, and Michaël Rusinowitch. The Term Rewriting Approach to Automated Theorem Proving. J. Log. Program., 14(1&2):71–99, 1992. doi:10.1016/0743-1066(92)90047-7.

[bib.bib21] [21] Nathan Jacobson. Basic algebra I. Dover Publications, Inc., Mineola, NY, 2nd edition, 2009.

[bib.bib22] [22] Sam Kamin and Jean-Jacques Levy. Two generalizations of the recursive path ordering. Technical report, Dept. of Computer Science, Univ. of Illinois at Urbana-Champaign, 1980.

[bib.bib23] [23] Stéphane Kaplan. Conditional Rewrite Rules. Theor. Comput. Sci., 33:175–193, 1984. doi:10.1016/0304-3975(84)90087-2.

[bib.bib24] [24] Deepak Kapur and Paliath Narendran. The Knuth-Bendix Completion Procedure and Thue Systems. SIAM J. Comput., 14(4):1052–1072, 1985. doi:10.1137/0214073.

[bib.bib25] [25] Deepak Kapur and G. Sivakumar. RRL: theorem proving environment based on rewriting techniques. SIGSOFT Softw. Eng. Notes, 10(4):67–68, 1985. doi:10.1145/1012497.1012522.

[bib.bib26] [26] Yutaka Kikuchi and Takuya Katayama. An Application of Term Rewriting Systems for Functional Programming. In Yutaka Ohno and Toshiko Matsuda, editors, Distributed Environments: Software Paradigms and Workstations, pages 79–106. Springer Japan, 1991. doi:10.1007/978-4-431-68144-1_7.

[bib.bib27] [27] Dohan Kim. Equational theorem proving for clauses over strings. Mathematical Structures in Computer Science, 34(10):1055–1078, 2024. doi:10.1017/S0960129524000112.

[bib.bib28] [28] Dohan Kim. Congruence Closure Modulo Groups. Logical Methods in Computer Science, Volume 21, Issue 1, 2025. doi:10.46298/lmcs-21(1:20)2025.

[bib.bib29] [29] D. E. Knuth and P. B. Bendix. Simple Word Problems in Universal Algebras. In Jörg H. Siekmann and Graham Wrightson, editors, Automation of Reasoning: 2: Classical Papers on Computational Logic 1967–1970, pages 342–376. Springer Berlin Heidelberg, 1983. doi:10.1007/978-3-642-81955-1.

[bib.bib30] [30] Donald E. Knuth, James H. Morris Jr., and Vaughan R. Pratt. Fast Pattern Matching in Strings. SIAM J. Comput., 6(2):323–350, 1977. doi:10.1137/0206024.

[bib.bib31] [31] Pierre Lescanne. Computer experiments with the REVE term rewriting system generator. In Proceedings of the 10th ACM SIGACT-SIGPLAN Symposium on Principles of Programming Languages, POPL ’83, pages 99–108, 1983. doi:10.1145/567067.567078.

[bib.bib32] [32] Salvador Lucas, Claude Marché, and José Meseguer. Operational termination of conditional term rewriting systems. Inf. Process. Lett., 95(4):446–453, 2005. doi:10.1016/J.IPL.2005.05.002.

[bib.bib33] [33] Klaus Madlener and Friedrich Otto. Using String-Rewriting for Solving the Word Problem for Finitely Presented Groups. Inf. Process. Lett., 24(5):281–284, 1987. doi:10.1016/0020-0190(87)90149-9.

[bib.bib34] [34] Massimo Marchiori. On the Expressive Power of Rewriting. In S. Ramesh and G. Sivakumar, editors, Foundations of Software Technology and Theoretical Computer Science, 17th Conference, Kharagpur, India, December 18-20, 1997, Proceedings, volume 1346 of Lecture Notes in Computer Science, pages 88–102. Springer, 1997. doi:10.1007/BFB0058025.

[bib.bib35] [35] M. H. A. Newman. On Theories with a Combinatorial Definition of “Equivalence”. Annals of Mathematics, 43(2):223–243, 1942. doi:10.2307/1968867.

[bib.bib36] [36] Tobias Nipkow, Lawrence C. Paulson, and Markus Wenzel. Isabelle/HOL - A Proof Assistant for Higher-Order Logic, volume 2283 of Lecture Notes in Computer Science. Springer, 2002. doi:10.1007/3-540-45949-9.

[bib.bib37] [37] Enno Ohlebusch. Advanced topics in term rewriting. Springer Science & Business Media, Berlin/Heidelberg, Germany, 2002.

[bib.bib38] [38] Friedrich Otto. On the Connections between Rewriting and Formal Language Theory. In Paliath Narendran and Michaël Rusinowitch, editors, Rewriting Techniques and Applications, 10th International Conference, RTA-99, Trento, Italy, July 2-4, 1999, Proceedings, volume 1631 of LNCS, pages 332–355. Springer, 1999. doi:10.1007/3-540-48685-2_27.

[bib.bib39] [39] James F Power. Thue’s 1914 paper: a translation. arXiv preprint arXiv:1308.5858, 2013. doi:10.48550/arXiv.1308.5858.

[bib.bib40] [40] C. C. Sims. Computation with finitely presented groups. Cambridge University Press, New York, NY, 1994.

[bib.bib41] [41] Christian Sternagel and Thomas Sternagel. Certifying Confluence of Quasi-Decreasing Strongly Deterministic Conditional Term Rewrite Systems. In Leonardo de Moura, editor, Automated Deduction - CADE 26 - 26th International Conference on Automated Deduction, Gothenburg, Sweden, August 6-11, 2017, Proceedings, volume 10395 of Lecture Notes in Computer Science, pages 413–431. Springer, 2017. doi:10.1007/978-3-319-63046-5_26.

[bib.bib42] [42] Christian Sternagel and René Thiemann. Abstract Rewriting. Arch. Formal Proofs, 2010, 2010. URL: https://www.isa-afp.org/entries/Abstract-Rewriting.shtml.

[bib.bib43] [43] Terese. Term Rewriting Systems, volume 55 of Cambridge Tracts in Theoretical Computer Science. Cambridge University Press, 2003.

[bib.bib44] [44] René Thiemann and Christian Sternagel. Certification of Termination Proofs Using CeTA. In Stefan Berghofer, Tobias Nipkow, Christian Urban, and Makarius Wenzel, editors, Theorem Proving in Higher Order Logics, 22nd International Conference, TPHOLs 2009, Munich, Germany, August 17-20, 2009. Proceedings, volume 5674 of Lecture Notes in Computer Science, pages 452–468. Springer, 2009. doi:10.1007/978-3-642-03359-9_31.

[bib.bib45] [45] Akihisa Yamada, Keiichirou Kusakari, and Toshiki Sakabe. A unified ordering for termination proving. Sci. Comput. Program., 111:110–134, 2015. doi:10.1016/J.SCICO.2014.07.009.

[bib.bib46] [46] Toshiyuki Yamada, Jürgen Avenhaus, Carlos Loría-Sáenz, and Aart Middeldorp. Logicality of conditional rewrite systems. Theor. Comput. Sci., 236(1-2):209–232, 2000. doi:10.1016/S0304-3975(99)00210-8.

An Isabelle/HOL Formalization of Semi-Thue and Conditional Semi-Thue Systems

Abstract

Keywords and phrases:

Copyright and License:

2012 ACM Subject Classification:

Supplementary Material:

Acknowledgements:

Funding:

DOI:

Event:

Editors:

Series and Publisher:

1 Introduction

2 Preliminaries

3 Semi-Thue Systems

Lemma 1.

Definition 2.

Lemma 3.

Lemma 4.

Lemma 5.

Definition 6.

Lemma 7.

Lemma 8.

Theorem 9.

Theorem 10.

Proof.

▶ Remark 11.

Definition 12.

Definition 13.

Lemma 14.

Definition 15 (cf. [18]).

Lemma 16.

Definition 17.

Lemma 18.

Theorem 19 (cf. [18]).

Sketch of the proof.

▶ Remark 20.

4 Conditional Semi-Thue Systems

Definition 21.

Definition 22.

Definition 23.

Definition 24.

Definition 25.

Definition 26.

Lemma 27.

Lemma 28.

▶ Remark 29.

Example 30.

Definition 31.

Example 32 (see [11]).

Lemma 33.

Definition 34.

Lemma 35 (see [11]).

Lemma 36.

Proof.

Example 37.

Definition 38.

▶ Remark 39.

Lemma 40.

Definition 41.

Theorem 42.

Proof.

5 Conclusion

References

$\blacktriangleright$ Remark 11.

$\blacktriangleright$ Remark 20.

$\blacktriangleright$ Remark 29.

$\blacktriangleright$ Remark 39.