2017-09-09から1日間の記事一覧

最左最外簡約の性質をCoqで証明する

Coq

正規形を持つ項は最左最外簡約によってもその正規形に簡約されるのは有名な話．これはかなり嬉しくて，最左最外簡約は値呼びとは何だったのかと言わんばかりの優秀な評価戦略と言えるでしょう．しかし，この性質は有名な割に定理証明支援系を使った証明を…