Conversation

Notices

1. きゅーけー (tojoqk@mastodon.tojo.tokyo)'s status on Thursday, 04-Feb-2021 10:19:49 JST きゅーけー

   適当に順序数を使って measure を定義したら、アッカーマン関数の停止性の証明に成功してしまった。 #ACL2 すごい！https://gitlab.com/tojoqk/sicp-acl2/-/commit/97b078fedf4fb2f3934cf35cd68ca87fc66b8591

   • hiromi_mi likes this.
   • きゅーけー (tojoqk@mastodon.tojo.tokyo)'s status on Thursday, 04-Feb-2021 10:26:50 JST きゅーけー

     in reply to

     アッカーマン関数の停止性の証明、順序数を使ったら良さげなところまでは分かったんだけど、そっからどうやって証明すればいいのかさっぱり分かってないのに指示したら #ACL2 がスパッと証明してくれたの、なんか禁断の領域に踏み込んだ気がする。

     hiromi_mi likes this.