愚痴です。スマヌ。えーと、学内のfundingに応募するために5ページのproposal書いているのですが。読むのが科学系一般の人たちということで何の基礎知識もなしで読めるものを書かないといけないそうです。しかも、割と複雑なことを書いてしまうと余裕で飛ば…

ACL2とはなんぞやということについて全く説明していないので一応。私なぞに解説する権利はないといえばないんですが、日本語での説明がろくにないというか日本語限定でACL2をぐぐるとこのブログがトップなんですが困ったな。たぶんオフィシャルサイトはACL2 …

まずmeasureを定義。関数定義はlispと同様でdefun。アイデアとしては、まずab and b ACL2 !>(defun m (a b c) (if (and (integerp a) (integerp b) (integerp c)) (if (<= a b) 0 (if (<= b c) (cons (cons 1 1) (- a b)) (cons (cons 1 2) (- a b)))) 0))こ…

連続体濃度がアレフ２より大きくなって欲しくない理由 - くるるの数学ノートid:w2allenさんにコメント欄で質問を受けたのをこちらに持ってきます。 今の話を身近な数の世界で考えると、アレフ０は自然数の濃度、アレフ２は実数の濃度となります。そして、ア…

もろもろの成り行きで、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のソースに比べると直感的になっているかなと思うの…

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

V=Lとtransitive collapseの話書けよ>自分

mixi某所で少し書いたことの拡張版をこちらに。V=Lというモデルが最小であるという仮定を使った議論と、モデルを拡大するforcingが似たように見えることがあるというお話。具体例はちょっと書けませんが、ある条件を満たすtopological spaceを強制法で構成し…

かがみさんの日記 - トンデモ(アレフ編)調べてみたら、ジョルダン曲線定理のmechanical proofに絡んだ人じゃないですか。要するに、コンピュータでチェックされていない証明は認めないという方針のようです。 ジョルダン曲線定理のウィキ先生による解説はこ…