In[]:=
Graph3D[ResourceFunction["MultiwayFunctionSystem"][Values[substitutionLemmas[#,x_∘y_<->y_∘x_]]&,((a∘b)∘(c∘d))∘(e∘f),5,"StatesGraphStructure"],GraphLayout"LayeredDigraphEmbedding",AspectRatio1]
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",AspectRatio1]&/@Groupings[Array[a,4],SmallCircle->2]
Out[]=
,
,
,
,
In[]:=
Graph[ResourceFunction["MultiwayFunctionSystem"][Values[substitutionLemmas[#,x_∘y_<->y_∘x_]]&,#,8,"StatesGraphStructure"],GraphLayout"LayeredDigraphEmbedding",AspectRatio1]&/@Groupings[Array[a,5],SmallCircle->2]
Out[]=
,
,
,
,
,
,
,
,
,
,
,
,
,
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",AspectRatio1]&,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",AspectRatio1]
Out[]=
while when applied to (a∘b)∘(c∘d) we get:
All this is a bit more familiar in the case of groups---though the typical axioms for these are slightly more complicated:
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
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
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
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
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 Applied to Rules
Rules where we keep applying a rule to each side
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
Finding proofs
Alternative Simple Case
Alternative Simple Case