In[]:=
PacletInstall["Wolfram/Lambda"]
Out[]=
PacletObject
Name: Wolfram/Lambda
Version: 1.0.6

In[]:=
Needs["Wolfram`Lambda`"]
In[]:=
LambdaFunctionTagLambdaλ.λ.[1[2]]λ.[1[2]],"Alphabet"//TraditionalForm
Out[]//TraditionalForm=
a(bb(a))(cc(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[]:=
ParseLambda
["(λy.λx.(y x) (x x)) λx.x"]
Out[]=
λ.λ.[2[1][1[1]]]λ.[1]
In[]:=
LambdaConvert
λ.λ.[1[2]]λ.[1[2]],"Combinator"
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[]=
λ.[1],λ.λ.[1],λ.λ.[2],λ.λ.λ.[1],λ.λ.λ.[2],λ.λ.λ.[3],λ.λ.λ.[1[1]],λ.λ.λ.[1[2]],λ.λ.λ.[1[3]],λ.λ.λ.[2[1]],λ.λ.λ.[2[2]],
⋯44711⋯
,λ.λ.λ.[3[3]]λ.[3[3]]λ.λ.[3[3]]λ.[3],λ.λ.λ.[3[3]]λ.[3[3]]λ.λ.[3[3]]λ.[1[1]],λ.λ.λ.[3[3]]λ.[3[3]]λ.λ.[3[3]]λ.[1[2]],λ.λ.λ.[3[3]]λ.[3[3]]λ.λ.[3[3]]λ.[1[3]],λ.λ.λ.[3[3]]λ.[3[3]]λ.λ.[3[3]]λ.[2[1]],λ.λ.λ.[3[3]]λ.[3[3]]λ.λ.[3[3]]λ.[2[2]],λ.λ.λ.[3[3]]λ.[3[3]]λ.λ.[3[3]]λ.[2[3]],λ.λ.λ.[3[3]]λ.[3[3]]λ.λ.[3[3]]λ.[3[1]],λ.λ.λ.[3[3]]λ.[3[3]]λ.λ.[3[3]]λ.[3[2]],λ.λ.λ.[3[3]]λ.[3[3]]λ.λ.[3[3]]λ.[3[3]]
Full expression not available
(
original memory size:
29.8 MB)
In[]:=
LeafCount/@%
Out[]=
{2,3,3,4,4,4,5,5,5,5,5,5,5,5,5,4,4,5,5,5,6,6,6,6,6,6,6,6,6,4,4,5,5,5,6,6,6,6,6,6,6,6,6,5,5,6,6,6,7,7,7,7,7,7,7,7,7,5,5,6,6,6,7,7,7,7,7,7,7,7,7,5,5,6,6,6,7,7,7,7,7,7,7,7,7,6,6,7,7,7,8,8,8,8,8,8,8,8,8,6,6,7,7,7,8,8,8,8,8,8,8,8,8,6,6,7,7,7,8,
⋯44494⋯
,15,15,15,15,15,15,15,13,13,14,14,14,15,15,15,15,15,15,15,15,15,13,13,14,14,14,15,15,15,15,15,15,15,15,15,13,13,14,14,14,15,15,15,15,15,15,15,15,15,13,13,14,14,14,15,15,15,15,15,15,15,15,15,13,13,14,14,14,15,15,15,15,15,15,15,15,15,13,13,14,14,14,15,15,15,15,15,15,15,15,15,13,13,14,14,14,15,15,15,15,15,15,15,15,15,13,13,14,14,14,15,15,15,15,15,15,15,15,15}
Full expression not available
(
original memory size:
1.1 MB)
In[]:=
Counts[%]
Out[]=
21,33,411,539,6115,7277,8663,91449,102970,115427,128262,1310206,148748,156561
In[]:=
RandomChoice[%313]
Out[]=
λ.λ.λ.[3]λ.λ.[1[1]]λ.[3]
In[]:=
LambdaSmiles[%]
Out[]=
In[]:=
LambdaConvert
,"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/@
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]
λx. (a x)
--------
a

Beta Reduction Multiway System

Out[]//InputForm=
Interpretation[λ, λ3177][Interpretation[1, λ3177][Interpretation[λ, λ3178][Interpretation[2, λ3177]]]]
Affine terms: every lambda uses its bound variable 0 or 1 times
Linear terms: use variables exactly once
Out[]//InputForm=
Interpretation[λ, λ3752][Interpretation[λ, λ3753][Interpretation[1, λ3753][Interpretation[1, λ3753]]]]
[[ What happens if one includes a recursion operation ? ]]