ACL2の強力なルールについて
投稿日: 2022-08-18 木
今日は XDOC — Practice-formulating-strong-rules の問題を解いていた。
Strong rule とは、仮定が少なくてRewriteルールでより書き換えしやすいルールのことである。
仮定がない定理をうまく記述できると、もっと式を簡単にできるのにRewriteルールが仮定にマッチしていないために発火しない……という問題に悩まされることが少なくなり自動証明がうまくいきやすくなる。
ACL2 では同じ意味の定理でも implies を使って同じことを記述するのと iff や equal のみで記述するのでは、
全然動きが違うのでここら辺はよく勉強しておかないと何故かルールが使われない問題にぶち当たりまくって詰んでしまう。
Term 3 は普通に正解できたが、 iff と equal の rewrite ルールの使い分けに関する知見が含まれていてよかった。
Term 5 と Term 6 だいぶ悩んだ結果答えを見て納得する感じだった。
Term 5 は分からなかったらあんまり深く考えずに切り上げるのがおすすめ。
Term 6 は重要で、ためらうことなく右辺に if を使うことの大切さが書かれていた。
私は nfix を使って if のないルールを書いてしまった(強いルールではある)が、
if を使った方が意味的に正しいし綺麗だしたぶんよりうまくルールが機能しそうだったので、
自分の解答よりも if を使う方がよさそうでありたいへん勉強になった。