为什么 λ-calculus 最优评估器能够在没有公式的情况下计算大模幂？

Question

教会数字是自然数作为函数的编码。

(\ f x → (f x))             -- church number 1
(\ f x → (f (f (f x))))     -- church number 3
(\ f x → (f (f (f (f x))))) -- church number 4

巧妙地，您只需应用 2 个教堂数字即可对其求幂。也就是说，如果你申请 4 到 2，你会得到教会编号16，或2^4。显然，这是完全不切实际的。教会数字需要线性内存，而且非常非常慢。计算10^10 之类的东西——GHCI 很快就能正确回答——这需要很长时间，而且无论如何都无法容纳计算机上的内存。

我最近一直在尝试使用最优 λ 评估器。在我的测试中，我不小心在我的最佳 λ 计算器上输入了以下内容：

10 ^ 10 % 13

它应该是乘法，而不是求幂。在我绝望地动动手指终止这个永远运行的程序之前，它回答了我的请求：

3
{ iterations: 11523, applications: 5748, used_memory: 27729 }

real    0m0.104s
user    0m0.086s
sys     0m0.019s

随着我的“错误警报”闪烁，我去谷歌验证，10^10%13 == 3 确实如此。 但是 λ 计算器不应该找到那个结果，它几乎不能存储 10^10。我开始强调它，为了科学。它立即回复了我20^20%13 == 3、50^50%13 == 4、60^60%3 == 0。我不得不使用external tools 来验证这些结果，因为Haskell 本身无法计算它（由于整数溢出）（如果你使用整数而不是整数，当然！）。将其推向极限，这是200^200%31的答案：

5
{ iterations: 10351327, applications: 5175644, used_memory: 23754870 }

real    0m4.025s
user    0m3.686s
sys 0m0.341s

如果我们为宇宙中的每个原子拥有一个宇宙副本，并且我们为每个原子拥有一台计算机，我们就无法存储教会编号200^200。这促使我质疑我的 Mac 是否真的那么强大。也许最佳评估器能够跳过不必要的分支并以与 Haskell 对惰性评估相同的方式直接得出答案。为了测试这一点，我将 λ 程序编译到 Haskell：

data Term = F !(Term -> Term) | N !Double
instance Show Term where {
    show (N x) = "(N "++(if fromIntegral (floor x) == x then show (floor x) else show x)++")";
    show (F _) = "(λ...)"}
infixl 0 #
(F f) # x = f x
churchNum = F(\(N n)->F(\f->F(\x->if n<=0 then x else (f#(churchNum#(N(n-1))#f#x)))))
expMod    = (F(\v0->(F(\v1->(F(\v2->((((((churchNum # v2) # (F(\v3->(F(\v4->(v3 # (F(\v5->((v4 # (F(\v6->(F(\v7->(v6 # ((v5 # v6) # v7))))))) # v5))))))))) # (F(\v3->(v3 # (F(\v4->(F(\v5->v5)))))))) # (F(\v3->((((churchNum # v1) # (churchNum # v0)) # ((((churchNum # v2) # (F(\v4->(F(\v5->(F(\v6->(v4 # (F(\v7->((v5 # v7) # v6))))))))))) # (F(\v4->v4))) # (F(\v4->(F(\v5->(v5 # v4))))))) # ((((churchNum # v2) # (F(\v4->(F(\v5->v4))))) # (F(\v4->v4))) # (F(\v4->v4))))))) # (F(\v3->(((F(\(N x)->F(\(N y)->N(x+y)))) # v3) # (N 1))))) # (N 0))))))))
main = print $ (expMod # N 5 # N 5 # N 4)

这会正确输出1 (5 ^ 5 % 4) - 但是在10^10 上方抛出任何东西都会卡住，从而消除假设。

optimal evaluator I used 是一个 160 行长、未优化的 JavaScript 程序，它不包含任何类型的指数模数学 - 而我使用的 lambda 演算模函数同样简单：

(λab.(b(λcd.(c(λe.(d(λfg.(f(efg)))e))))(λc.(c(λde.e)))(λc.(a(b(λdef.(d(λg.(egf))))(λd.d)(λde.(ed)))(b(λde.d)(λd.d)(λd.d))))))

我没有使用特定的模运算算法或公式。 那么，最佳评估者如何能够得出正确的答案？

Answer 1

这不是 anwser，而是建议您从哪里开始寻找。

有一种简单的方法可以在很小的空间内计算模幂，特别是通过重写

(a * x ^ y) % z

作为

(((a * x) % z) * x ^ (y - 1)) % z

如果评估者这样评估并保持累积参数a 为正常形式，那么您将避免使用太多空间。如果您的评估器确实是最佳的，那么大概它不能比这个做更多的工作，所以特别是不能使用比这个评估所花费的时间更多的空间。

我不太确定最佳评估者到底是什么，所以恐怕我不能让这个更严格。

Answer 2

这种现象来自于共享 beta-reduction 步骤的数量，这在 Haskell 风格的惰性评估（或通常的按值调用，在这方面并没有那么远）和 Vuillemin-Lévy 中可能有很大不同-Lamping-Kathail-Asperti-Guerrini-（等人……）“最佳”评估。这是一个通用功能，它完全独立于您可以在此特定示例中使用的算术公式。

共享意味着拥有您的 lambda-term 的表示形式，其中一个“节点”可以描述您所代表的实际 lambda-term 的几个相似部分。例如，您可以表示术语

\x. x ((\y.y)a) ((\y.y)a)

使用（有向无环）图，其中仅出现一次表示(\y.y)a 的子图，并且有两条边指向该子图。在 Haskell 术语中，你有一个 thunk，你只评估一次，还有两个指向这个 thunk 的指针。

Haskell 风格的记忆实现了完整子项的共享。这种共享水平可以用有向无环图来表示。最优共享没有这个限制：它还可以共享“部分”子项，这可能意味着图表示中的循环。

要查看这两种共享级别之间的区别，请考虑术语

\x. (\z.z) ((\z.z) x)

如果您的共享仅限于完整的子项，就像在 Haskell 中的情况一样，您可能只会出现一次 \z.z，但这里的两个 beta-redexes 将是不同的：一个是 (\z.z) x，另一个是是(\z.z) ((\z.z) x)，并且由于它们不是相等的术语，因此它们不能共享。 如果允许共享部分子项，则可以共享部分项(\z.z) []（这不仅仅是函数\z.z，而是“应用于某物的函数\z.z） , 无论这个论点是什么，它都在一步中评估为 something。因此，您可以有一个图，其中只有一个节点表示 \z.z 对两个不同参数的两个应用，其中这些一步可以约简两个应用，注意这个节点有一个循环，因为“第一次出现”的参数恰好是“第二次出现”。 最后，通过最佳共享，您可以从（表示）\x. (\z.z) ((\z.z) x)) 到（表示）结果\x.x，只需进行 beta 缩减（加上一些簿记）。这基本上就是您的最佳评估器中发生的事情（图形表示也是防止空间爆炸的原因）。

对于稍微扩展的解释，您可以查看论文Weak Optimality, and the Meaning of Sharing（您感兴趣的是引言和第 4.1 节，可能还有最后的一些参考书目指针）。

回到您的示例，对 Church 整数工作的算术函数的编码是“众所周知”的示例之一，其中最优评估器的性能优于主流语言（在这句话中，众所周知的实际上意味着少数专家知道这些例子）。 有关更多此类示例，请查看 Asperti 和 Chroboczek 的论文 Safe Operators: Brackets Closed Forever（顺便说一下，您会在这里找到有趣的非 EAL 类型的 lambda-terms；所以我鼓励您看一下oracles，从这篇 Asperti/Chroboczek 论文开始）。

正如您自己所说，这种编码是完全不切实际的，但它们仍然代表了一种理解正在发生的事情的好方法。最后让我提出一个进一步调查的挑战：你能找到一个例子，在这个例子上，对这些所谓的错误编码的最佳评估实际上与对合理数据表示的传统评估相当吗？ （据我所知，这是一个真正的悬而未决的问题）。