You are using a browser not supported by the Wolfram Cloud
Supported browsers include recent versions of Chrome, Edge, Firefox and Safari.
I understand and wish to continue anyway »
WOLFRAM NOTEBOOK
From Jonathan:
From Jonathan:
In[]:=
convertStringToOperator[string_String]:=Module[{expression,list},list=StringSplit[string,""];expression=list;While[Length[list]>1,expression=expression/.list(CenterDot[First[list],Rest[list]]);list=Rest[list]];expression/.listFirst[list]]FindStringProof[theorems_List,axioms_List]:=Module[{stringTheorems,stringAxioms},stringTheorems=(convertStringToOperator[First[#]]==convertStringToOperator[Last[#]])&/@theorems;stringAxioms=(convertStringToOperator[First[#]]==convertStringToOperator[Last[#]])&/@axioms;FindEquationalProof[stringTheorems,Join[{stringAxioms,ForAll[{a,b,c},CenterDot[a,CenterDot[b,c]]CenterDot[CenterDot[a,b],c]]}]]]FindStringProof[theorem_,axioms_List]:=FindStringProof[{theorem},axioms]/;!ListQ[theorem]FindStringProof[theorems_List,axiom_]:=FindStringProof[theorems,{axiom}]/;!ListQ[axiom]FindStringProof[theorem_,axiom_]:=FindStringProof[{theorem},{axiom}]/;(!ListQ[theorem]&&!ListQ[axiom])
In[]:=
FindStringProof[{"AA""AABBBB"},{"A""AB"}]
Out[]=
ProofObject
In[]:=
%["ProofGraph"]
Out[]=
More
More
Proof Diagram
Proof Diagram
In[]:=
StringProofDiagram[statements_,axioms_]:=With[{pf=FindStringProof[statements,axioms]},Graph[pf["ProofGraph"],VertexLabels->Thread[VertexList[pf["ProofGraph"]]->Map[#/.(s_Symbol:>ToString[StandardForm[Style[If[s=!=True,Subscript[StringTake[SymbolName[s],1],StringDrop[SymbolName[s],1]],True],Italic,Gray]]])&,Normal[Values[pf["ProofDataset"][All,"Statement"]]],{-1}]/.EqualLongLeftRightArrow/.CenterDotStringJoin],VertexSizeSmall]]
In[]:=
Graph[StringProofDiagram[{"AA""AABBBB"},{"A""AB"}]]
Out[]=
In[]:=
ResourceFunction["MultiwaySystem"][{"A""AB"},"AA",5,"StatesGraph"]
Out[]=
Causal Invariant Case
Causal Invariant Case
In[]:=
ResourceFunction["MultiwaySystem"][{"A""BBB","BB""A"},"A",5,"StatesGraph"]
Out[]=
In[]:=
StringProofDiagram[{"A""AA"},{"A""BBB","BB""A"}]
Out[]=
NKS Book Case
NKS Book Case
(This doesn’t seem to involve the very shortest strings)
Long Path Cases
Long Path Cases
Consider Equational Multiway Systems
Consider Equational Multiway Systems
Model Theory for Strings
Model Theory for Strings
Allow any x·y for any k-ary function, assuming it is associative......
[ Think of in terms of a monoid FSM ? ]