Formulating axioms as combinator rules
Formulating axioms as combinator rules
s[k[s]][s[k[s[k[s]]]][k]]
Nest[s[s[k[s]][k]],s[k],n]
{s[x_][y_][z_]->x[z][y[z]],k[x_][y_]->x}
Semigroup theory in combinators?
Semigroup theory in combinators?
For some combinator “dot” this would be true for all subtrees a, b, c
dot[a][dot[b][c]]==dot[dot[a][b]][c]
Equality can be thought of in terms of expression paths here....
The idea of relations is an axiomatic-level idea
The idea of relations is an axiomatic-level idea
is a knitting of expressions which is basically “spatial”
Two things end up being equivalent if they evolve to the same thing...
Two things end up being equivalent if they evolve to the same thing...
Univalence they can be considered equal
Univalence they can be considered equal
Coarse-graining an evolution graph ⟶ an equivalence statement
Coarse-graining an evolution graph ⟶ an equivalence statement
Do equivalence statements combine e.g. by substitution inevitably?
Do equivalence statements combine e.g. by substitution inevitably?
In the graph, AA == BAAB
In[]:=
Graph[With[{g=Graph[ResourceFunction["MultiwaySystem"][{"A""AA","A""BAAB"},"A",5,"StatesGraphStructure"],AspectRatio->1.5]},GraphUnion@@(PathGraph[#,DirectedEdgesTrue]&/@FindPath[g,"A","BAABAABAAB",All,All])],VertexLabelsAutomatic]
Out[]=
If AA==BAAB and AA == AAA what follows?
How do we derive laws of inference for statements [i.e. entailment for statements]
How do we derive laws of inference for statements [i.e. entailment for statements]
Assume that equality/two-way-ruleness is just shared future
Assume that equality/two-way-ruleness is just shared future
The evolutions converge:
e[x]==e[y]
We will write this as: x == y or x y
e[x]==e[y],e[a]==e[b]
e["AA"]==e["BAAB"]
e["AA"]==e["AAA"]
Usually substitution would imply
e["AAA"]==e["BAAB"]
If a and b converge to the same thing, and b and c converge to the same thing, does it follow that a and c must converge to the same thing?