kb84tkhrのブログ

何を書こうか考え中です あ、あと組織とは関係ないってやつです 個人的なやつ

定理証明手習い(96) しゅくだい(4)

reverse/reverseの証明に戻ってここからです

(if (atom x)
    't
    (equal
     (if (atom (reverse2 x '()))
         (reverse2 x '())
         (reverse2 (reverse2 x '()) '()))
     x))

(atom x)でなければ(if (atom (reverse2 x '()))が成り立つことはない、が証明されたので

     ((E 1 Q) (atom/reverse2 x '()))
     ((E 1) (if-false (reverse2 x '())
                      (reverse2 (reverse2 x '()) '())))

して
こうなりました

続きを読む

定理証明手習い(94) しゅくだい(3)

(atom x)でなければ(if (atom (reverse2 x '()))が成り立つことはない、を証明します

(J-Bob/prove (defun.reverse)
  '(((dethm atom/reverse2 (x res)
       (if (atom x)
           't
           (equal (atom (reverse2 x res)) 'nil)))
     (reverse2 x res) ; ←

ここ!これ!きっと!
本番はreverse2/reverse2的なものの証明だけど予行演習的に

続きを読む

定理証明手習い(94) しゅくだい(2)

行き詰まり気味なのでまず確実に進捗できそうなところを済ませます

(defun defun.reverse2 ()
  (J-Bob/define (prelude)
    '(((defun reverse2 (x res)
         (if (atom x)
             res
             (reverse2 (cdr x) (cons (car x) res))))
       (size x)
       ((Q) (natp/size x))
       (() (if-true (if (atom x) 't (< (size (cdr x)) (size x))) 'nil))
       ((E) (size/cdr x))
       (() (if-same (atom x) 't))))))

(defun defun.reverse ()
  (J-Bob/define (defun.reverse2)
    '(((defun reverse (x)
         (if (atom x)
             x
             (reverse2 x '())))
       nil))))

さて

続きを読む

定理証明手習い (93) しゅくだい

(reverse (reverse x))がどんなリストについてもxになるか」…(略)…読者への宿題にしておきます。

付録Cやってるあいだに証明も忘れかけてる気がするのでちょうどいいおさらい
最初は、これを証明すればいいかな、と思ったんですけどね

続きを読む

定理証明手習い (91) おさらい(1)

さすがに間が空きすぎて、始めのうち何をやってたか忘れてるような気がするのでおさらい
ほんとは最初にざっとみてこれくらい把握しておくんだろうなあ

はじめに、とか

  • 帰納法を使うことで再帰的な関数についての事実を明らかにする方法を知る
  • 入力の可能性が無限にあるときにどう扱うのか
  • それを解決するための帰納法とはなにか
  • 主張に対して等価な式変形を繰り返して'tにすることによって定理を証明する

(reverse (reverse x))がどんなリストについてもxになるか」…(略)…読者への宿題にしておきます。
せんせい、しゅくだいわすれました!

続きを読む

定理証明手習い (92) おさらい(2)

5 何回も何回も何回も考えよう

定理の証明

  • 洞察:内側から外側へと書き換えるべし
  • Ifの持ち上げ
  • 洞察:Ifを外側へ
  • 洞察:いつも心に定理を
続きを読む

定理証明手習い (90) J-Bob/define

J-Bob/defineを定義していきます
rewrite/proveは再利用
その後も、'tを返すか定義のリストに証明された定義を付け足すかくらいなので
それほど大きな違いはありません

続きを読む