程式與數學

幾個口號:

  1. 軟體規格與數學公理骨子裡根本一樣
  2. 寫程式跟寫證明也是一樣的,只是 …
  3. 程式我們關心造出什麼東西,而證明只要有就好。

第一個的理由是,數學公理通常我們是指無法被證明的事情,而確信為真,然而注意 model theory 發展的脈絡,我們可以有不同的 model 滿足該 axiom,例如 Peano axioms,在 set theory 用 ordinal number 中的 \omega 就是 \mathbb{N};在 category theory 也有對應的構造方式;在各種 type theory 可以藉由 well-founded type 構造出 \mathbb{N},或者直接嵌在 type theory 本身。而這時公理的就變成我們 model 所要滿足的條件。

而 model 就是公理的具現化,或對應程式的術語就是實做(implementation),而在程式中說明程式要滿足哪些條件一般稱為程式或軟體的規格 (specification)。當我們將軟體的規格用清楚的邏輯述句寫出來,而具體的實做同樣地也有很多種,跟數學的 model 是互相呼應的。最後,與其說數學公理是「確信」為真,不如說是被「當作」為真(或者,我們要他們為真,所以軟體規格有時候會要求不可能的任務;而數學公理通常是從經驗捕捉得來,用以描述一個認知上的性質,當出現矛盾時,會認為是公理敘述有誤而不是經驗有誤),前者主觀認定事情應當為真,而後者則是政治正確。

第二點根基於 Curry–Howard correspondence constructive mathematics 以及 BHK interpretation 等等,就不多說。

然而最後,到了 proof-irrelevent type theory 會發現我們並不在意 proof 「怎麼」構造出來,而是「有沒有」 proof 。所以有些系統對於用來表示 proposition 的 type, prop , 底下所有的 term 直接 reduce 成同一個元素,對於這件事情,原本無法證明的 K axiom,

K : (A : Set)(x : A)(P : Id A x x → Prop) → P refl → (p : Id A x x ) → P p

在這種情況下變得直接可證,因為只要「有」證明,而不關心是哪一個,雖然最後要得是 P p ,但所有的證明既然都是一樣的,而我們已經有其中一個,那就是了。甚至這在 Intuitionistic Type Theory, by Per Matin-Lof 裡面對於作為邏輯框架的寫法,也只關心有沒有元素在 A 裡頭,而不關心這個元素是什麼。或許對於 constructive proof 也是同樣的道理,witness 的確是要被構造出來,然而 proposition 卻只要有就好,而不限於直覺邏輯。

或許 \neg\neg{}A \rightarrow A 在這角度而言是成立的,因為對於性質上的證明我們只關心有跟沒有證明,在這角度而言將排中律帶進來,似乎並不違背建構式證明的概念;而對於構造出目標而言這點並不能適當地成立,因為除了知道有 witness 存在,更重要的是 witness 是什麼。這點或許可以說明 Bishop 在 Constructive Analysis 中為何 | x | \leq n^{-1} for all n \in \mathbb{N} 能夠導致 x = 0

真的是這樣嗎? 不過既然直覺邏輯稍微比古典邏輯來得弱,倒是不大可能混用的情況造成 inconsistent ,反倒是 prop 的 impredicative type 的問題到底是怎麼回事?

Advertisements

Leave a Reply

Fill in your details below or click an icon to log in:

WordPress.com Logo

You are commenting using your WordPress.com account. Log Out / Change )

Twitter picture

You are commenting using your Twitter account. Log Out / Change )

Facebook photo

You are commenting using your Facebook account. Log Out / Change )

Google+ photo

You are commenting using your Google+ account. Log Out / Change )

Connecting to %s