Coinductive Proof ?

正在看 Coq’Art 最後的 Infinite Objects and Proofs,順便玩一下 coinductive type 到底在 Coq 跟 Agda 這種基於 constructive type theory 的語言到底是怎麼回事,用 Agda 內建的  Data.Conat 寫下了幾個證明。先定義 bisimilar relation:

data _≈_ : (n m : Coℕ) → Set where
zero : zero ≈ zero
suc : ∀ {n m} (p : ∞ (♭ n ≈ ♭ m)) → suc n ≈ suc m

很直觀的定義沒什麼好說的。

∞+∞ : ∞ℕ + ∞ℕ ≈ ∞ℕ
∞+∞ = suc (♯ ∞+∞)

∞ℕ 的定義在 stdlib 裡頭,其實很簡單,就是用 suc 一直串下去。然後我們也可以定義有序關係,就像這樣:

data _≤_ : (n m : Coℕ) → Set where
z≤n : ∀ {n} → zero ≤ n
s≤s : ∀ {n m} → (∞ (♭ n ≤ ♭ m)) → suc n ≤ suc m

在 Coq 底下要用 Cofix 來定義,但是 Agda 底下把 codata 包裝起來,用來互相轉成 inductive type 跟 coinductive type,不過這邊的關係我還不是很理解。接下來,既然可以描述自然數的無限大,那我們也可以證明無限大大於等於所有的自然數

n≤∞ : ∀ n → n ≤ ∞ℕ
n≤∞ zero = z≤n
n≤∞ (suc n) = s≤s (♯ n≤∞ (♭ n))

那麼無限大是否小於無限大呢?按照這個定義事實上是的。小於其實定義為

_<_ : ∀ n m → Set
_<_ n m = suc (♯ n) ≤ m

也就是說,若(1 + n) \leq mn < m。但是因為無限大定義為 \infty = 1 + 1 + 1 ... ,那麼 1 + \infty 仍然是 \infty (在 bisimilar 的意義下),所以證明就只是

∞<∞ : ∞ℕ < ∞ℕ
∞<∞ = s≤s (♯ refl′)

其中 refl′ 是證明該有序關係是 reflexive 的。不過雖然 conductive type 處理 infinite object 看起來很威,但是遇到實際上是有限的資料,可就威不起來了 …

lem₁ : fromℕ 3 + fromℕ 4 ≈ fromℕ 7
lem₁ = suc (♯ suc (♯ suc (♯ refl)))

這是一個 3 + 4 = 7 的證明,在 inductive 的情況下,可以直接根據 reduction rule 算出 3 + 4 等於 7,進而簡化命題成為 7 = 7,直接就可以證明。但在 coinductive  下,要維持 strongly normalizing property,必須有限制地展開,所以像是 fromℕ 2 只會展開成 suc (fromℕ 1) 而不是 suc (♯ suc (♯ zero)) 。所以證明就是把 fromℕ 3 一直展開,一直得到 0 + fromℕ 4 ≈ fromℕ 4 為止,在 Coq 底下應該還要再使加法的部份再展開一次,但在 Agda 因為是包在 inductive type 裡頭,就直接把 0 + x 展開為 x 了。我需要再練習一下 coinductive,邊看 modal logic 邊寫起來好了 :p

Advertisements

One thought on “Coinductive Proof ?

  1. Agda 本來也是用 codata 的,後來發現許多問題。用 ♭ 和 ♯ 是 Nils Anders 的建議,目的是讓 ♭ 成為唯一可以對 coinductive data 做 pattern matching (並強制其運算)的運算元。

    Agda mailing list 上有討論許多,當時 Anton 也談了不少。在 Nils Anders 的做法出來前,他另外有一個他喜歡的做法。我問他有沒有想要做到 Agda 裡面,他手一攤說可惜他不知怎麼去改 Agda 的 source code.

    之後我就一直想要去 trace 它看看。至少把這能力學起來。

    _≈_ 的定義對 coList, coNat 這種只有一個後代的 type 都好寫。如果不是這樣的話(e.g. pi-calculus)就變得超囉唆的。

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