2007/10/27

copy of Braun Tree

我早上(或許是中午 XD)起床再為這些 code 加註,現在快睡著了 XD。


首先宣告這個 module 並引入需要的 library modules。

module Braun where

open import Logic.Base
open import Logic.Identity
open import Data.Nat
open import Data.Nat.Properties
open import Data.Bool

接著是題目對 Braun tree 的定義。

Parity = Bool

parity : Parity -> Nat
parity false = 0
parity true  = 1

data Braun (A : Set) : Nat -> Set where
  nul : Braun A 0
  bin : {n : Nat} -> A -> (p : Parity) ->
          Braun A (parity p + n) -> Braun A n ->
          Braun A (1 + parity p + (n + n))

要把一個自然數除以 2 很簡單:每找到兩個 suc 就換成一個。

half : Nat -> Nat
half (suc (suc n)) = suc (half n)
half _             = zero

兩個命題 isEven nisOdd n 分別宣稱 n 是偶數或奇數。前者的證明是 by induction,後者則是證明「減 1 後是偶數」。

data isEven : Nat -> Set where
  evenPfBase : isEven zero
  evenPfInd  : {n : Nat} -> isEven n -> isEven (suc (suc n))

data isOdd : Nat -> Set where
  oddPf : {n : Nat} -> isEven n -> isOdd (suc n)

接著有個 function 宣稱一個自然數非奇即偶,並附上證明。因為在 inductive step 要對 even-or-odd (n-2) 做 pattern matching 但 "with" construct 沒辦法運作,所以只好另外寫一個 function 接收額外的參數,然後讓這兩個 functions 彼此呼喚。

mutual

  even-or-odd : (n : Nat) -> (isEven n) \/ (isOdd n)
  even-or-odd zero = \/-IL evenPfBase
  even-or-odd (suc zero) = \/-IR (oddPf evenPfBase)
  even-or-odd (suc (suc m)) = even-or-odd-ind (even-or-odd m)
  -- Why didn't "with" work?
  -- even-or-odd (suc (suc m)) with (even-or-odd m)
  -- ... | \/-IL evenpf = \/-IL (evenPfInd evenpf)
  -- ... | \/-IR (oddPf evenpf) = \/-IR (oddPf (evenPfInd evenpf))

  even-or-odd-ind : {m : Nat} -> (isEven m) \/ (isOdd m) ->
                    (isEven (suc (suc m))) \/ (isOdd (suc (suc m)))
  even-or-odd-ind (\/-IL evenpf) = \/-IL (evenPfInd evenpf)
  even-or-odd-ind (\/-IR (oddPf evenpf)) = \/-IR (oddPf (evenPfInd evenpf))

接著是一些關於 half 的性質。首先有兩個定理:「若能證明 n 是偶數,則 (n + 1)/2 = n/2」以及「若能證明 n 是奇數,則 (n + 1)/2 = 1 + n/2」。舉第一個定理的證明為例:如果 n = 0 顯然成立(by reflexivity)。假設對 m 成立(half (suc m) ≡ half m),欲證明對 m + 2 也成立,即 half (suc (suc (suc m))) ≡ half (suc (suc m))。依 half 的定義,上式可化簡為 suc (half (suc m)) ≡ suc (half m),即對 induction hypothesis 的等式兩邊都加 1。因此用 congruence(x ≡ y implies f x ≡ f y)把 suc 套到兩邊就可以了。

halfevensuc : {n : Nat} -> isEven n -> half (suc n) ≡ half n
halfevensuc evenPfBase = refl
halfevensuc (evenPfInd indHyp) = cong suc (halfevensuc indHyp)

halfoddsuc : {n : Nat} -> isOdd n -> half (suc n) ≡ suc (half n)
halfoddsuc (oddPf evenpf) = cong suc (sym (halfevensuc evenpf))

接著我們證明 2 + n/2 + n/2 = (n + 2)/2 + (n + 2)/2 for all n。欲證式子的精神是 (suc m) + n ≡ suc (m + n),這就是 Data.Nat.Properties module 裡面的 +suc,再用 symmetry 和 congruence 湊一湊就可以得到。

suc²2half : (n : Nat) ->
  suc (suc (half n + half n)) ≡ half (suc (suc n)) + half (suc (suc n))
suc²2half n = cong suc (sym (+suc (half n) (half n)))

接著兩個定理告訴我們把兩個 n/2 加起來後和 n 的關係為何。偶數時兩者剛好相等,奇數時兩倍的 n/2 會比 n 少 1。後者的證明用到 substitutivity(是這樣拼嗎?):n+1 是奇數則 n 是偶數,用第一個定理我們就有 half n + half n ≡ n,現在要證到 suc (half (suc n) + half (suc n)) ≡ suc n。對於偶數我們知道 half (suc n) ≡ half n,所以 half (suc n) + half (suc n) ≡ half n + half n。這裡就用到 Max 談 equational logic 時一個基礎的技巧:把要證的式子寫成 x + x ≡ half n + half n,然後由 reflexivity 知道 x 代 half n 時顯然成立,又知道 half (suc n) ≡ half n,所以 x 代 half (suc n) 時亦成立。

doubleEven : {n : Nat} -> isEven n -> (half n + half n) ≡ n
doubleEven evenPfBase = refl
doubleEven {suc (suc n)} (evenPfInd evenpf) =
  trans (sym (suc²2half n)) (cong suc (cong suc (doubleEven evenpf)))

doubleOdd : {n : Nat} -> isOdd n -> suc (half n + half n) ≡ n
doubleOdd {suc n} (oddPf evenpf) =
  cong suc (trans
    (subst (\x -> x + x ≡ half n + half n) (halfevensuc evenpf) refl)
    (doubleEven evenpf))

最後抵達我們要的 copy function。以「n+1 為偶數」的分支(即最後一個 pattern)為例:n+1 為偶數代表 n 是奇數,我們使用 bin constructor 並遞迴呼叫 copy 造一棵符合條件的 Braun tree,但這棵 Braun tree 的 type 是 Braun A (suc (suc (half n + half n))),而最後要的 type 是 Braun A (suc n),所以我們必須證明 suc (suc (half n + half n)) ≡ suc n 之後用 substitutivity 把前者轉換為後者。而這個證明正好可以對 doubleOdd 做些調整而得到。

令人不解的是 Agda interpreter 告訴我 "[Braun.copy] does NOT termination check",這可能得問問 scm 老師嘍。

-- [Braun.copy] does NOT termination check; why?
copy : {A : Set} -> A -> (n : Nat) -> Braun A n
copy _ zero = nul
copy {A} a (suc n) with even-or-odd n
... | \/-IL evenpf =
  subst (\x -> Braun A x)
        (cong suc (sym (doubleEven evenpf)))
        (bin a false (copy a (half n)) (copy a (half n)))
... | \/-IR oddpf =
  subst (\x -> Braun A x)
        (cong suc (sym (doubleOdd oddpf)))
        (bin a true (copy a (suc (half n))) (copy a (half n)))

--
寫到後來跟寫 Lisp 差不多 XD。

Labels: ,

<< 回到主頁