エントリーの編集
エントリーの編集は全ユーザーに共通の機能です。
必ずガイドラインを一読の上ご利用ください。
CoqによるZ定理(及び,β簡約の合流性)の証明 - fetburner.core
記事へのコメント0件
- 注目コメント
- 新着コメント
このエントリーにコメントしてみましょう。
注目コメント算出アルゴリズムの一部にLINEヤフー株式会社の「建設的コメント順位付けモデルAPI」を使用しています
- バナー広告なし
- ミュート機能あり
- ダークモード搭載
関連記事
CoqによるZ定理(及び,β簡約の合流性)の証明 - fetburner.core
PPL 2019のポスター発表でZ定理[Dehornoy+08]なるものを知ったので,Coqで定式化してみる. それだけで... PPL 2019のポスター発表でZ定理[Dehornoy+08]なるものを知ったので,Coqで定式化してみる. それだけでは面白くないので,これを用いて簡約の合流性も証明する. Z定理[Dehornoy+08]とは? 抽象書き換え系は,以下のようなZ性を満たすが存在すれば満たせば合流するといった定理. 例えば簡約の合流性を示す際はcomplete development(見えているredexを全て簡約するもの)のZ性を証明するだけでよくて, 良く知られている証明のように並列簡約を用いなくても良いのがうれしいらしい. Z定理[Dehornoy+08]の証明 合流性と準合流性は等価なので,Z性を満たすが存在すればが準合流性を満たすことを証明すればよい. ならばだけステップ数に関する帰納法で示してしまえば, あとはとにZ性を適用するだけで下図のように準合流性を証明できる. Coqでの証明も難しく