Basic idea: make the expressions in the hypergraph have “built-in meanings”, corresponding to statements/predicates

{Equal,x,y}
{Equal,"AB","BA"}
{ConsistsOf,"AB","A","B"}
{ConsistsOf,"AB",{"A","B"}}
can be represented as
{{ConsistsOf,"AB",x},{IsAList,x,"A","B"}}
In a triplestore, it’s just entity, property, value [i.e. a ternary hyperedge]
In our case, we include arrays, that are higher-k hyperedges.

We encode “knowledge” as hyperedges

In[]:=
ResourceFunction["MultiwaySystem"][{"AB""BA","BA""AB"},"BBAA",6,"StatesGraph"]
Out[]=
I.e. AABB = BBAA

In the “content” formulation, this becomes a hyperedge

{EqualityContents,x,"AABB","BBAA"}
The evolution rule takes multiple hyperedges and “does inference” on them...

Claim: every hyperedge represents an equality

{"AABB","BBAA"}
The rule for the system is simply the application of that equality in another equality
{{x,y},{u,v}}{{SubstitutionSystem[uv][x],y},{x,y},{u,v}}
Really the internal edges are unordered (to represent equalities)
{{x,y},{u,v}}
In[]:=
ResourceFunction["MultiwaySystem"][{"AB""BA","BA""AB"},ResourceFunction["StringTuples"]["AB",3],6,"StatesGraph"]
Out[]=
In[]:=
ResourceFunction["MultiwaySystem"][{"AB""BA","BA""AB"},ResourceFunction["StringTuples"]["AB",4],6,"StatesGraph"]
Out[]=
In[]:=
TransitiveClosureGraph[%]
Out[]=
Axiom:
In[]:=
ResourceFunction["MultiwaySystem"][{"AB""BA","BA""AB"},ResourceFunction["StringTuples"]["AB",2],6,"StatesGraph"]
Out[]=
Add an axiom that says
{{x,y},{u,v}}{{StringJoin[x,u],StringJoin[y,v]},{x,y},{u,v}}

Rules of inference:

{{x,y},{u,v}}{{StringJoin[x,u],StringJoin[y,v]},{x,y},{u,v}}
{{x,y},{u,v}}{{SubstitutionSystem[uv][x],y},{x,y},{u,v}}
[[ may also need the replacement done on the second element ]]
In general, the second rule could be generating multiple outputs.....
{{x,y}}:>{{StringJoin[x,x],StringJoin[y,y]},{x,y}}

Implementation

{{x,y},{u,v}}{{StringJoin[x,u],StringJoin[y,v]},{x,y},{u,v}}
In[]:=
SubsetReplace[{{"A","B"},{"BA","AB"}},{{{x_,y_},{u_,v_}}Splice[{{StringJoin[x,u],StringJoin[y,v]},{x,y},{u,v}}],{{x_,y_}}Splice[{{StringJoin[x,x],StringJoin[y,y]},{x,y}}]}]
Out[]=
{{ABA,BAB},{A,B},{BA,AB}}
In[]:=
SubsetReplace[{{"A","B"},{"BA","AB"}},Reverse@{{{x_,y_},{u_,v_}}Splice[{{StringJoin[x,u],StringJoin[y,v]},{x,y},{u,v}}],{{x_,y_}}Splice[{{StringJoin[x,x],StringJoin[y,y]},{x,y}}]}]
Out[]=
{{AA,BB},{A,B},{BABA,ABAB},{BA,AB}}

“Free theorems”

In[]:=
NestList[SubsetReplace[#,Reverse@{{{x_,y_},{u_,v_}}Splice[{{StringJoin[x,u],StringJoin[y,v]},{x,y},{u,v}}],{{x_,y_}}Splice[{{StringJoin[x,x],StringJoin[y,y]},{x,y}}]}]&,{{"A","A"}},3]
Out[]=
{{{A,A}},{{AA,AA},{A,A}},{{AAAA,AAAA},{AA,AA},{AA,AA},{A,A}},{{AAAAAAAA,AAAAAAAA},{AAAA,AAAA},{AAAA,AAAA},{AA,AA},{AAAA,AAAA},{AA,AA},{AA,AA},{A,A}}}
In[]:=
NestList[SubsetReplace[#,Reverse@{{{x_,y_},{u_,v_}}Splice[{{StringJoin[x,u],StringJoin[y,v]},{x,y},{u,v}}],{{x_,y_}}Splice[{{StringJoin[x,x],StringJoin[y,y]},{x,y}}]}]&,{{"A","B"}},3]
Out[]=
{{{A,B}},{{AA,BB},{A,B}},{{AAAA,BBBB},{AA,BB},{AA,BB},{A,B}},{{AAAAAAAA,BBBBBBBB},{AAAA,BBBB},{AAAA,BBBB},{AA,BB},{AAAA,BBBB},{AA,BB},{AA,BB},{A,B}}}
In[]:=
NestList[SubsetReplace[#,Reverse@{{{x_,y_},{u_,v_}}Splice[{{StringJoin[x,u],StringJoin[y,v]},{x,y},{u,v}}],{{x_,y_}}Splice[{{StringJoin[x,x],StringJoin[y,y]},{x,y}}]}]&,{{"A","B"},{"A","A"},{"B","B"}},3]
Out[]=
{{{A,B},{A,A},{B,B}},{{AA,BB},{A,B},{AA,AA},{A,A},{BB,BB},{B,B}},{{AAAA,BBBB},{AA,BB},{AA,BB},{A,B},{AAAA,AAAA},{AA,AA},{AA,AA},{A,A},{BBBB,BBBB},{BB,BB},{BB,BB},{B,B}},{{AAAAAAAA,BBBBBBBB},{AAAA,BBBB},{AAAA,BBBB},{AA,BB},{AAAA,BBBB},{AA,BB},{AA,BB},{A,B},{AAAAAAAA,AAAAAAAA},{AAAA,AAAA},{AAAA,AAAA},{AA,AA},{AAAA,AAAA},{AA,AA},{AA,AA},{A,A},{BBBBBBBB,BBBBBBBB},{BBBB,BBBB},{BBBB,BBBB},{BB,BB},{BBBB,BBBB},{BB,BB},{BB,BB},{B,B}}}
[ This is only running the first rule ]

Adding substitution rule

In[]:=
NestList[SubsetReplace[#,Reverse@{​​{{x_,y_},{u_,v_}}Splice[{{StringJoin[x,u],StringJoin[y,v]},{x,y},{u,v}}],{{x_,y_}}Splice[{{StringJoin[x,x],StringJoin[y,y]},{x,y}}],​​{{x_,y_},{u_,v_}}Splice[{{Echo@StringReplace[x,Echo[uv]],y},{x,y},{u,v}}]​​}]&,{{"A","B"},{"A","A"},{"B","B"}},3]

Random rule application

Multiway version?

This is the spatial graph at this stage....
[[ We
Give it an obviously true fact, and it will generate other true facts......

Equivalence

Case 1: consider equalities (including axioms) to be represented by edges; then simply “apply all edges” using rules of inference in all possible ways

Initial condition consists of axioms and “obviously true” equalities [which can also be viewed as axioms]
The obviously true equalities contain “starting” LHS or RHSes of theorem
[ This is trivially causal invariant ]

Case 2: consider equalities to be represented by paths; axioms are “one-step paths”
[Is the transitive closure of #2 is the same as #1?]

Initial condition consists of all possible “starting” LHS or RHS

Rules of inference

[ Evaluation order is somewhat arbitrary, because of StringReplace ]
[[ We can also have a one-way version, not with equality, but e.g. with ordering ]]

Direct multiway system

Non-Fixed Length Example

[[[ Depends on the evaluation order which lemmas are applied at each step; this case is doing “generational” updates ]]]

Question: do we put lemmas “in the bag”?

Fuller Version [and CORRECT]

Case 1: Every edge represents an equality [equational logic]

The “state of the universe” is a collection of theorems, with each theorem corresponding to an edge.

Case 2: Equalities are represented by paths

[[[ Where are the self loops ? ]]]

Case 2a: Every edge is an equality

[[[ This is not an “ended system”; depends on evolution order ]]]

Beyond Duality

The reason for the duality above is that in case 1, “space” is just made of edges, just like a multiway graph is made of edges.
​
With different rules of inference, “space” could work differently.

Modus Ponens Inference

Only one input for each event.
modus ponens : A , A  B / B
Two-way inference is equivalence

Equational Proof Graph

Adding a critical pair lemma: {“ABAA”,”AAAB”}
OSZAR »