I proved TPPmark2014 using Agda. <a rel="nofollow" target="

Masahiro Sakai - 2014-11-16T05:52:35+0000 - 更新日時: 2014-11-16T05:52:35+0000

I proved TPPmark2014 using Agda. https://github.com/msakai/TPPmark2014/blob/submission-20141116/TPPmark2014.agda

Agda2でTPPmark2014の問題を解いてみた。自分のAgdaの知識はほとんどAgda1の時代で止まっていて、Agda2でtoyでないものを証明するのは初めてなので、色々改良できる点は多いはず。Agda証明士の方は是非アドバイスいただければと思う。

しかし、十数行が非形式的な証明が、Agdaで書いたら675行というのは流石に効率が悪すぎる。 SemiringSolverとか使えば、退屈な当式変形は減らせるとは思うけれど……

TPPmark2014/TPPmark2014.agda at submission-20141116 · msakai/TPPmark2014 · GitHub

Masahiro Sakai - 2014-11-16T23:57:55+0000

SemiringSolverを使ってみたが、なかなか面白い。多項式半環のSetoid上で正規化によって得られた同値性を、自由半環としての普遍性から、他の半環の同値性に写しているのかな。

Masahiro Sakai - 2014-11-21T15:53:00+0000

https://github.com/msakai/TPPmark2014/blob/6963bba29d95768f6d2a57173c03efcfa1253a4a/TPPmark2014.agda#L300 で、ある簡単な補題をインライン展開すると、型検査が死ぬほど遅くなるんだけど、なんでやろ……？