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大定理聲明對方程an+bn= cn，對正整數a，b與c，以及整數n>2，不存在解。這裡n=3且a，b，c在範圍[1..1000]。在一個使用32位整數的平台上，1000是一個合理的最大值，因為2*10003與231沒有太大差别。

結果是，當啟用優化時，幾個編譯器（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 <stdio.h>

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是更好還是更壞？沒有一個結果是合理的。