Find equivalence classes ; compare with actual entailments....
In[]:=
allexprs=Flatten[Table[Groupings[Tuples[{a,b},n],SmallCircle->2],{n,1,3}]]
Out[]=
{a,b,a∘a,a∘b,b∘a,b∘b,(a∘a)∘a,(a∘a)∘b,(a∘b)∘a,(a∘b)∘b,(b∘a)∘a,(b∘a)∘b,(b∘b)∘a,(b∘b)∘b,a∘(a∘a),a∘(a∘b),a∘(b∘a),a∘(b∘b),b∘(a∘a),b∘(a∘b),b∘(b∘a),b∘(b∘b)}
In[]:=
allax=Rest[Cases[Equal@@@Tuples[Flatten[Table[Groupings[Tuples[{x,y},n],SmallCircle->2],{n,1,3}]],2],_Equal]]
In[]:=
ResourceFunction["FindFiniteModels"][#,2]&/@Take[allax,10]
Out[]=
{{1}SmallCircle{{0,0},{0,1}},{3}SmallCircle{{0,0},{1,1}},{5}SmallCircle{{0,1},{0,1}},{7}SmallCircle{{0,1},{1,1}},{3}SmallCircle{{0,0},{1,1}},{5}SmallCircle{{0,1},{0,1}},,{1}SmallCircle{{0,0},{0,1}},{3}SmallCircle{{0,0},{1,1}},{4}SmallCircle{{0,1},{0,0}},{5}SmallCircle{{0,1},{0,1}},{6}SmallCircle{{0,1},{1,0}},{7}SmallCircle{{0,1},{1,1}},{9}SmallCircle{{1,0},{0,1}},{12}SmallCircle{{1,1},{0,0}},{13}SmallCircle{{1,1},{0,1}},{3}SmallCircle{{0,0},{1,1}},{12}SmallCircle{{1,1},{0,0}},{3}SmallCircle{{0,0},{1,1}},{4}SmallCircle{{0,1},{0,0}},{5}SmallCircle{{0,1},{0,1}},{12}SmallCircle{{1,1},{0,0}},{13}SmallCircle{{1,1},{0,1}},{3}SmallCircle{{0,0},{1,1}},{6}SmallCircle{{0,1},{1,0}},{9}SmallCircle{{1,0},{0,1}},{12}SmallCircle{{1,1},{0,0}},{5}SmallCircle{{0,1},{0,1}},{6}SmallCircle{{0,1},{1,0}},{9}SmallCircle{{1,0},{0,1}}}
In[]:=
ExprsByModel[exprs_,mat_]:=GroupBy[exprs,FromDigits[Flatten[ApplyFiniteModel[#,SmallCircle->mat,{a,b}]],2]&]
In[]:=
ExprsByModel[allexprs,{{0,0},{1,1}}]
Out[]=
3{a,a∘a,a∘b,(a∘a)∘a,(a∘a)∘b,(a∘b)∘a,(a∘b)∘b,a∘(a∘a),a∘(a∘b),a∘(b∘a),a∘(b∘b)},5{b,b∘a,b∘b,(b∘a)∘a,(b∘a)∘b,(b∘b)∘a,(b∘b)∘b,b∘(a∘a),b∘(a∘b),b∘(b∘a),b∘(b∘b)}
#[SmallCircle]&/@Values[{3}SmallCircle{{0,0},{1,1}},{12}SmallCircle{{1,1},{0,0}}]
Out[]=
{{{0,0},{1,1}},{{1,1},{0,0}}}
ApplyFiniteModel[]
ApplyFiniteModel[#,SmallCircle->{{0,1},{0,1}},{a,b}]
In[]:=
#->Association[(FromDigits[Flatten[#],2]->ExprsByModel[allexprs,#]&/@(#[SmallCircle]&/@Values[ResourceFunction["FindFiniteModels"][#,2]]))]&/@Take[allax,10]
Out[]=
In[]:=
Cases[Equal@@@Tuples[{a,a∘a,a∘b,(a∘a)∘a,(a∘a)∘b,(a∘b)∘a,(a∘b)∘b,a∘(a∘a),a∘(a∘b),a∘(b∘a),a∘(b∘b)},2],_Equal]
Out[]=
In[]:=
ParallelMap[FindEquationalProof[#,ForAll[{x,y},xx∘y],TimeConstraint2]&,%423]
All true....
x(x∘y)∘x33{a,a∘a,a∘b,(a∘a)∘a,(a∘a)∘b,(a∘b)∘a,(a∘b)∘b,a∘(a∘a),a∘(a∘b),a∘(b∘a),a∘(b∘b)},5{b,b∘a,b∘b,(b∘a)∘a,(b∘a)∘b,(b∘b)∘a,(b∘b)∘b,b∘(a∘a),b∘(a∘b),b∘(b∘a),b∘(b∘b)},43{a,(a∘a)∘a,(a∘b)∘a,(b∘b)∘a},5{b,(a∘a)∘b,(b∘a)∘b,(b∘b)∘b},0{a∘a,b∘b,a∘(a∘a),a∘(b∘a),a∘(b∘b),b∘(a∘a),b∘(a∘b),b∘(b∘b)},4{a∘b,a∘(a∘b)},2{b∘a,b∘(b∘a)},1{(a∘b)∘b,(b∘a)∘a},53{a,a∘a,b∘a,(a∘a)∘a,(a∘b)∘a,(b∘a)∘a,(b∘b)∘a,a∘(a∘a),a∘(b∘a),b∘(a∘a),b∘(b∘a)},5{b,a∘b,b∘b,(a∘a)∘b,(a∘b)∘b,(b∘a)∘b,(b∘b)∘b,a∘(a∘b),a∘(b∘b),b∘(a∘b),b∘(b∘b)},123{a,(a∘a)∘a,(a∘a)∘b,(a∘b)∘a,(a∘b)∘b},5{b,(b∘a)∘a,(b∘a)∘b,(b∘b)∘a,(b∘b)∘b},12{a∘a,a∘b,a∘(a∘a),a∘(a∘b),a∘(b∘a),a∘(b∘b)},10{b∘a,b∘b,b∘(a∘a),b∘(a∘b),b∘(b∘a),b∘(b∘b)},133{a,(a∘a)∘a,(a∘b)∘a,(b∘b)∘a},5{b,(a∘a)∘b,(b∘a)∘b,(b∘b)∘b},15{a∘a,b∘b,a∘(a∘a),a∘(b∘a),a∘(b∘b),b∘(a∘a),b∘(a∘b),b∘(b∘b)},13{a∘b,a∘(a∘b)},11{b∘a,b∘(b∘a)},7{(a∘b)∘b,(b∘a)∘a}
In[]:=
Length/@33{a,a∘a,a∘b,(a∘a)∘a,(a∘a)∘b,(a∘b)∘a,(a∘b)∘b,a∘(a∘a),a∘(a∘b),a∘(b∘a),a∘(b∘b)},5{b,b∘a,b∘b,(b∘a)∘a,(b∘a)∘b,(b∘b)∘a,(b∘b)∘b,b∘(a∘a),b∘(a∘b),b∘(b∘a),b∘(b∘b)},43{a,(a∘a)∘a,(a∘b)∘a,(b∘b)∘a},5{b,(a∘a)∘b,(b∘a)∘b,(b∘b)∘b},0{a∘a,b∘b,a∘(a∘a),a∘(b∘a),a∘(b∘b),b∘(a∘a),b∘(a∘b),b∘(b∘b)},4{a∘b,a∘(a∘b)},2{b∘a,b∘(b∘a)},1{(a∘b)∘b,(b∘a)∘a},53{a,a∘a,b∘a,(a∘a)∘a,(a∘b)∘a,(b∘a)∘a,(b∘b)∘a,a∘(a∘a),a∘(b∘a),b∘(a∘a),b∘(b∘a)},5{b,a∘b,b∘b,(a∘a)∘b,(a∘b)∘b,(b∘a)∘b,(b∘b)∘b,a∘(a∘b),a∘(b∘b),b∘(a∘b),b∘(b∘b)},123{a,(a∘a)∘a,(a∘a)∘b,(a∘b)∘a,(a∘b)∘b},5{b,(b∘a)∘a,(b∘a)∘b,(b∘b)∘a,(b∘b)∘b},12{a∘a,a∘b,a∘(a∘a),a∘(a∘b),a∘(b∘a),a∘(b∘b)},10{b∘a,b∘b,b∘(a∘a),b∘(a∘b),b∘(b∘a),b∘(b∘b)},133{a,(a∘a)∘a,(a∘b)∘a,(b∘b)∘a},5{b,(a∘a)∘b,(b∘a)∘b,(b∘b)∘b},15{a∘a,b∘b,a∘(a∘a),a∘(b∘a),a∘(b∘b),b∘(a∘a),b∘(a∘b),b∘(b∘b)},13{a∘b,a∘(a∘b)},11{b∘a,b∘(b∘a)},7{(a∘b)∘b,(b∘a)∘a}
Out[]=
32,46,52,124,136
In[]:=
33{a,a∘a,a∘b,(a∘a)∘a,(a∘a)∘b,(a∘b)∘a,(a∘b)∘b,a∘(a∘a),a∘(a∘b),a∘(b∘a),a∘(b∘b)},5{b,b∘a,b∘b,(b∘a)∘a,(b∘a)∘b,(b∘b)∘a,(b∘b)∘b,b∘(a∘a),b∘(a∘b),b∘(b∘a),b∘(b∘b)},43{a,(a∘a)∘a,(a∘b)∘a,(b∘b)∘a},5{b,(a∘a)∘b,(b∘a)∘b,(b∘b)∘b},0{a∘a,b∘b,a∘(a∘a),a∘(b∘a),a∘(b∘b),b∘(a∘a),b∘(a∘b),b∘(b∘b)},4{a∘b,a∘(a∘b)},2{b∘a,b∘(b∘a)},1{(a∘b)∘b,(b∘a)∘a},53{a,a∘a,b∘a,(a∘a)∘a,(a∘b)∘a,(b∘a)∘a,(b∘b)∘a,a∘(a∘a),a∘(b∘a),b∘(a∘a),b∘(b∘a)},5{b,a∘b,b∘b,(a∘a)∘b,(a∘b)∘b,(b∘a)∘b,(b∘b)∘b,a∘(a∘b),a∘(b∘b),b∘(a∘b),b∘(b∘b)},123{a,(a∘a)∘a,(a∘a)∘b,(a∘b)∘a,(a∘b)∘b},5{b,(b∘a)∘a,(b∘a)∘b,(b∘b)∘a,(b∘b)∘b},12{a∘a,a∘b,a∘(a∘a),a∘(a∘b),a∘(b∘a),a∘(b∘b)},10{b∘a,b∘b,b∘(a∘a),b∘(a∘b),b∘(b∘a),b∘(b∘b)},133{a,(a∘a)∘a,(a∘b)∘a,(b∘b)∘a},5{b,(a∘a)∘b,(b∘a)∘b,(b∘b)∘b},15{a∘a,b∘b,a∘(a∘a),a∘(b∘a),a∘(b∘b),b∘(a∘a),b∘(a∘b),b∘(b∘b)},13{a∘b,a∘(a∘b)},11{b∘a,b∘(b∘a)},7{(a∘b)∘b,(b∘a)∘a}[4]
Out[]=
3{a,(a∘a)∘a,(a∘b)∘a,(b∘b)∘a},5{b,(a∘a)∘b,(b∘a)∘b,(b∘b)∘b},0{a∘a,b∘b,a∘(a∘a),a∘(b∘a),a∘(b∘b),b∘(a∘a),b∘(a∘b),b∘(b∘b)},4{a∘b,a∘(a∘b)},2{b∘a,b∘(b∘a)},1{(a∘b)∘b,(b∘a)∘a}
In[]:=
CheckEquiv[axiom_,assoc_]:=ParallelMap[FindEquationalProof[#,ForAll[{x,y},axiom],TimeConstraint1]&,(Cases[Equal@@@Tuples[#,2],_Equal])]&/@assoc
This is for the case of 13:
In[]:=
CheckEquiv[x(x∘y)∘x,3{a,(a∘a)∘a,(a∘b)∘a,(b∘b)∘a},5{b,(a∘a)∘b,(b∘a)∘b,(b∘b)∘b},0{a∘a,b∘b,a∘(a∘a),a∘(b∘a),a∘(b∘b),b∘(a∘a),b∘(a∘b),b∘(b∘b)},4{a∘b,a∘(a∘b)},2{b∘a,b∘(b∘a)},1{(a∘b)∘b,(b∘a)∘a}]
Out[]=
In[]:=
ParallelMap[#->FindEquationalProof[#,ForAll[{x,y},x(x∘y)∘x],TimeConstraint1]&,(Cases[Equal@@@Tuples[{a,(a∘a)∘a,(a∘b)∘a,(b∘b)∘a},2],_Equal])]
Out[]=
a(a∘a)∘aProofObject,a(a∘b)∘aProofObject,a(b∘b)∘aFailure,(a∘a)∘aaProofObject,(a∘a)∘a(a∘b)∘aProofObject,(a∘a)∘a(b∘b)∘aFailure,(a∘b)∘aaProofObject,(a∘b)∘a(a∘a)∘aProofObject,(a∘b)∘a(b∘b)∘aFailure,(b∘b)∘aaFailure,(b∘b)∘a(a∘a)∘aFailure,(b∘b)∘a(a∘b)∘aFailure
In[]:=
ParallelMap[#->FindEquationalProof[#,ForAll[{x,y},x(x∘y)∘x],TimeConstraint2]&,(Cases[Equal@@@Tuples[{a,(a∘a)∘a,(a∘b)∘a,(b∘b)∘a},2],_Equal])]
Out[]=
a(a∘a)∘aProofObject,a(a∘b)∘aProofObject,a(b∘b)∘aFailure,(a∘a)∘aaProofObject,(a∘a)∘a(a∘b)∘aProofObject,(a∘a)∘a(b∘b)∘aFailure,(a∘b)∘aaProofObject,(a∘b)∘a(a∘a)∘aProofObject,(a∘b)∘a(b∘b)∘aFailure,(b∘b)∘aaFailure,(b∘b)∘a(a∘a)∘aFailure,(b∘b)∘a(a∘b)∘aFailure
x∘ y==(y∘x)∘y
x∘ y==(y∘x)∘y
Incomplete Models
Incomplete Models
If you have a complete model then expressions with different model codes must be different.
If the model is incomplete, then even different models code could actually be the same...
If the model is incomplete, then even different models code could actually be the same...
Within each bucket, which equivalences are correct ; but the underlying model is complete, there can no cross-code equivalences...
We want a community plot of connections within each bucket, and between buckets.... A good model has a complete graph of equivalences within a bucket.
Cleaner version
Cleaner version
Generate statements
Valid model: