Function Repository Resource:

FindKnuthBendixCompletion

Source Notebook

Find the Knuth-Bendix completion for a given multiway system evolution

Contributed by: Jonathan Gorard

ResourceFunction["FindKnuthBendixCompletion"][rules,init,n]

finds the Knuth-Bendix completion after n steps in the evolution of the multiway system with the specified rules starting from initial condition init.

Details and Options

Knuth-Bendix completion transforms an arbitrary rewrite system into a confluent (causally invariant) rewrite system by resolving critical pairs.
In the context of the multiway systems, critical pairs indicate bifurcations or ambiguities in the multiway system evolution.
ResourceFunction["FindKnuthBendixCompletion"] gives the minimal set of rules required to force all unresolved critical pairs to converge.
Multiway systems operate on strings, lists and WolframModel systems.
When rules are specified by an explicit association, the following elements can be included:
"StateEvolutionFunction"the list of successors for a given state
"StateEquivalenceFunction"whether two states should be considered equivalent
"StateEventFunction"the list of events obtained from a given state
"SystemType"system type name
"EventSelectionFunction"which events from a given state should be included
The initial condition can consist of a single state or a list of states.

Examples

Basic Examples (5) 

Find the Knuth-Bendix completion for a non-causally-invariant multiway system evolution:

In[1]:=
ResourceFunction[
 "FindKnuthBendixCompletion"][{"A" -> "AB", "AA" -> "BA"}, {"AAB"}, 3]
Out[1]=
In[2]:=
ResourceFunction[
 "FindKnuthBendixCompletion"][{{0} -> {0, 1}, {0, 0} -> {1, 0}}, {{0, 0, 1}}, 3]
Out[2]=

Find the Knuth-Bendix completion for a more complicated non-causally-invariant multiway system evolution:

In[3]:=
ResourceFunction[
 "FindKnuthBendixCompletion"][{"AA" -> "AAB", "AAA" -> "BAAB"}, {"AAA"}, 3]
Out[3]=
In[4]:=
ResourceFunction[
 "FindKnuthBendixCompletion"][{{0, 0} -> {0, 0, 1}, {0, 0, 0} -> {1, 0, 0, 1}}, {{0, 0, 0}}, 3]
Out[4]=

By picking a specific updating order, we can change the Knuth-Bendix completion:

In[5]:=
ResourceFunction[
 "FindKnuthBendixCompletion"][{"AA" -> "AAB", "AAA" -> "BAAB"} -> ({First[#], Last[#]} &), {"AAA"}, 3]
Out[5]=
In[6]:=
ResourceFunction[
 "FindKnuthBendixCompletion"][{{0, 0} -> {0, 0, 1}, {0, 0, 0} -> {1, 0, 0, 1}} -> ({First[#], Last[#]} &), {{0, 0, 0}}, 3]
Out[6]=

Determine that a multiway system is causally invariant:

In[7]:=
ResourceFunction[
 "FindKnuthBendixCompletion"][{"A" -> "AA", "B" -> "AB"}, {"ABA"}, 3]
Out[7]=
In[8]:=
ResourceFunction[
 "FindKnuthBendixCompletion"][{{0} -> {0, 0}, {1} -> {0, 1}}, {{0, 1, 0}}, 3]
Out[8]=

FindKnuthBendixCompletion can also find Knuth-Bendix completions for WolframModel evolutions:

In[9]:=
ResourceFunction["FindKnuthBendixCompletion"][
 "WolframModel" -> {{{1, 2}, {1, 3}, {1, 4}} -> {{1, 2}, {1, 3}, {1, 4}, {2, 3}}}, {{{1, 2}, {1, 3}, {1, 4}}}, 5]
Out[9]=
In[10]:=
ResourceFunction["FindKnuthBendixCompletion"][
 "WolframModel" -> {{{2, 2, 1}, {2, 2, 2}} -> {{1, 1, 3}, {1, 1, 1}, {2, 1, 2}, {3, 3, 2}}}, {{{0, 0, 0}, {0, 0, 0}, {0, 0, 0}}},
  1]
Out[10]=

Scope (1) 

FindKnuthBendixCompletion gives an empty list if and only if the multiway system is causally invariant:

In[11]:=
ResourceFunction[
 "FindKnuthBendixCompletion"][{"A" -> "AB", "B" -> "A"}, {"A"}, 3]
Out[11]=
In[12]:=
ResourceFunction[
 "FindKnuthBendixCompletion"][{{0} -> {0, 1}, {1} -> {0}}, {{0}}, 3]
Out[12]=

Publisher

Jonathan Gorard

Version History

  • 1.0.0 – 04 December 2019

Source Metadata

Related Resources

License Information