2010/06/29

Set-theoretic inductive types

中午有人問到 structural induction 是不是一條 axiom,Max 的答案最為全面:系統外我們自然認為 induction 對,至於在系統內的話,first-order logic 必須要設成 axiom (scheme?),到 FLOLAC '08 講的 second-order propositional logic(對應 polymorphic lambda-calculus)就可以用 Church encoding 表示自然數,從而自然地有 induction principle。我想的則是在型式系統的邊界處:在一般的數學架構下我們怎麼促成 induction?Category theory 用 initial F-algebra 弄得很漂亮,set theory 的話可以用 monotonic functions on sets + Knaster-Tarski Theorem 處理,都是把 inductive datatypes 定義得能夠做 induction。以下記錄第二種做法備查,因為我在回憶這種做法時有卡了一下 XD。

先在一個夠大的宇集裡隨便挑一個 constant z 和一個 injective "label" function s。(這句話有辦法說得更好嗎?或許用 axiom of infinity?)(不用假設 0 不在 s 的 range 裡面。直覺上,假設 0 = s (s 0')0' 是我們心目中真正的零,那麼我們定出來的自然數集就是從二開始算。)在集合上定義一個 function f S := { 0 } ∪ { s x | x ∈ S } f 在 set inclusion 下是 monotonic,意思是 X ⊆ Y 時有 f X ⊆ f Y。根據 Knaster-Tarski Theorem,f 有 least fixed-point N,它也會是所有滿足 f X ⊆ X 的 set X 裡面最小的 — 若 X 滿足前式,則一定有 N ⊆ X。現在我們就把 N 當作自然數。假設我們有個性質 P x 要證明對 N 的所有元素成立,定義 X := { x | P x },如果我們能夠證明 f X ⊆ X,即

  f X ⊆ X
⇔   { definition of f }
  { 0 } ∪ { s x | x ∈ X } ⊆ X
⇔   { since A ∪ B ⊆ C ⇔ A ⊆ C ∧ B ⊆ C }
  0 ∈ X ∧ (x ∈ X ⇒ s x ∈ X)
那麼我們就有 N ⊆ X,即 x ∈ N ⇒ x ∈ X,後件再用 P 改寫一下,就是 x ∈ N ⇒ P x。因此藉著如此定義 N,我們就免費得到 N 上的 induction principle 了。

--
寫這篇的時候也會卡,而且每次 monotonic 的意思都會想錯 XD。然後上面引的 axiom of infinity 裡面就有提只用到 set-theoretic axioms 的自然數建構法了 XD。

Labels:

Blogger Unknown7/02/2010 2:58 pm 說:

1. 在 ZFC 底下,空集合是從 axiom of selection 造出來的。也可以另外加一條假設空集合存在。

2. 自然數是從 Axiom of Infinity 造出來的,所謂在「夠大的宇集」其存在性由該公設得到,而藉由 Axiom of Selection 則將滿足該條件的集合取交集,得到自然數。

3. labelling function 在 set theory 要用集合的構造,一般是用 von Neumann ordinal 作,也就是 S(X) = X ∪ {X} 可以證明 S 是 injective 的。然而注意到,這是一個 class function。

 

<< 回到主頁