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

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

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

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

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[uv][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:

Rules of inference:

{{x,y},{u,v}}{{StringJoin[x,u],StringJoin[y,v]},{x,y},{u,v}}

{{x,y},{u,v}}{{SubstitutionSystem[uv][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

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”

“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

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[uv]],y},{x,y},{u,v}}]}]&,{{"A","B"},{"A","A"},{"B","B"}},3]

### Random rule application

Random rule application

#### Multiway version?

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

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

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

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?]

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?]

[Is the transitive closure of #2 is the same as #1?]

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

### Rules of inference

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

Direct multiway system

## Non-Fixed Length Example

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”?

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

## Fuller Version [and CORRECT]

Fuller Version [and CORRECT]

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

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

Case 2: Equalities are represented by paths

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

#### Case 2a: Every edge is an equality

Case 2a: Every edge is an equality

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

## Beyond Duality

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.

With different rules of inference, “space” could work differently.

## Modus Ponens Inference

Modus Ponens Inference

Only one input for each event.

modus ponens : A , A B / B

Two-way inference is equivalence

## Equational Proof Graph

Equational Proof Graph

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