J-Bobを作ってみよう(9) J-Bobをプロファイリング

J-Bobを動かしてみます

>> (load "j-bob.jbb")
Welcome to J-Bob
#<void>
>> (J-Bob/step
     '((dethm car/cons (x y) (equal (car (cons x y)) x)))
     '(car (cons 'ham '(eggs)))
     '((() (car/cons 'ham '(eggs)))))
'ham
>> (show-profile)
     '((untag 18159)
       (elem1 9304)
       (tag? 6366)
       :

意外とたくさん動いてる感じ

untagなんてただのcdrだけどuntagを解釈してcdrを実行するまでに
Racketのレベルでまたいろいろ動くわけだしなあ
これが一瞬で終わるだけでもすごいことって気もしてきた

これが、こういうインタプリタでコードを実行するならこんなもんです、バグじゃありません、って
確かめられるといいんだけどなあ
ソース見る限りとんでもなく無駄に回ってるところはないような気はするんだけどあてにはならない

J-Bob/proveはどうだろう
証明が終わるところまでは実行できなかったからまずは証明0ステップで

>> (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)))
(equal (first-of (pair a b)) a)
>> (show-profile)
     '((list-extend 226166)
       (list1 187381)
       (list0 187381)
       (untag 35768)
       (elem1 26557)
       (elem2 13393)
       :

ちょっと違う傾向が見える？
これで5秒くらい
なおpreludeを評価するとその時点で帰ってこなくなるので最低限の公理だけにしました

1ステップ伸ばしてみます

>> (J-Bob/prove
     :
     '(((dethm first-of-pair (a b)
          (equal (first-of (pair a b)) a))
        nil
        ((1 1) (pair a b)))))
(equal (first-of (cons a (cons b '()))) a)
>> (show-profile)
'((untag 232396)
  (list-extend 226166)
  (list1 195157)
  (list0 195157)
  (elem1 113728)
  (tag? 64900)
  :

終わらないのでしばらく放置してました
list-extendは226166のままですね
ステップ数にはよらない？

もう1ステップ

>> (J-Bob/prove
        :
        ((1 1) (pair a b))
        ((1) (first-of (cons a (cons b '())))))))
(equal (car (cons a (cons b '()))) a)
>> (show-profile)
'((untag 2538484)
  (elem1 1131874)
  (tag? 789077)
  (elem2 591683)
  (defun? 474576)
  :

untagは証明が1ステップ伸びるたびに一桁増えてるなあ
1ステップごとにn倍、じゃ普通のコンパイラでやったって動かなくなりそうだけど・・・？