今日は飲み会でした
で書くネタも用意してないわ電車の中でも書いてないわで
でも小さな習慣で決めてるから何か書かないとってやつなんですが
会社の人との飲み会なんですけどレベルの高い人達の集まりで
聞いてると楽しいんですけど自分がいていいんだっけって感じ
ちょっと発言も背伸び気味だったりして
あれくらいの集まりでも素でいられてかつgive&takeできるくらいに
なれるといいなあと思ったのでありました
定理証明手習い (27) 証明スタート
こんな定理を証明します
(dethm ctx?/sub (x y)
(if (ctx? x)
(if (ctx? y)
(equal (ctx? (sub x y)) 't)
't)
't))そういえばこの間
定理証明手習い (9) 「2 もう少し、いつものゲームを」 - kb84tkhrのブログ
'tってなんだよ'tって、と思いましたがこれはたぶん定理は常に'tでないと
いけないので入れてあるってことでしょう
なんて書きましたがこれ見てるときに思い出しました
自分でこんなこと書いてたのを
「AならばB」っていうのは「もしAが真ならばB」ってことだよね
Aが偽のときについては何も言ってないね
何も言ってないけど実はこういうことなんだよもしAが真ならばB
(妄想)「ならば」の教え方 - kb84tkhrのブログ
そうでなければ (Bが何だろうと気にしないで)真
そうか「ならば」を素直に書いてただけだったか
定理を真にしないと、っていうのはちょっと見当外れだったぽいです
さて
種としてはリストの帰納法でlist-inductionを使ったように、
スター型の機能法ではstar-inductionを使います
(defun star-induction (x)
(if (atom x)
x
(cons (star-induction (car x))
(star-induction (cdr x)))))やっぱり木を木のまま返すだけの関数
これが種になっているわけですがここからどうやって証明すべき式が出てくるのか
ちょっと見えてきません
とにかく種を与えてみます
(J-Bob/prove (defun.ctx?)
'(((dethm ctx?/sub (x y)
(if (ctx? x)
(if (ctx? y)
(equal (ctx? (sub x y)) 't)
't)
't))
(star-induction y))))どれどれ
(if (atom y)
(if (ctx? x) (if (ctx? y) (equal (ctx? (sub x y)) 't) 't) 't)
(if (if (ctx? x) (if (ctx? (car y)) (equal (ctx? (sub x (car y))) 't) 't) 't)
(if (if (ctx? x) (if (ctx? (cdr y)) (equal (ctx? (sub x (cdr y))) 't) 't) 't)
(if (ctx? x) (if (ctx? y) (equal (ctx? (sub x y)) 't) 't) 't)
't)
't))見るからにきっつい感じです
最初はifの持ち上げから
(if (ctx? x) ...)という形が何度も出てきているので、
ifの持ち上げを使ってやるとひとつにまとめることができます
分配法則を使ってるようなイメージ
ifの持ち上げ＋アルファでこれくらいに
(if (ctx? x)
(if (atom y)
(if (ctx? y) (equal (ctx? (sub x y)) 't) 't)
(if (if (ctx? (car y))
(equal (ctx? (sub x (car y))) 't)
't)
(if (if (ctx? (cdr y))
(equal (ctx? (sub x (cdr y))) 't)
't)
(if (ctx? y) (equal (ctx? (sub x y)) 't) 't)
't)
't))
't)終わるんでしょうか
定理証明手習い (26) 7. びっくりスター!
第7章はスター型関数に関する定理の証明
題材となるスター型関数はこれ
(defun ctx? (x)
(if (atom x)
(equal x '?)
(if (ctx? (car x))
't
(ctx? (cdr x)))))まずは全域性の証明
種は(size x)
証明すべき式はこれ
(if (natp (size x))
(if (atom x)
't
(if (< (size (car x)) (size x))
(if (ctx? (car x))
't
(< (size (cdr x)) (size x)))
'nil))
'nil)この関数が全域であるという主張は、本書の中でも特に複雑なものです。
そうですか
でも証明は特に難しくはありません
全域性の主張をどうやって構成するのかは、第８章で詳しく説明します。
おおざっぱに考えると
(if (natp (size x)) ... 'nil)はオマジナイで
あとは関数の形をもとにしつつ
(car x)や(cdr x)を見かけたらsizeが小さくなっていくことを
確かめるって感じでしょうか
(equal x '?)は全域だってわかってるから'tに変換するってことかな
でも全域だからって(atom x)を'tに置き換えちゃうとこれは変
明確なルールにするとすればどうなるんでしょう？
Q部はそのままとか？
もうちょっと何かありそう
Q部が再帰することもあるでしょうし
その時は1段ifを増やしてsizeが減ってることを言うんでしょうか
話が長い親
ムスメが450分って何時間？って聞いてきたわけです
そこで7時間30分だよ、って言えば話は終わりなんですけどね
答えを言うのは気が進まないんです
450÷60はいくつ？くらいで済ませればいいんですがそうは問屋がおろしません
1時間は何分？
60分だね
450分の中に60分はいくつある？
ん？わかんない？
じゃあ、60分は何時間？
120分は何時間？
180分は何時間？
うんうん、それはどういう計算でやってることになる？
そう、割り算してるんだね
じゃあ450÷60を考えてみよう
2桁で割る割り算は習ってない？
でも、工夫すればできると思うよ
10分のかたまりで考えてみよう
450分の中に10分のかたまりはいくつ？
60分の中には？
そうだね
45個のかたまりの中に6個のかたまりはいくつあるかな？
そう、7個あって余りは3個だね
どんな式で考えたの？
そう、45÷6だね
じゃあ、元の話に戻ってみよう
450分は何時間かな？
7時間と・・・？
3分じゃないんだな
さっきのは、10分のかたまりが3つ余ったってことだから？
そう、30分余るってことだね
つまり450分は7時間30分ってことだ
式で言うと、450÷60=7あまり30ってことだね
からの
さっき、450で考える代わりに60とか120とかで考えてみたよね
考えやすい例を考えてみるっていうやり方は役に立つよ
今度難しい問題でどうやっていいかわからないときは試してみ？
あたりまでが想定問答
まあ最後まではなかなか聞いてもらえませんけど
答えを教える
やり方を教える
考え方を教える
考え方の考え方を教える
ことによって考え方の考え方の考え方に気づいてほしい、という親の願いでした
2018 WorkFlowy RoadMap ですって
こんなの出てましたよ
- モバイルアプリの再設計
ちょっと今のモバイルアプリはひどいからがんばるよ！でもまだまだ先は長いよ！アルファ版もあるからよかったらどうぞ！ - モバイルアプリからの逆輸入
モバイルアプリの便利な機能はWe版やデスクトップ版でも使えるようにするよ！Quick AddボタンはGTDのInboxにちょうどいいよ！ - チーム作業の改善
今でもほかの人や他の機器と同期できるけど、もっと便利になるよ！ - 日付・リマインダー機能
お待ちかね！
だって
MemoFlowyとHandyFlowy使えばいいのにね！
定理証明手習い (25) 6 最後まで考え抜くのです
って話でしたがやっと帰納法です
ここでは「種」にlist-inductionという関数を使います
これはなんでしょうか
関数名は「リスト帰納法」ですね
実体はpreludeに入っていました
こういう関数です
(defun list-induction (x)
(if (atom x)
'()
(cons (car x)
(list-induction (cdr x)))))・・・なんこれ？
リストをそのまま返すだけの関数にしか見えませんが
リストじゃなければ'()を返しますがそこは大事じゃなさそうな気が
ここはこういうものとして、my/preludeで定義してやってから・・・
> (J-Bob/prove (dethm.memb?/remb2)
'(((dethm memb?/remb (xs)
(equal (memb? (remb xs)) 'nil))
(list-induction xs))))
(if (atom xs)
(equal (memb? (remb xs)) 'nil)
(if (equal (memb? (remb (cdr xs))) 'nil)
(equal (memb? (remb xs)) 'nil)
't))うんできました
数学的帰納法と言えばこんな感じのやつですが
- A(1)が成り立つ
- A(k)が成り立つと仮定するとA(k+1)も成り立つ
- ゆえに、任意の自然数nに対してA(n)が成り立つ
これに合わせて上の結果を読んでやると
(equal (memb? (remb '())) 'nil)が成り立つ(equal (memb? (remb (cdr xs))) 'nil)が成り立つと仮定すると
(equal (memb? (remb xs)) 'nil)が成り立つ- ゆえに、任意のリスト
xsについて(equal (memb? (remb xs)) 'nil)が成り立つ
てとこですかね
ぴったり
memb?/rembの定理でxsになっている箇所が、この式では(cdr xs)になっています。ここが、今証明しようとしている主張における、自然な再帰ということなんでしょうね。
主張について言うときは、（自然な）再帰ではなく、**帰納法のための前提**と呼びます。
ここテストに出るよ
しらんけど
list-inductionと、上のJ-Bob/proveの結果を見比べると
種に書いた関数は、それを呼んでどうこうするというより
証明の最初のステップのテンプレートみたいにして使われるっぽいようにも見えます
ただ、list-inductionのE部からそのままJ-Bob/proveの結果のE部が
出てくるってわけでもないし
ここにもうひとカラクリあるのか、それともテンプレートっていう予想が見当違いなのか
関数の全域の証明では(size xs)を種にしましたが
これもテンプレートっぽくはない
定理と関数で違う動きなんでしょうか
種を入れて証明すべき式が出てきたらあとはそれを'tにしてやるだけです
長いけど特別なことをするわけではありません
定理証明手習い (24) If持ち上げを定理に・・・
Ifの持ち上げを何回か書いてると面倒になってきます
これがパターンであるのなら定理として証明してしまえばいいのでは、
と思ったのですがそもそもパターンがJ-Bobで表現できるのかなあ
書けるとしたらこんな感じなんでしょうか
(J-Bob/prove (defun.remb)
'(((dethm if-lifting (original-focus Q A E)
(equal (original-focus (if Q A E))
(if Q (original-focus A) (original-focus E))))
nil
...)))でも(original-focus A)っていうような書き方は受け付けてくれないようです
これが通れば
(J-Bob/prove (dethm.if-lifting)
'(((dethm lift-test (x1)
(equal (memb? (if (equal x1 '?)
(remb '())
(cons x1 (remb '()))))
'nil))
nil
((1) (if-lifting memb?
(equal x1 '?)
(remb '())
(cons x1 (remb '())))))))で
(equal (memb? (if (equal x1 '?)
(remb '())
(cons x1 (remb '()))))
'nil)を
(equal (if (equal x1 '?)
(memb? (remb '()))
(memb? (cons x1 (remb '()))))
'nil)に置き換えることができそうなんですけど
証明的にやっちゃダメって話ではないような気がするので、J-Bobの表現力の問題？
そもそもJ-Bobの使い方がわかってないのかもしれないけど
でもここで出てこないということはそういうことなんだろうなあ
