We study and visualize string-rewriting systems and confluence in the context of solving word-problems in (finitely-presented) monoids. We implement the Knuth-Bendix Algorithm for monoids in Wolfram Language.

Introduction

Let
MMon〈X|R〉
be a finitely presented monoid. Then the set of relations
R
partitions the free monoid
F
X
into equivalence classes. When the set of these equivalence classes is equipped with the natural binary operation, we get
M
. Given two words in
F
X
, it is very natural to ask if there is an algorithm to deduce if they are equivalent in
M
,
i.e., lie in the same equivalence class. This problem is known is known as the word-problem for finitely-presented monoids, but, unfortunately, it is undecidable as was shown by Emil Post [1] in 1947. Still, Post’s result is not as devastating as it sounds since we can still attempt to solve the word-problem when
M
has some special structure. This is what this essay is about: Trying to solve the word problem when we have special structure.

Rewriting Systems and Reducing Orders

Let
X
be a finite alphabet equipped with a linear order, and let
≺
be the (strict) ShortLex order on
F
X
, i.e., we sort words by length first, and then we sort them lexicographically based on the linear order on the set
X
. As is usually the case, when
X
is a subset of the lower-case English alphabet (which comes with a linear order), we can implement the ShortLex order in Wolfram Language in the following manner:
In[]:=
shortLex[x_String,y_String]:=False/;x==y(*EnsuresshortLexisastrictorder*)​​shortLex[x_String,y_String]:=StringLength[x]<StringLength[y]/;Not[StringLength[x]==StringLength[y]](*Sortsstringsbylength*)​​shortLex[x_String,y_String]:=OrderedQ[{x,y}]/;And[StringLength[x]==StringLength[y],x!=y](*Sortsequallengthstringsbylexicogrpahic(dictionary)order*)
For example, we have
ab≺aba
and
ab≺ba
in
F
{a,b}
:
In[]:=
And[shortLex["ab","aba"],shortLex["ab","ba"]]
Out[]=
True
Notice that the order
≺
satisfies the following two properties:
◼
  • (
    F
    X
    ,≺)
    is well-ordered.
    • ◼
  • ≺
    is translation invariant: If
    a,b,c,d∈
    F
    X
    and
    a≺b
    , then cad
    ≺
    cbd.
    • (Note: For our purposes, we can work with any ordering that satisfies the two properties above. We choose ShortLex as the default order. The choice of ordering may matter for the results we get, and in some cases it may be more favorable to use some other order.)
    DEFINITION. A rewriting system
    R
    on
    F
    X
    is a set of rules of the form
    ab
    , with
    a,b∈
    F
    X
    and
    b≺a
    .
    A rewriting system has the ability to reduce words in
    F
    X
    by making them smaller with respect to
    ≺
    by performing string-substitutions based on the (one-directional) rules it contains.
    DEFINITION.The monoid defined by a rewriting system is the monoid we get when the rules in the rewriting system are considered as relations.
    For example, if the rewriting system on
    F
    {a,b}
    is
    {ababa,baab}
    , then the monoid defined by it is Mon
    〈a,b|ababa,baab〉
    .
    DEFINITION. Let
    R
    be a string rewriting system on
    F
    X
    , given two words
    u,v
    in
    F
    X
    ,
    ◼
  • Say that
    u∼v
    if
    u
    and
    v
    are equivalent in the monoid defined by
    R
    .
    • ◼
  • Say that
    uv
    if there is a rule
    ab
    in
    R
    such that
    uxay
    and
    vxby.
    • ◼
  • Say that
    u↦v
    if there is a sequence
    u
    1
    ,…,
    u
    n
    such that
    u
    1
    u
    ,
    u
    n
    v
    and for each
    1≤i<n
    we have
    u
    i
    
    u
    i+1
    .
    • We have the following easy to see proposition that connects
    ∼
    and
    ↦
    :
    PROPOSITION 1. Let
    R
    be a string-rewriting system on
    F
    X
    , given two words
    u,v∈
    F
    X
    , we have that
    u∼v
    if and only if there exists a sequence
    u
    1
    ,…,
    u
    n
    such that
    u
    1
    u
    ,
    u
    n
    v
    and for each
    1≤i<n
    we have
    u
    i
    ↦
    u
    i+1
    or
    u
    i+1
    ↦
    u
    i
    .
    THEOREM. Let
    R
    be a string-rewriting system on
    F
    X
    , then following three properties are equivalent.
    ◼
  • (Church-Rosser) For all words
    u,v
    if
    u∼v
    , then there is a
    q∈
    F
    X
    such that
    u↦q
    and
    v↦q
    .
    • ◼
  • (Confluence) For all words
    w,v,u
    if
    w↦v
    and
    w↦u
    then there exists a
    q∈
    F
    X
    such that
    v↦q
    and
    u↦q
    .
    • ◼
  • (Local Confluence) For all words
    w,v,u
    if
    wv
    and
    wu
    then there exists a
    q∈
    F
    X
    such that
    v↦q
    and
    u↦q
    .
    • PROOF. See Proposition 2.5 in [2].
    Let
    R
    be a string-rewriting system on
    F
    X
    , we say a word is reduced with respect to
    ↦
    if it can not be rewritten any further using
    R
    . Since
    ≺
    is a well order, every word can be rewritten with
    ↦
    into a reduced word.
    When
    X
    is a subset of the lower-case English alphabet, the following algorithm rewrites a word into a reduced word with respect to a rewriting system.
    In[]:=
    replace[word_,rules_]:=StringReplace[word,rules](*Replacesoccurencesofleftsidesofruleswithrightsides*)​​reduce[word_,rules_]:=FixedPoint[replace[#,rules]&,word](*Repeatedlyevaluatesreplaceuntilfixed-point*)
    For example we have:
    In[]:=
    reduce["ababc",{"ab"->"b","b"->""}]
    Out[]=
    c
    Now, if
    R
    satisfies the Church Rosser property, then the monoid defined by
    R
    solves the word-problem: If we want to check whether
    u∼v
    , we reduce both
    u
    and
    v
    into reduced words. If these reduced words are the same, then the words are equivalent, and if they are different, by the Church-Rosser property, the words lie in different equivalence classes. ​Let us now look at an example of a rewriting system: Consider the rewriting system
    R{aba,abab}
    over
    F
    {a,b}
    . This defines the monoid
    MMon〈a,b|aba,abab〉
    . We can visualize the graph of all words up to a certain length(in this case 5), where there is a directed edge between the words
    v
    ,
    w
    if
    vw
    , in the following manner:
    In[]:=
    alphabet={"a","b"};​​substrings=Flatten[Table[Tuples[alphabet,n],{n,0,5}],1];​​stringSubstrings=StringJoin/@substrings;(*Allsubstringsoflengthlessthanorequalto5*)​​allReplacements[str_String,substr_String,newstr_String]:=Module[{positions,replaceAtPos},​​positions=StringPosition[str,substr];​​replaceAtPos[pos_]:=StringReplacePart[str,newstr,pos];​​replaceAtPos/@positions]​​all[word_,rules_]:=Flatten[Table[allReplacements[word,Keys[rules][[i]],Values[rules][[i]]],{i,Length[rules]}]](*Allwords
    v
    suchthatword
    v
    *)​​fixedpoint[word_,rules_]:=If[reduce[word,rules]==word,True,False](*Checksifawordisreduced*)​​SimpleGraph[​​Union[​​Union[​​Flatten[​​Table[​​Table[​​stringSubstrings[[x]]all[stringSubstrings[[x]],{"ab"->"a","aba"->"b"}][[i]],{i,Length[all[stringSubstrings[[x]],{"ab"->"a","aba"->"b"}]]}],​​{x,1,Length[stringSubstrings]}]​​],​​Map[#->#&,Select[stringSubstrings,fixedpoint[#,{"ab"->"a","aba"->"b"}]&]]]​​],(*Alledgesoftheformspecified*)​​GraphLayout->"SpringElectricalEmbedding",​​VertexStyle->Union[Map[#->Black&,Select[stringSubstrings,Not[fixedpoint[#,{"ab"->"a","aba"->"b"}]]&]](*Colorsnon-reducedwordsblack*),Map[#->Red&,Select[stringSubstrings,fixedpoint[#,{"ab"->"a","aba"->"b"}]&]](*Colorsreducedwordsred*)],​​VertexSize->0.4,EdgeShapeFunction->{{"Arrow","ArrowSize"->0.015}},​​EdgeStyle->Darker[Blue]]//Quiet
    Out[]=
    (WARNING: Don’t be fooled by the connectivity of the graph above. The graph above is a subgraph of the actual(infinite) graph consisting of all word, and it is possible that two words are in the same weakly-connected component in the real graph but are not connected in the graph above because showing their connectivity requires going to a word above length 5.)​Of course, by Proposition 1, if two words are in the same weakly connected component, then they are equivalent in the monoid. So, the multiple red reduced words we see in some weakly-connected components are causing failure in the Church-Rosser property and preventing us from solving the word-problem using the strategy described earlier. ​More generally, we can define the following function that makes the visualisation above for any rewriting system over
    F
    {a,b}
    :
    In[]:=
    graphvis[rules_]:=SimpleGraph[Union[Union[Flatten[Table[Table[stringSubstrings[[x]]all[stringSubstrings[[x]],rules][[i]],{i,Length[all[stringSubstrings[[x]],rules]]}],{x,1,Length[stringSubstrings]}]]],Map[#->#&,Select[stringSubstrings,fixedpoint[#,rules]&]]],GraphLayout->"SpringElectricalEmbedding",VertexStyle->Union[Map[#->Black&,Select[stringSubstrings,Not[fixedpoint[#,rules]]&]],Map[#->Red&,Select[stringSubstrings,fixedpoint[#,rules]&]]],VertexSize->0.4,EdgeShapeFunction->{{"Arrow","ArrowSize"->0.015}},EdgeStyle->Darker[Blue]]

    Local Confluence

    As we said earlier, the Church-Rosser property guarantees the ability to solve the word-problem. At face value, the Church-Rosser property looks hard to check; however, it is equivalent to local confluence, which is easy to check thanks to the following theorem:
    THEOREM. Let
    R
    be a rewriting system. Suppose
    R
    is not locally confluent, say a word
    w
    is a minimal failure of local confluence if no sub word of it causes a failure in local confluence. Then if
    w
    is a minimal failure of local confluence one of the following holds:
    ◼
  • w
    is the left side of a rule in
    R
    and contains the left side of another rule in
    R
    .
    • ◼
  • w
    = abc where
    c
    is not the empty word and
    ab
    ,
    bc
    are both left sides of rules in
    R.
    • PROOF. It suffices to show that we must have an “overlap” between two rules in
    w
    . Suppose that there is no overlap between any two rules in
    w
    , then for any two reductions
    wu
    ,
    wv
    , we can apply to
    u
    the rule that was applied to
    w
    to get
    v
    and apply to
    v
    the rule that was applied to
    w
    to get
    u
    . Doing so, would give us the same word, but this is a contradiction with the fact that
    w
    is a failure of local confluence.
    In the next section, we shall use the theorem above to create a (semi-decision) algorithm that converts a rewriting system into a locally confluent system, and hence, a system satisfying the Church-Rosser property, without changing
    ∼
    .

    The Knuth-Bendix Algorithm

    Let
    R
    be a rewriting system. Let
    (P,Q)
    be a pair of rules in
    R
    ,
    ◼
  • Say a word
    w
    is an overlap of
    (P,Q)
    of type 1 if
    w
    = abc where
    c
    is not the empty word and
    ab
    is the left side of
    P
    and
    bc
    is the left side of
    Q
    .
    • Implements the Knuth-Bendix algorithm once.
    We can now repeatedly apply the above algorithm until we get a fixed-point. This is the Knuth-Bendix algorithm.
    We can also visualize the new edges that have been added due to the Knuth-Bendix algorithm:
    Simplifying the result we get
    For example we have:
    And,
    As expected.

    Acknowledgements

    The author would like to thank the instructors and TAs of the Wolfram Research program for several helpful conversations.

    Bibliography

    1. Emil L. Post. Recursive Unsolvability of a Problem of Thue. The Journal of Symbolic Logic, Vol. 12, No. 1. (Mar., 1947), pp. 1-11. URL: https://www.wolframscience.com/prizes/tm23/images/Post2.pdf​
    ​2. Charles C. Sims. Computation with finitely presented groups. Cambridge University Press, 1994.

    CITE THIS NOTEBOOK

    Monoids, String-Rewriting, Confluence, and the Knuth-Bendix Algorithm​
    by Vivaan Daga​
    Wolfram Community, STAFF PICKS, July 11, 2024
    ​https://community.wolfram.com/groups/-/m/t/3217387