最近、Coqで型付きラムダ計算を定義して、ProgressやPreservationを証明するという遊びにはまっています。とてもおもしろいので、みんなもやるといいと思うよ。で、最近、substitution lemmaの証明にチャレンジして、もろくも敗れ去りました。よくよく見直し…

30分プログラム、その689。ML系の言語といえばバリアント、バリアントと言えば木構造なので、2分木を作ってみました。 そのうち、B木とかに拡張できたらいいね。 使い方 - val t = List.foldl (curry insert) empty [10,3,1,4]; val t = Branch (10,Branch (…