Haskell簡介[0.5.5]--形式系統

Posted on | Edited on

雖然就上一篇的內容，好像FP是最近才被發明的新東西，但事實上FP和OOP都是五零年代的產物。但OOP在八零年代便開始盛行，FP卻一直到最近才開始在商業使用上慢慢出現。在此之前，FP一直都是為了學術討論而開發。以下我們來聊聊FP在學術領域的歷史。

在十九世紀末，數學正在漸漸公理化。從定義出嚴格的一階邏輯的公理、集合論的ZF公理，數學家開始推行著希爾伯特計畫，希望能將數學利用公理系統進行嚴謹的證明。為了這個目的，各種形式系統開始層出不窮。我在本系列會提到的是以下兩者：

  • λ演算(λ-calculus)：三零年代由邱奇(Alonzo Church)提出，進行λ項的建構與歸約。
  • 組合子邏輯(Combinatory logic)：五零年代由柯里(Haskell Brooks Curry[1])提出，將λ演算中的抽象化移除，並用組合子取代。

在深入詳細介紹這兩個形式系統前，先來介紹形式系統(formal system)吧。

形式系統

定義

先來看看嚴謹的定義。一個形式系統\(T\)是由以下四部分組成：

  • 字母表(\(\Sigma\))：形式語言中可以使用的字母集合

  • 形式語言 (\(L\), formal language)：一個由字母表的字母組成的字串的集合(\(L\subseteq\Sigma^*\))[2]。通常我們會使用形式文法 (\(G\), formal grammar)來描述哪些字串屬於這個集合（也就是哪些字串才是這個語言中的「句子」，稱為「合式公式(wff)」）。而形式文法由以下四部分組成：

    • 非結束符號(\(N\))
    • 結束符號(\(\Sigma\), 即為字母表)
    • 產生式規則(\(P\))
    • 開始符號(\(S\))

    且滿足

    • \(\Sigma\cap N = \varnothing\)
    • \(S \in N\)
    • \(P\subseteq(\Sigma\cup N)^*N(\Sigma\cup N)^*\times(\Sigma\cup N)^*\)

    給定文法\(G=(\Sigma,N,P,S)\)，我們可以定義\((\Sigma\cup N)^*\)上的二元運算\(\xrightarrow[G]{}\)（唸作「可由\(G\)經一步推得」）：\[x \xrightarrow[G]{} y := \exists u, v, p, q \in (\Sigma \cup N)^*: (x = upv) \wedge ((p, q) \in P) \wedge (y = uqv)\]並定義\(\xrightarrow[G]{*}\)（唸作「可由\(G\)推得」）為\(\xrightarrow[G]{}\)的傳遞閉包[3]。
    則\(G\)所規範的語言\(L(G):=\left\{x\in\Sigma^* \middle| S \xrightarrow[G]{} x\right\}\)，亦即所有可以從\(S\)由\(G\)推得的句子。
    

  • 公理 (\(A\))：一些假定為真[4]的合式公式。(\(A\subseteq L\))

  • 推論規則(\(P\))：描述如何透過已經被證明的定理推得到新的定理。
    註：對，這些敘述真的蠻複雜的，不過等等舉例時應該就可以理解了

接著我們要介紹形式證明(formal proof)的概念。擁有形式證明的wff才能被稱為定理。
定理\(S\)的形式證明為一個合式公式的序列\(S_1,\dots S_n\)，滿足：

  • \(\forall S_i : (S_i \in A) \lor (\exists a_1,\dots,a_k<i: (S_{a_1};\dots;S_{a_k}\vdash S_i)\in P)\)
    也就是過程中每一個公式皆可從可先前推得的結果或公理經由推論規則得到。
  • \(S_n = S\)

問題：公理算是定理嗎？

來看看兩個例子吧：

MIU系統

  • 字母表：\(\{M, I, U\}\)

  • 形式語言：所有由字母組成的字串

  • 公理：

    1. \(MI\)

  • 推論規則：
    1. \(xI\vdash xIU\)
    2. \(Mx\vdash Mxx\)
    3. \(xIIIy\vdash xUy\)
    4. \(xUUy\vdash xy\)
    其中\(x\)與\(y\)是任意長度的字串。（可為空）

有了此形式系統的定義，我們就可以證明此系統內的定理
定理：\(MUIIIIU\)
證明：

  1. \(\vdash^{i}MI\)
  2. \(1\vdash^{2}MII\)
  3. \(2\vdash^{2}MIIII\)
  4. \(3\vdash^{3}MUI\)
  5. \(4\vdash^{1}MUIU\)
  6. \(5\vdash^{2}MUIUUIU\)
  7. \(6\vdash^{4}MUIIU\)
  8. \(7\vdash^{2}MUIIUUIIU\)
  9. \(8\vdash^{4}MUIIIIU\)
    故得證

問題：\(MU\)在此形式系統下是定理嗎？

再舉一個例子好了

pq-系統

  • 字母表： \(\{p, q, -\}\)

  • 形式文法：

    • 終止符號：\(\{p, q, -\}\)
    • 非終止符號：\(\{S, D\}\)
    • 起始符號：\(S\)
    • 產生式規則：
      • \(S \rightarrow DpDqD\)
      • \(D \rightarrow -D\)
      • \(D \rightarrow -\)

  • 公理：

    1. \(xp-qx-\)

  • 推論規則：

    1. \(xpyqz\vdash xpy-qz-\)

讓我們試著利用文法創造一些wff吧：
\[S\rightarrow DpDqD \rightarrow Dp-DqD \rightarrow Dp--qD \rightarrow -p--qD \rightarrow -p--q-\]
故\(-p--q-\)為一個wff。
你會發現其實這個文法描述的就是所有形如\(-\cdots-p-\cdots-q-\cdots-\)的句子。

問題：\(--p--q----\)在此形式系統下是定理嗎？
問題：什麼樣的wff在此形式系統下是定理？[5]

後語

這篇文就是為啥去年發了一篇就卡住了QQ
發現我還要去翻一堆課本跟文獻QQ
所以決定先發這樣，剩下的lambda calculus跟combinatory logic就之後再發了Q

  1. 你猜對了，Haskell就是以他命名的。除了Haskell外，Brook及Curry也都是一種函式程式語言。 ↩

  2. 此星號為克萊尼星號，或稱為克萊尼閉包。若定義字串集合的乘法\(AB:=\{ab|a\in A,b\in B\}\)就是將兩集合中的字串兩兩配對串接行程的集合。則\[V^*:=V^0\cup V^1 \cup V^2 \cup\cdots\]，其中\(V^n\)就是\(V\)自乘\(n\)次，而\(V_0\)定義為\(\{\varepsilon\}\)，亦即是只有一個空字串的集合。（注意：此集合與空集合不同。） ↩

  3. 關係\(\rightarrow\)的傳遞閉包\(\xrightarrow{*}\)定義為\[x\xrightarrow{*} y := x\rightarrow y\lor(\exists a : x\xrightarrow{*} a\land a\rightarrow y)\]也就是可經由有限次的\(\rightarrow\)得到。
    例如若\(x\rightarrow y:=x=y+1\)，則\(\xrightarrow{*}\)就是\(>\)，因為\(x>y\Leftrightarrow x\rightarrow x-1 \rightarrow\cdots\rightarrow y\) ↩

  4. 其實不是為真，可能比較像「存在」。畢竟本文基本上都只討論語法學。 ↩

  5. 你會發現\(p\)就是plus，\(q\)就是equal。 ↩