Wolfram Research

Function Repository Resource:

CanonicalKnuthBendixCompletion

Source Notebook

Compute the canonical Knuth-Bendix completion for a given multiway system

Contributed by: Jonathan Gorard

ResourceFunction["CanonicalKnuthBendixCompletion"][rules]

generates a list of canonical (i.e. initial condition-independent) Knuth-Bendix completion rules for the multiway system with the specified rules.

ResourceFunction["CanonicalKnuthBendixCompletion"][rules,n]

generates a list of canonical (i.e. initial condition-independent) Knuth-Bendix completion rules for the multiway system with the specified rules after n steps.

Details and Options

Rules can be specified in the following ways:
{"lhs1"->"rhs1",…} string substitution system
{{l11,l12,…}->{r11,r12,..},…} list substitution system
WolframModel[rules] Wolfram Model system
CellularAutomaton[rules] cellular automaton system
"type"rules system of the specified type
Supported rule types include:
"StringSubstitutionSystem" rules given as replacements on strings
"ListSubstitutionSystem" rules given as replacements on lists
"CellularAutomaton" rules given as a list of CellularAutomaton rule specifications
"WolframModel" rules given as replacements on hypergraphs
ResourceFunction["CanonicalKnuthBendixCompletion"] accepts both indiviudal rules and lists of rules.
Knuth-Bendix completion transforms an arbitrary rewrite system into a confluent (causal invariant) rewrite system by resolving critical pairs.
In the context of the multiway systems, critical (branch) pairs indicate bifurcations or ambiguities in the multiway evolution.
ResourceFunction["CanonicalKnuthBendixCompletion"] gives the minimal set of rules required to force all unresolved canonical branch pairs to converge.

Examples

Basic Examples

Generate the list of all canonical Knuth-Bendix completion rules for a string substitution system:

In[1]:=
ResourceFunction[
 "CanonicalKnuthBendixCompletion"][{"AA" -> "ABA", "AAA" -> "B"}]
Out[1]=

Generate the list of canonical Knuth-Bendix completion rules necessary to force confluence after 2 steps:

In[2]:=
ResourceFunction[
 "CanonicalKnuthBendixCompletion"][{"AA" -> "ABA", "AAA" -> "B"}, 2]
Out[2]=

CanonicalKnuthBendixCompletion can handle Wolfram models and other system types:

In[3]:=
ResourceFunction["CanonicalKnuthBendixCompletion"][
 "WolframModel" -> {{{2, 2, 1}, {2, 2, 2}} -> {{1, 1, 3}, {3, 3, 2}}}]
Out[4]=
In[5]:=
Take[ResourceFunction["CanonicalKnuthBendixCompletion"][
  "WolframModel" -> {{{2, 2, 1}, {2, 2, 2}} -> {{1, 1, 3}, {3, 3, 2}}}, 10], 20]
Out[5]=

Provide a cellular automaton as input:

In[6]:=
Take[ResourceFunction["CanonicalKnuthBendixCompletion"][
  CellularAutomaton[30], 2], 20]
Out[6]=

Scope

System Types

CanonicalKnuthBendixCompletion supports both string and list substitution systems:

In[7]:=
ResourceFunction[
 "CanonicalKnuthBendixCompletion"][{"BB" -> "AA", "ABB" -> "BA"}]
Out[7]=

Use substitutions on lists:

In[8]:=
ResourceFunction[
 "CanonicalKnuthBendixCompletion"][{{1, 1} -> {0, 0}, {0, 1, 1} -> {1,
     0}}]
Out[8]=

CanonicalKnuthBendixCompletion also supports multiway generalizations of cellular automata:

In[9]:=
Take[ResourceFunction["CanonicalKnuthBendixCompletion"][
  CellularAutomaton[{170, 240}]], 20]
Out[9]=

Generate a Knuth-Bendix completion for left- and right-shift cellular automaton rules after 5 steps:

In[10]:=
Take[ResourceFunction["CanonicalKnuthBendixCompletion"][
  CellularAutomaton[{170, 240}], 5], 20]
Out[10]=

Determine that the rule 30 cellular automaton is not total causal invariant:

In[11]:=
Take[ResourceFunction["CanonicalKnuthBendixCompletion"][
  CellularAutomaton[30], 5], 20]
Out[11]=

CanonicalKnuthBendixCompletion also supports multiway generalizations of Wolfram Models:

In[12]:=
ResourceFunction["CanonicalKnuthBendixCompletion"][
 "WolframModel" -> {{{2, 2, 1}, {2, 2, 2}} -> {{1, 1, 2}, {2, 2, 2}}}]
Out[12]=

Determine that this Wolfram model rule is not total causal invariant:

In[13]:=
Take[ResourceFunction["CanonicalKnuthBendixCompletion"][
  "WolframModel" -> {{{2, 2, 1}, {2, 2, 2}} -> {{1, 1, 2}, {2, 2, 2}}}, 5], 20]
Out[13]=

Applications

Causal Invariant Rules

Prove that the Xor and And functions are total causal invariant (due to associativity):

In[14]:=
ResourceFunction[
 "CanonicalKnuthBendixCompletion"][{"TT" -> "F", "TF" -> "T", "FT" -> "T", "FF" -> "F"}, 1]
Out[14]=
In[15]:=
ResourceFunction[
 "CanonicalKnuthBendixCompletion"][{"TT" -> "T", "TF" -> "F", "FT" -> "F", "FF" -> "F"}, 1]
Out[15]=

On the other hand, the Nand function is not associative, so it is not total causal invariant:

In[16]:=
ResourceFunction[
 "CanonicalKnuthBendixCompletion"][{"TT" -> "F", "TF" -> "T", "FT" -> "T", "FF" -> "T"}, 1]
Out[16]=

Properties and Relations

CanonicalKnuthBendixCompletion returns an empty list of canonical Knuth-Bendix completion rules if and only if the rule is total causal invariant:

In[17]:=
ResourceFunction[
 "CanonicalKnuthBendixCompletion"][{"TT" -> "F", "TF" -> "T", "FT" -> "T", "FF" -> "T"}, 1]
Out[17]=
In[18]:=
ResourceFunction[
 "CanonicalKnuthBendixCompletion"][{"TT" -> "F", "TF" -> "T", "FT" -> "T", "FF" -> "F"}, 1]
Out[18]=

Resource History

Source Metadata

Related Resources

License Information