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

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

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

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

\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)，无论这个参数是什么，它在一个步骤中评估只是 something。因此你可以有一个图表其中只有一个节点表示 \z.z 对两个不同参数的两个应用，并且这两个应用可以在一步中减少。注意这个节点上有一个循环，因为“第一次出现”的说法恰恰是“第二次出现”。最后，通过最佳共享，您可以从(代表图表)\x。 (\z.z) ((\z.z) x)) 到(表示的图形)结果 \x.x 只需一个 beta 缩减步骤(加上一些簿记)。这基本上就是您的最佳评估器中发生的情况(图形表示也是防止空间爆炸的原因)。

稍微扩展的解释可以看论文Weak Optimality, and the Meaning of Sharing (您感兴趣的是引言和第 4.1 节，也许还有最后的一些引用书目)。

回到你的例子，对 Church 整数进行算术函数编码是“众所周知”的例子之一，在这些例子中，最优评估器可以比主流语言表现得更好(在这句话中，众所周知实际上意味着一些专家知道这些例子)。有关更多此类示例，请查看论文 Safe Operators: Brackets Closed Forever由 Asperti 和 Chroboczek 撰写(顺便说一句，您会在这里发现有趣的 lambda 项，这些 lambda 项不是 EAL 可类型化的；所以我鼓励您从这篇 Asperti/Chroboczek 论文开始看一看预言机)。

正如您自己所说，这种编码完全不切实际，但它们仍然是一种理解正在发生的事情的好方法。让我以进一步调查的挑战作为结束:你能否找到一个例子，在这些例子中，对这些所谓的错误编码的最佳评估实际上与对合理数据表示的传统评估相当？ (据我所知，这是一个真正的开放性问题)。