Combinator Reduction Wolfram Mathematica

Question

如何在Mathematica中实现Combinators {S，K，I}的正常还原策略？ 下面是规则： S [X] [Y] [Z] - > X [Y] [Z [Y]] K [X] [Y] [Z] - > X

另外，我们有Y组合器（固定点），因此Y [a] = a [Ya]]。

而且，我们必须 “评估” 之类的表达，例如，S [K] [K] [A] = K [A] [K [A] =一

它是有非常重要的减少一个步骤。因此，结果将在应用程序中多次执行。

感谢您期待任何建议！

Answer 1

我们来定义一个名为eval的函数，它将执行组合器评估的一个步骤。首先，我们需要考虑究竟构成一个单一的步骤。任意地，我们将首先评估左边最外面的表达并从那里开始工作。

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 

请注意，规则仅适用于实际更改表达式的情况。这些定义的尴尬是由于Mathematica缺乏一种模式表达式，它会匹配任意长的curried参数列表。

现在，我们可以定义公认的组合程序，小号，ķ和我：

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

的符号是小写这里主要是为了避免方式数学呈现内置符号I，虚数单位。

任何其他组合程序将被视为变量并留下未评估：

eval1[e_] := e 

现在我们可以尝试一下基本情况：

i[f] // eval 

(* f *) 

k[f][g] // eval 

(* f *) 

s[f][g][h] // eval 

(* f[h][g[h]] *) 

更多有趣的情况，让我们定义evalAll显示所有评估链中的步骤：

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采用可选的“count”参数来限制显示的步数。这是不同的表达有用的 - 像Ÿ组合子的直接表达：

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]]]]] 
*) 

...但它是表达在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[...]]] 
*)