Wolfram Language Paclet Repository
Community-contributed installable additions to the Wolfram Language
Wolfram`Lambda`
LambdaCombinator  |
|
| | ||||
Details and Options
Examples
(1)
Basic Examples
(1)
Convert lambda to a combinator using progressively more elimination rules:
In[1]:=
lambda=λ.[λ.[2[1[1]]][λ.[2[1[1]]]]][λ.[λ.[λ.[1[λ.[λ.[λ.[1]]]][λ.[λ.[2]]]][1][λ.[λ.[λ.[2[3[2][1]]]]][λ.[λ.[1]]]][λ.[λ.[λ.[3[2[1]]]]][1][2[λ.[λ.[λ.[3[λ.[λ.[1[2[4]]]]][λ.[2]][λ.[1]]]]][1]]]]]]][λ.[λ.[2[2[2[1]]]]]];
In[2]:=
 | LambdaCombinator |
Out[2]=
S[S[S[K[S]][S[K[K]][S[K][K]]]][K[S[S[K][K]][S[K][K]]]]][S[S[K[S]][S[K[K]][S[K][K]]]][K[S[S[K][K]][S[K][K]]]]][S[K[S[S[S[K[S[S[S[K][K]][K[K[K[S[K][K]]]]]][K[S[K[K]][S[K][K]]]]]][S[K][K]]][K[S[K[S[S[K[S]][S[K[K]][S[K][K]]]]]][S[S[K[S]][S[K[S[K[S]]]][S[K[S[K[K]]]][S[S[K[S]][S[K[K]][S[K][K]]]][K[S[K][K]]]]]]][K[K[S[K][K]]]]][K[S[K][K]]]]]]]][S[K[S[S[K[S[S[K[S]][S[K[K]][S[K[S]][S[K[K]][S[K][K]]]]]][K[S[S[K[S]][S[K[K]][S[K][K]]]][K[S[K][K]]]]]]][S[K][K]]]]][S[S[K[S]][S[K[K]][S[K][K]]]][K[S[K[S[S[K[S]][S[K[S[K[S]]]][S[S[K[S]][S[K[S[K[S]]]][S[K[S[K[K]]]][S[S[K[S]][S[K[K]][S[K][K]]]][K[S[K[S[K[S[S[K][K]]]]]][S[K[S[K[K]]]][S[K[S[S[K][K]]]][S[K[K]][S[K][K]]]]]]]]]]][K[K[S[K[K]][S[K][K]]]]]]]][K[K[K[S[K][K]]]]]]][S[K][K]]]]]]][S[S[K[S]][S[K[K]][S[K][K]]]][S[S[K[S]][S[K[K]][S[K][K]]]][S[S[K[S]][S[K[K]][S[K][K]]]][K[S[K][K]]]]]]
In[3]:=
| LambdaCombinator |
Out[3]=
S[S[S[K[S]][S[K[K]][I]]][K[S[I][I]]]][S[S[K[S]][S[K[K]][I]]][K[S[I][I]]]][S[K[S[S[S[K[S[S[I][K[K[K[I]]]]][K[S[K[K]][I]]]]][I]][K[S[K[S[S[K[S]][S[K[K]][I]]]]][S[S[K[S]][S[K[S[K[S]]]][S[K[S[K[K]]]][S[S[K[S]][S[K[K]][I]]][K[I]]]]]][K[K[I]]]][K[I]]]]]]][S[K[S[S[K[S[S[K[S]][S[K[K]][S[K[S]][S[K[K]][I]]]]][K[S[S[K[S]][S[K[K]][I]]][K[I]]]]]][I]]]][S[S[K[S]][S[K[K]][I]]][K[S[K[S[S[K[S]][S[K[S[K[S]]]][S[S[K[S]][S[K[S[K[S]]]][S[K[S[K[K]]]][S[S[K[S]][S[K[K]][I]]][K[S[K[S[K[S[I]]]]][S[K[S[K[K]]]][S[K[S[I]]][S[K[K]][I]]]]]]]]]][K[K[S[K[K]][I]]]]]]][K[K[K[I]]]]]][I]]]]]][S[S[K[S]][S[K[K]][I]]][S[S[K[S]][S[K[K]][I]]][S[S[K[S]][S[K[K]][I]]][K[I]]]]]
In[4]:=
| LambdaCombinator |
Out[4]=
S[S[B[B][I]][K[S[I][I]]]][S[B[B][I]][K[S[I][I]]]][B[S[S[B[S[S[I][K[K[K[I]]]]][K[B[K][I]]]][I]][K[B[S[B[B][I]]][S[B[S][B[B[B]][S[B[B][I]][K[I]]]]][K[K[I]]]][K[I]]]]]][B[S[B[S[B[B][B[B][I]]][K[S[B[B][I]][K[I]]]]][I]]][S[B[B][I]][K[B[S[B[S][B[B[S]][S[B[S][B[B[B]][S[B[B][I]][K[B[B[S[I]]][B[B[K]][B[S[I]][B[K][I]]]]]]]]][K[K[B[K][I]]]]]]][K[K[K[I]]]]][I]]]]]][S[B[B][I]][S[B[B][I]][S[B[B][I]][K[I]]]]]
In[5]:=
| LambdaCombinator |
Out[5]=
S[C[B[B][I]][S[I][I]]][C[B[B][I]][S[I][I]]][B[S[C[B[C[C[I][K[K[I]]]][B[K][I]]][I]][B[S[B[B][I]]][C[B[C][B[B[B]][C[B[B][I]][I]]]][I]][K[I]]]]][B[S[B[C[B[B][B[B][I]]][C[B[B][I]][I]]][I]]][C[B[B][I]][B[C[B[C][B[B[C]][C[B[C][B[B[B]][C[B[B][I]][B[B[C[I]]][B[C[I]][I]]]]]][B[K][I]]]]][I]][I]]]]][S[B[B][I]][S[B[B][I]][C[B[B][I]][I]]]]
In[6]:=
| LambdaCombinator |
Out[6]=
S[C[B][S[I][I]]][C[B][S[I][I]]][B[S[C[C[C[I][K[K[I]]]][K]][S[B][K[I]]]]][B[S[B]][C[B][C[B[C][B[B[C]][C[B[C][B[B[B]][C[B][B[B[C[I]]][C[I]]]]]][K]]]][I]]]]][S[B][S[B][I]]]
Reduce the resulting combinator:
In[7]:=
%2
[s][z]//.{I
[x_]x,K
[x_][_]x,C
[x_][y_][z_]x[z][y],B
[x_][y_][z_]x[y[z]],S
[x_][y_][z_]x[z][y[z]]}Out[7]=
s[s[s[s[s[s[z]]]]]]
 |
|
""