Combinators avoid variables

eq[p[x],q[y]]
eq[p[x]][q[y]]
Function[{eq,p,q,x,y},eq[p[x]][q[y]]]
In[]:=
Function[{eq,p,q,x,y},eq[p[x]][q[y]]][eq,p,q,x,y]
Out[]=
eq[p[x]][q[y]]

“Abstraction algorithm”

https://www.wolframscience.com/nks/notes-11-12--combinators/
In[]:=
ToC[expr_,vars_]:=Fold[rm,expr,Reverse[vars]]
In[]:=
rm[v_,v_]=s[k][k]
Out[]=
s[k][k]
In[]:=
rm[f_[v_],v_]/;FreeQ[f,v]=f
Out[]=
f
In[]:=
rm[h_,v_]/;FreeQ[h,v]=k[h]
Out[]=
k[h]
In[]:=
rm[f_[g_],v_]:=s[rm[f,v]][rm[g,v]]
In[]:=
ToC[x[y[x][z]],{x,y,z}]
Out[]=
s[s[k[s]][s[k[k]][s[k[s]][k]]]][s[k[s[s[k][k]]]][k]]
In[]:=
ToC[x[y],{x,y}]
Out[]=
s[k][k]
In[]:=
CombinatorEvolutionGraph[{s[x_][y_][z_]x[z][y[z]],k[x_][y_]x},s[k][k][x][y],4]
Out[]=
In[]:=
FixedPointList[#/.{s[x_][y_][z_]x[z][y[z]],k[x_][y_]x}&,s[k][k][x][y]]
Out[]=
{s[k][k][x][y],k[x][k[x]][y],x[y],x[y]}
In[]:=
FixedPointList[#/.{s[x_][y_][z_]x[z][y[z]],k[x_][y_]x}&,s[s[k[s]][s[k[k]][s[k[s]][k]]]][s[k[s[s[k][k]]]][k]][x][y][z]]
Out[]=
In[]:=
ToC[x[y[y]],{x,y}]
Out[]=
s[s[k[s]][k]][k[s[s[k][k]][s[k][k]]]]
In[]:=
FixedPointList[#/.{s[x_][y_][z_]x[z][y[z]],k[x_][y_]x}&,ToC[x[y[y]],{x,y}]]
Out[]=
{s[s[k[s]][k]][k[s[s[k][k]][s[k][k]]]],s[s[k[s]][k]][k[s[s[k][k]][s[k][k]]]]}
In[]:=
FixedPointList[#/.{s[x_][y_][z_]x[z][y[z]],k[x_][y_]x}&,s[s[k]][x][y]]
Out[]=
{s[s[k]][x][y],s[k][y][x[y]],k[x[y]][y[x[y]]],x[y],x[y]}

Goodstein sequences etc.

Their halting cannot be proved in Peano arithmetic

E.g. we could turn this into a question about the halting of a S,K combinator head, fed all possible inputs [or maybe Church numeral inputs]
In[]:=
Nest[s,k,6]
Out[]=
s[s[s[s[s[s[k]]]]]]
[[ What is the minimal TM whose halting cannot be proved in Peano arithmetic ? ]] [[ Peano arithmetic can only handle up to
ϵ
0
]]

What is the minimal universal lambda expression?

Minimal universal combinator

Emulation of lambda calculus by S, K is trivial
In[]:=
CombinatorEvolutionGraph[{e[x_][y_]x[y[y]]},e[e][e][e][e],13]
Out[]=
In[]:=
Groupings[Table[e,4],Construct2]
Out[]=
{e[e][e][e],e[e[e][e]],e[e[e]][e],e[e[e[e]]],e[e][e[e]]}
In[]:=
CombinatorEvolutionGraph[{e[x_][y_]x[y[y]]},#,12]&/@Groupings[Table[e,3],Construct2]
Out[]=

,

In[]:=
CombinatorEvolutionGraph[{e[x_][y_]x[y[y]]},#,8]&/@Groupings[Table[e,4],Construct2]
Out[]=
In[]:=
CombinatorEvolutionGraph[{e[x_][y_]x[y[y]]},#,12]&/@Groupings[Table[e,4],Construct2]
Out[]=
In[]:=
CombinatorEvolutionGraph[{e[x_][y_]x[y[y]]},#,8]&/@Groupings[Table[e,5],Construct2]
Out[]=

Systematic Search for Minimal Case

Size 2 RHSs

[[ Everything seems to have reached a fixed point ]]

Size 3 RHSs