You are using a browser not supported by the Wolfram Cloud
Supported browsers include recent versions of Chrome, Edge, Firefox and Safari.
I understand and wish to continue anyway »
WOLFRAM NOTEBOOK
λ
x
In[]:=
Get["Wolfram`Lambda`"]
In[]:=
FunctionLambda[Function[x,x[x][x]]]
Out[]=
λ.[1[1][1]]
In[]:=
LambdaConvert[%,"Application"]
Out[]=
λ.[111]
In[]:=
1@1@1
Out[]=
1[1[1]]
In[]:=
churchNum[n_Integer]:=λ.[λ.[Nest[2,1,n]]]
In[]:=
churchNum[3]
Out[]=
λ.[λ.[2[2[2[1]]]]]
In[]:=
LambdaFunction[TagLambda[churchNum[1],"Alphabet"]]
In[]:=
Function[a,Function[b,a[b]]][s][z]
Out[]=
s[z]
In[]:=
Table[LambdaFunction[TagLambda[churchNum[n],"Alphabet"]][s][z],{n,0,5}]
Out[]=
{z,s[z],s[s[z]],s[s[s[z]]],s[s[s[s[z]]]],s[s[s[s[s[z]]]]]}
In[]:=
LambdaFunction[TagLambda[churchNum[5],"Alphabet"]]
In[]:=
λ[a,λ[b,a[a[a[a[a[b]]]]]]][s][z]
Out[]=
s[s[s[s[s[z]]]]]
In[]:=
LambdaCombinator[FunctionLambda[λ[x,λ[y,y[x]]]]]
Out[]=
K[Function[y,y[x]]]
In[]:=
FunctionLambda[λ[x,λ[y,y[x]]]]
Out[]=
λ.[Function[y,y[x]]]
In[]:=
LambdaCombinator[λ.[λ.[1[2]]]]
Out[]=
S[K[S[S[K][K]]]][S[K[K]][S[K][K]]]
In[]:=
S//FullForm
Out[]//FullForm=
CombinatorS
In[]:=
Sx_y_z_xz(yz)
Out[]=
Sx_y_z_xz(yz)
In[]:=
FunctionLambda[Function[x,Function[y,y[x]]]]
Out[]=
λ.[λ.[1[2]]]
In[]:=
Table[FunctionLambda[LambdaFunction[TagLambda[churchNum[n],"Alphabet"]]],{n,0,5}]
Out[]=
{λ.[λ.[1]],λ.[λ.[2[1]]],λ.[λ.[2[2[1]]]],λ.[λ.[2[2[2[1]]]]],λ.[λ.[2[2[2[2[1]]]]]],λ.[λ.[2[2[2[2[2[1]]]]]]]}
In[]:=
FunctionLambda/@%
Out[]=
{λ.[λ.[1]],λ.[λ.[2[1]]],λ.[λ.[2[2[1]]]],λ.[λ.[2[2[2[1]]]]],λ.[λ.[2[2[2[2[1]]]]]],λ.[λ.[2[2[2[2[2[1]]]]]]]}
In[]:=
true=λ.[λ.[2]];false=λ.[λ.[1]];isZero=λ.[1[λ.[false]][true]];
In[]:=
BetaReduce[isZero[z]]
Out[]=
λ.[λ.[2]]
In[]:=
isZero
Out[]=
λ.[1[λ.[λ.[λ.[1]]]][λ.[λ.[2]]]]
In[]:=
LambdaFunction[TagLambda[λ.[λ.[2[1[1]]][λ.[2[1[1]]]]],"Alphabet"]]
Out[]=
Function[a,Function[b,a[b[b]]][Function[c,a[c[c]]]]]
In[]:=
Function[f,Function[x,f[x[x]]][Function[x,f[x[x]]]]][g]
Out[]=
g[TerminatedEvaluation[RecursionLimit]]
In[]:=
NestList[BetaReduce[#,1]&,λ.[λ.[2[1[1]]][λ.[2[1[1]]]]][f],5]
Out[]=
{λ.[λ.[2[1[1]]][λ.[2[1[1]]]]][f],λ.[1[λ.[2[1[1]]][λ.[2[1[1]]]]]][f],λ.[1[1[λ.[2[1[1]]][λ.[2[1[1]]]]]]][f],λ.[1[1[1[λ.[2[1[1]]][λ.[2[1[1]]]]]]]][f],λ.[1[1[1[1[λ.[2[1[1]]][λ.[2[1[1]]]]]]]]][f],λ.[1[1[1[1[1[λ.[2[1[1]]][λ.[2[1[1]]]]]]]]]][f]}
In[]:=
BetaReduce/@EnumerateLambdas[2,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]],λ.[λ.[2]],λ.[λ.[1[1]]],λ.[λ.[1[2]]],λ.[λ.[2[1]]],λ.[λ.[2[2]]],λ.[1],λ.[1],λ.[1],λ.[1],λ.[1],λ.[1],λ.[1],λ.[1[1]],λ.[λ.[1]],λ.[1],λ.[λ.[1[1]][λ.[1[1]]]],λ.[1[1]],λ.[1[λ.[2[1]]]],λ.[1[1]],λ.[1[1]],λ.[1],λ.[1],λ.[1[1]],λ.[1[1]],λ.[1[1]],λ.[1[1]],λ.[1[1]],λ.[1[λ.[1]]],λ.[1[λ.[2]]],λ.[1[λ.[1[1]]]],λ.[1[λ.[1[2]]]],λ.[1[λ.[2[1]]]],λ.[1[λ.[2[2]]]],λ.[1[1]],λ.[1[1]],λ.[1[1]],λ.[1[1]],λ.[1[1]],λ.[1[1]],λ.[1[1]]}
In[]:=
#->BetaReduce[#]&/@EnumerateLambdas[2,2]
Out[]=
{λ.[1]λ.[1],λ.[λ.[1]]λ.[λ.[1]],λ.[λ.[2]]λ.[λ.[2]],λ.[λ.[1[1]]]λ.[λ.[1[1]]],λ.[λ.[1[2]]]λ.[λ.[1[2]]],λ.[λ.[2[1]]]λ.[λ.[2[1]]],λ.[λ.[2[2]]]λ.[λ.[2[2]]],λ.[1[1]]λ.[1[1]],λ.[1[λ.[1]]]λ.[1[λ.[1]]],λ.[1[λ.[2]]]λ.[1[λ.[2]]],λ.[1[λ.[1[1]]]]λ.[1[λ.[1[1]]]],λ.[1[λ.[1[2]]]]λ.[1[λ.[1[2]]]],λ.[1[λ.[2[1]]]]λ.[1[λ.[2[1]]]],λ.[1[λ.[2[2]]]]λ.[1[λ.[2[2]]]],λ.[λ.[1][1]]λ.[1],λ.[λ.[1][λ.[1]]]λ.[λ.[1]],λ.[λ.[1][λ.[2]]]λ.[λ.[2]],λ.[λ.[1][λ.[1[1]]]]λ.[λ.[1[1]]],λ.[λ.[1][λ.[1[2]]]]λ.[λ.[1[2]]],λ.[λ.[1][λ.[2[1]]]]λ.[λ.[2[1]]],λ.[λ.[1][λ.[2[2]]]]λ.[λ.[2[2]]],λ.[λ.[2][1]]λ.[1],λ.[λ.[2][λ.[1]]]λ.[1],λ.[λ.[2][λ.[2]]]λ.[1],λ.[λ.[2][λ.[1[1]]]]λ.[1],λ.[λ.[2][λ.[1[2]]]]λ.[1],λ.[λ.[2][λ.[2[1]]]]λ.[1],λ.[λ.[2][λ.[2[2]]]]λ.[1],λ.[λ.[1[1]][1]]λ.[1[1]],λ.[λ.[1[1]][λ.[1]]]λ.[λ.[1]],λ.[λ.[1[1]][λ.[2]]]λ.[1],λ.[λ.[1[1]][λ.[1[1]]]]λ.[λ.[1[1]][λ.[1[1]]]],λ.[λ.[1[1]][λ.[1[2]]]]λ.[1[1]],λ.[λ.[1[1]][λ.[2[1]]]]λ.[1[λ.[2[1]]]],λ.[λ.[1[1]][λ.[2[2]]]]λ.[1[1]],λ.[λ.[1[2]][1]]λ.[1[1]],λ.[λ.[1[2]][λ.[1]]]λ.[1],λ.[λ.[1[2]][λ.[2]]]λ.[1],λ.[λ.[1[2]][λ.[1[1]]]]λ.[1[1]],λ.[λ.[1[2]][λ.[1[2]]]]λ.[1[1]],λ.[λ.[1[2]][λ.[2[1]]]]λ.[1[1]],λ.[λ.[1[2]][λ.[2[2]]]]λ.[1[1]],λ.[λ.[2[1]][1]]λ.[1[1]],λ.[λ.[2[1]][λ.[1]]]λ.[1[λ.[1]]],λ.[λ.[2[1]][λ.[2]]]λ.[1[λ.[2]]],λ.[λ.[2[1]][λ.[1[1]]]]λ.[1[λ.[1[1]]]],λ.[λ.[2[1]][λ.[1[2]]]]λ.[1[λ.[1[2]]]],λ.[λ.[2[1]][λ.[2[1]]]]λ.[1[λ.[2[1]]]],λ.[λ.[2[1]][λ.[2[2]]]]λ.[1[λ.[2[2]]]],λ.[λ.[2[2]][1]]λ.[1[1]],λ.[λ.[2[2]][λ.[1]]]λ.[1[1]],λ.[λ.[2[2]][λ.[2]]]λ.[1[1]],λ.[λ.[2[2]][λ.[1[1]]]]λ.[1[1]],λ.[λ.[2[2]][λ.[1[2]]]]λ.[1[1]],λ.[λ.[2[2]][λ.[2[1]]]]λ.[1[1]],λ.[λ.[2[2]][λ.[2[2]]]]λ.[1[1]]}
In[]:=
Select[%,#[[1]]=!=#[[2]]&]
Out[]=
{λ.[λ.[1][1]]λ.[1],λ.[λ.[1][λ.[1]]]λ.[λ.[1]],λ.[λ.[1][λ.[2]]]λ.[λ.[2]],λ.[λ.[1][λ.[1[1]]]]λ.[λ.[1[1]]],λ.[λ.[1][λ.[1[2]]]]λ.[λ.[1[2]]],λ.[λ.[1][λ.[2[1]]]]λ.[λ.[2[1]]],λ.[λ.[1][λ.[2[2]]]]λ.[λ.[2[2]]],λ.[λ.[2][1]]λ.[1],λ.[λ.[2][λ.[1]]]λ.[1],λ.[λ.[2][λ.[2]]]λ.[1],λ.[λ.[2][λ.[1[1]]]]λ.[1],λ.[λ.[2][λ.[1[2]]]]λ.[1],λ.[λ.[2][λ.[2[1]]]]λ.[1],λ.[λ.[2][λ.[2[2]]]]λ.[1],λ.[λ.[1[1]][1]]λ.[1[1]],λ.[λ.[1[1]][λ.[1]]]λ.[λ.[1]],λ.[λ.[1[1]][λ.[2]]]λ.[1],λ.[λ.[1[1]][λ.[1[2]]]]λ.[1[1]],λ.[λ.[1[1]][λ.[2[1]]]]λ.[1[λ.[2[1]]]],λ.[λ.[1[1]][λ.[2[2]]]]λ.[1[1]],λ.[λ.[1[2]][1]]λ.[1[1]],λ.[λ.[1[2]][λ.[1]]]λ.[1],λ.[λ.[1[2]][λ.[2]]]λ.[1],λ.[λ.[1[2]][λ.[1[1]]]]λ.[1[1]],λ.[λ.[1[2]][λ.[1[2]]]]λ.[1[1]],λ.[λ.[1[2]][λ.[2[1]]]]λ.[1[1]],λ.[λ.[1[2]][λ.[2[2]]]]λ.[1[1]],λ.[λ.[2[1]][1]]λ.[1[1]],λ.[λ.[2[1]][λ.[1]]]λ.[1[λ.[1]]],λ.[λ.[2[1]][λ.[2]]]λ.[1[λ.[2]]],λ.[λ.[2[1]][λ.[1[1]]]]λ.[1[λ.[1[1]]]],λ.[λ.[2[1]][λ.[1[2]]]]λ.[1[λ.[1[2]]]],λ.[λ.[2[1]][λ.[2[1]]]]λ.[1[λ.[2[1]]]],λ.[λ.[2[1]][λ.[2[2]]]]λ.[1[λ.[2[2]]]],λ.[λ.[2[2]][1]]λ.[1[1]],λ.[λ.[2[2]][λ.[1]]]λ.[1[1]],λ.[λ.[2[2]][λ.[2]]]λ.[1[1]],λ.[λ.[2[2]][λ.[1[1]]]]λ.[1[1]],λ.[λ.[2[2]][λ.[1[2]]]]λ.[1[1]],λ.[λ.[2[2]][λ.[2[1]]]]λ.[1[1]],λ.[λ.[2[2]][λ.[2[2]]]]λ.[1[1]]}
In[]:=
Length[Union[%]]
Out[]=
15
In[]:=
Union[EnumerateLambdas[2,2]]//Length
Out[]=
56
EnumerateLambdas[1,4]
In[]:=
PacletInstall["https://wolfr.am/1q5XjM6t9",ForceVersionInstall->True]
Out[]=
PacletObject
In[]:=
<<ProcessTheoryLoader`
In[]:=
EnumerateLambdas[2,1]
Out[]=
{λ.[1],λ.[λ.[1]],λ.[λ.[2]]}
In[]:=
Outer[#1[#2]->BetaReduce[#1[#2]]&,EnumerateLambdas[2,1],EnumerateLambdas[2,1]]
Out[]=
{{λ.[1][λ.[1]]λ.[1],λ.[1][λ.[λ.[1]]]λ.[λ.[1]],λ.[1][λ.[λ.[2]]]λ.[λ.[2]]},{λ.[λ.[1]][λ.[1]]λ.[1],λ.[λ.[1]][λ.[λ.[1]]]λ.[1],λ.[λ.[1]][λ.[λ.[2]]]λ.[1]},{λ.[λ.[2]][λ.[1]]λ.[λ.[1]],λ.[λ.[2]][λ.[λ.[1]]]λ.[λ.[λ.[1]]],λ.[λ.[2]][λ.[λ.[2]]]λ.[λ.[λ.[2]]]}}
In[]:=
Outer[#1[#2]->BetaReduce[#1[#2]]&,EnumerateLambdas[1,2],EnumerateLambdas[2,1]]
Out[]=
{{λ.[1][λ.[1]]λ.[1],λ.[1][λ.[λ.[1]]]λ.[λ.[1]],λ.[1][λ.[λ.[2]]]λ.[λ.[2]]},{λ.[1[1]][λ.[1]]λ.[1],λ.[1[1]][λ.[λ.[1]]]λ.[1],λ.[1[1]][λ.[λ.[2]]]λ.[λ.[λ.[2]]]}}
Major Searches
Major Searches
Multiway
Multiway
Tromp’s busy beaver
Tromp’s busy beaver