Map[FunctionToApplication,{s[x_][y_][z_]x[z][y[z]],k[x_][y_]x},{2}]
In[]:=
s[Application]x_[Application]y_[Application]z_x[Application]z[Application]y[Application]z,k[Application]x_[Application]y_x
Out[]=
ResourceFunction["FindFiniteModels"][((b.·c.)·a.)·(b.·((b.·a.)·b.))a.,2]
In[]:=
{8}CenterDot{{1,0},{0,0}},{14}CenterDot{{1,1},{1,0}}
Out[]=
ResourceFunction["FindFiniteModels"][s[][Application]x[Application]y[Application]z==x[Application]z[Application]y[Application]z,k[][Application]x[Application]y==x,2]
In[]:=

Out[]=
ResourceFunction["FindFiniteModels"][s[][Application]x[Application]y[Application]z==x[Application]z[Application]y[Application]z,k[][Application]x[Application]y==x,3]
In[]:=

Out[]=
ResourceFunction["FindFiniteModels"][s[][Application]x[Application]y[Application]z==x[Application]z[Application]y[Application]z,k[][Application]x[Application]y==x,4,"Parallelize"True]
In[]:=
SubKernels`SubKernels
::timekernels
:Timeout for subkernels. Received only 9 of 12 connections.

Out[]=
ResourceFunction["FindFiniteModels"][k[][Application]x[Application]y==x,2]
In[]:=

Out[]=
ResourceFunction["FindFiniteModels"][k[][Application]x[Application]y==x,3]
In[]:=

Out[]=
ResourceFunction["FindFiniteModels"][k[][Application]x[Application]y==x,4]
In[]:=

Out[]=
ResourceFunction["FindFiniteModels"][k[][Application]x[Application]y==x,5]
In[]:=

Out[]=
ResourceFunction["FindFiniteModels"][k[][Application]x[Application]y==x,6]
In[]:=

Out[]=
ResourceFunction["FindFiniteModels"][s[][Application]x[Application]y[Application]z==x[Application]z[Application]y[Application]z,2]
In[]:=
{0,0}Application{{0,0},{0,0}},s0,{0,1}Application{{0,0},{0,0}},s1,{1,1}Application{{0,0},{0,1}},s1,{5,0}Application{{0,1},{0,1}},s0,{5,1}Application{{0,1},{0,1}},s1,{7,0}Application{{0,1},{1,1}},s0,{15,0}Application{{1,1},{1,1}},s0,{15,1}Application{{1,1},{1,1}},s1
Out[]=
Length[%149]
In[]:=
8
Out[]=
ResourceFunction["FindFiniteModels"][s[][Application]x[Application]y[Application]z==x[Application]z[Application]y[Application]z,3]
In[]:=
Out[]=
Length[%]
In[]:=
285
Out[]=
Previous Approach
Function[tab,TestTreeEvaluate[Map[TreeEvaluate[#,tab]&,EquivalenceGroups[6],{2}]]][{{2,1},{2,2}}]
In[]:=
True
Out[]=
Function[tab,TestTreeEvaluate[Map[TreeEvaluate[#,tab]&,EquivalenceGroups[7],{2}]]][{{2,1},{2,2}}]
In[]:=
True
Out[]=
Function[tab,TestTreeEvaluate[Map[TreeEvaluate[#,tab]&,EquivalenceGroups[8],{2}]]][{{2,1},{2,2}}]
In[]:=
True
Out[]=
Function[tab,TestTreeEvaluate[Map[TreeEvaluate[#,tab]&,EquivalenceGroups[9],{2}]]][{{2,1},{2,2}}]
In[]:=
True
Out[]=
Function[tab,TestTreeEvaluate[Map[TreeEvaluate[#,tab]&,EquivalenceGroups[10],{2}]]][{{2,1},{2,2}}]
In[]:=
False
Out[]=
TestTreeEvaluate[%163]
In[]:=
False
Out[]=
AllTrue[%163,Apply[SameQ]]
In[]:=
False
Out[]=
%163[[878]]
In[]:=
{1,1,1,2}
Out[]=
EquivalenceGroups[10][[878]]
In[]:=
{s[s[s]][s[s[s[s]][s]][s][s]],s[s[s]][s[s][s][s[s]][s[s]]],s[s[s]][s[s[s]][s][s][s[s]]],s[s][s[s[s]][s[s[s]]]][s[s]]}
Out[]=
Position[Apply[SameQ]/@%163,False]
In[]:=
{{878}}
Out[]=
SCombinatorAutomatonTreeGeneral[#,Application[x_,y_]({{2,1},{2,2}}[[x,y]]),1,VertexSize.6,ImageSize{UpTo[120],UpTo[120]}]&/@{s[s[s]][s[s[s]][s][s][s[s]]],s[s][s[s[s]][s[s[s]]]][s[s]]}
In[]:=

,

Out[]=
What happens if we look at larger combinator expressions? It keeps working---until we get to two particular size-10 expressions, which have the same fixed point, but different “values”:

,

Out[]=
CombinatorFixedPointList/@{s[s[s]][s[s[s]][s][s][s[s]]],s[s][s[s[s]][s[s[s]]]][s[s]]}
In[]:=
{{s[s[s]][s[s[s]][s][s][s[s]]],s[s[s]][s[s][s][s[s]][s[s]]],s[s[s]][s[s[s]][s[s[s]]][s[s]]],s[s[s]][s[s][s[s]][s[s[s]][s[s]]]],s[s[s]][s[s[s[s]][s[s]]][s[s][s[s[s]][s[s]]]]]},{s[s][s[s[s]][s[s[s]]]][s[s]],s[s[s]][s[s[s]][s[s[s]]][s[s]]],s[s[s]][s[s][s[s]][s[s[s]][s[s]]]],s[s[s]][s[s[s[s]][s[s]]][s[s][s[s[s]][s[s]]]]]}}
Out[]=
Length/@%
In[]:=
{5,4}
Out[]=
Map[TreeEvaluate[#,{{2,1},{2,2}}]&,EquivalenceGroups[10],{2}]
In[]:=
Max[%166]
In[]:=
2
Out[]=
Position[%166,2]
In[]:=
{{878}}
Out[]=
EquivalenceGroups[13]//Length
In[]:=
36735
Out[]=
ResourceFunction["ParallelMapMonitored"][Function[tab,TestTreeEvaluate[Map[TreeEvaluate[#,tab]&,EquivalenceGroups[13],{2}]]],{{{2,3,2},{2,2,2},{2,2,1}},{{3,3,2},{3,1,3},{3,3,3}}}]
In[]:=
{False,False}
Out[]=
Length[Union[#]]&/@Map[TreeEvaluate[#,{{2,3,2},{2,2,2},{2,2,1}}]&,EquivalenceGroups[13],{2}]
In[]:=
{1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,
⋯36533⋯
,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1}
large output
show less
show more
show all
set size limit...
Out[]=