In[]:=
PacletInstall["Wolfram/Lambda"]
Out[]=
PacletObject
In[]:=
Needs["Wolfram`Lambda`"]
In[]:=
LambdaFunction[TagLambda[λ.[λ.[1[2]][λ.[1[2]]]],"Alphabet"]]//TraditionalForm
Out[]//TraditionalForm=
a(bb(a))(cc(a))
In[]:=
LambdaFunction[TagLambda[λ.[λ.[1[2]][λ.[1[2]]]],"Alphabet"]]
Out[]=
Function[a,Function[b,b[a]][Function[c,c[a]]]]
In[]:=
LambdaFunction[TagLambda[λ.[λ.[1[2]][λ.[1[2]]]],"Alphabet"]]
In[]:=
Function[a,Function[b,b[a]][Function[c,c[a]]]][x]
Out[]=
x[x]
In[]:=
Out[]=
λ.[λ.[2[1][1[1]]]][λ.[1]]
In[]:=
Out[]=
S[S[K[S[S[K][K]]]][S[K[K]][S[K][K]]]][S[K[S[S[K][K]]]][S[K[K]][S[K][K]]]]
In[]:=
EnumerateLambdas[3]
Out[]=
In[]:=
LeafCount/@%
Out[]=
In[]:=
Counts[%]
Out[]=
21,33,411,539,6115,7277,8663,91449,102970,115427,128262,1310206,148748,156561
In[]:=
RandomChoice[%313]
Out[]=
λ.[λ.[λ.[3]][λ.[λ.[1[1]][λ.[3]]]]]
In[]:=
LambdaSmiles[%]
Out[]=
In[]:=
LambdaConvert[
%316
,"Tree"]Out[]=
In[]:=
EnumerateLambdas[2]
Out[]=
{λ.[1],λ.[λ.[1]],λ.[λ.[2]],λ.[λ.[1[1]]],λ.[λ.[1[2]]],λ.[λ.[2[1]]],λ.[λ.[2[2]]],λ.[1[1]],λ.[1[λ.[1]]],λ.[1[λ.[2]]],λ.[1[λ.[1[1]]]],λ.[1[λ.[1[2]]]],λ.[1[λ.[2[1]]]],λ.[1[λ.[2[2]]]],λ.[λ.[1][1]],λ.[λ.[1][λ.[1]]],λ.[λ.[1][λ.[2]]],λ.[λ.[1][λ.[1[1]]]],λ.[λ.[1][λ.[1[2]]]],λ.[λ.[1][λ.[2[1]]]],λ.[λ.[1][λ.[2[2]]]],λ.[λ.[2][1]],λ.[λ.[2][λ.[1]]],λ.[λ.[2][λ.[2]]],λ.[λ.[2][λ.[1[1]]]],λ.[λ.[2][λ.[1[2]]]],λ.[λ.[2][λ.[2[1]]]],λ.[λ.[2][λ.[2[2]]]],λ.[λ.[1[1]][1]],λ.[λ.[1[1]][λ.[1]]],λ.[λ.[1[1]][λ.[2]]],λ.[λ.[1[1]][λ.[1[1]]]],λ.[λ.[1[1]][λ.[1[2]]]],λ.[λ.[1[1]][λ.[2[1]]]],λ.[λ.[1[1]][λ.[2[2]]]],λ.[λ.[1[2]][1]],λ.[λ.[1[2]][λ.[1]]],λ.[λ.[1[2]][λ.[2]]],λ.[λ.[1[2]][λ.[1[1]]]],λ.[λ.[1[2]][λ.[1[2]]]],λ.[λ.[1[2]][λ.[2[1]]]],λ.[λ.[1[2]][λ.[2[2]]]],λ.[λ.[2[1]][1]],λ.[λ.[2[1]][λ.[1]]],λ.[λ.[2[1]][λ.[2]]],λ.[λ.[2[1]][λ.[1[1]]]],λ.[λ.[2[1]][λ.[1[2]]]],λ.[λ.[2[1]][λ.[2[1]]]],λ.[λ.[2[1]][λ.[2[2]]]],λ.[λ.[2[2]][1]],λ.[λ.[2[2]][λ.[1]]],λ.[λ.[2[2]][λ.[2]]],λ.[λ.[2[2]][λ.[1[1]]]],λ.[λ.[2[2]][λ.[1[2]]]],λ.[λ.[2[2]][λ.[2[1]]]],λ.[λ.[2[2]][λ.[2[2]]]]}
In[]:=
EnumerateLambdas[1,1]
Out[]=
{λ.[1]}
In[]:=
EnumerateLambdas[1,3]
Out[]=
{λ.[1],λ.[1[1]],λ.[1[1][1]],λ.[1[1[1]]]}
In[]:=
LambdaDiagram/@%
Out[]=
,,,
In[]:=
LambdaDiagram[λ.[1][λ.[1]]]
Out[]=
In[]:=
NestList[λ.[1],λ.[1],5]
Out[]=
{λ.[1],λ.[1][λ.[1]],λ.[1][λ.[1][λ.[1]]],λ.[1][λ.[1][λ.[1][λ.[1]]]],λ.[1][λ.[1][λ.[1][λ.[1][λ.[1]]]]],λ.[1][λ.[1][λ.[1][λ.[1][λ.[1][λ.[1]]]]]]}
In[]:=
LambdaDiagram/@%
Out[]=
,,,,,
In[]:=
BetaReductions/@
%325
Out[]=
{{},{λ.[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]]]]]}}
In[]:=
Length/@%
λx. (a x)
--------
a
--------
a
Beta Reduction Multiway System
Beta Reduction Multiway System
Affine terms: every lambda uses its bound variable 0 or 1 times
Linear terms: use variables exactly once
[[ What happens if one includes a recursion operation ? ]]