kb84tkhrのブログ

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

定理証明手習い (20) 尺度

全域性を証明するために尺度を導入します
関数が再帰的に呼び出されるたびに尺度が減少することを示すことによって
いつかは再帰が終わることを証明します
無限下降法的な何か?

sizeはリストを作るために必要なconsの数でした
以下のような公理を使って全域性を証明します

  • (size x)自然数である
  • (size (car x))(size x)より小さい
  • (size (cdr x))(size x)より小さい

関数の場合は「種」に尺度を入れてやるようです
すると、全域性を主張する式が返されます

> (J-Bob/prove (defun.list2?)
    '(((defun list? (x)
         (if (atom x)
             (equal x '())
             (list? (cdr x))))
       (size x))))
(if (natp (size x)) (if (atom x) 't (< (size (cdr x)) (size x))) 'nil)

どんなしくみで式を作ってるんでしょうか

  • 尺度は自然数である
  • ifのQ部はそのまま
  • 再帰は引数の尺度が現在の尺度よりも減っているという式に変換
  • それら以外の式(全域と分かってる式ってことかな)は'tに変換

みたいな感じでしょうか
例をひとつ見ただけなのでまだなんとも言えません
第8章で説明されるそうです
最終的には付録CがJ-Bob自身の解説なので、そこを読めば完璧?

で、あとは主張の式を公理や関数適用で置き換えていって'tであることを示します
ここは今までと同じ

  • 再帰しない関数については全域性は自明

なので証明も不要だったわけですね
そのためにも組み込み関数はすべて全域である必要があると

今度は0.9mm芯書き比べ

もやっと感がおさまらないので結局0.9mmの芯もいろいろ買ってきました

今回試してみるのはこの4種類
この間買ったCampus 0.9mm 2B
uni Nano Dia 0.9mm 2B
PILOT neox GRAPHITE 0.9mm 2B
プレスマン用替芯 0.9mm 2B
前回ちょっと薄めに感じたAinSTEINは候補から外しました

書いてみた結果

f:id:kb84tkhr:20180120172254p:plain

傾向としては0.7mmと同じですかね
太くなった分は滑らかさとかは感じます
Campusがちょっと薄いくらいでどれも及第点かな

しかし元々入ってた芯はなんなのかという謎は解決せず・・・
もう1本シャーペン本体買ってみるか

定理証明手習い (19) atom

前回のlist?シリーズでlist?のA部の(equal x '())(=list0?)が
list1?list2?では'nilに置き換えられているのは
何か一般的な書き換え規則があるんでしょうか
Scheme風に書いた方では#t#fになってます
何かあるような気がしますが思いつきません

他の再帰する関数でやってみるとどうなるかな

ちょっと先回りしてrembという関数を持ってきました
Booleanじゃない関数の方が違いがわかるかなと思って

(defun remb (xs)
  (if (atom xs)
      '()
      (if (equal (car xs) '?)
          (remb (cdr xs))
          (cons (car xs) (remb (cdr xs))))))

ちょっと長いですがやってみます
こう・・・かなあ?

(defun remb0 (xs) '())

(defun remb1 (xs)
  (if (atom xs)
      '()
      (if (equal (car xs) '?)
          (remb0 (cdr xs))
          (cons (car xs) (remb0 (cdr xs))))))

(defun remb2 (xs)
  (if (atom xs)
      '()
      (if (equal (car xs) '?)
          (remb1 (cdr xs))
          (cons (car xs) (remb1 (cdr xs))))))

さっきの話をあてはめてみるとrembのA部の'()remb0と同じで、
remb1remb2のA部では何かに置き換えられる・・・
いやそこ意味ないんじゃないの?
なんでもいいのかな

list1?は長さ1のリストかどうかを判定する関数だからどんな長さのリストでも
わかりやすい値が決まりますが
remb1は長さ1のリストから'?を削除する関数だと考えると
長さ1のリスト以外では意味のある値を持ちませんね
部分関数の時の話からすると、そういうときはなんでもいいってことですかね?
なんでもいいことにしました

なんでもいいことにするとしたら、remb0はむしろこういう形?

(defun remb0 (xs) 
  (if (atom xs)
      '()
      (なんでもいい))

(defun remb1 (xs)
  (if (atom xs)
      (なんでもいい)
      (if (equal (car xs) '?)
          (remb0 (cdr xs))
          (cons (car xs) (remb0 (cdr xs))))))

(defun remb2 (xs)
  (if (atom xs)
      (なんでもいい)
      (if (equal (car xs) '?)
          (remb1 (cdr xs))
          (cons (car xs) (remb1 (cdr xs))))))

こう考えればrembremb0remb1remb2の関係は明確になってるか
これでいいか

定理証明手習い (18) atom

対話的定理証明器という言葉を見かけました
j-bobに1行足しては結果を見てまた1行足す、ってやってるのを思い出して
ああこれは対話してたんだ、と思うなど

さて

(defun list0? (x)
  (equal x '()))

(defun list1? (x)
  (if (atom x) 'nil (list0? (cdr x))))

(defun list2? (x)
  (if (atom x) 'nil (list1? (cdr x))))

からの

(defun list? (x)
  (if (atom? x) (equal x '()) (list? (cdr x))))

ですが、この書き方が慣れません
'()がアトムとされてるので、xがアトムであるか判定したあと
さらにx'()かどうかを判断しないといけないですよね

Schemeならこう
こっちのほうがすっきりしてませんか

(define (list0? x) (null? x))

(define (list1? x)
  (if (null? x) #f (list0? (cdr x))))

(define (list2? x) 
  (if (null? x) #f (list1? (cdr x))))

(define (list? x)
  (if (null? x) #t (list? (cdr x))))

っていうかnull?がないのがよくないのか

'()がアトムとされてたり、null?がなかったりするのにも
(car '())'()としたのは全域性のため、みたいに何か背景があるんでしょうか

定理証明見習い (17) 部分関数

  • 部分関数の置き換えを認めると矛盾が発生する

部分関数の例はこれ

(defun partial (x) (if (partial x) 'nil 't))

こうじゃないのはなぜか

(defun partial (x) (partial x))

いちおう値を返しそうな雰囲気はかもし出しておきたい、くらいかな
であれば、こうじゃないのはなぜか

(defun partial (x) (if (partial x) 't 'nil))

評価してみて返ってくるかどうかで部分関数かどうかを判定するっていう意味合い?
いやちょっと無理があるか

さてpartialは部分関数なのでこういうの書いても'tになることはないでしょうから
証明なしで定義する必要があります

(J-Bob/prove (my/prelude)
  '(((defun partial (x)
       (if (partial x) 'nil 't))
     ...

この間は無理やり公理のリストに付け足してやりましたが
J-Bobのお作法ではlist-extendというのを使うようです
list-extendはそんなに特別な処理をしてるわけではなくて、
項目を追加したリストを返す関数ですが、リスト内にすでに同じ項目がある場合は
何もせず元のリストを返します なるほど
(J-Bob/prove (my/prelude) ...)の代わりに
(J-Bob/prove (list-extend (my/prelude) A) ...)としてやれば
一時的にmy/preludeに定義Aを付け加えて証明を記述することができます

いまさら気が付きましたが(J-Bob/define (prelude) ...)
preludeを囲んでるカッコは構文上のカッコじゃなくて
単に関数適用のカッコですね
マクロかと思ってました

で部分関数の置き換えが可能だとどんなことになっていくかやっていきます
以下の...に置き換えを書いていきます
付録Bだとdethmの行のインデントがずれてて構造が見にくくなってます
カッコの数は数えないので!

(J-Bob/prove
  (list-extend (my/prelude)
    '(defun partial (x)
       (if (partial x) 'nil 't)))
  '(((dethm contradiction () 'nil)
     nil
     ...)))

(略)ということでpartialが適用できてしまうと'nil'tになってしまいます

どういうカラクリかと見てみると
(partial x)(if (partial x) 'nil 't)に置き換えたときに
真偽が反転してます
なので

(defun partial (x) (if (partial x) 't 'nil))

ではそういうことは起こりません そういうことか
これも部分関数ではありますが

部分関数が全部悪いわけじゃないけど念のため全部ダメなことにする、ってことでしょうか
矛盾は引き起こさないとしても値を返さないことがあるんだからやっぱダメかな

部分関数を置き換えるのはまずいとして
じゃあ公理を使って例えば'nil(if (partial x) 'nil 'nil)
書き換えるのは問題ないんでしょうか
'nilの値は'nilですが(if (partial x) 'nil 'nil)は値を返さないので
もうすでにこの時点でおかしくなってるはず
いや、それを言うならmy/preludepartialを追加した時点でおかしいのか
追加できたということは全域であると宣言してるようなものだから

さらにこれは部分関数かどうか

(defun partial (x) (if (partial x) 't 't))

普通に動かしたら無限ループですがif-sameの公理が使えれば'tになります
if-sameを使ってはいけない条件というのがあるんでしょうか
単に関数定義の中では公理による置き換えは使えないというだけかな

同じ形の定理なら証明できますけどだからといって関数が全域であるとは言えなさそう

(J-Bob/prove
  (list-extend (my/prelude)
    '(defun partial (x)
       (if (partial x) 't 'nil)))
  '(((dethm partial-theorem (x)
       (if (partial x)
           't
           't))
     nil
     (() (if-same (partial x) 't)))))

せっかく矛盾を導けたので、矛盾を使って任意の命題を証明する、っていうのが
できないかと思いましたが
「帰結」がないのでDethmの法則が適用できませんね
残念

全域関数でも、矛盾した結果が証明されてしまうものがあるのではないでしょうか?
ありません。

無矛盾性?
どういう証明になるのかな
帰納法でやるんだろうけれども

Campus 0.9mm 2B

というわけでCampus 0.9mm 2Bの芯を買ってきたわけなんですが

違う・・・薄い

じゃあ今入ってるこの芯は何なの
家には0.9mmの替芯なんてないし
それ以外で入れ替える機会なんてあるかなあ
KOKUYOだけどCampusじゃない芯なの?

むー
またあるだけ買ってくるのか
これは最悪、全部試したあげくにやっぱ不満、まであるな

主力は万年筆なのになんでこんな必死になってるの
ほんとうはCapless DecimoのFがほしいんですけど

定理証明手習い (16) 全域

  • 全域とは、どんな値を渡しても関数が値を持つということ

この間pairは全域、って話が出てました

組み込み関数は、すべて全域です。
そうだったんですか!

そうだったんですか!

Scheme手習いでは

lcarは何ですか。
ここで
l'()です。
答えはありません。

って掟になってたけどこれは全域じゃないってことだよな
素のRacket(r5rsにしても)でやるとエラーになります

全域なら(car '())の値はなんだろう
j-bob-lang.scmより

(define (car x) (if (pair? x) (s.car x) '()))
(define (cdr x) (if (pair? x) (s.cdr x) '()))

'()
そういえばCommon Lispでは(car '())(cdr '()))'()だったっけ?
Schemeと比べてなんか変だなと思ったけど全域であることを大事にしたってことでしょうか

すぐ下にはこう書いてあります

意外かもしれませんが、そうなのですよ。
それじゃあ、(cdr 'grapefruit)の値は何になるっていうんですか?
考慮するのは、コンスしたものに対するcdrの結果だけです。(cdr 'grapefruit)には何かしら値があるはずですが、それが何であるかを知る必要はなく、値があるということだけわかれば十分なのです。

ふーん
理屈上、そんな引数で評価されることはないわけだから何でもいいってことかな
実用的な観点からはエラーにしてほしい気がするけど
理論上は全域じゃないと取り扱いが面倒な感じはする

ここでは、全域というのはいつでも正しい値を返すという意味じゃなくて、
ただいつでも値を返すっていう意味と理解して進みます
組み込み関数もifも必ず値を返すのでそれらを組み合わせただけなら
必ず値を返すはず
値を返さないっていうのは無限ループしちゃってるときくらいですかね

Defunの法則は更新されて最終バージョンに
再帰的であっても全域であれば置き換えていいことになりました