もろもろの成り行きで、ADを仮定するとがmeasurableになるとかそういうのの証明を読んでいます。次の節はADからWoodin cardinalの整合性が出るってやつです。割と普通に読めて嬉しいんですが、ふと我にかえるとclub filterがultrafilterってどういうことよ、…

fine structure argumentがforcingに見えてくる瞬間 - くるるの数学ノートこういう話をした直後に、やっぱりdiamond-plusから行けそうな気がしてくるってのはどういう現象なんでしょうか？まあ、やりとりがあると脳が活性化するとか言う無難な線で納得しよう…

数理科学的バグ撲滅方法論のすすめ - 第2回 「単一代入」と「末尾再帰」：ITpro IT Pro連載第2回 - sumiiの日記ACL2の通常モードだとループが全く書けないのにむかついていたのですが、これを見てなんとなく納得できました。住井さん、ありがとうございます。

ACL2いじっているよネタの続き。とりあえず、普通の(3変数の)たらいまわし関数の停止性が証明できました。Call-by-needで、なんだけど拡張をすることメインで考えているのでご愛嬌。とりあえず、例のMooreのソースに比べると直感的になっているかなと思うの…

二週間に一回は書かないと。さすがに。