Acronym Combinator Wolfram Mathematica

Question

How can I implement a standard reduction strategy for {S, K, I} combinators in Mathematica? Here are the rules: S [x] [y] [g] → x [y] [g [g]] K [x] [y] [g] → x

We also have Y combinator (fixed point), so Y [a] = a [Ya]].

And we must “evaluate” the expression, for example, S [K] [K] [a] = K [a] [K [a]] = a

It is very important to have ONE reduction step. Thus, the result will be in the application one step many times.

Thank you pending any suggestions !!!

Answer 1

Define a function called eval that will perform one step of evaluating the combinator. First, we need to consider what exactly is one step. Arbitrarily, we will first evaluate the left outer expression and work from there.

 ClearAll[eval] eval[e_] := Module[{r = eval1[e]}, r /; r =!= e] eval[e:f_[g_]] := Module[{r = eval[f][g]}, r /; r =!= e] eval[e:f_[g_]] := Module[{r = f[eval[g]]}, r /; r =!= e] eval[e_] := e 

Please note that the rules only apply if they really change the expression. The awkwardness of these definitions is due to the lack of a Mathematica template expression that will correspond to arbitrarily long cardboard argument lists.

Now we can define the recognized combinators S, K, and I:

 ClearAll[eval1] eval1[s[f_][g_][h_]] := f[h][g[h]] eval1[k[f_][_]] := f eval1[i[f_]] := f 

The characters here are lowercase, mainly to avoid that Mathematica displays an inline character I , an imaginary unit.

Any other combinators will be taken as variables and left invaluable:

 eval1[e_] := e 

Now we can try the main cases:

 i[f] // eval (* f *) k[f][g] // eval (* f *) s[f][g][h] // eval (* f[h][g[h]] *) 

For more interesting cases, let's define evalAll , which shows all the steps in the evaluation chain:

 ClearAll[evalAll] evalAll[e_, n_:Infinity] := FixedPointList[eval, e, n+1] // Most // Column s[k][k][a] // evalAll (* s[k][k][a] k[a][k[a]] a *) s[s[m][n][r]][k[a][b]][c] // evalAll (* s[s[m][n][r]][k[a][b]][c] s[m][n][r][c][k[a][b][c]] m[r][n[r]][c][k[a][b][c]] m[r][n[r]][c][a[c]] *) f[s[i[k]][k][g][i[f]]] // evalAll (* f[s[i[k]][k][g][i[f]]] f[i[k][g][k[g]][i[f]]] f[k[g][k[g]][i[f]]] f[g[i[f]]] f[g[f]] *) 

evalAll accepts the optional argument "count" to limit the number of steps shown. This is useful for divergent expressions - as a direct expression of Y combinator:

 eval1[y[f_]] := f[y[f]] y[f] // evalAll[#, 4]& (* y[f] f[y[f]] f[f[y[f]]] f[f[f[y[f]]]] f[f[f[f[y[f]]]]] *) 

... but it is more interesting to express such sequences in terms of SKI:

 Module[{y = s[k[s[i][i]]][s[s[k[s]][k]][k[s[i][i]]]]} , evalAll[y[f], 28] ] (* s[k[s[i][i]]][s[s[k[s]][k]][k[s[i][i]]]][f] k[s[i][i]][f][s[s[k[s]][k]][k[s[i][i]]][f]] s[i][i][s[s[k[s]][k]][k[s[i][i]]][f]] i[s[s[k[s]][k]][k[s[i][i]]][f]][i[s[s[k[s]][k]][k[s[i][i]]][f]]] s[s[k[s]][k]][k[s[i][i]]][f][i[s[s[k[s]][k]][k[s[i][i]]][f]]] s[k[s]][k][f][k[s[i][i]][f]][i[s[s[k[s]][k]][k[s[i][i]]][f]]] k[s][f][k[f]][k[s[i][i]][f]][i[s[s[k[s]][k]][k[s[i][i]]][f]]] s[k[f]][k[s[i][i]][f]][i[s[s[k[s]][k]][k[s[i][i]]][f]]] k[f][i[s[s[k[s]][k]][k[s[i][i]]][f]]][k[s[i][i]][f][i[s[s[k[s]][k]][k[s[i][i]]][f]]]] f[k[s[i][i]][f][i[s[s[k[s]][k]][k[s[i][i]]][f]]]] <-- f[...] f[s[i][i][i[s[s[k[s]][k]][k[s[i][i]]][f]]]] f[i[i[s[s[k[s]][k]][k[s[i][i]]][f]]][i[i[s[s[k[s]][k]][k[s[i][i]]][f]]]]] f[i[s[s[k[s]][k]][k[s[i][i]]][f]][i[i[s[s[k[s]][k]][k[s[i][i]]][f]]]]] f[s[s[k[s]][k]][k[s[i][i]]][f][i[i[s[s[k[s]][k]][k[s[i][i]]][f]]]]] f[s[k[s]][k][f][k[s[i][i]][f]][i[i[s[s[k[s]][k]][k[s[i][i]]][f]]]]] f[k[s][f][k[f]][k[s[i][i]][f]][i[i[s[s[k[s]][k]][k[s[i][i]]][f]]]]] f[s[k[f]][k[s[i][i]][f]][i[i[s[s[k[s]][k]][k[s[i][i]]][f]]]]] f[k[f][i[i[s[s[k[s]][k]][k[s[i][i]]][f]]]][k[s[i][i]][f][i[i[s[s[k[s]][k]][k[s[i][i]]][f]]]]]] f[f[k[s[i][i]][f][i[i[s[s[k[s]][k]][k[s[i][i]]][f]]]]]] <-- f[f[...]] f[f[s[i][i][i[i[s[s[k[s]][k]][k[s[i][i]]][f]]]]]] f[f[i[i[i[s[s[k[s]][k]][k[s[i][i]]][f]]]][i[i[i[s[s[k[s]][k]][k[s[i][i]]][f]]]]]]] f[f[i[i[s[s[k[s]][k]][k[s[i][i]]][f]]][i[i[i[s[s[k[s]][k]][k[s[i][i]]][f]]]]]]] f[f[i[s[s[k[s]][k]][k[s[i][i]]][f]][i[i[i[s[s[k[s]][k]][k[s[i][i]]][f]]]]]]] f[f[s[s[k[s]][k]][k[s[i][i]]][f][i[i[i[s[s[k[s]][k]][k[s[i][i]]][f]]]]]]] f[f[s[k[s]][k][f][k[s[i][i]][f]][i[i[i[s[s[k[s]][k]][k[s[i][i]]][f]]]]]]] f[f[k[s][f][k[f]][k[s[i][i]][f]][i[i[i[s[s[k[s]][k]][k[s[i][i]]][f]]]]]]] f[f[s[k[f]][k[s[i][i]][f]][i[i[i[s[s[k[s]][k]][k[s[i][i]]][f]]]]]]] f[f[k[f][i[i[i[s[s[k[s]][k]][k[s[i][i]]][f]]]]][k[s[i][i]][f][i[i[i[s[s[k[s]][k]][k[s[i][i]]][f]]]]]]]] f[f[f[k[s[i][i]][f][i[i[i[s[s[k[s]][k]][k[s[i][i]]][f]]]]]]]] <-- f[f[f[...]]] *)