In[]:=
Graph3D[ResourceFunction["MultiwayFunctionSystem"][Values[substitutionLemmas[#,x_∘y_<->y_∘x_]]&,((a∘b)∘(c∘d))∘(e∘f),5,"StatesGraphStructure"],GraphLayout"LayeredDigraphEmbedding",AspectRatio1]
In[]:=
Groupings[Array[a,4],SmallCircle->2]
Out[]=
{((a[1]∘a[2])∘a[3])∘a[4],a[1]∘((a[2]∘a[3])∘a[4]),(a[1]∘(a[2]∘a[3]))∘a[4],a[1]∘(a[2]∘(a[3]∘a[4])),(a[1]∘a[2])∘(a[3]∘a[4])}
In[]:=
Graph[ResourceFunction["MultiwayFunctionSystem"][Values[substitutionLemmas[#,x_∘y_<->y_∘x_]]&,#,8,"StatesGraphStructure"],GraphLayout"LayeredDigraphEmbedding",AspectRatio1]&/@Groupings[Array[a,4],SmallCircle->2]
Out[]=

,
,
,
,

In[]:=
Graph[ResourceFunction["MultiwayFunctionSystem"][Values[substitutionLemmas[#,x_∘y_<->y_∘x_]]&,#,8,"StatesGraphStructure"],GraphLayout"LayeredDigraphEmbedding",AspectRatio1]&/@Groupings[Array[a,5],SmallCircle->2]
Out[]=

,
Contents cannot be rendered at this time; please try again later
,
,
,
,
,
,
,
,
,
,
,
,

In[]:=
VertexCount/@%
Out[]=
{16,16,16,16,16,16,16,16,16,16,16,16,16,16}
In[]:=
Map[Graph[ResourceFunction["MultiwayFunctionSystem"][Values[substitutionLemmas[#,x_∘y_<->y_∘x_]]&,#,8,"StatesGraphStructure"],GraphLayout"LayeredDigraphEmbedding",AspectRatio1]&,RandomSample[Groupings[Array[a,6],SmallCircle->2],10]]
Out[]=
{
,
,
,
,
,
,
,
,
,
}
In[]:=
VertexCount/@%
Out[]=
{32,32,32,32,32,32,32,32,32,32}
In[]:=
Graph3D[ResourceFunction["MultiwayFunctionSystem"][Values[substitutionLemmas[#,x_∘y_<->y_∘x_]]&,((a∘b)∘(c∘d))∘(e∘f),5,"StatesGraphStructure"],GraphLayout"LayeredDigraphEmbedding",AspectRatio1]
Out[]=
In[]:=
VertexOutDegree[
]
Out[]=
{5,5,5,5,5,5,5,5,5,5,5,5,5,5,5,5,5,5,5,5,5,5,5,5,5,5,5,5,5,5,5,5}
In[]:=
VertexList
Contents cannot be rendered at this time; please try again later

Out[]=
{(a ∘ b) ∘ (c ∘ d),(a ∘ b) ∘ (d ∘ c),(b ∘ a) ∘ (c ∘ d),(c ∘ d) ∘ (a ∘ b),(b ∘ a) ∘ (d ∘ c),(c ∘ d) ∘ (b ∘ a),(d ∘ c) ∘ (a ∘ b),(d ∘ c) ∘ (b ∘ a)}
In[]:=
ToExpression/@%
Out[]=
{(a∘b)∘(c∘d),(a∘b)∘(d∘c),(b∘a)∘(c∘d),(c∘d)∘(a∘b),(b∘a)∘(d∘c),(c∘d)∘(b∘a),(d∘c)∘(a∘b),(d∘c)∘(b∘a)}
In[]:=
Level[#,{-1}]&/@%
Out[]=
{{a,b,c,d},{a,b,d,c},{b,a,c,d},{c,d,a,b},{b,a,d,c},{c,d,b,a},{d,c,a,b},{d,c,b,a}}
In[]:=
Complement[Permutations[{a,b,c,d}],%]
Out[]=
{{a,c,b,d},{a,c,d,b},{a,d,b,c},{a,d,c,b},{b,c,a,d},{b,c,d,a},{b,d,a,c},{b,d,c,a},{c,a,b,d},{c,a,d,b},{c,b,a,d},{c,b,d,a},{d,a,b,c},{d,a,c,b},{d,b,a,c},{d,b,c,a}}
In[]:=
UndirectedGraph[ResourceFunction["MultiwayFunctionSystem"][Values[substitutionLemmas[#,x_∘y_<->y_∘x_]]&,#,8,"StatesGraphStructure"],AspectRatio1]&@First[Groupings[Array[a,5],SmallCircle->2]]
Out[]=
Contents cannot be rendered at this time; please try again later
In[]:=
Table[UndirectedGraph[ResourceFunction["MultiwayFunctionSystem"][Values[substitutionLemmas[#,x_∘y_<->y_∘x_]]&,#,8,"StatesGraphStructure"],AspectRatio1]&@First[Groupings[Array[a,n],SmallCircle->2]],{n,2,5}]
Out[]=
{
,
,
,
}
In[]:=
x_⊕(y_⊕z_)(x_⊕y_)⊕z_/.CirclePlus->SmallCircle
Out[]=
x_∘(y_∘z_)(x_∘y_)∘z_
In[]:=
UndirectedGraph[
]
Out[]=
Out[]=
Contents cannot be rendered at this time; please try again later
while when applied to (a∘b)∘(c∘d) we get:
In[]:=
Graph[ResourceFunction["MultiwayFunctionSystem"][Values[substitutionLemmas[#,{x_⊕y_y_⊕x_,x_⊕(y_⊕z_)(x_⊕y_)⊕z_,x_⊕x_<->(x_⊕x_)⊕x_}]]&,(a⊕b)⊕(c⊕d),10,"StatesGraphStructure"]]
Out[]=
Contents cannot be rendered at this time; please try again later
​
​
All this is a bit more familiar in the case of groups---though the typical axioms for these are slightly more complicated:
We can think of our expressions as corresponding to words in the semigroup. So in this case what we’re seeing is that there are an infinite number of equivalences between words.
​
​
​
In the mathematical
So what this means is that in this case there are an infinite number of equivalences
But what is the mathematical significance of this? Each expression corresponds to a “word” in a presentation of the semigroup. And our multiway graph then tells us a certain set of words that are equivalent according to the axioms and relations of the semigroup.
​
under the captures what collection of words In effect our multiway graph captures
This is an Abelian semigroup.....
Because axioms don’t change size, result from starting from a given expression will be finite.....
Adding more “relations” more theorems will be true....
E.g. if just commutative have XXX == XXXX ; associative XXX == XXX
More theorems are true.....
[ Relation to Cayley graph for group ]

Generated Variables

If we start with a∘a and do no unification, we’ll get:
With uniquification, but not canonicalization we’ll get a pure tree:
But with canonicalization this is reduced to:
A confusing feature of this particular example is that this same result would have been obtained just by canonicalizing the original “assume-all-x_’s-are-the-same” case.

Rules Applied to Rules

Rules where we keep applying a rule to each side

The dot just drops its first element (like the K combinator)
What does a proof look like here?
Forward light cone of the initial expr intersected with the past light cone of the destination.......

Finding proofs

Alternative Simple Case