Combinator Relations
Combinator Relations
Standard Combinators
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
Other combinators
“Rulogenic rules”
“Rulogenic rules”
[[ To be compared to the TEG for the same process ]]
“Non-rulogenic rules”
“Non-rulogenic rules”
Substitution Lemmas
Substitution Lemmas
[[ ?? does the branchial graph correctly only go one level up ?? ]]
Here every theorem is like a global state of the (physical) universe
Here every theorem is like a global state of the (physical) universe
Critical Pair Lemmas
Critical Pair Lemmas
[To what extent like genetic algorithm crossover ?]
Substitution
Substitution
can be applied anywhere in
[I.e. any subtree can independently have rulelhs exchange with rulerhs ]
General case
General case
Metamath
Metamath