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

Question

我开始学习函数式编程语言，如Haskell、ML，大部分练习都会展示以下内容：

   foldr (+) 0 [ 1 ..10]

相当于

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

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

  sum reverse list == sum list

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

Answer 1

编译器通常不会尝试自动证明这种事情，因为它很难实现。

除了向编译器添加逻辑以将一段代码转换为另一段代码外，您还必须非常小心，它只会在实际安全的情况下尝试执行此操作 - 即通常有很多“附带条件”担心。例如，在上面的示例中，有人可能编写了 Num 类型类的实例（因此是 (+) 运算符），其中 a + b 不是 b + a。

但是，GHC 确实有 rewrite rules，您可以将其添加到您自己的源代码中，并且可以用于涵盖一些相对简单的情况，例如您上面列出的情况，特别是如果您不太担心附带条件。

例如，我还没有对此进行测试，您可以对上述示例之一使用以下规则：

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

请注意 reverse list 周围的括号 - 您在问题中所写的内容实际上是指 (sum reverse) list 并且不会进行类型检查。

编辑：

当您在寻找官方资料和研究指南时，我列出了一些。 显然，很难证明是否定的，但没有人给出一个通用编译器的例子来例行执行这种事情，这一事​​实本身可能是非常有力的证据。

• 正如其他人所指出的，即使是简单的算术优化也非常危险，尤其是在浮点数上，并且编译器通常有标志来关闭它们 - 例如Visual C++、gcc。即使是整数运算也并不总是一目了然，人们偶尔会big arguments 讨论如何处理溢出等问题。

• 正如 Joachim 所指出的，循环中的整数变量是应用稍微更复杂的优化的地方，因为实际上有重大的胜利。 Muchnick's book 可能是该主题的最佳通用来源，但它并不便宜。 The wikipedia page on strength reduction 可能是对此类标准优化之一的很好的介绍，并且对相关文献有一些参考。

• FFTW 是一个在内部进行各种数学优化的库示例。它的一些代码是generated by a customised compiler 作者专门为此目的编写的。这是值得的，因为作者拥有特定领域的优化知识，在库的特定上下文中既值得努力又安全

• 人们有时使用模板元编程来编写“自我优化库”，这又可能依赖于算术身份，例如参见 Blitz++。 Todd Veldhuizen's PhD dissertation 有一个很好的概述。

• 如果你进入玩具和学术编译器的领域，各种各样的事情都会发生。例如my own PhD dissertation 是关于编写低效的功能程序以及解释如何优化它们的小脚本。许多示例（参见第 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 x c l，其中 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

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

Answer 4

您所描述的内容类似于super-compilation。在您的情况下，如果表达式具有 Int 之类的 monomorphic 类型（与多态 Num a => a 相反），编译器可以推断出表达式 foldr (+) 0 [1 ..10] 没有外部依赖项，因此可以在编译时对其进行评估并替换为55。但是，AFAIK 目前还没有主流编译器进行这种优化。

（在函数式编程中，“证明”通常与不同的东西相关联。在具有dependent types 类型的语言中，类型足以表达复杂的命题，然后通过Curry-Howard correspondence 程序成为此类命题的证明。）

Answer 5

正如其他人所指出的，目前还不清楚您的简化是否适用于 Haskell。例如，我可以定义

newtype NInt = N Int
instance Num NInt where
  N a + _ = N a
  N b * _ = N b
  ... -- etc

现在sum . reverse :: Num [a] -> a 不等于sum :: Num [a] -> a，因为我可以将每个都专门化为[NInt] -> NInt，而sum . reverse == sum 显然不成立。

这是围绕优化“复杂”操作存在的一种普遍矛盾——实际上，您需要大量信息才能成功证明优化某些东西是可以的。这就是为什么确实存在的语法级编译器优化通常是单态的并且与程序的结构相关——它通常是一个如此简化的域，以至于优化“没有办法”出错。即使这样也常常是不安全的，因为域从来没有相当如此简化并为编译器所熟知。

例如，一个非常流行的“高级”句法优化是流融合。在这种情况下，编译器被提供了足够的信息来知道流融合可能发生并且基本上是安全的，但即使在这个规范的例子中，我们也必须绕开不终止的概念。

那么如何将\x -> sum [0..x] 替换为\x -> x*(x + 1)/2？编译器需要内置的数论和代数。这在 Haskell 或 ML 中是不可能的，但在 Coq、Agda 或 Idris 等依赖类型语言中变得可能。在那里你可以指定诸如

之类的东西

revCommute :: (_+_ :: a -> a -> a) 
            -> Commutative _+_ 
            -> foldr _+_ z (reverse as) == foldr _+_ z as

然后，理论上，告诉编译器根据revCommute 重写。这仍然是困难和挑剔的，但至少我们有足够的信息。为了清楚起见，我在上面写了一些非常奇怪的东西，一个依赖类型。类型不仅取决于为内联参数引入类型和名称的能力，还取决于您的语言“在类型级别”的整个语法的存在。

不过，我刚刚写的和你在 Haskell 中做的有很多不同。首先，为了形成可以认真对待此类承诺的基础，我们必须抛弃一般递归（因此我们已经不必像流融合那样担心不终止的问题）。我们还必须有足够的结构来创建类似 Promise Commutative _+_ 的东西——这可能取决于语言的标准库中内置了完整的运算符和数学理论，否则您需要自己创建。最后，表达这些理论所需的类型系统的丰富性给整个系统增加了很多复杂性，并且抛弃了你今天所知道的类型推断。

但是，考虑到所有这些结构，我永远无法为定义为在NInts 上工作的_+_ 创建一个义务Commutative _+_，因此我们可以确定foldr (+) 0 . reverse == foldr (+) 0 实际上确实成立。

但现在我们需要告诉编译器如何实际执行优化。对于流融合，编译器规则只有在我们以完全正确的句法形式编写某些东西以“清楚地”成为优化 redex 时才会生效。同样的限制也适用于我们的sum . reverse 规则。事实上，我们已经沉没了，因为

foldr (+) 0 . reverse
foldr (+) 0 (reverse as)

不匹配。由于我们可以证明一些关于(.) 的规则，它们“显然”是相同的，但这意味着现在编译器必须调用两个内置规则才能执行我们的优化。

---

归根结底，您需要对已知规律集进行非常智能的优化搜索，以实现您所说的那种自动优化。

所以我们不仅给整个系统增加了很多复杂性，需要大量的基础工作来构建一些有用的代数理论，并且失去了图灵完备性（这可能不是最糟糕的事情），我们也只得到一个挑剔的承诺，除非我们在编译期间执行指数级痛苦的搜索，否则我们的规则甚至会触发。

布莱赫。

---

今天存在的妥协往往是有时我们对正在编写的内容有足够的控制权大部分确定某个明显可以进行优化。这是流融合的机制，它需要大量隐藏类型、精心编写的证明、参数化的利用和挥手致意，才能让社区足够信任以在他们的代码上运行。

而且它甚至不总是开火。有关解决该问题的示例，请查看 Vector 的所有 RULES pragma 的来源，其中指定了 Vector 的流融合优化应该启动的所有常见情况。

---

所有这些都不是对编译器优化或依赖类型理论的批评。两者都非常不可思议。相反，它只是对引入这种优化所涉及的权衡的放大。不能轻易做。

Answer 6

有趣的事实：给定两个任意公式，对于相同的输入，它们是否都给出相同的输出？这个微不足道的问题的答案是不可计算的！换句话说，在数学上不可能编写一个总是在有限时间内给出正确答案的计算机程序。

鉴于这一事实，没有人拥有能够神奇地将所有可能的计算转换为最有效形式的编译器，这也许不足为奇。

另外，这不是程序员的工作吗？如果您想要一个算术序列的总和足够普遍，以至于它成为性能瓶颈，为什么不自己编写一些更高效的代码呢？同样，如果您真的想要斐波那契数（为什么？），请使用 O(1) 算法。