2019-08-01から1ヶ月間の記事一覧

Coqで「停止性 + 弱合流性 = 合流性」の証明

Coq

小ネタです。 Abstract Rewriting Systemにおいて、「停止性と弱合流性(局所合流性)を持つ書き換え系は合流性を持つ」という定理があります*1。 この証明は、書き換え系の停止性から整礎帰納法を使って示すのが一般的です。 整礎帰納法はCoqでどうやるんだろ…