编译器可以在数学上推断/证明吗？

Question

我开始学习函数式编程语言Haskell,ML大多数练习都会展示如下:

   foldr (+) 0 [ 1 ..10]

这相当于

   sum = 0
     for( i in [1..10] ) 
         sum += i

所以这让我想到为什么编译器不能知道这是算术级数并使用O(1)公式来计算？特别是对于FP没有副作用的纯语言？这同样适用

  sum reverse list == sum list

给定一个+ b = b + a和反向定义,编译器/语言可以自动证明吗？

Answer 1

编译器通常不会尝试自动证明这种情况,因为它很难实现.

除了将逻辑添加到编译器以将一个代码片段转换为另一个代码片段之外,您还必须非常小心,它只会在实际安全时尝试执行它 - 即通常需要担心许多"边条件".例如,在你上面的例子,有人会写的类型类的一个实例Num(因此(+)运营商),其中a + b是不是b + a.

但是,GHC确实有重写规则,您可以将其添加到您自己的源代码中,并可用于覆盖一些相对简单的情况,例如您在上面列出的情况,特别是如果您对侧面条件不太感兴趣.

例如,我还没有对此进行测试,您可以对上面的一个示例使用以下规则:

{-# RULES
  "sum/reverse"    forall list .  sum (reverse list) = sum list
    #-}

请注意括号reverse list- 您在问题中写的内容实际上意味着(sum reverse) list并且不会进行类型检查.

编辑:

当你正在寻找官方消息来源和研究指南时,我列举了一些.显然,很难证明是消极的,但事实上没有人给出了一个通用编译器的例子,它常常做这种事情本身可能是非常有力的证据.

• 正如其他人所指出的那样,即使是简单的算术优化也是非常危险的,特别是在浮点数上,编译器通常会有标志来关闭它们 - 例如Visual C++,gcc.即使是整数运算并不总是很明确,人们偶尔会有关于如何处理溢出等事情的大论点.

• 正如Joachim所指出的,循环中的整数变量是应用稍微复杂的优化的地方,因为实际上有很大的胜利.Muchnick的书可能是关于这个主题的最好的一般来源,但它并不便宜.关于强度降低的维基百科页面可能与这种标准优化中的任何一个一样好,并且对相关文献有一些参考.

• FFTW是一个在内部进行各种数学优化的库的例子.它的一些代码是由作者专门为此目的编写的定制编译器生成的.这是值得的,因为作者具有针对特定领域的优化知识,这些知识在图书馆的特定环境中既值得又安全

• 人们有时会使用模板元编程来编写"自我优化库",这些库又可能依赖于算术身份,例如参见Blitz ++.Todd Veldhuizen的博士论文有一个很好的概述.

• 如果你进入玩具和学术编纂领域的各种各样的事情.例如,我自己的博士论文是关于编写低效的函数程序以及解释如何优化它们的小脚本.许多示例(请参阅第6章)依赖于应用算术规则来证明基础优化的合理性.

此外,值得强调的是,最后几个示例是专门的优化,仅应用于代码的某些部分(例如,调用特定库),预计这些部分是值得的.正如其他答案所指出的那样,编译器搜索可能适用优化的整个程序中的所有可能位置实在太昂贵了.我上面提到的GHC重写规则是编译器的一个很好的例子,它为各个库提供了一种通用机制,以最适合它们的方式使用.

Answer 2

答案

不,编译器不会那样做.

一个原因

对于您的示例,它甚至会出错:由于您没有提供类型注释,Haskell编译器将推断出最常见的类型,即

foldr (+) 0 [ 1 ..10]  :: Num a => a

和类似的

(\list -> sum (reverse list)) :: Num a => [a] -> a

并且Num正在使用的类型的实例可能无法满足您建议的转换所需的数学定律.在其他任何事情之前,编译器应该避免改变程序的含义(即语义).

更务实:编译器可以检测到这种大规模转换的情况在实践中很少发生,因此实现它们是不值得的.

例外

注意值得注意的例外是循环中的线性变换.大多数编译器都会重写

for (int i = 0; i < n; i++) {
   ... 200 + 4 * i ...
}

至

for (int i = 0, j = 200; i < n; i++, j += 4) {
   ... j ...
}

或类似的东西,因为该模式经常出现在工作在数组上的代码中.

Answer 3

即使在存在单形类型的情况下,您所考虑的优化也可能无法完成,因为有太多的可能性和所需的知识.例如,在此示例中:

sum list == sum (reverse list)

编译器需要知道或考虑以下事实:

• sum = foldl(+)0
• (+)是可交换的
• 反向列表是列表的排列
• foldl xcl,其中x是可交换的,c是常量,对于l的所有排列产生相同的结果.

这一切似乎微不足道.当然,编译器最有可能查找sum并内联它的定义.可能要求(+)是可交换的,但请记住,这+只是另一个没有附加到编译器意义的符号.第三点需要编译器证明一些非平凡的属性reverse.

但重点是:

1. 您不希望执行编译器来对每个表达式执行这些计算.请记住,要使其真正有用,您必须积累大量关于许多标准函数和运算符的知识.

2. 您仍然无法替换上面的表达式,True除非您可以排除列表或某个列表元素位于底部的可能性.通常,人们不能这样做.f x == f x在所有情况下,您甚至无法进行以下"琐碎"优化

    f x `seq` True
   

对于,考虑一下

f x = (undefined :: Bool, x)

然后

f x `seq` True    ==> True
f x == f x        ==> undefined

话虽如此,关于你的第一个例子稍微修改了单态:

 f n = n * foldl (+) 0 [1..10] :: Int

可以想象通过将表达式移出其上下文并将其替换为常量的名称来优化程序,如下所示:

const1 = foldl (+) 0 [1..10] :: Int
f n = n * const1

这是因为编译器可以看到表达式必须是常量.