$\newcommand{\defeq}{\mathrel{\mathop:}=}$

## 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


kind Parity = Even | Odd

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


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)


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)


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

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.


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


--

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 --> []

Exactly 0 rules match:

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


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 --> []

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 --> []



--

Labels:

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." 大概我弄得比較複雜，還多用了一堆定理的關係。

Bin :: Balanced {parity {plus m n}} m n
-> Parity' {parity {plus m n}}
-> Tree a m -> Tree a n
-> Tree a {plus m n}