看看程式語言學在幹嘛
回到中研院後，我對 FLOLAC 的規劃籌辦有了更直接的主導權。雖然疫情愈發嚴峻，FLOLAC 2020 或許最終不得不取消，我還是先發動了 FLOLAC 的形象識別設計案。FLOLAC 某些年份有做簡單的形象設計，但礙於成本並沒請設計師表現出特屬於 FLOLAC 的意象，而且各年分開設計，沒有主題延續感。這次的設計案打算多花點成本，做出一個能忠實反映「FLOLAC 在教什麼」（或者說「程式語言學在做什麼」）的標誌並延伸至週邊（網站、講義、證書等等），長久使用下去。為此，我為設計師準備了一點關於程式語言學的科普介紹，這篇網誌是事後整理的文字版。好的形象設計必須傳達適當的視覺印象，而程式語言學給人的第一印象往往是密度極高的符號，因此我刻意準備了一些具體的符號使用例子，但目的只是讓設計師對我們習慣的東西長相有比較具體的印象，不見得要看懂。以下文字最好和我在會談當天使用的投影片對照著看：
我會標示出各節對應的 pdf 頁碼，例如 -1- 代表現在看的是第 1 頁。
-2- 先給一個概觀。程式語言學的研究對象是程式，可以想成是「寫得很詳細、可以一步步照著做的規則／流程」；程式不一定非得和電腦扯上關係，像 SOP（標準作業流程）和飛行員必用的 checklists（檢查表）就是寫給人執行（照著做）的程式。程式語言學的最大特點是用符號作為主要工具，精準（無歧義）簡練（不冗長）地表示出程式和相關概念，以及研究它們的各種性質。除了精準簡練以外，我們喜歡的符號有以下這些特質：
- 厲害：用符號把關於程式的事情好好寫下來之後，我們就可以用數學方法確鑿地談這些事情，用數學證明確保厲害的好性質，例如「符合某些條件的程式絕對不會出錯」。
- 易用：符號是我們解決程式相關問題的工具，在符號設計上我們會有所講究，為各種問題量身設計順手易用的專門符號。
- 內涵：好的符號往往有多個面向層次的意義，幫助我們用不同角度思考問題；我們特別喜歡向數學和邏輯學借用符號，和他們長久累積發展的深刻概念互通。
接下來用幾個具體例子說明這三個特質。
厲害：規則、符號、好性質
-3- 首先是一個比較大的例子，實際看看一種程式的長相，以及符號能帶給我們什麼好處。
通訊程式
-4- 這個例子是在拍賣網站的購物流程。一種常見的購物說明是
先詢問有無存貨，賣家回覆有貨才可下標。下標後將收件資訊告知賣家，完成匯款後賣家出貨。
這個格式並不是很容易照著做 — 對於比較小心的買家（例如政府機關 😓），若把確切步驟一行行寫下來，實際進行時便能一行行照著做，方便追蹤進度到哪以及下一步該做什麼，確保沒有遺漏。一個可能的格式是
![請問還有沒有貨]
▹{ 缺貨 : stop
有貨 : if 老婆說可以買
then ◃ 下標
![收件資訊]
![錢]
?(貨)
stop
else ◃ 算了
stop }
我們用上了一些符號（取自 Honda 等人於 1998 年發表的「訊程算則」session calculus），但引進這些符號只是為了精簡記述一些頻繁使用的概念，對照一下就可以翻譯回白話： ‘!’ 是「送出」、 ‘?’ 是「接收」、 ‘▹’ 是「對方做選擇」、 ‘◃’ 是「自己做選擇」、‘stop’ 是「停止動作」、‘if … then … else …’ 是「當 if 後面的條件成立就執行 then 後面那一串動作，否則執行 else 後面那一串動作」。上面那段程式翻譯回白話就是
送出「請問還有沒有貨」的訊息。當對方選擇「缺貨」或「有貨」時，做對應的事情。若對方選擇「缺貨」則停止動作。若對方選擇「有貨」，就根據「老婆說可以買」這個條件決定接下來做什麼。若老婆說可以買，選擇「下標」、送出收件資訊、送出錢、接收貨、然後停止動作；若否，選擇「算了」然後停止動作。
可以看到這段程式的意思用白話寫出來會顯得比較繁瑣，改用符號的話，只要先把符號的意思規定好就不用寫得這麼麻煩（甚至比較清晰）。 -5- 賣方也可用同一套符號寫下他們的動作流程：
?(請問還有沒有貨)
if 查了一下有貨
then ◃ 有貨
▹{ 算了 : stop
下標 : ?(收件資訊)
?(錢)
![貨]
stop }
else ◃ 缺貨
stop
這裡需要強調的是程式的合法長相（學名是「語法」syntax）必須明確定義，而且這種定義有一套標準的寫法（學名是「文法」grammar）。換句話說，哪些程式合法／錯誤是有明確判準的，並非把白話換成符號就是程式。投影片 -6- 展示了訊程算則的語法定義，粗略解釋的話，這裡是把所有可能出現在程式裡的動作都列出來，並規定對應符號的使用格式。（上面的程式是簡化過的版本，並未嚴格遵照此處的定義。）
程式執行
-7- 實際進行購物時，雙方就根據自己的程式一行一行地做。 -8- 首先買家送出訊息（‘![請問還有沒有貨]’）、賣家接收訊息（‘?(請問還有沒有貨)’），一送一收剛好對應，雙方做完後 -9- 把各自的第一行劃掉，繼續做剩下部分。此時買家要等對方做選擇（‘▹’），而賣家要查有沒有貨（‘if 查了一下有貨’）決定如何進行。比較有趣的情況是賣家查了發現有貨，這時賣家會繼續執行 then 後面的那串動作。 -10- 於是賣家選擇「有貨」，買家也跟著繼續執行他的程式裡「有貨」後面那串動作。 -11- 這時買家必須徵詢老婆的意見，一樣我們假設比較有趣的情況，即老婆同意，那買家就會執行 then 後面那串動作。 -12- 於是買家選擇「下標」，賣家跟著執行「下標」後列的動作。雙方 -13- 送出／接收收件資訊、 -14- 送出／接收錢、 -15- 接收／送出貨、 -16- 最後一起停止動作。
以上這段關於程式執行的敘述相當繁瑣，但程式語言學也有一些用符號描述程式執行的方式（這個例子用的是「結構化運行語意」structural operational semantics），可以把程式的執行步驟精簡地定義下來。投影片 -17- 是訊程算則運行語意的主要定義。這些規則一樣都可以翻譯為白話，例如 [Com] 這條規則
$$ (k![\tilde e]; P_1) \mid (k?(\tilde x)\ \mathtt{in}\ P_2) ~~\to~~ P_1 \mid P_2[\tilde c/\tilde x] \qquad (\tilde e \downarrow \tilde c) $$
大意是說當兩個程式一起執行而且一邊要送 (‘$!$’) 另一邊要收 (‘$?$’) ，那麼這步做完後兩邊會繼續執行剩下的部分（而且接收方會收到另一方送的東西）。[Label] 這條規則也類似，
$$ (k \lhd l_i; P) \mid (k \rhd \set{\, l_1 : P_1 \mathrel{[\!]} \cdots \mathrel{[\!]} l_n : P_n \,}) ~~\to~~ P \mid P_i \qquad (1 \leq i \leq n) $$
說的是當兩個程式一邊選擇 (‘$\lhd$’)、另一邊等對方選擇 (‘$\rhd$’) 時，前者會繼續執行剩下部分，後者會繼續做對方選擇的部分。
型別安全定理：保證不發生配對錯誤
花了這麼多力氣把東西用符號寫下來，有什麼好處呢？計算學界和業界有各種強弱不一的機制和方法讓程式執行不（容易）出錯；程式語言學用符號把所有東西都精準定義下來，從而能用數學證明保證絕對不可能出錯，是最強的程式驗證方法之一。
回到上面的例子，可觀察到兩個程式一起執行時，正確的動作配對（‘!’ 對應 ‘?’ 、 ‘◃’ 對應 ‘▹’）很重要，若兩邊動作沒對好就無法進行下去。 -18- 比方說如果買家以為可以貨到付款而把程式裡 ‘![錢]’ 和 ‘?(貨)’ 兩行順序對調，那麼雙方傳完收件資訊後就會陷入僵局，買家等著收貨、賣家等著收錢，而無法繼續。 -19- 若回到現實狀況考慮，這樣的配對錯誤之所以發生，問題是出在買家沒遵守最一開始的購物說明。訊程算則提出的解法是要求把雙方必須遵守的通訊協議也清楚寫下來，雙方編寫程式時就能檢查程式是否遵守協議，從而保證通訊無礙。例如買方應遵守的通訊規則（學名是「訊程型別」session type）可以寫成
!詢問存貨
&{ 缺貨 : end
有貨 : +{ 下標 : !收件資訊 !錢 ?貨 end
算了 : end } }
這裡的兩個新符號 ‘&’ 和 ‘+’ 意思分別是「對方所有可能的選擇」和「自己所有可能的選擇」。把這個型別翻譯成白話就是
送出詢問存貨的訊息。對方可能選擇「缺貨」或「有貨」。若對方選擇「缺貨」就結束；若選擇「有貨」，則自己可以選擇「下標」或「算了」。若選擇「下標」，則送出收件資訊、送出錢、接收貨、然後結束；若選擇「算了」就直接結束。
和程式相比，訊程型別只描述通訊行為，因此像「買家如何決定要下標還是算了」這些與通訊無關的事情並不會出現在型別裡面。 -20- 寫下訊程型別之後，我們就可以檢查程式是否遵守這個訊程型別，包括當型別要求送出訊息時 (‘!’) 程式確實會送出 (‘!’) 正確種類的訊息（而不是做其他動作，如接收）、型別列出自己所有可能選擇時 (‘+’) 程式確實會選 (‘◃’) 其中列的一個選擇（而不會隨便選一個不存在的選項）、型別列出對方所有可能選擇時 (‘&’) 程式必須為每個可能選項 (‘▹’) 都準備後續動作（才不會對方選了一個選項後自己卻不知道要做什麼）等等。 -21- 另一方面，賣方的程式也有應該遵守的通訊規則／訊程型別。因為訊程型別只描述通訊行為，買方和賣方的訊程型別會有個直接的「對偶」關係，我們只要把買方型別裡所有動作都換成與之相對的動作（‘!’ 與 ‘?’ 相對、‘&’ 和 ‘+’ 相對）就是賣方型別：
?詢問存貨
+{ 缺貨 : end
有貨 : &{ 下標 : ?收件資訊 ?錢 !貨 end
算了 : end } }
-22- 然後我們也要求賣方的程式必須遵守這個型別。
總述一下引進訊程型別後整個機制如何運作：把通訊協議表示成兩個對偶的訊程型別，分別給買賣雙方，各自編寫程式時檢查是否遵守分到的型別。若沒引進訊程型別作為中介，要直接檢查兩個程式（如上面買賣雙方的程式）是否能無礙地一起執行並不太容易；反之若照這個機制運作，雙方程式的通訊行為就會如同各自的訊程型別所描述，而這兩個訊程型別又對偶，於是就能保證雙方行為永遠是相對的，不會發生配對錯誤。 -23- 這樣的保證我們可以寫成一個型別安全定理：
若兩個通訊程式遵守對偶的訊程型別，則它們一起執行時不可能發生配對錯誤。
當然，這裡面涉及的概念都必須用符號好好定義，包括訊程型別可能的長相、何謂程式遵守型別、配對錯誤等等。一旦這些都定義好之後，上述定理的證明就相當於窮盡所有遵守對偶型別的程式執行的可能性，推論出所有情況下都不可能發生錯誤。用符號把所有東西寫下來並不容易，但相對地可以換來這種全面且絕對的掌握。
易用：解決問題的好工具
-24- 至此可以看到我們處處使用大量符號，從寫程式和描述程式行為一直到寫證明，符號可說是程式語言學解決問題不可或缺的工具。和其他工具一樣，設計符號的時候我們也希望讓符號順手易用。不過什麼是順手易用的符號呢？
-25- 這裡只舉一個大家熟悉的例子：數字運算。小學數學常見的一種應用題是
小明買了 24 枝 9 元的鉛筆和 12 個 15 元的橡皮擦，請問小明總共要付多少錢？
我們都能熟練地列式計算：
9 × 24 + 15 × 12 = 216 + 180 = 396
我們對算數已經太過熟悉、往往不會多想，但若我們細想發生了什麼事，就會看出符號的威力以及算數這套符號設計的巧妙之處。首先列式就已經是重要的一步，因為我們得以擺脫鉛筆橡皮擦這些無關緊要的細節，把我們關注的部分寫成數字，只要學會一套數字上的通用計算規則，就可以解決所有同質但細節各異的問題，無需每個問題重想一次。將乘法這個概念提煉出來也很關鍵：如果沒有乘法，我們就只能把 9 連加 24 次、15 連加 12 次，但有了乘法以及相關的計算規則之後我們就能很容易地列式並算出答案。另外一個小細節是「先乘除後加減」這個慣例讓我們為這類「購物清單總金額」（加總一堆乘積）的問題列式時可以省掉不少括號，這也屬於易用符號設計的一環。乘法的直式計算也設計得很巧妙：在只會做單位數乘法（背了九九乘法表）的假設下，若想做多位數乘法，我們必須拆解數字並用分配律把兩數逐位相乘得到多項，最後全部加起來，例如
15 × 12 = (10 + 5) × (10 + 2) = 100 + 20 + 50 + 10 = 180
這樣的計算隨著位數增多會變得麻煩，因為這個格式下有很多零參雜在裡面，除了零的個數必須小心不能寫錯，把乘得的四項加起來的時候也不容易看出是哪些位要加在一起。直式的設計就解決了這些問題：
15
× 12
————
10
2
5
1
————
180
（為了和上面的橫式對應，這裡把逐位相乘得到的全部四項都寫出來，看起來比平常計算過程累贅，是因為平常計算時有些項在心裡就已經先相加合併了。）我們根據權重把各項排好，於是就不需寫出低位的零，同時也能直接看出是哪些位要相加。
以上觸及的幾項原則 — 提煉常用概念為符號與計算規則、訂立讓符號容易書寫的慣例、設計方便計算解題的符號格式 — 都是程式語言學創造新符號時經常引用的。 -26- 我們甚至有一套「程式計算」理論 (program calculation) 直接仿效了算數的精神，但計算的不是數字而是程式：和解算數應用問題一樣，我們先把想用程式達成的事情寫下來（列式），然後用一套特別設計的計算規則不斷改寫，最後解出正確的程式。不過程式比數字複雜得多，程式計算也比數字運算困難得多，這裡就不詳述。
內涵：數學、邏輯學
-27- 上面提到的程式計算並非程式語言學裡唯一和數學有所呼應的理論 — 事實上程式語言學和數學、邏輯學的關聯極其密切，前者常向後兩者借用概念和符號。好的符號往往可用多種角度理解，相當於幫助我們用各種角度思考問題，而當符號設計得帶有數學和邏輯學上的意義時，我們就能藉以引入數學和邏輯學長久以來發展淬煉的想法，這樣的設計策略常收奇效。接下來要介紹的 λ 算則 (λ-calculus) 是程式語言學裡最具代表性和影響力的一套符號系統，定義簡單卻又能力強大，而且是計算學、數學、邏輯學的匯集點，數個學門的概念在此互通；其涉及的範圍既廣又深，我不打算詳述，以下就只走馬看花。
-28- 中學數學最重要的一個概念是「函數」，用以表達數上的對應／轉換關係，例如
$$ f(x) = x^2 + 1 $$
定義了一個函數 $f$ 把任意數字 $x$ 轉換成 $x^2 + 1$。給定一個函數，我們可以代入一個具體的數，計算這個數被轉換成哪個數，例如我們可算出 $f$ 把 $5$ 轉換成 $26$：
$$ f(5) = 5^2 + 1 = 26 $$
算法就是把函數定義裡的 $x$ 代換成 $5$ 然後化簡。 -29- λ 算則可以想成是一套極簡的符號系統，只捕捉「函式定義」和「函式代入」兩個概念，像上面定義的函數 $f$ 在 λ 算則裡會省去名字 $f$ 只寫成
$$ \lambda x.\,x^2 + 1 $$
而要把 $5$ 代入這個函數時就只是把 $5$ 記在後面（然後一樣代換化簡）：
$$ (\lambda x.\,x^2 + 1)\ 5 = 5^2 + 1 = 26 $$
不過以上式子其實已經超出 λ 算則的範圍 — λ 算則設計極簡，並未直接包含平方、加法、$1$ 這些概念。 -30- 相較於訊程算則的語法有十幾條，λ 算則的語法只有三條；程式執行也類似，訊程算則我們看到了十條核心規則（以及一些其他的輔助規則），而 λ 算則只有一條核心規則（捕捉「代換」這個計算步驟）。然而 λ 算則就已足以編寫出所有目前合理想像得到的計算。 -31- 例如若想計算 $2 + 3$，我們可以把 $2$ 編寫成 $\lambda f.\,\lambda x.\,f\,(f\,x)$（裡面 $f$ 出現兩次，對應於 $2$）、類似地 $3$ 編寫成 $\lambda f.\,\lambda x.\,f\,(f\,(f\,x))$、加法則是 $\lambda m.\,\lambda n.\,\lambda f.\,\lambda x.\,m\,f\,(n\,f\,x)$，然後把 $2$ 和 $3$ 代入「加法」不斷代換化簡，最後就能算出 $\lambda f.\,\lambda x.\,f\,(f\,(f\,(f\,(f\,x))))$，即 $5$。
-32- 「型別」這個機制也出現在 λ 算則裡面，不過這裡不詳細解說，只點出我們有一套樹狀的符號系統用來進行型別上的推理。和我們上面看到的種種符號一樣，這些推理樹都是用一組既定的規則建構而成，而有趣的是這些規則其實蘊含了邏輯意義。 -33- 例如有一條規則是
$$ \frac{~ \Gamma \vdash t : A \to B \qquad \Gamma \vdash u : A ~}{\Gamma \vdash t\,u : B} $$
其中三個冒號右邊的型別部分可解讀為一條標準的邏輯規則：如果 $A$ 發生會導致 $B$ 發生 ($A \to B$)、而且 $A$ 發生了，那麼 $B$ 也會發生。（橫線上方的 $A \to B$ 和 $A$ 是前提、下方的 $B$ 是結論。）λ 算則的型別理論最初發展時並沒有這種邏輯解讀，是過了一陣子才發現和邏輯學那邊獨立發展的系統其實是同一回事。這打通了本來獨立發展的兩個領域：兩邊的研究者都得以用另一邊的角度重新省視理解自己這邊的成果，發展新理論的時候也可以自由使用任一邊的角度思考。這個計算與邏輯的對應關係現在已是程式語言學最重要的基石之一。
總結
-34- 程式語言學以符號為工具精準簡練地表達程式與相關概念（例如通訊程式和它們的執行過程），但我們並不是把白話寫成符號就滿意了：我們用符號做厲害的事（例如證明滿足特定條件的程式不可能出錯），設計易用的符號（例如可以像計算數字一般地算出程式），並且特別喜歡有多重內涵 — 特別是具有數學和邏輯學意義 — 的符號（例如 λ 算則）。有興趣嗎？歡迎來 FLOLAC 看看！
致謝
感謝我的行政助理林柏芬自告奮勇聽我試講這份介紹，以及（別人的 XD）研究助理賴廷彥和林子期也應邀來聽我試講；三位都提供不少點子讓整份介紹變得比較順暢易懂。
