In[]:=
Function[x,x+1][8]
Out[]=
9
In[]:=
(x|->x+1)[10]
Out[]=
11
In[]:=
Function[x,x+y][10]
Out[]=
10+y
In[]:=
Function[y,Function[x,x+y]][10][17]
Out[]=
27
In[]:=
Function[y,Function[x,x+y]][a]
In[]:=
Function[x$,x$+a][b]
Out[]=
a+b
f[x][y]
f[x,y]
In[]:=
Plus[2,3,4]
Out[]=
9
λx.x+1
Function[x,Function[x,x+x]]
In[]:=
Function[z,Function[x,x+z]]
Out[]=
Function[z,Function[x,x+z]]
In[]:=
Function[y,Function[x,x+y]]
Out[]=
Function[y,Function[x,x+y]]
In[]:=
PacletInstall["Wolfram/Lambda"]
Out[]=
PacletObject
Name: Wolfram/Lambda
Version: 1.0.0

In[]:=
Needs["Wolfram`Lambda`"]
In[]:=
RandomLambda
[][x.]
Out[]=
λ.[λ.[2[1]][λ.[2[1]]]][x.]
In[]:=
EnumerateLambdas
[1,2]
Out[]=
{λ.[1],λ.[1[1]]}
x|->x
x|->x[x]
In[]:=
EvalLambda
[#[x]]&/@
EnumerateLambdas
[1,2]
Out[]=
{x,x[x]}
In[]:=
EvalLambda
[#[x]]&/@
EnumerateLambdas
[2,2]
$IterationLimit
:Iteration limit of 4096 exceeded.
Out[]=
{x,λ.[1],λ.[x],λ.[1[1]],λ.[1[x]],λ.[x[1]],λ.[x[x]],x[x],x[λ.[1]],x[λ.[x]],x[λ.[1[1]]],x[λ.[1[x]]],x[λ.[x[1]]],x[λ.[x[x]]],x,λ.[1],λ.[x],λ.[1[1]],λ.[1[x]],λ.[x[1]],λ.[x[x]],x,x,x,x,x,x,x,x[x],λ.[1],x,TerminatedEvaluation[IterationLimit],x[x],x[λ.[x[1]]],x[x],x[x],x,x,x[x],x[x],x[x],x[x],x[x],x[λ.[1]],x[λ.[x]],x[λ.[1[1]]],x[λ.[1[x]]],x[λ.[x[1]]],x[λ.[x[x]]],x[x],x[x],x[x],x[x],x[x],x[x],x[x]}
In[]:=
#->
EvalLambda
[#[x]]&/@
EnumerateLambdas
[2,2]
$IterationLimit
:Iteration limit of 4096 exceeded.
Out[]=
{λ.[1]x,λ.[λ.[1]]λ.[1],λ.[λ.[2]]λ.[x],λ.[λ.[1[1]]]λ.[1[1]],λ.[λ.[1[2]]]λ.[1[x]],λ.[λ.[2[1]]]λ.[x[1]],λ.[λ.[2[2]]]λ.[x[x]],λ.[1[1]]x[x],λ.[1[λ.[1]]]x[λ.[1]],λ.[1[λ.[2]]]x[λ.[x]],λ.[1[λ.[1[1]]]]x[λ.[1[1]]],λ.[1[λ.[1[2]]]]x[λ.[1[x]]],λ.[1[λ.[2[1]]]]x[λ.[x[1]]],λ.[1[λ.[2[2]]]]x[λ.[x[x]]],λ.[λ.[1][1]]x,λ.[λ.[1][λ.[1]]]λ.[1],λ.[λ.[1][λ.[2]]]λ.[x],λ.[λ.[1][λ.[1[1]]]]λ.[1[1]],λ.[λ.[1][λ.[1[2]]]]λ.[1[x]],λ.[λ.[1][λ.[2[1]]]]λ.[x[1]],λ.[λ.[1][λ.[2[2]]]]λ.[x[x]],λ.[λ.[2][1]]x,λ.[λ.[2][λ.[1]]]x,λ.[λ.[2][λ.[2]]]x,λ.[λ.[2][λ.[1[1]]]]x,λ.[λ.[2][λ.[1[2]]]]x,λ.[λ.[2][λ.[2[1]]]]x,λ.[λ.[2][λ.[2[2]]]]x,λ.[λ.[1[1]][1]]x[x],λ.[λ.[1[1]][λ.[1]]]λ.[1],λ.[λ.[1[1]][λ.[2]]]x,λ.[λ.[1[1]][λ.[1[1]]]]TerminatedEvaluation[IterationLimit],λ.[λ.[1[1]][λ.[1[2]]]]x[x],λ.[λ.[1[1]][λ.[2[1]]]]x[λ.[x[1]]],λ.[λ.[1[1]][λ.[2[2]]]]x[x],λ.[λ.[1[2]][1]]x[x],λ.[λ.[1[2]][λ.[1]]]x,λ.[λ.[1[2]][λ.[2]]]x,λ.[λ.[1[2]][λ.[1[1]]]]x[x],λ.[λ.[1[2]][λ.[1[2]]]]x[x],λ.[λ.[1[2]][λ.[2[1]]]]x[x],λ.[λ.[1[2]][λ.[2[2]]]]x[x],λ.[λ.[2[1]][1]]x[x],λ.[λ.[2[1]][λ.[1]]]x[λ.[1]],λ.[λ.[2[1]][λ.[2]]]x[λ.[x]],λ.[λ.[2[1]][λ.[1[1]]]]x[λ.[1[1]]],λ.[λ.[2[1]][λ.[1[2]]]]x[λ.[1[x]]],λ.[λ.[2[1]][λ.[2[1]]]]x[λ.[x[1]]],λ.[λ.[2[1]][λ.[2[2]]]]x[λ.[x[x]]],λ.[λ.[2[2]][1]]x[x],λ.[λ.[2[2]][λ.[1]]]x[x],λ.[λ.[2[2]][λ.[2]]]x[x],λ.[λ.[2[2]][λ.[1[1]]]]x[x],λ.[λ.[2[2]][λ.[1[2]]]]x[x],λ.[λ.[2[2]][λ.[2[1]]]]x[x],λ.[λ.[2[2]][λ.[2[2]]]]x[x]}
In[]:=
Take
EnumerateLambdas
[2,2],5
Out[]=
{λ.[1],λ.[λ.[1]],λ.[λ.[2]],λ.[λ.[1[1]]],λ.[λ.[1[2]]]}
In[]:=
Trace
EvalLambda
[λ.[λ.[1[2]][λ.[1]]][x]],_LambdaSubstitute
Out[]=
{{{{{LambdaSubstitute[λ.[1],1x],{LambdaSubstitute[1,2x]}}}}},{LambdaSubstitute[1[2],1λ.[1],2x],{LambdaSubstitute[1,1λ.[1],2x]},{LambdaSubstitute[2,1λ.[1],2x]}},{LambdaSubstitute[1,1x]}}
In[]:=
ResourceFunction["TraceGraph"]
EvalLambda
[λ.[λ.[1[2]][λ.[1]]][x]],_LambdaSubstitute
Out[]=
x |-> (E [x])
Eta reduction:
https://tromp.github.io/cl/diagrams.html
https://github.com/prathyvsh/lambda-calculus-visualizations
https://alexandria.tue.nl/repository/freearticles/597619.pdf