In[]:=
ii=s[k][k]
Out[]=
s[k][k]
In[]:=
dd=s[ii][ii]
Out[]=
s[s[k][k]][s[k][k]]
In[]:=
k[s][dd[dd]]
Out[]=
k[s][s[s[k][k]][s[k][k]][s[s[k][k]][s[k][k]]]]
In[]:=
ResourceFunction["MultiwayCombinator"][k[s][s[s[k][k]][s[k][k]][s[s[k][k]][s[k][k]]]],2]
Out[]=
In[]:=
CombinatorEvaluateAll[s[s[s]][s][s][s][s],SKBasis,20]
Out[]=
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]][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[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]]]]]]]]
In[]:=
LeafCount/@CombinatorEvaluateAllSteps[s[s[s]][s][s][s][s[k]],SKBasis,100]
Out[]=
{8,8,9,9,12,13,14,16,22,33,51,19,30,41,53,66,104,110,99,137,175,214,254,373,379,368,380,392,405,419,460,516,522,511,567,623,680,738,911,952,896,910,916,905,919,933,948,964,1011,1058,996,1011,981,1045,1109,1030,1077,1013,1028,998,1079,1160,1064,1128,1047,1094,1030,1045,1015,1113,1211,1098,1179,1081,1145,1064,1111,1047,1062,1032,1147,1262,1132,1230,1115,1196,1098,1162,1081,1128,1064,1079,1049,1181,1313,1166,1281,1149,1247,1132}
In[]:=
ListLinePlot[%]
Out[]=
In[]:=
Depth[%]
Out[]=
8
In[]:=
LeafCount/@CombinatorEvaluateAllSteps[s[s[s[s]]][s][s][s][k],SKBasis,1000];
In[]:=
ListLinePlot[%]
Out[]=
In[]:=
ListLinePlot[LeafCount/@NestList[#/.SKBasis&,s[s[s[s]]][s][s][s][k],40]]
Out[]=
In[]:=
ListLinePlot[LeafCount/@CombinatorEvaluateAllSteps[s[s[s[s]]][s][s][s][k],SKBasis,40]]
Out[]=
Lambda
Lambda
In[]:=
LambdaToSK[Lambda[{x},x[x]]]
Out[]=
s[s[k][k]][s[k][k]]
LambdaToSK[Lambda[{x},x[x]]]
In[]:=
LambdaToSK[Lambda[{x},x[x[x]]]]
Out[]=
s[s[k][k]][s[s[k][k]][s[k][k]]]
In[]:=
LambdaToSK[Lambda[{x,y},x[x[y]]]]
Out[]=
s[s[k[s]][s[k[k]][s[k][k]]]][s[s[k[s]][s[k[k]][s[k][k]]]][s[s[k[s]][k[k]]][k[k]]]]
In[]:=
LambdaEvaluateAllSteps[Lambda[{x,y},x[x[y]]][Lambda[{x,y},x[x[y]]]],10]
Out[]=
{Lambda[{x,y},x[x[y]]][Lambda[{x,y},x[x[y]]]],Lambda[{y},Lambda[{x,y},x[x[y]]][Lambda[{x,y},x[x[y]]][y]]],Lambda[{y},Lambda[{y$63103},Lambda[{x,y},x[x[y]]][y][Lambda[{x,y},x[x[y]]][y][y$63103]]]],Lambda[{y},Lambda[{y$63103},Lambda[{y$63104},y[y[y$63104]]][Lambda[{x,y},x[x[y]]][y][y$63103]]]],Lambda[{y},Lambda[{y$63103},y[y[Lambda[{x,y},x[x[y]]][y][y$63103]]]]],Lambda[{y},Lambda[{y$63103},y[y[Lambda[{y$63105},y[y[y$63105]]][y$63103]]]]],Lambda[{y},Lambda[{y$63103},y[y[y[y[y$63103]]]]]]}
In[]:=
LambdaEvaluateAllSteps[Lambda[{x,y},x[x[y]]][Lambda[{x,y},x[x[y]]]],20]
Out[]=
{Lambda[{x,y},x[x[y]]][Lambda[{x,y},x[x[y]]]],Lambda[{y},Lambda[{x,y},x[x[y]]][Lambda[{x,y},x[x[y]]][y]]],Lambda[{y},Lambda[{y$63109},Lambda[{x,y},x[x[y]]][y][Lambda[{x,y},x[x[y]]][y][y$63109]]]],Lambda[{y},Lambda[{y$63109},Lambda[{y$63110},y[y[y$63110]]][Lambda[{x,y},x[x[y]]][y][y$63109]]]],Lambda[{y},Lambda[{y$63109},y[y[Lambda[{x,y},x[x[y]]][y][y$63109]]]]],Lambda[{y},Lambda[{y$63109},y[y[Lambda[{y$63111},y[y[y$63111]]][y$63109]]]]],Lambda[{y},Lambda[{y$63109},y[y[y[y[y$63109]]]]]]}
In[]:=
LeafCount/@%
Out[]=
{14,18,23,21,17,15,11}
In[]:=
ee=Lambda[{x,y},x[x[y]]];
In[]:=
LeafCount/@LambdaEvaluateAllSteps[ee[ee[ee]],50]
Out[]=
{21,32,36,32,51,63,59,63,59,64,60,58,54,52,48,52,48,53,49,47,43,41,37,49,45,49,45,50,46,44,40,38,34,38,34,39,35,33,29,27,23}
In[]:=
LambdaToNum/@LambdaEvaluateAllSteps[ee[ee[ee]],50]
Out[]=
{16,16,16,16,16,16,16,16,16,16,16,16,16,16,16,16,16,16,16,16,16,16,16,16,16,16,16,16,16,16,16,16,16,16,16,16,16,16,16,16,16}
In[]:=
zero
Out[]=
Lambda[{g,x},x]
In[]:=
LambdaEvaluateAll[succ[zero]]
Out[]=
Lambda[{g,x},g[x]]
In[]:=
LambdaEvaluateAll[Nest[succ,zero,5]]
Out[]=
Lambda[{g,x},g[g[g[g[g[x]]]]]]
In[]:=
Groupings[{s,s,s,s,k,k},Construct2]
Out[]=
{s[s][s][s][k][k],s[s[s][s][k][k]],s[s[s][s][k]][k],s[s[s[s][k][k]]],s[s[s][s]][k][k],s[s[s[s][k]][k]],s[s[s[s][k]]][k],s[s[s[s[k][k]]]],s[s[s]][s][k][k],s[s[s[s]][k][k]],s[s[s[s]][k]][k],s[s[s[s[k]][k]]],s[s[s[s]]][k][k],s[s[s[s[k]]][k]],s[s[s[s[k]]]][k],s[s[s[s[k[k]]]]],s[s][s[s]][k][k],s[s[s][s[k]][k]],s[s[s][s[k]]][k],s[s[s[s][k[k]]]],s[s][s][s[k]][k],s[s[s][s][k[k]]],s[s][s[s][k]][k],s[s[s][s[k][k]]],s[s[s]][s[k]][k],s[s[s[s]][k[k]]],s[s][s[s[k]]][k],s[s[s][s[k[k]]]],s[s][s][s][k[k]],s[s][s[s][k][k]],s[s[s][s]][k[k]],s[s][s[s[k][k]]],s[s[s]][s][k[k]],s[s][s[s[k]][k]],s[s[s[s]]][k[k]],s[s][s[s[k[k]]]],s[s][s[s]][k[k]],s[s][s[s][k[k]]],s[s][s][s[k][k]],s[s][s][s[k[k]]],s[s[s]][s[k][k]],s[s[s]][s[k[k]]]}
Known Universal Combinators
Known Universal Combinators
William Craig: to simulate S,K you need two combinators [one being a selector, like K] (at least for proper combinators)
https://www.wolframscience.com/nks/notes-11-12--testing-universality-in-symbolic-systems/
“Improper combinator”
“Improper combinator”
https://www.wolframscience.com/nks/notes-11-12--single-universal-combinators/
Proper Combinators
Proper Combinators
Single variable
Single variable
Matthew claims that none of these can do anything interesting....
e[e] evaluates to the rhs /. x->e
Two Variables
Two Variables
n x’s and m y’s in any order
This applies improperly, only picking up the x’s
This applies improperly, only picking up the x’s
Proper application
Proper application
[ WRONG ] Church numeral for 2
[ WRONG ] Church numeral for 2
NKS page 102
Candidate
Candidate
Candidates: {x[x[y][y]],x[x[y]][y],x[y[x[y]]]}
Candidates: {x[x[y][y]],x[x[y]][y],x[y[x[y]]]}
y[x[y[x]]]
y[x[y[x]]]