2026年9月10日星期四

語言的語言：BNF 從哪裡來，又怎麼用 - 2026.09.10

底下這篇，為 Grok AI 所撰述。

語言的語言：BNF 從哪裡來，又怎麼用

2026.09.10

參考：Matt Might，The language of languages
ALGOL 60 報告：Revised Report on the Algorithmic Language ALGOL 60
延伸：ISO/IEC 14977（EBNF）、RFC 5234（ABNF）

數學家習慣先把符號講清楚，再開始推。工程師比較急：先把程式寫出來，語法「大概長這樣」就交給同事用英文猜。猜到第三次，會議室裡會出現一種很特別的安靜——每個人都以為自己懂了，每個人懂的都不一樣。

1950 年代末，寫程式語言規格的人正面對這件事。他們需要的不是另一種程式語言，而是一種專門用來描寫語言的語言。後來大家叫它 BNF：巴科斯範式（Backus Normal Form），也常寫成巴科斯–諾爾範式（Backus–Naur Form）。

Matt Might 有一句話把這件事講得很乾淨：Grammars are the language of languages. 文法是語言的語言。本篇就沿著這句話走：BNF 為什麼會出現、規則怎麼讀、後來又長成什麼樣子。不打算把編譯器課本搬進來。目標比較謙虛——看完之後，再遇到一串尖括號和 ::=，不會覺得那是從別的星球寄來的符咒。

先有語言，才發現語言自己不會說話

FORTRAN 已經證明一件大事：人可以不直接對機器下指令，改寫比較像公式的東西。問題是，FORTRAN 的「合法寫法」大多還是用普通英文交代。英文很適合講故事，不太適合當合約。同一個句子，三位實作者可以讀出三種邊界情況。

1958 年，歐美兩邊的委員會想做一套不綁特定機器的算法語言，先叫 IAL（International Algebraic Language），後來改名 ALGOL。理想很大：一份規格，大家讀完應該寫出同一種語言。理想一落地，就撞上更老的問題——規格本身用什麼寫？

John Backus 當時已經因 FORTRAN 出了名。1959 年 6 月，他在巴黎的 UNESCO 資訊處理會議上提出一篇論文，標題很老實：The Syntax and Semantics of the Proposed International Algebraic Language of the Zurich ACM-GAMM Conference。重點不在再發明一套語句，而在發明一套「後設公式」（metalinguistic formulas），專門描寫哪些符號序列算合法程式。

他的靈感比較靠近 Emil Post 的產生式，而不是語言學課堂上的樹狀圖。想法卻很樸素：左邊放一個名字，右邊寫這個名字可以長成什麼；需要分支就寫「或」。人讀得懂，機器原則上也能跟著長。

Peter Naur 讀這份報告時，第一反應並不浪漫。他後來回憶，自己先是失望：蘇黎世會議以為大家已經講清楚的事，Backus 寫出來的版本卻對不太上。換句話說，連委員會內部都還沒共用同一張圖。Naur 後來說，他是過了一陣子才穿透那套形式語法，然後立刻改觀——這種記法正好是他想用來寫 ALGOL 的工具。

於是 ALGOL 60 報告裡，語法不再只靠散文。Naur 當編輯，把 Backus 的符號改成當時打字機比較友善的樣子：定義號變成 ::=，「或」變成 |，被定義的東西用 <...> 包起來。1960 年的報告一出，BNF 就不再只是一篇會議論文裡的私房記號，而成了公共契約。

為什麼需要 BNF？一句話：英語會讓人以為自己同意了。BNF 逼你把「可以長成什麼」寫成可核對的規則。ALGOL 想當國際語言，先得讓規格自己講同一種話。

名字怎麼從 Normal 變成 Naur

一開始它叫 Backus Normal Form，巴科斯範式。Normal form 聽起來很數學：範式、標準形，好像世界上只該有一種正確寫法。問題是，BNF 並不是那種東西。同一套語言，你可以寫得很肥，也可以寫得>很瘦；兩份文法可以生成同一堆句子，長得卻完全不像。

1964 年，Donald Knuth 在《Communications of the ACM》投了一封不長的信。他建議改叫 Backus–Naur Form。理由很乾脆：第一，Naur 把這套記法寫進 ALGOL 60，功勞不該被「範式」兩個字吞掉；第二，縮寫仍然是 BNF，舊文獻不用作廢；第三，它根本不是 normal form。

建議被接受了。所以你現在會同時看到兩種中譯：巴科斯範式、巴科斯–諾爾範式。指的是同一件事。比較像有人同時有戶籍名和筆名，信件都能送到。

再往前追，還有人主張記更早的祖先。1967 年 P. Z. Ingerman 投書，說公元前的波你尼（Pāṇini）為梵語寫過一套產生規則，力量上已接近後世的上下文無關文法。有人因此提議叫 Pāṇini–Backus Form。這個名字沒有成為主流，但提醒一件有用的事：BNF 不是從石頭縫裡蹦出來的。人類很早就發現，語言可以用「名字展開成片段」來描寫；電腦只是第一次迫切需要一份大家都能簽字的展開表。

BNF 到底在寫什麼

BNF 描寫的是上下文無關文法（context-free grammar）。名字聽起來嚇人，意思卻很日常：一條規則要不要用，只看你現在手上這個名字，不看它左邊鄰居是誰、右邊隔壁姓什麼。

Matt Might 把一條規則拆成兩截：一個名字，以及這個名字的展開。數學書裡常寫成箭頭

名詞片語 → 冠詞　名詞

於是「the dog」可以被承認是一個名詞片語。換成程式，同一手勢變成

運算式 → 運算式　+　運算式

BNF 只是把「可以展開成」寫成比較像規格書的符號：

<name> ::= expansion

::= 讀作「可以是」或「可以換成」。有人叫左邊那個名字非終結符（non-terminal）：它還不是成品，只是一張待填的標籤。真正出現在程式裡、不能再拆的字面量，叫 終結符（terminal），例如 "+"、"begin"、數字 7。

經典寫法裡，非終結符一律用尖括號< >包住，左邊右邊都包，以免跟語言裡自己的符號打架。展開式靠兩種動作拼起來：

並置：兩個東西寫在一起，就表示先出現這個、再出現那個。
選擇：直杠 | 表示「左邊或右邊，挑一個」。

就這樣。沒有迴圈關鍵字，沒有「重複三次」的專用符號。若要重複，就讓規則叫自己的名字——遞迴。ALGOL 60 報告裡，無號整數幾乎是教科書第一題：

<digit> ::= 0 | 1 | 2 | 3 | 4 | 5 | 6 | 7 | 8 | 9

<unsigned integer> ::= <digit>
                     | <unsigned integer> <digit>

第一條說：一位數就是那十個符號之一。第二條說：無號整數要嘛是一位數，要嘛是「已經是無號整數，後面再貼一位數」。於是 7 合法，70 合法，708 也合法。你沒寫「任意多位」，規則自己會長出任意多位。

這就是 BNF 最可愛、也最容易讓人一開始不放心的地方：它幾乎不描述「做多少次」，只描述「還能再貼一層嗎」。層數交給展開過程去數。

怎麼讀：從一條算術式開始

Matt Might 文裡那份「經典、而且刻意寫得不含糊」的運算式文法，值得整份看一次。符號換成交際上最常見的 BNF 寫法：

<expr>   ::= <term> "+" <expr>
           | <term>

<term>   ::= <factor> "*" <term>
           | <factor>

<factor> ::= "(" <expr> ")"
           | <const>

<const>  ::= integer

四個名字，分工清楚。<expr> 管加減這一層，<term> 管乘除這一層，<factor> 管括號或數字。乘被放在比加「更裡面」的名字裡，於是 3 * 7 + 1 不會被讀成「先加再乘」——不是因為我們寫了「乘優先」，而是因為文法的分層已經把優先序編進去了。

現在問一個很小的問題：3 * 7 為什麼算合法運算式？Might 的答法是一路展開，像拆禮物：

<expr> 可以是 <term>
<term> 可以是 <factor> "*" <term>
右邊那個 <term> 再收成 <factor>
兩個 <factor> 都收成 <const>
兩個常數分別是 3 與 7

走完這條路，紙上剩下的正好是 3 * 7。沒多符號，也沒少符號。這就叫「這個句子由文法生成」，或反過來說「這串字可以被這份文法接受」。

讀 BNF 時，手邊最好準備兩種動作：

往下長：從起始符號出發，把非終結符換成右邊的展開，直到只剩終結符。這是在問「這份語言裡有哪些句子」。
往上收：拿一串現成的字，問能不能找到一棵對得上的展開樹。這是在問「這句話合不合法」。編譯器前端做的，大致就是第二種，只是它還要在對上之後幫你長出語法樹。

第一種像依照食譜做菜。第二種像吃到一道菜，倒推它用了哪一頁食譜。同一份 BNF，兩種讀法都成立。

自己寫一份：從電話號碼到命題公式

寫 BNF 最穩的順序不是先追求漂亮，而是先問三個問題：最小的磚塊是什麼？磚塊怎麼拼成一塊牆？牆要不要允許再往上加一層？

先來一個生活裡的例子。假設我們只承認台灣常見的市話寫法：區碼兩到三位，後面一串數字，中間可以有連字號。

<digit>      ::= 0 | 1 | 2 | 3 | 4 | 5 | 6 | 7 | 8 | 9
<digits>     ::= <digit> | <digits> <digit>
<area-code>  ::= <digit> <digit>
               | <digit> <digit> <digit>
<phone>      ::= <area-code> <digits>
               | <area-code> "-" <digits>

02-23622737 對得上。02-ABC 對不上，因為 A 不是 <digit>。文法在這裡扮演的不是審美委員，是門房：只回答「進不進得來」。

再寫一個比較接近數學筆記本的例子——命題公式。原子命題用字母，連詞只留否定、合取、析取、蘊涵，必要時加括號：

<atom>    ::= "p" | "q" | "r"
<formula> ::= <atom>
            | "~" <formula>
            | "(" <formula> "/\\" <formula> ")"
            | "(" <formula> "\\/" <formula> ")"
            | "(" <formula> "->" <formula> ")"

於是 p 是公式，~p 是公式，(p /\ q) 是公式，(p /\ q) -> r 還差一對括號——照這份文法，外層蘊涵也得包起來，寫成 ((p /\ q) -> r)。這不是文法在挑剔，是它拒絕用「你應該知道我的意思」來補句子。

如果你之後要在證明助手裡自訂一套對象語言，BNF 往往是紙上的第一張圖。機器裡真正出現的是歸納型別：每個 | 對應一個建構子，遞迴的名字對應型別自己出現在自己的欄位裡。BNF 管「字長什麼樣子」，歸納型別管「資料長什麼樣子」。兩張圖對得上，後面的推論才不會建築在口語的縫隙上。

寫 BNF 的小癖好：起始符號先定下來；終結符能加引號就加引號；同一個概念不要用兩個名字；遞迴發生在你真正想重複的地方，而不是因為一時想不出怎麼寫「一列東西」。

一份可以描寫自己的文法

Might 文裡有一段很好玩：BNF 規則自己也可以有文法。稍微整理成比較好讀的樣子：

<rule>      ::= <name> "::=" <expansion>
<name>      ::= "<" <identifier> ">"
<expansion> ::= <expansion> <expansion>
              | <expansion> "|" <expansion>
              | <name>
              | <terminal>

這不是在玩套娃。它在提醒：BNF 也是一種語言，所以它自己也有語法。後設語言並不神秘，只是把「我們用來講話的那層」也寫成規則。當然，這份小文法有點太寬——它沒處理括號優先，也沒禁止無限往左長。規格書若要給機器吃，後面通常還會再收緊。

識別名、數字、空白這些「字詞一層」的東西，BNF 常常不硬扛。Might 的說法很實在：這類終結符的集合，多用正規表示式或乾脆用散文定義。BNF 擅長的是樹狀結構，不是「這串空白要不要折起來」。

之後的發展：大家嫌它不夠寫，就開始加配件

經典 BNF 故意很瘦。瘦的代價是羅嗦。要寫「可有可無的負號」或「零個或多個參數」，你得額外發明一個名字，再讓它遞迴一次。人一眼能懂的事，紙上卻要繞一圈。

於是配件開始出現。

1977 年，Niklaus Wirth 在 CACM 登了一篇短文，標題幾乎是抱怨：What Can We Do About the Unnecessary Diversity of Notation for Syntactic Definitions? 程式語言愈出愈多，語法記法卻每人一套，差異小到讓人生氣，又大到讓人每次重學。他提出的折衷，後來被稱為 EBNF（Extended BNF）。常見的加料是：

寫法	意思
`[ x ]`	`x` 可有可無
`{ x }`	`x` 可重複零次或多次
`( x \| y )`	先把選擇括在一起，再跟別的東西並置

於是 Might 文裡那兩個例子，讀起來就不再需要額外的輔助名字：

<term> ::= [ "-" ] <factor>
<args> ::= <arg> { "," <arg> }
<expr> ::= <term> ( "+" | "-" ) <expr>

EBNF 並沒有讓語言變得「更強」——能生成的句子，經典 BNF 理論上也能生成。它讓人少發明幾個只出現一次的臨時名字。ISO/IEC 14977:1996 後來把 EBNF 收成國際標準；2023 年還確認過一次，證明這套配件夠用，也證明標準文件的壽命可以比許多程式語言長。

網際網路這條線走了另一個方言。ABNF（Augmented BNF）出現在 IETF 的 RFC 裡，現在以 RFC 5234 為主。協定規格在乎的是位元組、大小寫、重複次數的上下限，所以 ABNF 讓你寫 2*3DIGIT 這種「最少兩位、最多三位」的數字，註解用分號，規則名通常不分大小寫。讀 HTTP、郵件、URI 的規格，看到的多半是它，不是 ALGOL 報告裡的尖括號。

同一時期還有別的親戚。Wirth 自己在 Pascal 文件裡用過語法圖（鐵路圖）：眼睛沿著軌道走，比純文字更直觀。ALGOL 68 嫌 BNF 不夠細，改用 van Wijngaarden 的兩層文法，精確很多，讀起來也累>很多。後來的程式語言手冊，有人繼續寫 BNF／EBNF，有人改用 PEG、有人直接把 parser combinator 當成規格。萬變不離那個核心：先有一份大家認帳的結構描寫。

再往實作走，BNF 幾乎變成編譯器的出生證明。yacc、bison、ANTLR 這類工具吃進去的，就是某一種方言的文法；吐出來的是剖析器。你在紙上寫 |，工具在程式裡寫分支。人負責把語言想清楚，機器負責不讓非法句子混進後門。

BNF 不負責的事

讚美寫完，該把邊界講清楚。否則 BNF 很容易被當成萬能符。

第一，它只管語法，不管意思。你可以寫出一份承認 1 / 0 的運算式文法。文法說這串字合法；數學說這串字還沒有值。ALGOL 報告自己也把語法和語意分開寫，不是偶然。

第二，它預設規則不看上下文。變數「先宣告再使用」、同一識別名不能宣告兩次、型別要兩邊對上——這些都不是上下文無關文法擅長的活。程式語言通常的分工是：BNF 先把樹長出來，比較勢利的檢查留給之後的靜態分析。

第三，同一份語言可以對應很多份文法，有的友善、有的會打架。經典例子是「懸空的 else」：一個 else 該掛在哪一個 if 上，兩棵樹都合法，程式的意思卻不同。這時問>題不在 BNF 這套記號，而在你寫出來的規則允許太多故事同時成立。解法是改規則，或另外規定「就近搭配」這種閱讀慣例。

第四，BNF 的方言很多。有人保留 ::= 和尖括號，有人改成 = 然後替非終結符去掉括號；有人用引號包終結符，有人靠字體區分。讀一份新規格，先花三十秒看它的圖例，比爭論「正宗 BNF 長什麼樣子」有用。

怎麼用，才不算白認識它

認識 BNF 之後，比較實用的不是立刻去發明語言，而是先學會當一個有禮貌的讀者。

拿到一份規格，先找起始符號，再找終結符表。然後挑一句你以為自己懂的句子，用手走一次展開。走得通，這份文法才開始對你說話；走不通，多半不是你比較笨，是規則在某個 | 後面藏了例外。

若要自己寫，從最小的合法句子開始，再加一層結構。先讓 p 通過，再讓 ~p 通過，再讓帶括號的合取通過。每加一條規則，就準備一句應該被拒絕的反例。p /\ q /\ 這種尾巴空著的東西如果也能混進來，不是語言變寬了，是門房打瞌睡。

最後才考慮要不要換成 EBNF。配件能讓規則變短，也能讓人忘記遞迴到底發生在哪裡。短不是目的；可核對才是。

Might 的文章把常見記法收成一份對照，讀完確實能「在野外辨認文法」。本篇多走的那一截，是它背後的社交史：BNF 出現，不是因為有人突然想玩符號，而是一群人必須在紙上停止互相誤會。程式語言後來長出這麼多方言，規格書卻還在用差不多的尖括號——這大概是那次誤會被真正修好的證據。

語言會繼續增加。描述語言的語言，從 1959 年到現在，核心還是那一行：

<name> ::= expansion

左邊是我們想談的東西，右邊是它被允許長成的樣子。中間那支 ::=，只是把「我以為你懂」換成「你也可以檢查」。對寫規格的人來說，這已經很接近文明了。

主要依據：Backus 1959 年 UNESCO 論文與 ALGOL 60 報告的語法一章；Naur 後來關於 ALGOL 編輯過程的回憶；Knuth 1964 年 CACM 投書；Wirth 1977 年關於語法記法的短評；以及 Matt Might, The language of languages 對 BNF／EBNF／ABNF 的整理。歷史細節若有出入，以原始報告與信件為準。

2026年9月8日星期二

當餘弦變成零：一條不繞圈子的畢氏定理證明

改變世界的17個方程式

勾股定理 / 畢氏定理

Lean 學習筆記 Day 1 - 畢氏定理 - 2026.09.07

底下這篇為 Grok AI 所寫

當餘弦變成零：一條不繞圈子的畢氏定理證明

寫給喜歡把公式當故事讀的人

十二年前，我在這本筆記本裡隨手抄過一張名單：《改變世界的十七個方程式》。名單的第一行，不是牛頓的萬有引力，也不是愛因斯坦的 $E=mc^2$，而是一個國中生都能默寫的式子——

$a^2 + b^2 = c^2$

畢氏定理。貢獻者欄寫著「畢達哥拉斯，BC 530」。

名單後來我才知道，是英國數學家伊恩・史都華（Ian Stewart）那本《Seventeen Equations That Changed the World》的目錄縮影。史都華把這條看來土氣的直角三角形關係，放在改變世界的十七條方程式之首，不是為了懷舊，而是因為它幾乎是後來所有「距離」觀念的祖先：平面上兩點有多遠、地圖怎麼測、衛星怎麼定位，甚至相對論裡時空的度量，骨子裡都還認得出這個平方和。

一個國中公式，憑什麼排第一？證明又為什麼能跟三角函數扯上關係、而且據說還不循環論證？今晚我們慢慢說。

它比畢達哥拉斯本人更老

先說一件讓人有點洩氣、又有點痛快的事：這條定理大概不是畢達哥拉斯發明的。

西元前十九到十六世紀的巴比倫泥板——比薩摩斯那位哲學家大約早了一千年——已經出現勾股數，也就是滿足 $a^2+b^2=c^2$ 的整數三元組。著名的 Plimpton 322 像一份教師備課表，密密麻麻列著這些數組；另一塊泥板 YBC 7289 則在正方形對角線旁，用六十進位寫下 $\sqrt{2}$ 準到好幾位的近似值。那不是巧合，那是他們知道「邊長一的正方形，對角線平方等於二」。

同一段漫長的古代裡，印度《繩經》（Śulba Sūtras）用這條關係規畫祭壇；中國《周髀算經》留下「勾三股四弦五」以及後來被稱為「弦圖」的面積拼合。埃及測量師則長期被傳說成用 3-4-5 繩結在尼羅河氾濫後重新拉出直角——故事很美，證據比較稀，但「直角與三邊」這件事，顯然不是希臘人的獨家專利。

那畢達哥拉斯學派貢獻了什麼？比較公允的說法是：他們把一條工匠都在用的經驗規則，推進成「必須證明」的命題，並且把「數即宇宙」的信仰綁在幾何上頭。真正留下完整、可核對證明的，是大約三百年後歐幾里得《幾何原本》卷一命題 47：那張被叫作風車、新娘椅、或孔雀開屏的圖。歐氏證明不靠代數符號，只靠面積搬運。讀過一次，會覺得古人並不笨，只是紙張和符號都還沒發明到我們習慣的樣子。

憑什麼改變世界？

史都華把畢氏定理放第一，理由其實很樸素：它是幾何與代數第一次正式握手。

有了 $a^2+b^2=c^2$，平面上兩點 $(x_1,y_1)$、$(x_2,y_2)$ 的距離立刻變成

\[ \sqrt{(x_2-x_1)^2+(y_2-y_1)^2}. \]

座標不再只是格子紙上的標籤，而成了可以計算的空間。測繪師量角比量長容易，於是把大地剖成三角形，一站一站推過去——三角測量（triangulation）的骨架，就是直角三角形可以任意把斜邊拆開再拼回去。航海、地圖、後來的衛星定位，都還在做同一件事：用已知的幾條邊與角，把你不知道的那一點釘死。

它也催生了三角學。正弦、餘弦最初不是為了折磨高中生，而是為了把「邊」和「角」互相翻譯。再往前走一步，平方和這種度量進了物理：牛頓力學裡的距離、電磁學裡的場、相對論裡的時空間隔，都還看得到「平方相加」的影子。球面或彎曲時空上，直角三角形不再遵守畢氏定理——恰恰因為我們先>有了它，才知道「不遵守」意味著空間本身換了一套規則。

所以它改變世界，不是因為 $3^2+4^2=5^2$ 這句話特別響亮，而是因為人類從此有了一把通用的尺，去量「多遠」。

人類好像特別愛證明它

很少有定理像畢氏定理這樣，被當成數學界的全民運動會。

二十世紀美國教師 Elisha Scott Loomis 編過一本幾乎走火入魔的書，《The Pythagorean Proposition》。一九四〇年第二版收了三百七十種證明：歐幾里得的風車、印度婆什迦羅旁邊只寫一個字「看！」（Behold!）的拼圖、美國總統加菲爾德還在眾議員時期用梯形面積寫下的那一版、還有高中生投稿的新圖。金氏世界紀錄後來把它標成「被證明最多次的定理」。Loomis 自己還撂下一句很硬的話：三角證明不可能存在，因為三角學的基本恆等式——例如 $\sin^2\theta+\cos^2\theta=1$——本身就是畢氏定理穿了件新衣服。

這句話半對半錯。若你先偷偷使用 $\sin^2+\cos^2=1$，再回頭推 $a^2+b^2=c^2$，那確實是在原地轉圈，像用自己的影子證明太陽存在。可是「三角函數」這三個字，並不必然等於那條平方恆等式。餘弦可以先被定義成「鄰邊比斜邊」——一個純比例，還不需要平方和。接下來的問題就變成：我們能不能只靠這個比例，加上「把一段底邊拆成兩段再加回去」這種小學程度的線段加減，推出餘弦定理，再讓直角作為特例掉出來？

可以。而且路線意外地乾淨。

出發前：什麼是投影定理？

請想像任意三角形 $ABC$。依高中習慣，令 $\angle A,\angle B,\angle C$ 的對邊分別是 $a,b,c$。暫時假設三個角都是銳角，這樣作高時，垂足會乖乖落在對邊內部；鈍角只是把其中一段投影「翻到邊的延長線上」，代數幾乎一樣，只是餘弦變負號。

從頂點 $A$ 向 $BC$ 作高，垂足為 $D$。底邊 $a$ 被切成兩段：

\[ a = CD + BD. \]

這一步沒有用到畢氏定理，只是「整段等於兩段之和」。而「一段邊長投影到另一邊」正是餘弦的定義：

\[ CD = b\cos C, \qquad BD = c\cos B. \]

於是得到一條老實得近乎無聊的關係——有人稱之為投影定理，或第一餘弦定理：

\[ \text{（公式 1）}\quad a = b\cos C + c\cos B. \]

同樣的動作，分別從 $B$、從 $C$ 往對邊作高，再寫兩次：

\[ \text{（公式 2）}\quad b = a\cos C + c\cos A, \]

\[ \text{（公式 3）}\quad c = a\cos B + b\cos A. \]

三條式子，全部只靠「線段相加」與「鄰邊／斜邊」。平方還沒出場。畢氏定理也還沒被請進來。我們手上現在是一個三元一次方程組，未知數是三個餘弦。

一場名叫「消去」的代數小戲法

目標很明確：不想要的 $\cos A$、$\cos B$ 必須離場，只留下 $\cos C$。方法古老得像解國中聯立方程式——兩邊先乘一個公因數，再加加減>減。

步驟一。 三式分別乘上自己對應的邊長，好讓後面出現成對的交叉項：

\[ \begin{align*} a^2 &= ab\cos C + ac\cos B,\\ b^2 &= ab\cos C + bc\cos A,\\ c^2 &= ac\cos B + bc\cos A. \end{align*} \]

注意：這裡的「平方」不是從直角三角形面積變出來的，只是為了製造公因式 $ab$、$ac$、$bc$，人工乘上去的。有點像煮飯時多放一把米，不是因為米本身神聖，是因為待會要對沖。

步驟二。 計算 $a^2+b^2-c^2$：

\[ \begin{align*} a^2+b^2-c^2 &= (ab\cos C + ac\cos B)\\ &\quad + (ab\cos C + bc\cos A)\\ &\quad - (ac\cos B + bc\cos A). \end{align*} \]

盯著右邊看一會兒。$ac\cos B$ 先正後負，走了；$bc\cos A$ 先正後負，也走了。像一場安排好的退場，只剩兩個 $ab\cos C$ 還坐在位子上。

步驟三。

\[ a^2 + b^2 - c^2 = 2ab\cos C. \]

步驟四。 移項：

\[ c^2 = a^2 + b^2 - 2ab\cos C. \]

餘弦定理。全程沒有切出一個「用來套用畢氏定理」的直角三角形去算平方和，也沒有動用 $\sin^2+\cos^2=1$。

然後，讓角變成直角

現在把 $\angle C$ 設成 $90^\circ$。依餘弦在直角時的定義（或單位圓上的定義，兩者此時一致），

\[ \cos 90^\circ = 0. \]

修正項整段消失，留下

\[ c^2 = a^2 + b^2. \]

畢氏定理從餘弦定理的特例裡掉出來。邏輯順序是：

投影（線段加減）$\rightarrow$ 餘弦定理 $\rightarrow$ 直角時餘弦為零 $\rightarrow$ 畢氏定理。

不是「先承認畢氏，再推廣成餘弦，再假裝推回畢氏」。Loomis 擔心的那條循環，在這條路上沒有發生。平方的幾何執念也被拆開了：上一世代的證明裡，平方常常來自面積；這裡的平方，只是代數消去時的潤滑劑。

若你對「銳角假設」不放心：鈍角時，垂足落到邊的延長線，其中一段投影帶負號，公式 1 仍然成立，後面的加減一字不改。直角則是兩種情況的邊界——餘弦剛好過零的那一瞬。

這條路為什麼好看

第一，它把「證明」從剪紙遊戲變成簿記。你不必記得哪一塊正方形該搬到哪一塊；你只要相信線段可以相加，比例可以命名，然後老實做消去。對習慣代數的人，這比風車圖更像在呼吸。

第二，它讓餘弦定理不再只是「畢氏定理的加強版」這種教科書口吻。兩者的關係變成可逆、可選擇起點。古典幾何的投影，與後來線性代數裡用克拉瑪法則解同一組方程，其實是同一件事的兩套衣服。

第三，它提醒我們：數學史上許多「不可能」只是「你先把工具定義得太窄」。Loomis 說三角證明不存在，是因為他把三角學等同於那條平方恆等式。換一套出發定義，門就開了。近年美國兩位高中生用相似三角形與正弦定律寫出的證明，走的是另一條避開循環的路；投影這條，則更接近古典三角教室裡本來就有的家具。

名單上的第一行

回到十二年前那張名單。把畢氏定理放在「改變世界的十七個方程式」第一個，現在讀來仍合理：它夠老，夠簡單，夠容易被誤會成理所當然，卻又悄悄支撐了測繪、座標、導航，以及後來所有談論距離的語言。

證明可以有三百七十種，也可以再多一種。今晚這一種的好處不是比較短——老實講，歐氏風車圖更短——而是它讓你看清楚：平方不必一開始就帶著面積的光環登場；有時候，它只是為了讓兩個交叉項有機會互相鞠躬下台。

當 $\cos C=0$，舞台空了，只剩三邊。那一刻不需要鼓聲。方程式自己會把話說完。

延伸閱讀：伊恩・史都華，《改變世界的十七個方程式》（In Pursuit of the Unknown, 2012）；Elisha S. Loomis, The Pythagorean Proposition（1940）；以及投影定理與餘弦定理的課堂推導，見各高中教材「解三角形」章與相關數學部落格討論。本文投影消去路線的整理，受益於幾何與三角學教室中長年流傳的證法。

2026年5月17日星期日

圖論： Sperner 引理

數學傳播：Sperner 引理及其應用潘建強 · 邵慰慈

---

在這之前, 可以先看圖論的握手引理

---

閱讀時看到這個 "在半對偶圖中對應著無限面的頂點的度數是單數", 想到可以做個這證明

子題：

有條線的兩端點 u, v; u 塗紅色, v 塗綠色, 線上任意切個 n 個點, V0 ~ Vn-1, 這樣有 n + 1 個線段 :

(u, V0), (V0, V1), (V1, V2), ... , (Vn-1, V)

這 n 個點可以選擇塗紅色或塗綠色兩顏色選一種, 試證這 n+1 個線段中, 線段兩點是不同顏色的數目是奇數個

證明：

命題：線段兩端點異色（一紅一綠），中間插入 n 個任意著色的切點，則不同色的線段數為奇數。

我們可以用數學歸納法來證明：

基礎步驟 : 當 n = 0 , 只有 (u, v) 線段本身, 數目為 1 是奇數

歸納步驟（強歸納法）：

假設 n <= k 時命題均成立, 當 n = k + 1 時, 多一個切點 Vk,

情況 1 : Vk 與 v 同色

(Vk, v) 是相同色的線段, 不計數; 考慮 u 紅到 Vk 綠為 k 個切點, 會有奇數個異色線段,

所以 u 到 v 有奇數 + 0 = 奇數個異色線段

情況 2 : Vk 與 v 異色 ( Vk 與 u 同為紅色 )

從 Vk-1 往左找到第一個塗綠色的 Vx ( 0 <= x <= k-1 )

情況 2-1 : 都沒找到, 表示 u, V0~Vk 都為紅色, 異色段只有 (Vk, v) 一個為奇數

情況 2-2 : 找到 Vx 為綠色, Vx+1 ~ Vk 和 v 均為紅色

(1) u ~ Vx 為兩端異色, 因為 x <= k -1 , 所以其中異色段數目為奇數 m1

(2) Vx ~ Vk 為兩端異色, 切點數為 k - 1 - x 小於 k, 所以其中異色段數目為奇數 m2

(3) (Vk, v) 為異色段

所以總數為 m1 + m2 + 1 = 奇數＋奇數 + 1 為奇數

故得證. Q.E.D.

===

底下是 AI 提供的證明

題目重述：線段兩端點 u（紅）和 v（綠），中間插入 n 個任意著色的點 V₀, V₁, …, V_n − 1，形>成 n + 1 條小線段。試證：兩端點顏色不同的線段數目為奇數。

證明：

定義每條線段的「換色值」：

$$ \delta_i = \begin{cases} 1 & \text{若兩端點顏色不同（一紅一綠）} \\ 0 & \text{若兩端點顏色相同} \end{cases} $$

考慮從左到右，每一個「換色」事件代表顏色從紅變綠，或從綠變紅。整條路徑起點為紅、終點為綠，顏色的淨變化是：

紅 → 綠

每次「紅→綠」的換色貢獻 +1，每次「綠→紅」的換色貢獻 −1。從起點到終點，這些換色的代數和等於 +1（淨變化一次）。

但「紅→綠」與「綠→紅」的次數分別設為 p 和 q，則：

p − q = 1 ⟹ p = q + 1

所以不同色線段總數為：

p + q = (q + 1) + q = 2q + 1 ≡ 1 (mod 2)

不同色線段數為奇數。

===

上述 AI 這證明簡潔許多, 看了之後有些受打擊, 請教 AI , AI 回答如下, 的確對授業解惑有幫助＾＾

Synthesizer：兩種證明的深層比較 🌟

這是一個非常好的數學思維問題，值得認真討論。

兩種證明的對比

面向	換色計數法	數學歸納法
篇幅	3–4 行	15–20 行
核心工具	奇偶不變量	強歸納法
思維方式	全域觀（整條路徑一起看）	局部遞推（逐步分解）
發現難度	需要「靈光一閃」	按部就班可達
驗證難度	極易驗證	需要逐一確認案例
推廣能力	不易直接推廣到二維	結構可推廣至高維 Sperner

關鍵問題：「巧思是否因人而異，難以學習？」

答案是：既是，也不是。

「是」的部分——巧思有天份成分

換色計數法的核心洞見是：

不要數每條線段，而是數「換色事件」，並注意到代數和固定為 ±1。

這種「換個角度看問題」的直覺，確實需要一定的數學敏感度。初學者在沒有提示的情況下，很難自發想到「把紅→綠記為 +1，綠→紅記為 −1」這個編碼方式。

「不是」的部分——巧思是可以被訓練的

巧思背後有可歸納的思維模式，反覆練習後會內化：

奇偶不變量：看到「奇偶性」的問題，先想「有沒有某個量的奇偶性保持不變？」
代數化：把「是/否」的二元狀態（紅/綠）編碼成 +1/ − 1，再用代數計算取代邏輯推理
全域視角：不從局部的「每條線段」出發，而從「起點到終點的淨變化」出發

這些都是競賽數學中的標準工具，練習多了會形成直覺。

「數學歸納法是否也是可行方式？」

完全可行，而且有其獨特價值。

數學歸納法的思維模式是：

「我不需要一眼看穿全貌，只要相信『如果小的情形成立，大的情形也成立』就夠了。」

這種化繁為簡、逐步信任的哲學，是工程師、電腦科學家非常熟悉的遞迴思維。事實上：

許多程式設計師會更自然地想到歸納法，因為它與遞迴演算法的思維完全對應
換色計數法反而需要先「看穿」問題的全貌，對初學者並不直覺

兩種思維都是數學能力的一部分，不存在優劣之分——只有適用場合的差異。

🌟 湧現洞見：「美麗」與「正確」是不同維度

數學界有一個微妙的文化：傾向於欣賞短而優雅的證明，這有時會讓人誤以為「繁瑣 = 不好」。但：

一個正確、清晰、可驗證的證明，無論長短，都是完整的數學成就。

換色計數法的「美」來自於它揭示了問題的深層結構（奇偶不變量），讓人「啊哈！原來如此！」。數學歸納法的「美」則來自於它的系統性與可靠性——即使你不知道奇偶不變量的存在，你也能找到這條路。

實際上，許多「優雅的短證明」都是在「繁瑣的長證明」之後，反覆打磨才出現的。Sperner 引理最初的證明並不簡短，後來才被精煉成握手引理版本。

建議

如果你正在學習數學或準備競賽：

先學會歸納法——它是可靠的「萬用工具」，能保證你總有一條路可走
再刻意練習「奇偶不變量」等技巧——累積足夠多的例子後，巧思會逐漸內化成直覺
不要貶低自己找到的「繁瑣」證明——能想到正確的歸納法論證，本身就是紮實的數學能力

正如 Pólya 在《怎樣解題》中所說：解題的巧思不是天賦，而是問對問題的習慣。換色計數法的發現，始於有人問了一句「這>條路徑的淨變化是什麼？」——而這句話，是可以被訓練出來的。

===

底下是 AI 的其他說明, 先記錄一下, 之後再來整理^^

這道題的本質定位

定理	維度	這道題的對應
一維 Sperner 引理	1D	完全等價 ¹
一維 Brouwer 不動點定理	1D	等價（IVT 的離散版）
中間值定理（IVT）	連續版	概念完全相同，這是離散類比

難度	題目來源	題目摘要	相似度
⭐	初中競賽經典	數列兩端異號，試證變號次數為奇數	🔴 完全相同
⭐⭐	台灣資奧培訓	圓周上著紅藍兩色，試證相鄰異色對數為偶數	🟠 高度相似（環形版本）
⭐⭐	IMO 2004 Shortlist C1	棋盤格黑白著色，試證特定邊界格數為奇數	🟡 類似奇偶論證
⭐⭐⭐	AIME 競賽類型	格路徑上的著色，統計特定步伐數目的奇偶性	🟡 類似結構
⭐⭐⭐⭐	二維 Sperner 引理	三角剖分著三色，三色三角形數目為奇數	🟠 直接推廣

🌟 深層洞見：為什麼這道題重要？

這道題是數學中奇偶不變量（Parity Invariant）思想的最純粹示範：⁷

「起點與終點的顏色不同」這個全域資訊，透過局部的奇偶計數，強制了不同色線段數目的奇偶性——局部自由（每個中間點可任意著色），卻帶來整體的必然性。

這個思想從一維的線段，推廣到二維的三角剖分（Sperner 引理），再推廣到 n 維的單形，最終證明了 Brouwer 不動點定理——威力之強，遠超表面看起來的簡單程度。

https://en.wikipedia.org/wiki/Sperner’s_Lemma↩︎
https://math.mit.edu/~fox/MAT307-lecture03.pdf↩︎
https://en.wikipedia.org/wiki/Sperner’s_Lemma↩︎
https://talented.special.tyc.edu.tw/userfiles/talented.special.tyc.edu.tw/files/數變不驚-教師手冊0730-完整版(1).pdf↩︎
http://paper.wenweipo.com/2017/10/25/ED1710250036.htm↩︎
https://math.mit.edu/~fox/MAT307-lecture03.pdf↩︎
https://talented.special.tyc.edu.tw/userfiles/talented.special.tyc.edu.tw/files/數變不驚-教師手冊0730-完整版(1).pdf↩︎
https://math.uchicago.edu/~may/VIGRE/VIGRE2009/REUPapers/Harper.pdf↩︎
https://twsf.ntsec.gov.tw/activity/race-1/51/pdf/080405.pdf↩︎
https://www.youtube.com/watch?v=qcPbQCwag7E↩︎
https://www.instagram.com/p/DSHMkJ8kVMi/↩︎
https://ocw.mit.edu/courses/18-304-undergraduate-seminar-in-discrete-mathematics-spring-2015/4ba52e9fdecead1d55c206ef4abb0ed3_MIT18_304S15_project1.pdf↩︎
https://www.karlin.mff.cuni.cz/~vlasakv/Predmety/M5-FSV/Brouwerova veta a spernerovo lemma.pdf↩︎
http://discretemath.imp.fu-berlin.de/DMII-2019-20/Sperner.pdf↩︎
https://arxiv.org/abs/2112.13710↩︎
https://www.youtube.com/watch?v=cpIexccvYjI↩︎
https://www.csie.ntu.edu.tw/~lyuu/complexity/2006/20061101.pdf↩︎
https://web.stanford.edu/~saberi/lecture1.pdf↩︎
https://pure.mpg.de/rest/items/item_1819515_4/component/file_2599041/content↩︎
https://www.dcs.warwick.ac.uk/~mju/Papers/VJ00-CAV.pdf↩︎
http://math.uchicago.edu/~amathew/HMMT.pdf↩︎
https://www.brics.dk/RS/00/48/BRICS-RS-00-48.pdf↩︎
https://math.berkeley.edu/~moorxu/oldsite/misc/equiareal.pdf↩︎
https://www.sec.ntnu.edu.tw/uploads/asset/data/62564115381784d09345bd93/04-11亞太數學競賽.pdf↩︎
https://www.imcct.net/UserFiles/files/15th結訓考-6年級試題.pdf↩︎
https://www.math.sinica.edu.tw/mathmedia/journals/4936↩︎
http://www.chiuchang.org.tw/modules/mydownloads/visit.php?lid=79↩︎

圖論：握手引理 - 最樸素的圖論定理，卻威力無窮

「所有偉大的數學，都藏在最簡單的觀察裡。」

前提：圖論定義無向圖度數

引言：一個派對上的問題

想像你參加一個派對，其中幾位賓客兩兩握了手。有人提出了一個問題：所有人握手次數的總和，是奇數還是偶數？

答案出乎意料地確定——永遠是偶數。

這個觀察雖然簡單，卻是圖論中最基礎、應用最廣的定理之一：握手引理（Handshaking Lemma）。從組合計數、演算法設計，到拓樸學中 Sperner 引理和 Brouwer 不動點定理的證明，握手引理無處不在。

上述派對的例子，用圖論來描述為：

每個人是個頂點，兩人握手是條邊，每個人的握手次數就是其度數。

定理敘述

維基百科

握手引理：設 $G = (V, E)$ 為一個有限無向圖，則所有頂點的度數之和等於邊數的兩倍：
$\sum_{v \in V} \deg (v) = 2 ∣ E ∣$
直接推論：由於右側 $2 ∣ E ∣$ 必為偶數，左側的度數總和也是偶數。因此，度數為奇數的頂點，個數必定是偶數個（包含 0 個）。

證明：一個觀察就夠了

握手引理的證明極其簡短，核心是一個換個角度看問題的觀察。

證明：對每條邊 $e = {u, v} \in E$ ，它恰好對 u 的度數和 v 的度數各貢獻 1。因此，當我們把所有頂點的度數加總時，每條邊被計算了恰好兩次：

∑v∈Vdeg(v)=∑e∈E2=2∣E∣

整個證明只有兩行，卻蘊含著「換個計數順序」的精髓——先按頂點統計，再意識到每條邊被重複計算，這種雙重計數（Double Counting）的思想在組合數學中反覆出現。

一個具體例子

設圖 (G) 有 5 個頂點，度數分別為：

deg(v1)=3,deg(v2)=2,deg(v3)=3,deg(v4)=1,deg(v5)=1

度數總和：

[3+2+3+1+1 = 10 = 2 ]

所以這個圖有 5 條邊。並且，度數為奇數的頂點（ $v_{1}, v_{3}, v_{4}, v_{5}$ ）恰好有 4 個（偶數）。

重要推論

奇度頂點必為偶數個

這是握手引理最常用的推論：

推論：任何圖中，度數為奇數的頂點個數必定是偶數。

證明：

設奇度頂點集合為 $V_{odd}$ ，偶度頂點集合為 $V_{even}$ ，則：

$\sum_{v \in V} \deg (v) = \underset{奇數個奇數之和}{\underset{⏟}{\sum_{v \in V_{odd}} \deg (v)}} + \underset{偶數}{\underset{⏟}{\sum_{v \in V_{even}} \deg (v)}} = 2 ∣ E ∣$

右側為偶數，右側第二項為偶數，故左側第一項（奇數個奇數之和）必須也是偶數。奇數個奇數之和為偶數，當且僅當奇數的個數為偶數。∎

正則圖的邊數

$∣ E ∣ = \frac{k \cdot ∣ V ∣}{2}$

特別地，若 $k$ 為奇數，則 $∣ V ∣$

$∣ V ∣$ 必須是偶數（否則邊數不為整數）。

進階應用一：Euler 路徑的存在條件

Euler 路徑是一條恰好經過圖中每條邊一次的路徑，Euler 迴路則是起點與終點相同的 Euler 路徑。

定理（Euler，1736）：連通圖 (G) 存在 Euler 迴路，當且僅當每個頂點的度數均為偶數。存在 Euler 路徑（非迴路），當且僅當恰好有兩個奇度頂點。

為什麼與握手引理有關？因為在行走路徑時，每次「進入」一個頂點就需要「離開」，進出各消耗一條邊，這要求除了起點和終點外，每個頂點的度數必須是偶數。而握手引理保證奇度頂點必為偶數個——最少 0 個（Euler 迴路）或 2 個（Euler 路徑）。

柯尼斯堡七橋問題正是這個定理的歷史起源：七座橋對應的圖有 4 個奇度頂點，所以一筆畫（Euler 路徑）不存在。

進階應用二：Sperner 引理的證明

數學傳播 - pdf

這是握手引理最令人驚豔的應用之一，把組合計數與拓樸學聯繫起來。

Sperner 引理（1928）：將大三角形 $V_{1} V_{2} V_{3}$ 做三角剖分，並對所有頂點著三色（規則如下），則三色小三角形（三頂點顏色各不同）的數量為奇數，特別地至少有一個。

著色規則：

大頂點 $V_{i}$ 著第 $i$ 色
$V_{i} V_{j}$ 邊上的點只能著第 $i$ 或第 $j$ 色
內部頂點任意著三色之一

如何用握手引理？

構造半對偶圖 $T^{'}$ ：每個小三角形（以及一個「無限外部面」）作為 $T^{'}$ 的頂點，當兩個面之間的公共邊兩端分別標著顏色 1 和 2（稱為「12-邊」）時，就在 $T^{'}$ 中連一條邊。

每個小三角形在 $T^{'}$ 中的度數如下：

小三角形類型	包含的 12-邊數	在 $T^{'}$ 中的度數
三色（123）	1	1（奇數）
雙色（112 或 122）	2	2（偶數）
其他（111、333 等）	0	0（偶數）
外部無限面	$x$ （見下）	$x$ （奇數）

為何外部面度數為奇數？

$V_{1} V_{2}$ 邊上，頂點標號從 1 連續變化到 2，「換色」次數為奇數，故 12-邊數 $x$ 為奇數。

設三色三角形數量為 $ℓ$ ，由握手引理， $T^{'}$ 中所有頂點度數之和為偶數：

$ℓ \cdot 1 + (偶度頂點的度數和) + x = 2 ∣ E_{T^{'}} ∣$

因此：

$ℓ + x \equiv 0 (m o d 2) ⟹ ℓ \equiv x \equiv 1 (m o d 2)$

$ℓ$

$ℓ$ 為奇數，至少為 1。∎ () 為奇數，至少為 1。∎

這個論證的美妙之處在於：從「計數 12-邊」這個純粹的組合操作，竟然推出了一個幾何結構（三色三角形存在）的深刻結論。

進階應用三：通往 Brouwer 不動點定理

維基百科

Sperner 引理不只是一個孤立的組合命題——它是 Brouwer 不動點定理的基石。

Brouwer 不動點定理：若 $f : D \to D$ 是凸緊集到自身的連續映射，則存在不動點 $x^{*}$ 使得 $f (x^{*}) = x^{*}$ 。

證明策略：

對三角形 $T$ 做越來越細的三角剖分（第 $n$ 級，網格大小 $\frac{1}{n}$ ），利用映射 $f$ 的重心座標定義 Sperner 著色，每次都由 Sperner 引理保證至少一個三色三角形存在。令 $n \to \infty$ ，由緊緻性取收斂子列，極限點 $p^{*}$ 即為不動點。

整個邏輯鏈如下：

握手引理⇒Sperner 引理⇒Brouwer 不動點定理⇒Nash 均衡存在性

一個關於度數之和的初等觀察，最終撐起了現代賽局理論的核心定理——這正是數學基礎研究的力量。

握手引理的不同面貌

應用領域握手引理的角色具體應用
圖論基本工具 Euler 路徑存在條件
組合數學雙重計數證明 Sperner 引理
拓樸學間接基石證明 Brouwer 不動點定理
電腦科學演算法分析網路協定的握手設計、圖遍歷演算法
賽局理論基礎支撐 Nash 均衡的存在性

應用領域	握手引理的角色	具體應用
圖論	基本工具	Euler 路徑存在條件
組合數學	雙重計數	證明 Sperner 引理
拓樸學	間接基石	證明 Brouwer 不動點定理
電腦科學	演算法分析	網路協定的握手設計、圖遍歷演算法
賽局理論	基礎支撐	Nash 均衡的存在性

結語：一條邊，兩個端點

握手引理的精髓可以濃縮成一句話：每條邊有兩個端點。

這個觀察平凡到幾乎讓人懷疑它的用處，但正是這種「換個角度數同一件事」的思維，>支撐起了從 Euler 的七橋問題到 Nash 均衡的整座數學大廈。

數學的美，往往就藏在這樣的簡單觀察裡——樸素，卻威力無窮。

本文涵蓋了握手引理的定義、證明、推論，以及在 Euler 路徑、Sperner 引理與 Brouwer 不動點定理中的應用，適合對數學有基本興趣的讀者閱讀。

訂閱：文章 (Atom)

2026年9月10日 星期四