2007/09/05

Statically-Checked Balanced Tree

首先是一些基本定義和定理。

plus :: Nat ~> Nat ~> Nat
{plus Z y} = y
{plus (S x) y} = S {plus x y}

assoc :: Nat' x -> Equal {plus x (S y)} {plus (S x) y}
assoc Z = Eq
assoc (S x) = Eq where theorem indHyp = assoc x

theorem associativity = assoc

接著是 Parity kind 和相對應的 singleton type Parity' 的定義。我照著〈Putting Curry-Howard to Work〉的語法在 Parity 定義後寫 deriving Singleton Parity' 可是不 work,所以手工定義一個。

kind Parity = Even | Odd

data Parity' :: Parity ~> *0 where
  Even :: Parity' Even
  Odd :: Parity' Odd

再來是 static proposition Balanced。令左子樹大小為 m、右子樹大小為 n、節點的 parity 為 p,命題 Balanced p m n 是說,mn 符合平衡的定義(i.e., m = n + 1 or m = n),而且在此節點上的 parity p 是對的。定義是 by induction。比較奇怪的地方是,定義裡面沒有明確指出 m = n + 1 or m = n,但此事可以從這個定義簡單歸納推得。

prop Balanced :: Parity ~> Nat ~> Nat ~> *0 where
  Base :: Balanced Even Z Z
  InsLeft :: Balanced Even m n -> Balanced Odd (S m) n
  InsRight :: Balanced Odd m n -> Balanced Even m (S n)

最後是 Treeinsert 的定義。

data Tree :: *0 ~> Nat ~> *0 where
  Nul :: Tree a Z
  Tip :: a -> Tree a (S Z)
  Bin :: Balanced p m n =>
         Parity' p -> Tree a m -> Tree a n -> Tree a {plus m n}
  
insert :: a -> Tree a n -> Tree a (S n)
insert x Nul = Tip x
insert x (Tip y) = Bin Even (Tip x) (Tip y)
insert x (Bin p t u) = case p of
  Even -> Bin Odd (insert x t) u
  Odd -> Bin Even t (insert x u)

最需要 defend 的地方應該是 Bin constructor 是不是足以證明樹是平衡的。scm 老師在我寫 p 的地方都寫 {parity {plus m n}},其中 parity :: Nat ~> Parity,但這樣似乎需要另外給不少定理。我目前看覺得沒問題,因為 pBalanced p m n 所限制,不能亂給。

--
Balanced 應該還有別的表述方法。


不過直接使用 Bin 時發生一些問題,目前無法解決。狀況是:

prompt> insert 1 (insert 2 (insert 3 (insert 4 (insert 5 Nul))))
(Bin Odd (Bin Odd (Bin Even (Tip 1) (Tip 3)) (Tip 4)) (Bin Even (Tip 2) (Tip 5))
) : Tree Int 5t

但如果在源碼內加入

t = (Bin Odd (Bin Odd (Bin Even (Tip 1) (Tip 3)) (Tip 4)) (Bin Even (Tip 2) (Tip 5)))

就會導致

While type checking: t
Under the truths: 
We tried to solve: Balanced Odd {plus {plus 1t 1t} 1t} {plus 1t 1t},Balanced Odd
 {plus 1t 1t} 1t
But we were left with: Balanced Odd {plus 1t 1t} 1t, Balanced Odd {plus {plus 1t
 1t} 1t} {plus 1t 1t}
The proposition: (Balanced Odd {plus 1t 1t} 1t) is refutable.

或是像這樣直接在 interpreter 下說:

prompt> let t2 = insert 4 (insert 5 Nul)
t2 
prompt> t2
(Bin Even (Tip 4) (Tip 5)) : Tree Int 2t
prompt> let t3 = insert 1 (insert 2 (insert 3 Nul))
t3 
prompt> t3
(Bin Odd (Bin Even (Tip 1) (Tip 2)) (Tip 3)) : Tree Int 3t
prompt> Bin Odd (Bin Odd (Bin Even (Tip 1) (Tip 2)) (Tip 3)) (Bin Even (Tip 4) (
Tip 5))
Unresolved obligations:
  Balanced Odd 3t 2t => Tree Int 5t
prompt> Bin Odd t3 t2
(Bin Odd (Bin Odd (Bin Even (Tip 1) (Tip 2)) (Tip 3)) (Bin Even (Tip 4) (Tip 5))
) : Tree Int 5t

最後這段我實在傻眼了 XD。

--
有盲點?


我打開追蹤模式 check 很長的那一串,更令人費解。最後一步是

Trying to find evidence for the predicate:
   Balanced Odd 3t 2t
Under assumptions:
   []
Currently solving subproblems from the rules: Base,InsLeft,InsRight,InsLeft,Base
,InsLeft,InsRight,Base,InsLeft,InsRight
Possibly matching rules are
  Axiom InsRight(Balanced): [] => Balanced Even 'a (1+'b)t --> [Balanced Odd 'a 
'b],
  Axiom InsLeft(Balanced): [] => Balanced Odd (1+'c)t 'd --> [Balanced Even 'c '
d],
  Axiom Base(Balanced): [] => Balanced Even 0t 0t --> []

press return to step, 'c' to continue:


Exactly 0 rules match:
  

Unresolved obligations:
  Balanced Odd 3t 2t => Tree Int 5t

對照組:我改而 check Bin Odd t3 t2,前兩步是:

Trying to find evidence for the predicate:
   Balanced Odd 3t 2t
Under assumptions:
   []
Currently solving subproblems from the rules: 
Possibly matching rules are
  Axiom InsRight(Balanced): [] => Balanced Even 'a (1+'b)t --> [Balanced Odd 'a 
'b],
  Axiom InsLeft(Balanced): [] => Balanced Odd (1+'c)t 'd --> [Balanced Even 'c '
d],
  Axiom Base(Balanced): [] => Balanced Even 0t 0t --> []

press return to step, 'c' to continue:


Rule : InsLeft
Matched term: Balanced Odd 3t 2t
 Rewrites to: Balanced Even 2t 2t
 Under subst: {e=2t, f=2t}
Prerequisite: 

Exactly 1 rules match:
  


Trying to find evidence for the predicate:
   Balanced Even 2t 2t
Under assumptions:
   []
Currently solving subproblems from the rules: InsLeft
Possibly matching rules are
  Axiom InsRight(Balanced): [] => Balanced Even 'a (1+'b)t --> [Balanced Odd 'a 
'b],
  Axiom InsLeft(Balanced): [] => Balanced Odd (1+'c)t 'd --> [Balanced Even 'c '
d],
  Axiom Base(Balanced): [] => Balanced Even 0t 0t --> []

press return to step, 'c' to continue:

--
我放棄了…

Labels:

Anonymous scm9/05/2007 8:16 am 說:

哇,動作好快!辛苦啦!

1. 我也無法 derive Singleton Parity.

2. 關於:
> 喔,是因為已經賦予 assoc 一個 type,所以只寫 Eq 就可以做 interence 嗎?

我想是的。 :)

3. 我之前也試過把 Bin 的 type 給成類似 Balanced p m n => Parity' p ->... 的形式。結果我甚至無法讓 insert typecheck. 我碰到的 error message 也是 "The proposition: ... is refutable." 大概我弄得比較複雜,還多用了一堆定理的關係。

後來我改用這個 type:
Bin :: Balanced {parity {plus m n}} m n
-> Parity' {parity {plus m n}}
-> Tree a m -> Tree a n
-> Tree a {plus m n}

只是把 => 變成 ->。兩者的差別是在前者中,Balanced 是 compile time 去 check 的定理;後者中,我們在 runtime 要給一個 Balanced 的證明。這其實也蠻像印象中的 Curry-Howard isomorphism: type 是定理、term 是證明。

這樣當然是很沒效率。

但不知為什麼,換用後者之後一切就比較好寫了。我剛剛試了試,在 interpreter 中那個 Bin t2 t3 的例子也 okay. 我想這你也許發現了 Omega 的 bug. 在我的做法中我需要把 term 給他,所以 type checker 知道怎麼去證明。而在前者之中,不知怎麼地 typechecker 就失敗了。

既然你發現了很明顯的 bug, 我可直接寫信給 Tim Sheard 問問看。謝啦!

我把我的檔案另外寄給你。

 

<< 回到主頁