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))こ…

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

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