[译]C编译器反证Fermat大定理

作者:JohnRegehr, Professor of Computer Science, University of Utah, USA

原文地址: http://blog.regehr.org/archives/140

【更新:本文没有非常清楚地解释底下的问题。 我写了一篇更好的新博
】。

显然,我不是认真的:编译器不擅长解决高层次的数学问题,并且有很好的理由相信这个定理不能被反证。

不过我的话说得有点过了。最近——出于在这里无关紧要的原因——我想写一个无限循环的C代码,但编译器不理解这个循环是无限的。相反,如果我只是写

while (1) { }

for (;;) { }

大多数优化编译器将看到这个循环不能退出,并生成相应的代码。例如,给定这个C代码:

void foo (void)

{

for (;;) { }

open_pod_bay_doors();

}

大多数编译器将发布像这样的代码:

foo:

L2: jmp L2

在这个情形里,编译器不会发布对open_pod_bay_doors()的调用,也不会发布最后的返回指令,因为可证明两者都不会得到执行。

也许很有趣,LLVM/Clang认识到这个稍模糊的无限循环永不退出:

unsigned int i = 0;

do {

i+=2;

} while (0==(i&1));

面对有点头脑的一个循环优化器,我决定不再浪费时间,编写一个能阻挠所有编译器的终止分析的循环:

const int MAX = 1000;

int a=1,b=1,c=1;

while ((c*c*c) != ((a*a*a)+(b*b*b))) {

a++;

if (a>MAX) {

a=1;

b++;

}

if (b>MAX) {

b=1;

c++;

}

if (c>MAX) {

c=1;

}

}

这个循环仅当找到Fermat大定理一个特殊情形的一个反例。当然,Fermat大定理声明对方程a n
+b n
= c n
,对正整数a,b与c,以及整数n>2,不存在解。这里n=3且a,b,c在范围[1..1000]。在一个使用32位整数的平台上,1000是一个合理的最大值,因为2*1000 3
与2 31
没有太大差别。

结果是,当启用优化时,几个编译器(LLVM/Clang 2.7,Open64-x864.2.3,SunCC 5.10与IntelCC 11.1.072)亟不可待地允许这个循环终止。特别地,当这个循环被包含在一个函数里时,编译器发布看起来像这样的x86汇编代码:

fermat:

ret

当然,这意味着编译器已经反证了Fermat大定理。面对这个令人难以置信的数学发现,我屏住呼吸,在该函数末尾添加了一行代码来打印个反例:a,b,与c的值。不幸的是,它们的虚张声势以这个方式调用,所有的编译器发布实际执行所要求计算的代码,它当然不会终止。我感觉这些工具——像Fermat本身——在空白处没有足够的空间来解释它们的推理。

这里真正发生的是编译器优化以及终止分析长期不相称。换而言之,如果编译器对保留所翻译代码的终止属性有责任,它们应该不能执行(或执行难度增加)某些它们用来创建高效代码的优化。编译器开发者做出的一个选择——可能有意识的,虽然很难确定——速度优先于正确性。不过,都不是坏消息:WindRiver Diab C编译器,以及GCC的几个版本都做对了,没有改变我尝试例子的终止属性。

5/1周六的更新:看来LLVM开发人员不久前一直着手这个问题,他们最新的SVN没有包含这个错误。非常好!

5/1周六的更新:Reddit上的某人注意到(我的一个学生证实)Microsoft编译器确实有终止错误。VisualStudio 2008与2010中的编译器为Fermat函数生成代码,但然后对这个函数的调用被丢弃了,因为它被认为没有副作用(这也是LLVM在修复这个问题之前的行为)。

4/30周五的更新

我在这里尝试澄清在Reddit上及评论中出现的几个问题。同样我修正了Reddit上某人指出的,在Fermat大定理陈述中的一个错误。谢谢!

问:这真的重要吗?

答:是的,但仅在开发嵌入式软件时出现的非常特殊的情形里。 这里
描述了一个例子:发帖者希望main()退出时程序被模拟挂起。权宜之计是关闭优化编译代码。在一个嵌入式系统更新了固件,并等待看门狗时钟将处理器重启到新版本时,出现另一个例子。Gcc与WindRiver C编译器——两者都被大量用于嵌入式领域——得到正确的结束不是巧合。

问:因为无限循环是不好的形式,编译器终止它们不行吗?人们不应该让CPU睡眠,阻塞正在运行的线程吗,还是怎么着?

答:首先,不是所有的程序都有一个起作用的操作系统或甚至线程系统。嵌入式软件通常运行在裸硬件上。其次,一个程序的含义由语言标准定义,形式与此无关。参考我之前的博文 The compiler doesn’t care about yourintent

问:C标准允许还是禁止编译器终止无限循环?

答:在如何实现C程序上,编译器被给予了相当大的自由,但其输出的外部可见行为必须与程序在由 标准
描述的“C抽象机器”解释的时相同。许多学识渊博的人(包括我)把这视为必须不能该程序的终止行为。显然某些编译器作者不同意,或者不相信它很重要。理性的人不同意这个解释的事实,看起来意味着C标准是有缺陷的。相比之下, Java语言定义相当清晰,无限循环不会被JVM终止

问:你是说编译器应该进行终止分析吗?稍加简化为停机问题,那是不可能的。

答:终止分析完全不需要成为编译器的一部分。不过,我(及其他人)声明编译器在删除任何无用的循环之前,应该执行一个终止分析。虽然一般问题是不可计算的,但许多特定的实例是很容易解决的。

问:在本博中的Fermat代码会执行有符号整数溢出或其他未定义行为吗?

答:我不认为。

5/1周六的更新

问:你不知道费马大定理在1995年被证明了吗?

答:我确实知道。因为我在1995年获得了我的数学学位,对我来说错过这件事几乎不可能J。我开了个小玩笑,也是指出事实,证明,特别是复杂证明,会包含错误。实际上,正如有人会在注释里注意到,Wiles一开始的证明是错的。也注意到n=3的特例早就在1770年被证明了。

问:如果真的希望一个C里的无限循环,最好变通是什么?

答:正如几个人指出的,在一个volatile限定的变量上循环可能是最好的选择。但记住, 编译器不总是遵守volatile
……

5/1周六的另一个更新

这是一个有趣的完整程序,它比上面的代码更令人信服,因为它显式使用来自代码“反证定理”分支的返回值:

int fermat (void)

{

const int MAX = 1000;

int a=1,b=1,c=1;

while (1) {

if (((a*a*a) ==((b*b*b)+(c*c*c)))) return 1;

a++;

if (a>MAX) {

a=1;

b++;

}

if (b>MAX) {

b=1;

c++;

}

if (c>MAX) {

c=1;

}

}

return 0;

}

#include

int main (void)

{

if (fermat()) {

printf (“Fermat’sLast Theorem has been disproved.n”);

} else {

printf(“Fermat’s Last Theorem has not been disproved.n”);

}

return 0;

}

这是Inte与Sun编译器的输出:

[email protected]:~$icc fermat2.c -o fermat2

[email protected]:~$./fermat2

Fermat’s Last Theoremhas been disproved.

[email protected]:~$suncc -O fermat2.c -o fermat2

“fermat2.c”,line 20: warning: statement not reached

[email protected]:~$./fermat2

Fermat’s Last Theoremhas been disproved.

Open64-x86与LLVM/Clang 2.7具有相同的行为。虽然许多无关紧要的人不同意,看起来对我非常清楚:这是这些编译器中一个严重的错误。我的意思是,为什么返回1?返回0是更好还是更坏?没有一个结果是合理的。

稿源:wuhui_gdnt的专栏 (源链) | 关于 | 阅读提示

本站遵循[CC BY-NC-SA 4.0]。如您有版权、意见投诉等问题,请通过eMail联系我们处理。
酷辣虫 » 综合技术 » [译]C编译器反证Fermat大定理

喜欢 (0)or分享给?

专业 x 专注 x 聚合 x 分享 CC BY-NC-SA 4.0

使用声明 | 英豪名录

登录

忘记密码 ?

切换登录

注册