Defined

Coqで同値関係

最近仕事でlistの要素を仲間分けしてリストのリストを返す 次のような関数をOCamlで定義した。 let rec classify rel l = match l with | [] -> [] | x::xs -> let (ys,zs) = List.partition (fun y -> rel x y) xs in (x, ys) :: classify rel zs この関数…

しりとりの圏をCoqで実装してみた

Coq で しりとりの圏を形式化した記事を見つけた。 型によるしりとりの成立判定 - コンピュータってすごいらしい via 完全実装付きでもう一度お送りします、しりとりの圏 - 檜山正幸のキマイラ飼育記すばらしかったので、私もちょっと真似して実装してみた。…