普通のバランス木ですね。これを
GaersAgda という CbC に対応したAgda の一種の手続き型言語で書く
で、それを Hoare Logic 的な方法で証明していく
なんですが、割と難航してて。去年は学生と一緒にやったんだけど、
Invariant とFind
ぐらいまででな。その後のバランスさせながら上にあがるってのが面白いんだが
バランスさせるのは case1 から case6 まであるんだが、なんか case5まで到達
思ったより複雑なんですが、たぶん、今年のプロシンのネタにすると思います
削除の方も同じ Invariant 使えれば、まぁ
それで、こいつを CbC にコンパイルできるはずなんだが
No comments:
Post a Comment