碎碎念 Knaster-Tarski 定理

Knaster-Tarski 定理是 denotational semantics 上很關鍵的一個定理。因為我看它的證明常常會卡住，所以直接寫一篇極端囉唆版的證明擺在這裡備查，順便當通識推廣 XD。喜歡看一般精簡版證明的人可以看 Tarski 的論文。

既然是通識版，就從最基本的定義開始嘍。一個 partially ordered set (poset) 是一個集合 S 和其上的一個 partial order ≤。所謂 partial order 是一個 binary relation，滿足

• reflexivity，即 x ≤ x for all x ∈ S；
• transitivity，即當 x ≤ y 且 y ≤ z 時必有 x ≤ z；
• antisymmetry，即當 x ≤ y 且 y ≤ x 時必有 x = y。

稱之為 "partial" 是因為在 partial order 下並非任兩個元素都能比較，例如集合的包含關係 ⊆。

我們今天的主角是一種特殊的 poset，稱為 complete lattice。這種 poset 的特異功能是：給定任意一個子集 T，都可以在 S 裡面找到

• T 的最大下界（greatest lower bound），記為 inf T；
• T 的最小上界（least upper bound），記為 sup T。

inf T 的定義是（對於任意 x ∈ S）"x ≤ inf T" if and only if "x ≤ y for all y ∈ T"。令左邊的 x = inf T，則左邊根據 ≤ 的 reflexivity 成立，於是右邊 "inf T ≤ y forall y ∈ T" 也成立 ─ 這就說明了 inf T 是 T 的下界。從右邊讀回來，如果有個 x 滿足右邊的條件，意思是 x 是 T 的下界，那麼左邊就告訴我們 x ≤ inf T ─ 意思就是 inf T 是所有下界之中最大的一個。sup T 的定義和 inf T 對偶："sup T ≤ x" if and only if "y ≤ x for all y ∈ T"，詮釋也是對偶的。

一個重要特例是取 T = ∅，此時 "x ≤ y for all y ∈ ∅" 對於任意 x ∈ S 都成立（vacuously true），所以我們就有 x ≤ inf ∅ for all x ∈ S，亦即 inf ∅ 是 S 裡面的最大元素，我們記之為 max S。可以想像「最大下界」就是儘可能地往遞增的方向推進，直到被 T 中的元素擋下來為止。如果 T = ∅，這個推進過程便無法可擋，推著推著就推到最大元素了。相同道理，sup ∅ 就是 S 裡面的最小元素，我們記為 min S。所以 complete lattice 必有最大元素和最小元素。

最後介紹 monotonic function 和 fixed point。令 f 是一個定義在 poset (S, ≤) 上的 function。若 x ≤ y 時必有 f(x) ≤ f(y)，我們就稱 f 是一個 monotonic (increasing) function，又稱 order-preserving function（因為把 f 套用到 ≤ 的兩邊，方向不會因此顛倒）。另外若有一點 p 滿足 p = f(p)，則我們稱 p 為 f 的一個 fixed point（中譯為不動點、固定點，英文有時寫為 fixpoint）。

現在就讓 Knaster-Tarski 定理登場嘍！

定理（Knaster-Tarski）

令 φ 是定義域和值域都在 complete lattice (S, ≤) 上面的 monotonic function，P 是 φ 所有 fixed points 所形成的集合 { x | φ(x) = x }。那麼 (P, ≤) 也是一個 complete lattice。此外，令 P_≤ = { x | φ(x) ≤ x } 和 P_≥ = { x | φ(x) ≥ x }，則 min P = min P_≤、max P = max P_≥。

剛剛提到 complete lattice 必有最大和最小元素，因此 Knaster-Tarski 定理的一個重要推論（corollary）就是「complete lattice 上的 monotonic function 必有最大和最小的 fixed point（兩者可能是同一個）」。這在 denotational semantics 上非常重要，可用來定義 recursive definitions（包括 induction 和 coinduction）的語意。（詳情在 FLOLAC '08 會談，5/22 就截止報名了喔！）事實上，這個推論可說是定理的核心 ─ 整個定理的證明就是從這個推論開始的。這是一個常見的情況：定理的完整證明奠基於其特例。

開始證明！根據 ≤ 的 reflexivity 和 antisymmetry，我們知道 P = P_≤ ∩ P_≥。用形狀比較特異的 Venn diagram 表示：

考慮 ℓ = inf P_≤，即左邊藍色集合的最大下界。我們的目標是證明 ℓ 就在 P_≤ 裡面，然後更進一步證明 ℓ也在 P 裡面。既然 ℓ 是 P_≤ 的下界，它也是 P 的下界，而且因為它就在 P 裡面，所以它就是 P 的最小元素。「u = sup P_≥ 是 P 的最大元素」可透過對偶的論證得到。

怎麼證明 ℓ 的確在 P_≤ 裡面呢？證明 ℓ 滿足 P_≤ 的「入團條件」φ(ℓ) ≤ ℓ 就行了。而正好 ℓ 是 P_≤ 的「最大」下界，所以我們只要證明 φ(ℓ) 是 P_≤ 的一個下界，就可以免費得到 φ(ℓ) ≤ ℓ！任取一點 x ∈ P_≤。我們有 ℓ ≤ x 因為 ℓ 是 P_≤ 的（最大）下界。然後因為 φ 是 monotonic function，我們就有 φ(ℓ) ≤ φ(x)。x 在 P_≤ 裡面，所以 φ(x) ≤ x，於是就得到 φ(ℓ) ≤ x。最後因為當初 x 是任意取的，所以 φ(ℓ) ≤ x 對於所有 x ∈ P_≤ 都成立，亦即 φ(ℓ) 是 P_≤ 的一個下界。但 ℓ 是 P_≤ 的「最大」下界，我們就得到入團條件 φ(ℓ) ≤ ℓ，因此 ℓ 在 P_≤ 裡面。

我們已經成功把 ℓ 推進 P_≤，現在我們得寸進尺，繼續把它推進 P 裡面。藉著 φ 的 monotonicity 和 ℓ 的入團條件 φ(ℓ) ≤ ℓ，我們可以得到 φ(φ(ℓ)) ≤ φ(ℓ)，而這正是 φ(ℓ) 的入團條件，所以 φ(ℓ) ∈ P_≤。不要忘記 ℓ 是 P_≤ 的（最大）下界，因此 ℓ ≤ φ(ℓ)。根據 ≤ 的 antisymmetry，我們就有 φ(ℓ) = ℓ，那就代表 ℓ 在 P 裡面。根據一開始的論證，ℓ 就是 P 的最小元素。同理可推得 u 是 P 的最大元素。

至此我們已經證畢 Knaster-Tarski 定理的核心部份，即 P 有最小和最大元素（也就是 φ 的 least and greatest fixed point）。過程值得再簡述一遍：φ(ℓ) 靠著 ℓ 的最大下界身分努力成為 ℓ 的下界把 ℓ 推進 P_≤，然後自己跟著進去，最後利用 ℓ 是一個下界的事實把 ℓ 推進 P 裡。不覺得 φ(ℓ) 真是勞苦功高嗎？XD

我們繼續證明 (P, ≤) 本身是個 complete lattice，即證明對於 P 的任意子集 A，都可以在 P 裡面找到 inf A 和 sup A。令 I = { x | x ≤ inf A } ⊆ S，這也是一個 complete lattice ^(*)。我們的目標是證明「φ 定義在 I 上的部份」φ' 的 greatest fixed point 就是 A 在 P 裡的最大下界，方法是對 I 和 φ' 套用 Knaster-Tarski 定理的核心部份，找到比 inf A 小的最大 fixed point，這就是 A 在 P 裡的最大下界。透過對偶的論證也可找到 A 在 P 裡的最小上界。

首先我們必須確定 φ' 的值域是 I，才能套用 Knaster-Tarski 定理的核心部份，得到 φ' 的 greatest fixed point。因為定義域是 I = { x | x ≤ inf A }，所以 φ'(x) ≤ φ'(inf A)。我們只要證明 φ'(inf A) ≤ inf A，就能確定 φ' 的值都落在 I 裡面。要證明一點比最大下界小，最簡單的方法就是證明它是一個下界。任取一個 x ∈ A，因為 A 也是 fixed point(s) 的集合，所以 φ(x) = x。接著，inf A ≤ x 因為 inf A 是 A 的（最大）下界，套上 monotonic φ 之後得到 φ(inf A) ≤ φ(x) = x。x 任意，所以 φ(inf A) 是 A 的一個下界。又因為 inf A 是「最大」下界，因此 φ(inf A) = φ'(inf A) ≤ inf A。

現在 Knaster-Tarski 定理的核心部份所需要的條件已經全部滿足了：I 是個 complete lattice、φ' 是個從 I 映射到 I 的 function，因此我們知道 φ' 有 greatest fixed point，令它為 p。顯然 p 在 P 裡面，因為 p 也是 φ 的 fixed point。p 在 φ' 的定義域裡，故 p ≤ inf A ≤ x for all x ∈ A，即 p 是 A（在 P 裡）的一個下界。最後只要證明 p 是 A 在 P 裡的「最大」下界就結束了，而這很簡單：A 若有其他下界 q (≤ inf A)，q 必為 φ' 的 fixed point 而一定有 q ≤ p，因為 p 是 φ' 的 greatest fixed point。透過對偶的論證也可以找到 A 在 P 裡的最小上界。至此我們終於把整個 Knaster-Tarski 定理證完了！    ∎

^(*) 更一般地，任何 I = { x | a ≤ x ≤ b } ⊆ S 都是 complete lattice。任取 I 的子集 K，我們有 inf K ≤ b 因為 b 在 I 裡面。a 必為 K 的一個下界，所以根據 inf K 的「最大」性質，我們也有 a ≤ inf K。於是 a ≤ inf K ≤ b，因此 inf K 也在 I 裡面。同理，sup K 也在 I 裡面。

--
難怪沒人要寫這種證明… 下一步是試試看能不能從操作意義上了解它。