Decompiling combinators to lambda calculus
Introduction
Introduction
I wrote a function that decompiles SK combinators into lambda functions. I also attempted to decompile randomly generated combinator expressions further, from lambda expressions on to a higher level decomposition, but had less luck with that.
Code
Code
In[]:=
replaceWithList[expr_,pattern_,replaceWith_]:=ReplacePart[expr,Thread[Position[expr,pattern]replaceWith]]
randomTree[leafCount_]:=Nest[ReplacePart[#,RandomChoice[Position[#,x]]{x,x}]&,{x,x},leafCount-2]
In[]:=
treeToFunctions[tree_]:=ReplaceRepeated[tree,{x_,y_}x[y]]
In[]:=
randomCombinator[leafCount_]:=treeToFunctions[replaceWithList[randomTree[leafCount],x,RandomChoice[{s,k},leafCount]]]
In[]:=
symbolicSystem::cnt="Combinator did not terminate";
In[]:=
symbolicSystemList[init_,rule_,maxIterations_:Infinity,maxSize_:Infinity]:=With[{output=NestWhileList[#/.rule&,init,UnsameQ[##]&&LeafCount[#2]<maxSize&,2,maxIterations]},If[!FreeQ[Last[output],Alternatives@@First/@rule],Message[symbolicSystem::cnt]];output]
In[]:=
symbolicSystem[init_,rule_,maxIterations_:Infinity,maxSize_:Infinity]:=Last[symbolicSystemList[init,rule,maxIterations,maxSize]]
In[]:=
s=CombinatorS;
In[]:=
k=CombinatorK;
In[]:=
sKRule={k[x_][y_]x,s[x_][y_][z_]x[z][y[z]]};
In[]:=
myReplacePart[expr_,{}new_]:=new
In[]:=
myReplacePart[expr_,rule_]:=ReplacePart[expr,rule]
In[]:=
myMapAt[f_,expr_,{}]:=f[expr]
In[]:=
myMapAt[f_,expr_,pos_]:=MapAt[f,expr,pos]
In[]:=
lambdaToFun[lambda[vars_List,f_]]:=lambdaToFun[Fold[Function[#2,#1]&,f,Reverse[vars]]]
In[]:=
(*Functionsym,symFunctionistodealwithtroublesaroundevaluatinganexpressioninsideWolfram'sFunctionfunction.*)
In[]:=
lambdaToFun[expr_/;!FreeQ[expr,lambda]]:=((expr/.lam_lambdalambdaToFun[lam])//.Functionsym)/.symFunction
In[]:=
lambdaToFun[expr_]:=expr
In[]:=
lambdaToFun[lambda[var_,f_]]:=Function[var,Evaluate[f]]
In[]:=
funToLambda[x_/;FreeQ[x,Function]]:=x
In[]:=
funToLambda[expr_]:=expr/.HoldPattern[f:Function[x_,y_]]funToLambda[f]
In[]:=
funToLambda[HoldPattern[Function[var_,f_]]]:=lambda[var,funToLambda[f]]
In[]:=
funToLambda[lambda[{x__},HoldPattern[Function[y_,z_]]]]:=funToLambda[lambda[{x,y},z]]
In[]:=
funToLambda[HoldPattern[Function[x_,Function[y_,z_]]]]:=funToLambda[lambda[{x,y},z]]
In[]:=
onlySkQ[expr_]:=ContainsOnly[Cases[expr,_?AtomQ,{0,Infinity},HeadsTrue],{s,k}]
In[]:=
firstSksPosition[expr_]:=FirstPosition[expr,First[MaximalBy[Cases[expr,_?onlySkQ,{0,Infinity},HeadsTrue],LeafCount]]]
In[]:=
lambdalizeOuter[expr_?(FreeQ[s|k]),___]:=expr
(*Theresaspecificcasewhereacombinatorexpressionignorestheargumentaddedtoit.Ijustmanuallyturntheseintoaspecificlambdaexpressionthatdoesthesame,"argumentIgnorer".*)
In[]:=
argumentIgnorer=lambda[{x1,x2},x1[x2][x1]][lambda[{x1,x2,x3},x2[x3][x2]]];
In[]:=
lambdalizeOuter[expr_,maxIterations_:Infinity,maxSize_:Infinity]:=Catch[lambda[First[#2],#1]&@@Reap[Module[{i=1},NestWhile[Check[symbolicSystem[#[Sow[ToExpression["x"<>ToString[i++]]]],sKRule,maxIterations,maxSize],Abort[],symbolicSystem::cnt]&,expr,If[MatchQ[#1,#2],Throw[argumentIgnorer];False,True]&&(!FreeQ[#2,k[x_][y_]|s[x_][y_][z_]]||MatchQ[#2,s[_][_]|s[_]|s|k[_]|k])&,2]]]]
In[]:=
lambdalizeStep[expr_/;FreeQ[expr,s|k],___]:=expr
In[]:=
lambdalizeStep[expr_,maxIterations_:Infinity,maxSize_:Infinity]:=(myMapAt[lambdalizeOuter[#,maxIterations,maxSize]&,expr,firstSksPosition[expr]]//.Functiong)/.gFunction
In[]:=
lambdalize[expr_,maxIterations_:Infinity,maxSize_:Infinity]:=FixedPoint[lambdalizeStep[#,maxIterations,maxSize]&,expr]
Church Encodings
Church Encodings
In[]:=
true=lambda[{a_,b_},a_]
Out[]=
lambda[{a_,b_},a_]
In[]:=
false=lambda[{a_,b_},b_]
Out[]=
lambda[{a_,b_},b_]
In[]:=
lambdaDecompilers={lambda[{p_,c_,a_},p_[c_][a_]]"if",lambda[{p_,q_},p_[q_][p_]]"and",lambda[{p_,q_},p_[p_][q_]]"or",lambda[p_,p_[false][true]]"not",lambda[{x_,y_,z_},z_[x_][y_]]"cons",lambda[{p_},p_[true]]"car",lambda[{p_},p_[false]]"cdr",lambda[{x_},true]"null",lambda[{x_},x_[lambda[{y_,z_},false]]]"nullQ",lambda[{n_},n_[lambda[{x_},false]][true]]"zeroQ",lambda[{n_,g_,x_},g_[n_[g_][x_]]]"succ",lambda[{a_,b_,g_,x_},a_[g_][b_[g_][x_]]]"add",lambda[{a_,b_},a_]"true",lambda[f_,lambda[x_,f[x_,x_]][lambda[x_,f[x_,x_]]]]"yComb",false"zero"};
In[]:=
unroll[x_]:=x
In[]:=
unroll[f[x_]]:=Flatten[{f,unroll[x]}]
In[]:=
lambdaToNum[x_]:=x
In[]:=
lambdaToNum[lam:lambda[{f_,x_},f_[y_]]/;MatchQ[unroll[f[y]],{f..,x}]]:=Length[unroll[f[y]]]-1
In[]:=
lambdaDecompile[lam_lambda]:=(lam/.x_lambdaToNum[x])//.lambdaDecompilers
Results
Results
Here’s an example of a randomly generated combinator expression being decompiled into a corresponding lambda expression.
In[]:=
#->lambdalize[#]&[randomCombinator[10]]
Out[]=
S[S[S][K]][S[S[K][S[S[K]]]]]lambda[{x1},x1[lambda[{x1,x2},x2[x1[x2]]][x1]][x1]]
Here are parts of that combinator evaluating.
In[]:=
symbolicSystemList[S[S[S][K]][S[S[K][S[S[K]]]]][a],sKRule]//Column
Out[]=
S[S[S][K]][S[S[K][S[S[K]]]]][a] |
S[S][K][a][S[S[K][S[S[K]]]][a]] |
S[a][K[a]][S[S[K][S[S[K]]]][a]] |
a[S[S[K][S[S[K]]]][a]][K[a][S[S[K][S[S[K]]]][a]]] |
a[S[S[K][S[S[K]]]][a]][a] |
a[S[S[K][S[S[K]]]][a]][a] |
In[]:=
symbolicSystemList[S[S[K][S[S[K]]]][a][b],sKRule]//Column
Out[]=
S[S[K][S[S[K]]]][a][b] |
S[K][S[S[K]]][b][a[b]] |
K[b][S[S[K]][b]][a[b]] |
b[a[b]] |
b[a[b]] |
Here is a function which turns lambda expressions into appliable functions, to show that the lambda expression is functionally equivalent.
In[]:=
lambdaToFun[lambda[{x1,x2},x2[x1[x2]]]]
Out[]=
Function[x1,Function[x2,x2[x1[x2]]]]
In[]:=
lambdaToFun[lambda[{x1},x1[lambda[{x1,x2},x2[x1[x2]]][x1]][x1]]]
Out[]=
Function[x1,x1[Function[x2,x2[x1[x2]]]][x1]]
In[]:=
%[a]
Out[]=
a[Function[x2$,x2$[a[x2$]]]][a]
Attempts at decompiling further did not go as well. I tried decompiling the lambda terms into a set of higher level functions which were likely to match, but I tended to only get ocasional matches with lambda expressions that correspond to “true”, “false”, and “and. One exciting time the entire expression compiled to “car”, but that was the only time any other higher level functions matched, out of the times I tried.
Also, in this code you can see me setting maxIterations and maxSize to 100. This is to keep combinator expressions from entering an infinite loop when they do not terminate.
Also, in this code you can see me setting maxIterations and maxSize to 100. This is to keep combinator expressions from entering an infinite loop when they do not terminate.