<p>I would like to use <a href="https://en.wikipedia.org/wiki/Semi-Thue_system" rel="nofollow noreferrer">semi-Thue systems</a> (a.k.a. string rewriting systems) to study complexity theory formally. Note that &quot;semi-&quot; in the name means &quot;unidirectional [Thue system]&quot;.</p>
<p>Unlike in grammars (where I always worked with a fixed starting symbol), I don't want to start with a fixed starting symbol or (as written in older books) a set of &quot;axioms&quot;. Instead, I want a semi-Thue system to operate on an input word; I want to define (semi)deciders in terms of semi-Thue systems. I think they are more convenient than Turing machines for the following reasons.</p>
<ul>
<li>Computation state is fully captured by a single list; it doesn't require us to speak of both a tape and head state.</li>
<li>You can insert or delete in the middle; you don't have to traverse the tape to shift everything.</li>
<li>Rules can match on segments of arbitrary (constant) length; you don't have to define auxiliary states just to check the neighborhood and more auxiliary states to write down more than one symbol.</li>
</ul>
<p>Informally speaking, I take the input word, I lift it to a superset of the input alphabet, I prepend a special starting symbol, and then rewriting starts; the word is accepted if a special accepting symbol is obtained. Formal definition (Lean 4):</p>
<pre><code>import Mathlib.Computability.Language

/-- Sum type of alphabet `α` and special symbols `β` -/
inductive Symbol (α : Type) (β : Type)
  | letter (a : α) : Symbol α β
  | marker (b : β) : Symbol α β

/-- Rewrite rule -/
structure Rule (α : Type) (β : Type) where
  input : List (Symbol α β)
  output : List (Symbol α β)

/-- Semi-Thue system (a.k.a. string rewriting system) -/
structure System (α : Type) where -- alphabet
  special : Type                  -- markers
  starting : special              -- to be prepended
  accepting : special             -- goal: derive a singleton [accepting]
  ruleset : List (Rule α special) -- rewrite rules

variable {α : Type}

/-- What happens to the input before computation starts -/
def System.initiate (h : System α) (w : List α) : List (Symbol α h.special) :=
  Symbol.marker h.starting :: List.map Symbol.letter w

/-- One step of rewriting -/
def System.Transforms (h : System α) (w₁ w₂ : List (Symbol α h.special)) : Prop :=
  ∃ r : Rule α h.special,
    r ∈ h.ruleset ∧
    ∃ u v : List (Symbol α h.special), w₁ = u ++ r.input ++ v ∧ w₂ = u ++ r.output ++ v

/-- Closure (reflexive+transitive) of the above, with step counting. Predicate `h.derives s t n` means
    the semi-Thue system `h` can transform `t` to `n` in exactly `n` rewriting step. -/
inductive System.Derives (h : System α) : List (Symbol α h.special) → List (Symbol α h.special) → ℕ → Prop
  | refl (w : List (Symbol α h.special)) : h.Derives w w 0
  | tail (u v w : List (Symbol α h.special)) (n : ℕ) : h.Derives u v n → h.Transforms v w → h.Derives u w (n+1)

/-- Language recognized by given semi-Thue system. -/
def System.Semidecides (h : System α) : Language α :=
  { w | ∃ n : ℕ, h.Derives (h.initiate w) [Symbol.marker h.accepting] n }

/-- Definition of recursively-enumerable languages in terms of semi-Thue systems. -/
def Language.IsRE (L : Language α) : Prop :=
  ∃ h : System α, h.Semidecides = L
</code></pre>
<p>In literature, semi-Thue systems are often used to simulate Turing machines. However, they might be used as the primary model of computation, enabling us to write algorithms in full details with less difficulty than when expressing the same algorithm using Turing machines.</p>
<p>Sure, semi-Thue systems also have disadvantages. It is easier to simulate Turing machines on RAM than to simulate semi-Thue systems on RAM. Nevertheless, asymptotic overhead can by avoided by using doubly-linked lists to simulate semi-Thue systems on RAM or in usual programming languages.</p>
<p>By now, you probably believe that semi-Thue systems can be used as a convenient Turing-complete model of computation. My main question is <strong>how to define deterministic computation?</strong> I didn't find any &quot;standard&quot; definition of deterministic semi-Thue systems in books (please, let me know if you there is any). I want to build classes like P. There are two ideas on my mind and I cannot decide which is better...</p>
<p>The first idea is to define determinism as a <strong>semantic</strong> property: a semi-Thue system is deterministic if there is always at most one option how to continue from any string that can be derived by the system. Formally:</p>
<pre><code>def System.IsDeterministic (h : System α) : Prop :=
  ∀ w : List α, ∀ s : List (Symbol α h.special), ∀ n : ℕ, h.Derives (h.initiate w) s n →
    ∀ x y : List (Symbol α h.special), h.Transforms s x ∧ h.Transforms s y → x = y
</code></pre>
<p>The second idea is to define determinism as a <strong>syntactic</strong> property: a semi-Thue system is deterministic if every rule has exactly one special symbol on both sides and no two rules overlap in applicability. Formally:</p>
<pre><code>def has_one_marker {β : Type} (s : List (Symbol α β)) : Prop :=
  ∃ u : List α, ∃ X : β, ∃ v : List α,
    s = List.map Symbol.letter u ++ [Symbol.marker X] ++ List.map Symbol.letter v

def actually_overlap {β : Type} (s₁ s₂ : List (Symbol α β)) : Prop :=
  ∃ t : List (Symbol α β), (has_one_marker t ∧ (
    (∃ u₁ v₁ : List (Symbol α β), u₁ ++ s₁ ++ v₁ = t) ∧
    (∃ u₂ v₂ : List (Symbol α β), u₂ ++ s₂ ++ v₂ = t)))

def System.IsDeterministicSyntax (h : System α) : Prop :=
  (∀ r ∈ h.ruleset, has_one_marker r.input ∧ has_one_marker r.output) ∧
  (∀ r₁ ∈ h.ruleset, ∀ r₂ ∈ h.ruleset, actually_overlap r₁.input r₂.input → r₁ = r₂)
</code></pre>
<p>Note that the syntactic property implies the semantic property.</p>
<p><strong>TL;DR</strong> In order to form and prove statements about complexity classes using semi-Thue systems, is it better to define the notion of &quot;deterministic semi-Thue system&quot; as a semantic property or a syntactic property?</p>

CC BY-SA 4.0
2023-08-21T15:55:45.217Z
The theory of rewriting grapples with these issues at length, (though they usually use the weaker notion of "local confluence" in place of your semantic notion, and "orthogonality" as the syntactic one). Have you considered checking the string rewriting literature to see how they do things?
cody
CC BY-SA 4.0
2023-08-21T16:49:39.927Z
Do you @cody have a particular literature in mind? I remember seeing the words "confluence" and "orthogonality" in texts about term rewriting systems, and I don't know whether it is relevant for semi-Thue systems.
Martin Dvorak
CC BY-SA 4.0
2023-08-21T18:15:33.643Z
FWIW, string rewriting = semi-Thue. I am not an expert, though I guess orthogonality applies to string rewrite systems, though it may be quite restrictive (as is your criterion!)

Confluence, of course, is extensively studied for SRSes (though mostly to find new exciting decision procedures).

Perhaps a reasonable first question might be: is strong confluence enough for your purposes? https://en.wikipedia.org/wiki/Confluence_(abstract_rewriting)#Strong_confluence
cody
CC BY-SA 4.0
2023-08-21T18:16:23.420Z
"Term Rewriting and All That" is a great reference, though it focuses more on terms than on strings. https://www21.in.tum.de/~nipkow/TRaAT/
cody
CC BY-SA 4.0
2023-08-22T10:53:27.437Z
As Cody mentions, a lot of properties of rewrite systems can be defined abstractly, see, in addition to Nipkow/Baader, e.g. J. W. Klop, [*Term Rewriting Systems*](https://www.cs.tau.ac.il/~nachum/papers/klop.pdf).
Martin Berger
CC BY-SA 4.0
2023-08-23T11:10:55.857Z
The semantic determinism is indeed stricter than confluence. If I change the definition from accepting by special symbol to accepting by empty string, then confluence serves for the same purpose as my semantic determinism. I don't see, however, why defining determinism via confluence would be better. I'll be happy to reconsider the decision if you give me a reason why confluence would be useful for the definitions of complexity classes.
Martin Dvorak
CC BY-SA 4.0
2023-08-23T14:10:55.343Z
What you call "semantic" is simpler, doesn't need an additional character, and closer to existing definitions (in particular the standard definition of determinism in automata, Turing-machines and process calculi). Have you got any indication that either definition affects the complexity classes you get?
Martin Berger
CC BY-SA 4.0
2023-08-23T18:02:49.460Z
What do you mean by "doesn't need an additional character" please? I need to extend the alphabet either way. As for the standard definition of determinism in Turing machines, it is on the syntactic side of things.
Martin Dvorak
<fl.formal-languages><church-turing-thesis><definitions>
Semi-Thue systems and deterministic computation
Martin Dvorak
# Semi-Thue systems and deterministic computation

(Asked by: username_0 on 2023-08-19)

I would like to use semi-Thue systems (a.k.a. string rewriting systems) to study complexity theory formally. Note that "semi-" in the name means "unidirectional [Thue system]".
Unlike in grammars (where I always worked with a fixed starting symbol), I don't want to start with a fixed starting symbol or (as written in older books) a set of "axioms". Instead, I want a semi-Thue system to operate on an input word; I want to define (semi)deciders in terms of semi-Thue systems. I think they are more convenient than Turing machines for the following reasons.

Computation state is fully captured by a single list; it doesn't require us to speak of both a tape and head state.
You can insert or delete in the middle; you don't have to traverse the tape to shift everything.
Rules can match on segments of arbitrary (constant) length; you don't have to define auxiliary states just to check the neighborhood and more auxiliary states to write down more than one symbol.

Informally speaking, I take the input word, I lift it to a superset of the input alphabet, I prepend a special starting symbol, and then rewriting starts; the word is accepted if a special accepting symbol is obtained. Formal definition (Lean 4):
import Mathlib.Computability.Language

/-- Sum type of alphabet `α` and special symbols `β` -/
inductive Symbol (α : Type) (β : Type)
  | letter (a : α) : Symbol α β
  | marker (b : β) : Symbol α β

/-- Rewrite rule -/
structure Rule (α : Type) (β : Type) where
  input : List (Symbol α β)
  output : List (Symbol α β)

/-- Semi-Thue system (a.k.a. string rewriting system) -/
structure System (α : Type) where -- alphabet
  special : Type                  -- markers
  starting : special              -- to be prepended
  accepting : special             -- goal: derive a singleton [accepting]
  ruleset : List (Rule α special) -- rewrite rules

variable {α : Type}

/-- What happens to the input before computation starts -/
def System.initiate (h : System α) (w : List α) : List (Symbol α h.special) :=
  Symbol.marker h.starting :: List.map Symbol.letter w

/-- One step of rewriting -/
def System.Transforms (h : System α) (w₁ w₂ : List (Symbol α h.special)) : Prop :=
  ∃ r : Rule α h.special,
    r ∈ h.ruleset ∧
    ∃ u v : List (Symbol α h.special), w₁ = u ++ r.input ++ v ∧ w₂ = u ++ r.output ++ v

/-- Closure (reflexive+transitive) of the above, with step counting. Predicate `h.derives s t n` means
    the semi-Thue system `h` can transform `t` to `n` in exactly `n` rewriting step. -/
inductive System.Derives (h : System α) : List (Symbol α h.special) → List (Symbol α h.special) → ℕ → Prop
  | refl (w : List (Symbol α h.special)) : h.Derives w w 0
  | tail (u v w : List (Symbol α h.special)) (n : ℕ) : h.Derives u v n → h.Transforms v w → h.Derives u w (n+1)

/-- Language recognized by given semi-Thue system. -/
def System.Semidecides (h : System α) : Language α :=
  { w | ∃ n : ℕ, h.Derives (h.initiate w) [Symbol.marker h.accepting] n }

/-- Definition of recursively-enumerable languages in terms of semi-Thue systems. -/
def Language.IsRE (L : Language α) : Prop :=
  ∃ h : System α, h.Semidecides = L

In literature, semi-Thue systems are often used to simulate Turing machines. However, they might be used as the primary model of computation, enabling us to write algorithms in full details with less difficulty than when expressing the same algorithm using Turing machines.
Sure, semi-Thue systems also have disadvantages. It is easier to simulate Turing machines on RAM than to simulate semi-Thue systems on RAM. Nevertheless, asymptotic overhead can by avoided by using doubly-linked lists to simulate semi-Thue systems on RAM or in usual programming languages.
By now, you probably believe that semi-Thue systems can be used as a convenient Turing-complete model of computation. My main question is how to define deterministic computation? I didn't find any "standard" definition of deterministic semi-Thue systems in books (please, let me know if you there is any). I want to build classes like P. There are two ideas on my mind and I cannot decide which is better...
The first idea is to define determinism as a semantic property: a semi-Thue system is deterministic if there is always at most one option how to continue from any string that can be derived by the system. Formally:
def System.IsDeterministic (h : System α) : Prop :=
  ∀ w : List α, ∀ s : List (Symbol α h.special), ∀ n : ℕ, h.Derives (h.initiate w) s n →
    ∀ x y : List (Symbol α h.special), h.Transforms s x ∧ h.Transforms s y → x = y

The second idea is to define determinism as a syntactic property: a semi-Thue system is deterministic if every rule has exactly one special symbol on both sides and no two rules overlap in applicability. Formally:
def has_one_marker {β : Type} (s : List (Symbol α β)) : Prop :=
  ∃ u : List α, ∃ X : β, ∃ v : List α,
    s = List.map Symbol.letter u ++ [Symbol.marker X] ++ List.map Symbol.letter v

def actually_overlap {β : Type} (s₁ s₂ : List (Symbol α β)) : Prop :=
  ∃ t : List (Symbol α β), (has_one_marker t ∧ (
    (∃ u₁ v₁ : List (Symbol α β), u₁ ++ s₁ ++ v₁ = t) ∧
    (∃ u₂ v₂ : List (Symbol α β), u₂ ++ s₂ ++ v₂ = t)))

def System.IsDeterministicSyntax (h : System α) : Prop :=
  (∀ r ∈ h.ruleset, has_one_marker r.input ∧ has_one_marker r.output) ∧
  (∀ r₁ ∈ h.ruleset, ∀ r₂ ∈ h.ruleset, actually_overlap r₁.input r₂.input → r₁ = r₂)

Note that the syntactic property implies the semantic property.
TL;DR In order to form and prove statements about complexity classes using semi-Thue systems, is it better to define the notion of "deterministic semi-Thue system" as a semantic property or a syntactic property?

**Tags:** fl.formal-languages, church-turing-thesis, definitions

> **Comments:**
> **username_1**: The theory of rewriting grapples with these issues at length, (though they usually use the weaker notion of "local confluence" in place of your semantic notion, and "orthogonality" as the syntactic one). Have you considered checking the string rewriting literature to see how they do things?  
> **username_0**: Do you @username_1 have a particular literature in mind? I remember seeing the words "confluence" and "orthogonality" in texts about term rewriting systems, and I don't know whether it is relevant for semi-Thue systems.  
> **username_1**: FWIW, string rewriting = semi-Thue. I am not an expert, though I guess orthogonality applies to string rewrite systems, though it may be quite restrictive (as is your criterion!)  Confluence, of course, is extensively studied for SRSes (though mostly to find new exciting decision procedures).  Perhaps a reasonable first question might be: is strong confluence enough for your purposes? https://en.wikipedia.org/wiki/Confluence_(abstract_rewriting)#Strong_confluence  
> **username_1**: "Term Rewriting and All That" is a great reference, though it focuses more on terms than on strings. https://www21.in.tum.de/~nipkow/TRaAT/  
> **username_2**: As Cody mentions, a lot of properties of rewrite systems can be defined abstractly, see, in addition to Nipkow/Baader, e.g. J. W. Klop, [*Term Rewriting Systems*](https://www.cs.tau.ac.il/~nachum/papers/klop.pdf).  
> **username_0**: The semantic determinism is indeed stricter than confluence. If I change the definition from accepting by special symbol to accepting by empty string, then confluence serves for the same purpose as my semantic determinism. I don't see, however, why defining determinism via confluence would be better. I'll be happy to reconsider the decision if you give me a reason why confluence would be useful for the definitions of complexity classes.  
> **username_2**: What you call "semantic" is simpler, doesn't need an additional character, and closer to existing definitions (in particular the standard definition of determinism in automata, Turing-machines and process calculi). Have you got any indication that either definition affects the complexity classes you get?  
> **username_0**: What do you mean by "doesn't need an additional character" please? I need to extend the alphabet either way. As for the standard definition of determinism in Turing machines, it is on the syntactic side of things.  

---

## 0 answers

