Mai*_*tor 130 algorithm haskell functional-programming lambda-calculus modular-arithmetic
教会号码是自然数字作为函数的编码.
(\ 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^10GHCI快速正确回答的类似计算的东西需要很长时间,无论如何都无法适应你计算机上的内存.
我最近一直在尝试最佳的λ评估员.在我的测试中,我不小心在我的最佳λ计算器上键入了以下内容:
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.我不得不使用外部工具来验证这些结果,因为Haskell本身无法计算它(由于整数溢出)(当然,如果你使用整数而不是Ints!).推动它到极限,这是答案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-calculus模数函数同样简单:
(?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))))))
我没有使用特定的模运算法或公式.那么,最佳评估者如何能够得出正确的答案呢？
小智 120
这种现象来自共享的β减少步骤的数量,这在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风格的memoization实现了完整子项的共享.这种共享级别可以由有向非循环图表示.最佳共享没有这个限制:它还可以共享"部分"子项,这可能意味着图表表示中的循环.
要查看这两个共享级别之间的差异,请考虑该术语
\x. (\z.z) ((\z.z) x)
如果您的共享被限制为完整的子类,就像Haskell中的情况一样,您可能只有一次出现\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,只需一步减少β(加上一些簿记).这基本上是在您的最佳评估器中发生的事情(图表表示也是防止空间爆炸的原因).
对于略微扩展的解释,您可以查看论文弱最优性和共享的含义(您感兴趣的是引言和4.1节,也可能是最后的一些书目指针).
回到你的例子,对教会整数起作用的算术函数的编码是一个"众所周知"的例子,其中最优评估者的表现优于主流语言(在这句话中,众所周知的实际意味着少数几个专家知道这些例子).有关更多此类示例,请查看Asperti和Chroboczek撰写的安全操作员:Brackets Forever关闭的文章(顺便说一下,您将在这里找到有趣的lambda术语,这些术语不是EAL类型的;所以我鼓励您采取从这篇Asperti/Chroboczek论文开始,看一下神谕.
正如你自己所说,这种编码完全不实用,但它们仍然是理解正在发生的事情的好方法.最后,让我对进一步调查提出挑战:您能否找到一个例子,对这些所谓的不良编码进行最佳评估实际上与传统的合理数据表示评估相同？(据我所知,这是一个真正的开放式问题).
这不是一个anwser,但它建议你可以开始寻找.
有一种简单的方法可以在很小的空间内计算模幂运算,特别是通过重写
(a * x ^ y) % z
如
(((a * x) % z) * x ^ (y - 1)) % z
如果评估者像这样评估并保持a正常形式的累积参数,那么您将避免使用太多空间.如果你的评估者确实是最优的,那么可能它不能做比这个更多的工作,所以特别是不能使用比评估时间更多的空间.
我真的不确定最佳评估者究竟是什么,所以我担心我不能做得更严谨.