为什么 λ- 微积分最优计算器能够在没有公式的情况下计算大的模幂?

教堂数字是将自然数作为函数进行编码。

(\ 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

巧妙地,你可以用两个教堂的数字来指数化它们。也就是说,如果你应用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。为了科学,我开始强调它。它立即回答我 20^20%13 == 350^50%13 == 460^60%3 == 0。我必须使用 外部工具来验证这些结果,因为使用的是 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和它将被卡住,消除假设。

我用的最佳评估器是一个长达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))))))

我没有使用特定的同余关系算法或公式

5854 次浏览

这不是一个答案,但它是一个建议,你可能会开始寻找。

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

(a * x ^ y) % z

作为

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

如果计算器像这样计算,并且将累积参数 a保持为正常形式,那么您将避免使用太多的空间。如果您的评估器 确实是最优的,那么可以推测它不能做比这个更多的工作,所以特别是不能使用比这个时间更多的空间进行评估。

我真的不知道什么是最佳评估者,所以恐怕我不能把它做得更严格。

这种现象来自于共享的 β 减少步骤的数量,在 Haskell 风格的惰性评估(或通常的逐值调用,在这方面并不遥远)和 Vuillemin-Lévy-Lamping-Kathail-Asperti-Guerrini-(et al。.)“最佳”评估。这是一个通用特性,它完全独立于您可以在此特定示例中使用的算术公式。

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

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

使用一个(有向无环)图,其中只有一个代表 (\y.y)a的子图出现,以及针对该子图的两条边。用哈斯克尔的术语来说,你有一个只能评估一次的“思维”,这个“思维”有两个指标。

Haskell 风格的制表实现了完整子项的共享。这种级别的共享可以用有向无环图来表示。最优共享没有这个限制: 它也可以共享“部分”子项,这可能意味着图表示中的循环。

要了解这两个共享级别之间的区别,请考虑这个术语

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

如果你的分享仅限于完整的子条款,就像哈斯克尔的情况一样,你可能只有一个出现的 \z.z,但这里的两个 beta 索引将是不同的: 一个是 (\z.z) x,另一个是 (\z.z) ((\z.z) x),因为它们不是相等的条款,它们不能被共享。 如果允许共享部分子项,那么就可以共享部分术语 (\z.z) [](不仅仅是函数 \z.z,而是“应用于 什么的的函数 \z.z”) ,无论这个参数是什么,它在一个步骤中计算得到的结果只有 什么的。因此,您可以有一个图,其中只有一个节点表示 \z.z的两个应用程序到两个不同的参数,并且这两个应用程序可以在一个步骤中简化。注意,这个节点上有一个循环,因为“第一次出现”的参数恰好是“第二次出现”。 最后,通过最佳的共享,您可以从(表示图形的) \x. (\z.z) ((\z.z) x))到(表示图形的)结果 \x.x,只需要一个 beta 缩减步骤(加上一些簿记)。这基本上就是在最优计算器中发生的情况(图表也是防止空间爆炸的因素)。

对于稍微扩展的解释,您可以查看论文 弱最优性与共享的意义(您感兴趣的是引言和第4.1节,也许还有最后的一些书目指南)。

回到你的例子,在 Church 整数上运行的算术函数的编码是一个“众所周知”的例子,在这些例子中,最优计算器可以比主流语言表现得更好(在这个句子中,众所周知实际上意味着一些专家意识到了这些例子)。 更多这样的例子,看看阿斯珀蒂和 Chroboczek 的论文 安全操作员: 支架永远关闭(顺便说一下,你会在这里发现有趣的 lambda-术语,不是 EAL 类型的,所以我鼓励你看看甲骨文,从这篇 Asperti/Chroboczek 的论文开始)。

就像你自己说的,这种编码完全不实用,但它们仍然代表了一种很好的方式来理解正在发生的事情。最后,我想对进一步的研究提出一个挑战: 你能否找到一个例子,对这些所谓的坏编码的最佳评估实际上与对合理的数据表示的传统评估相当?(据我所知,这是一个非常开放的问题)。