J-Bobを作ってみよう(10) 組み込み関数を追加する

たかだか証明を数ステップ進めるだけで関数を何百万会も呼ばなきゃいけないのかという
疑問を脇に押しのけてたくさん呼ばれてる関数を組み込み関数にしてみます
なんにも頭を使わない力技

一部抜き出すとこんな感じ

これでlist0からtagあたりまでの関数を組み込みにしました

(define (op1 op arg)
  (cond ((eq? op 'car) (jcar arg))
        :
        ((eq? op 'untag) (jcdr arg))
        ((eq? op 'elem1) (jcar arg))
        :

まずは変更前の状態で計測

> (time
   (jeval
    '(J-Bob/prove
       '((dethm car/cons (x y) (equal (car (cons x y)) x))
         (dethm equal-same (x) (equal (equal x x) 't))
         (defun pair (x y) (cons x (cons y '())))
         (defun first-of (x) (car x)))
       '(((dethm first-of-pair (a b)
            (equal (first-of (pair a b)) a))
          nil)))))
cpu time: 7711 real time: 7709 gc time: 31
'(equal (first-of (pair a b)) a)

8秒弱
では変更後

> (time
   (jeval
    '(J-Bob/prove
          :
       '(((dethm first-of-pair (a b)
            (equal (first-of (pair a b)) a))
          nil)))))
cpu time: 1938 real time: 1939 gc time: 13
'(equal (first-of (pair a b)) a)

2秒弱
けっこう速くはなった
けど昨日みたいなペースで時間がかかっていくようだと・・・？

1ステップ追加

> (time
   (jeval
    '(J-Bob/prove
          :
       '(((dethm first-of-pair (a b)
            (equal (first-of (pair a b)) a))
          nil
          ((1 1) (pair a b)))))))
cpu time: 3275 real time: 3277 gc time: 22
'(equal (first-of (cons a (cons b '()))) a)

お、そんなに長くなってない
もう1ステップ長くしても？

> (time
   (jeval
    '(J-Bob/prove
          :
       '(((dethm first-of-pair (a b)
            (equal (first-of (pair a b)) a))
          nil
          ((1 1) (pair a b))
          ((1) (first-of (cons a (cons b '())))))))))
cpu time: 16231 real time: 16228 gc time: 76
'(equal (car (cons a (cons b '()))) a)

全然待てるレベルになってる
これはもしかして証明完了できるかも？

> (time
   (jeval
    '(J-Bob/prove
       '((dethm car/cons (x y) (equal (car (cons x y)) x))
         (dethm equal-same (x) (equal (equal x x) 't))
         (defun pair (x y) (cons x (cons y '())))
         (defun first-of (x) (car x)))
       '(((dethm first-of-pair (a b)
            (equal (first-of (pair a b)) a))
          nil
          ((1 1) (pair a b))
          ((1) (first-of (cons a (cons b '()))))
          ((1) (car/cons a (cons b '())))
          (() (equal-same a)))))))
cpu time: 279645 real time: 282110 gc time: 1134
''t

できた
でも5分弱かあ
ちょっと実用には遠いなあ

公理も最小限しか入れてないし

preludeにはもっとたくさんの公理が入ってるし
第一証明がふたつ含まれてると来た

> (time (jeval '(prelude)))

まったく帰ってきませんな
さてこの先どうしたものか