Combinator Relations

Standard Combinators

[Code from Nik]
combinatorTree[comb_]:=If[Length[comb]==0,Tree[comb,{}],With[{head=combinatorTree[comb[[0]]],child=combinatorTree[comb[[1]]]},If[Length@TreeChildren[head]==0,Tree[TreeData@head,{child}],TreeInsert[head,child,-1]]​​]​​]
In[]:=
Map[ResourceFunction["CombinatorExpressionGraph"],formalizePatterns/@DeleteDuplicates@Catenate@Values@TwoWayMultiReplaceList[{S[a_][b_][c_]a_[c_][b_[c_]],K[a_][b_]a_},1,"Identity"->False,"Deduplicate"->True,"Canonicalize"->True,"SubstitutionLemmas"->False,"CriticalPairLemmas"->True,"Sample"->5],{2}]
Out[]=


,

,

,

,

,

,

,

,

,

,

,

,

,

,

,

,

,

,

,

,

,

,

,

,

,

,

,

,

,

,

,

,

,

,

,

,

,

,

,

,

,

,

,


In[]:=
Map[ResourceFunction["CombinatorExpressionGraph"],formalizePatterns/@DeleteDuplicates@Catenate@Values@TwoWayMultiReplaceList[{S[a_][b_][c_]a_[c_][b_[c_]]},1,"Identity"->False,"Deduplicate"->True,"Canonicalize"->True,"SubstitutionLemmas"->False,"CriticalPairLemmas"->True,"Sample"->5],{2}]
Out[]=


,

,

,

,

,

,

,

,

,

,

,

,

,

,

,

,

,

,

,


In[]:=
Map[ResourceFunction["CombinatorExpressionGraph"],formalizePatterns/@DeleteDuplicates@Catenate@Values@TwoWayMultiReplaceList[{S[a_][b_][c_]a_[c_][b_[c_]]},1,"Identity"->False,"Deduplicate"->True,"Canonicalize"->True,"SubstitutionLemmas"->False,"CriticalPairLemmas"->False,"Sample"->5],{2}]
Out[]=



In[]:=
Map[ResourceFunction["CombinatorExpressionGraph"],formalizePatterns/@DeleteDuplicates@Catenate@Values@TwoWayMultiReplaceList[{S[a_][b_][c_]a_[c_][b_[c_]]},2,"Identity"->False,"Deduplicate"->True,"Canonicalize"->True,"SubstitutionLemmas"->False,"CriticalPairLemmas"->False,"Sample"->5],{2}]
Out[]=



Random sample:::
In[]:=
Map[ResourceFunction["CombinatorExpressionGraph"],formalizePatterns/@DeleteDuplicates@Catenate@Values@TwoWayMultiReplaceList[{S[a_][b_][c_]a_[c_][b_[c_]]},2,"Identity"->False,"Deduplicate"->True,"Canonicalize"->True,"SubstitutionLemmas"->False,"CriticalPairLemmas"->True,"Sample"->5],{2}]

Other combinators

“Rulogenic rules”

[[ To be compared to the TEG for the same process ]]

“Non-rulogenic rules”

Substitution Lemmas

[[ ?? does the branchial graph correctly only go one level up ?? ]]

Here every theorem is like a global state of the (physical) universe

Critical Pair Lemmas

[To what extent like genetic algorithm crossover ?]

Substitution

can be applied anywhere in
[I.e. any subtree can independently have rulelhs exchange with rulerhs ]

General case

Metamath