Combinators avoid variables
Combinators avoid variables
eq[p[x],q[y]]
eq[p[x]][q[y]]
Function[{eq,p,q,x,y},eq[p[x]][q[y]]]
Function[{eq,p,q,x,y},eq[p[x]][q[y]]][eq,p,q,x,y]
In[]:=
eq[p[x]][q[y]]
Out[]=
“Abstraction algorithm”
“Abstraction algorithm”
https://www.wolframscience.com/nks/notes-11-12--combinators/
ToC[expr_,vars_]:=Fold[rm,expr,Reverse[vars]]
In[]:=
rm[v_,v_]=s[k][k]
In[]:=
s[k][k]
Out[]=
rm[f_[v_],v_]/;FreeQ[f,v]=f
In[]:=
f
Out[]=
rm[h_,v_]/;FreeQ[h,v]=k[h]
In[]:=
k[h]
Out[]=
rm[f_[g_],v_]:=s[rm[f,v]][rm[g,v]]
In[]:=
ToC[x[y[x][z]],{x,y,z}]
In[]:=
s[s[k[s]][s[k[k]][s[k[s]][k]]]][s[k[s[s[k][k]]]][k]]
Out[]=
ToC[x[y],{x,y}]
In[]:=
s[k][k]
Out[]=
CombinatorEvolutionGraph[{s[x_][y_][z_]x[z][y[z]],k[x_][y_]x},s[k][k][x][y],4]
In[]:=
Out[]=
FixedPointList[#/.{s[x_][y_][z_]x[z][y[z]],k[x_][y_]x}&,s[k][k][x][y]]
In[]:=
{s[k][k][x][y],k[x][k[x]][y],x[y],x[y]}
Out[]=
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]]
In[]:=
Out[]=
ToC[x[y[y]],{x,y}]
In[]:=
s[s[k[s]][k]][k[s[s[k][k]][s[k][k]]]]
Out[]=
FixedPointList[#/.{s[x_][y_][z_]x[z][y[z]],k[x_][y_]x}&,ToC[x[y[y]],{x,y}]]
In[]:=
{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]]]]}
Out[]=
FixedPointList[#/.{s[x_][y_][z_]x[z][y[z]],k[x_][y_]x}&,s[s[k]][x][y]]
In[]:=
{s[s[k]][x][y],s[k][y][x[y]],k[x[y]][y[x[y]]],x[y],x[y]}
Out[]=
Goodstein sequences etc.
Goodstein sequences etc.
Their halting cannot be proved in Peano arithmetic
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]
Nest[s,k,6]
In[]:=
s[s[s[s[s[s[k]]]]]]
Out[]=
[[ 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?
What is the minimal universal lambda expression?
Minimal universal combinator
Minimal universal combinator
Emulation of lambda calculus by S, K is trivial
CombinatorEvolutionGraph[{e[x_][y_]x[y[y]]},e[e][e][e][e],13]
In[]:=
Out[]=
Groupings[Table[e,4],Construct2]
In[]:=
{e[e][e][e],e[e[e][e]],e[e[e]][e],e[e[e[e]]],e[e][e[e]]}
Out[]=
CombinatorEvolutionGraph[{e[x_][y_]x[y[y]]},#,12]&/@Groupings[Table[e,3],Construct2]
In[]:=
,
Out[]=
CombinatorEvolutionGraph[{e[x_][y_]x[y[y]]},#,8]&/@Groupings[Table[e,4],Construct2]
In[]:=
Out[]=
CombinatorEvolutionGraph[{e[x_][y_]x[y[y]]},#,12]&/@Groupings[Table[e,4],Construct2]
In[]:=
Out[]=
CombinatorEvolutionGraph[{e[x_][y_]x[y[y]]},#,8]&/@Groupings[Table[e,5],Construct2]
In[]:=
Out[]=
CombinatorEvolutionGraph[{e[x_][y_]x[y[y]]},#,8]&/@Groupings[Table[e,5],Construct2]
Groupings[{x,x,y},Construct2]
In[]:=
{x[x][y],x[x[y]]}
Out[]=
CombinatorEvolutionGraph[{e[x_][y_]x[x][y]},#,8]&/@Groupings[Table[e,5],Construct2]
In[]:=
Out[]=
Groupings[{x,y,y},Construct2]
In[]:=
{x[y][y],x[y[y]]}
Out[]=
CombinatorEvolutionGraph[{e[x_][y_]x[y][y]},#,8]&/@Groupings[Table[e,5],Construct2]
In[]:=
Out[]=
Systematic Search for Minimal Case
Systematic Search for Minimal Case
Groupings[#,Construct2]&/@Tuples[{x,y},2]
In[]:=
{{x[x]},{x[y]},{y[x]},{y[y]}}
Out[]=
Groupings[#,Construct2]&/@Tuples[{x,y},3]
In[]:=
Out[]=
Union[Flatten[%]]
In[]:=
{x[x[x]],x[x[y]],x[y[x]],x[y[y]],y[x[x]],y[x[y]],y[y[x]],y[y[y]],x[x][x],x[x][y],x[y][x],x[y][y],y[x][x],y[x][y],y[y][x],y[y][y]}
Out[]=
Size 2 RHSs
Size 2 RHSs
Function[rule,UndirectedGraph[CombinatorEvolutionGraph[rule,#,8],ImageSizeUpTo/@{40,40}]&/@Groupings[Table[e,4],Construct2]]/@({e[x_][y_]#}&/@Flatten[Groupings[#,Construct2]&/@Tuples[{x,y},2]])
In[]:=
Out[]=
Function[rule,UndirectedGraph[CombinatorEvolutionGraph[rule,#,10],ImageSizeUpTo/@{40,40}]&/@Groupings[Table[e,5],Construct2]]/@({e[x_][y_]#}&/@Flatten[Groupings[#,Construct2]&/@Tuples[{x,y},2]])
In[]:=
Out[]=
VertexList
In[]:=
{e[e][e[e]],e[e],e[e][e[e][e]],e[e[e]][e],e[e[e][e]][e],e[e][e][e[e][e]],e[e][e][e[e]]}
Out[]=
Function[rule,UndirectedGraph[CombinatorEvolutionGraph[rule,#,10],ImageSizeUpTo/@{40,40}]&/@Groupings[Table[e,6],Construct2]]/@({e[x_][y_]#}&/@Flatten[Groupings[#,Construct2]&/@Tuples[{x,y},2]])
In[]:=
Out[]=
({e[x_][y_]#}&/@Flatten[Groupings[#,Construct2]&/@Tuples[{x,y},2]])
In[]:=
{{e[x_][y_]x[x]},{e[x_][y_]x[y]},{e[x_][y_]y[x]},{e[x_][y_]y[y]}}
Out[]=
Groupings[Table[e,6],Construct2][[3]]
In[]:=
e[e[e][e][e]][e]
Out[]=
CombinatorEvolutionGraph[{e[x_][y_]x[x]},e[e[e][e][e]][e],15]
In[]:=
Out[]=
Function[rule,UndirectedGraph[CombinatorEvolutionGraph[rule,#,12],ImageSizeUpTo/@{40,40}]&/@Groupings[Table[e,6],Construct2]]/@({e[x_][y_]#}&/@Flatten[Groupings[#,Construct2]&/@Tuples[{x,y},2]])
In[]:=
Out[]=
[[ Everything seems to have reached a fixed point ]]
Size 3 RHSs
Size 3 RHSs
Function[rule,UndirectedGraph[CombinatorEvolutionGraph[rule,#,8],ImageSizeUpTo/@{40,40}]&/@Groupings[Table[e,2],Construct2]]/@({e[x_][y_]#}&/@Flatten[Groupings[#,Construct2]&/@Tuples[{x,y},3]])
In[]:=
Out[]=
Function[rule,UndirectedGraph[CombinatorEvolutionGraph[rule,#,8],ImageSizeUpTo/@{40,40}]&/@Groupings[Table[e,3],Construct2]]/@({e[x_][y_]#}&/@Flatten[Groupings[#,Construct2]&/@Tuples[{x,y},3]])
In[]:=
Out[]=
Function[rule,UndirectedGraph[CombinatorEvolutionGraph[rule,#,8],ImageSizeUpTo/@{40,40}]&/@Groupings[Table[e,4],Construct2]]/@({e[x_][y_]#}&/@Flatten[Groupings[#,Construct2]&/@Tuples[{x,y},3]])
In[]:=
Out[]=
Function[rule,rule(UndirectedGraph[CombinatorEvolutionGraph[rule,#,6],ImageSizeUpTo/@{40,40}]&/@Groupings[Table[e,4],Construct2])]/@({e[x_][y_]#}&/@Flatten[Groupings[#,Construct2]&/@Tuples[{x,y},3]])
In[]:=
Out[]=
Function[rule,rule(UndirectedGraph[CombinatorEvolutionGraph[rule,#,4],ImageSizeUpTo/@{40,40}]&/@Groupings[Table[e,5],Construct2])]/@({e[x_][y_]#}&/@Flatten[Groupings[#,Construct2]&/@Tuples[{x,y},3]])
In[]:=
Out[]=