组合器归约 Wolfram Mathematica

Posted 2023-05-08

【中文标题】组合器归约 Wolfram Mathematica

【英文标题】：Combinator Reduction Wolfram Mathematica

【发布时间】：2012-05-24 16:13:05

【问题描述】：

如何在 Mathematica 中实现组合子 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]]=a

一步减少是非常重要的。因此，结果将在应用中一步多次..

期待您的任何建议！！！

【问题讨论】：

还有 a Mathematica Stack Exchange site 用于 Mathematica 问题。

S和K的定义有错别字。它们应该是：S[x][y][z] -> x[z][y[z]] 和 K[x][y] -> x。哦，Y[a] -> a[Y[a]] 中缺少括号。

谢谢，关于缺少括号的问题是正确的。在我看来，使用这样简单的规则很有问题，因为这样 Mathematica 本身决定了应用它们的方式，但以特殊顺序使用它们对我来说非常重要——每次都应用到最左边的 redex

【参考方案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 缺少一个模式表达式来匹配任意长的柯里化参数列表。

现在我们可以定义可识别的组合子，S、K和I：

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

这里的符号都是小写的，主要是为了避免 Mathematica 渲染内置符号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”参数来限制显示的步数。这对于发散的表达式很有用——比如 Y 组合子的直接表达式：

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

【讨论】：

为了响应@Anna 对所需评估顺序的说明，我已将代码从“评估的应用顺序”更改为“正常的评估顺序”。我最初实现了前者，因为它缩短了我用作测试用例的推导，而且生成的推导与我在撰写此响应时咨询的来源相匹配。我仍然对评估顺序做出了一些随意的选择，但希望我已经展示了如果需要其他选择，可以如何调整代码。