DynalistとWorkflowy
たいしたアクセスもないこのブログですがアクセス解析を見ていると
ここ２ヶ月くらいはずっとこの記事がアクセス数１位をキープしてます
はっきり数は出ませんがアクセス数も増えてるんじゃないかな
ちょっとずつDynalistがポピュラーになってきてるんでしょうか
でもその後はこんな感じなんですよね
Memoflowy的なアプリも出るみたいだしDynalistもバージョンアップしてるようなんで
その後状況は変わってるかもしれないんですけどね
結局Workflowyの「書き味」というか「哲学」的なところが自分に合ってるようです
とTwitterのタイムラインを見て思いましたとさ
これからアウトライナー始めようっていう人は機能の多さだけで決めずに
どっちも試してみてほしいです
データの移行は完璧を目指さなければ両方向いけます
＃なおDynalistよりWorkflowyがいいよと言ってるわけではないです
そんだけ！
定理証明手習い (3) 「1.いつものゲームに新しいルールを」
『Scheme手習い』を読んだことは？
'nil
#tですよ！
- ある式に等しい式は無数にあるが、値はひとつしかない
- 変数の値が決まってなくても式の値が決まることがある
- 注目する部分を「フォーカス」、その外側を「文脈」と呼ぶ
フォーカスを、それに等しい式で置き換えていくことにより値を求める、というのを
練習していきます
Little Schemerではこんな感じで考えてましたが
(length '(a b))
= (add1 (length '(b)))
= (add1 (add1 (length '())))
= (add1 (add1 0))
= (add1 1)
= 2Little Proverではこんな感じ
(equal 'flapjack (atom (cons a b)))
= (equal 'flapjack 'nil)
= 'nil何が違うかというと
Little Schemerでは仮引数に値を入れることからスタート
Little Proverでは仮引数に値を入れないでスタート
してるってことですかね
だから仮引数の値にかかわらず等しくなるような式で置き換えなければならない、と
- 真(
't)であると想定した基本的な仮定を公理という - 常に真となる式を定理という
- 定理には証明が必要
さっきの式変形も実は公理に基づいていて使った公理は以下のように書きます
(dethm atom/cons (x y)
(equal (atom (cons x y)) 'nil))この公理で(atom (cons a b))を'nilに書き換えてるわけですね
Consの公理（最初のバージョン）の日本語訳（？）
といっても、コンスはアトムではない、って言っちゃうと使えなくなっちゃうな
(atom (cons x y))と'nilは等しい(car (cons x y))とxは等しい(cdr (cons x y))とyは等しい
最初のバージョン、と言ってるということはまだ追加があるんでしょうね
あと何かなあ
等しいものは置き換えていいよ、っていうのがDethmの法則
えーと、参照透過性、ってやつでしたっけ
副作用があるとできないやつですね
(equal 'nil 'nil)を'tにするのは単に関数適用？
引数が確定してれば公理じゃなくて普通に関数として評価すればいいのかな？
違うな
これも公理でした
(dethm equal-same(x)
(equal (equal x x) 't))置き換えてもいいよ、と言ってるequalと置き換え対象のequalが入り混じって
なんだかややこしいです
なお、このequalは(atom (cons x y))を'nilが等しいことを言っているので
(atom (cons x y))を'nilに書き換えるだけでなく
'nilを(atom (cons x y))に書き換えるのに使うこともできます
わかりませんが意外な使いみちがあるかもしれません
これも公理
Equalの公理（最初のバージョン）
(equal x x)は'tに等しい(equal x y)は(equal y x)に等しい
反射律と対象律だからあとは推移律が追加になるのかな？
(equal x y)かつ(equal y z)ならばxはzに等しい、みたいなやつ
ならば？
例によって1ステップずつしつこく練習させてくれます
J-Bobは、ある式を別の式に書き換えるのを手助けしてくれるプログラムです。
以下次号
定理証明手習い (2) J-Bobを動かす
「自分で動かしながら楽しみたい」という読者のために、J-Bobという簡素な定理証明支援系を用意してあります。
必須じゃないという書き方ですね
でもせっかくですから動かしてみたい
まずはThe Little Proverのページにアクセスしてみます
J-BobはGitHubからダウンロードできます
SchemeやRacketでも動くって書いてありますね
よかったよかった
Racketで動かすにはDracuraっていうパッケージがいるようです
でもSchemeで動くならそれでよさそうな気もするけど
どっちでやってみるかな
まずはDracuraから見てみよう
DracuraはACL2のためのプログラミング環境です、か
なるほど
DrRacketとACLをくっつけてぐちゃっとするとDraculaになりそうだな
uが足りないか
DrRacketは入ってるから、まずACL2を動かさないと
なかなか大変だな
ACL2からたどっていくとMac OS Xにはpre-built binary distributionがあるらしい
さらにACL2 SedanっていうバイナリやドキュメントやEclipseベースの開発環境が
全部入りのがあるって書いてあるな
別にRacketにこだわらなきゃこれ入れとけば済むのかな
でも今ネット環境がなくてiPhoneのテザリングでJDKとEclipse落とすのはちょっとつらい
・・・
考えるのに疲れてScheme版の方を試すことに
RacketでScheme版を動かす手順も書いてあります
以下、LittleProverフォルダを使うことにします
- GitHubからj-bobをダウンロード
- schemeフォルダをj-bobという名前でLittleProverフォルダに保存
- DrRacketのLanguageメニューからChoose Languageを選択
- Other Languages、R5RSを選択
- Show Detailsを選択してDisallow redefinition of initial bindingsのチェックを外す
- FileメニューのNewで新規ファイルを作成し、test.scmという名前でLittleProverフォルダに保存
で以下のコードを入力してやればいけそう
(load "j-bob/j-bob-lang.scm")
(load "j-bob/j-bob.scm")意味はわかりませんがちょっと先回りしてテスト
> (defun chapter1.example1 ()
(J-Bob/step (prelude)
'(car (cons 'ham '(eggs)))
'(((1) (cons 'ham '(eggs)))
(() (car '(ham eggs))))))
> (chapter1.example1)
'hamどうやら使えるようになったみたいです
今はACL2を使いたいってわけではないのでこれでいいかな
定理証明手習い (1) はじめに、とか
では『定理証明手習い』ゆっくり読んでいきます
Litter Schemerシリーズは何冊もあって全貌はよくわかってないんですが
知ってる範囲では以下の４冊があります
- The Little Schemer (Scheme手習い)
- The Seasoned Schemer (Scheme修行)
- The Reasoned Schemer (たぶん未訳)
- The Little Prover (定理証明手習い)
ナントカSchemerってやつはDaniel FriedmanとMatthias Felleisenの共著ですが
Little ProverはFelleisenとCarl Eastlundの共著となっています
Carl Eastlundはどういうひとかわかりませんが自動証明の研究をしている人らしいです
Seasoned Schemerまでは読んだので次はReasoned Schemerかなあ、
しかたないから英語で読むか、
と思っていたんですが
ここでLitter Proverの和訳が出たのでじゃあそっちから、てな感じです
Reasoned Schemerまでやったらコンプリート気分なのでいつかやります
では序文、はじめに、あとがきあたりから
ここからネタバレです
Little Schemerで再帰を覚えて、Little Proverでそれを証明する方法を覚える、と
前にも書きましたけど、この本は訳者の名前は出てこなくて監訳者の中野圭介さんの
名前だけが表紙に書いてあります
ちょっとめずらしいパターンかなという気がしますがその監訳者さんの序文によると
この本はプログラムの正しさを証明するための入門書、といいます
プログラムの正しさってなんでしょうか
仕様どおりに動くってことですかね
現実世界ではそもそも仕様がキッチリ決まっていることがなかったりしますが
定理を表す主張に対して等価な式変形を繰り返して定理を証明するそうです
定理の証明はJ-Bobというツールがサポートしてくれるらしい
J-BobをマスターしたらACL2に進むのもよいし
Coq、Agda、Isabelle/HOLといった証明支援系に挑戦してみるのもよいとのこと
Coqだけ聞いたことありますが他はちょっと
Coqも名前しか聞いたことないですけど
序文はJ Strother Mooreさん
定理証明器を研究してきた人でACL2の作成者のひとりで
その研究でACMの賞を取ってるくらいなので分野の大御所的な人でしょうか
上に出てきたJ-BobのJはこの人の名前からとったものだそうです
JにピリオドがついてないってことはほんとにJさん？
関数やプログラムの振る舞いを記述するための数理論理学とはどのようなものだろうか？「定理」とは何であろうか？定理をどうやって「証明」するのだろうか？「自動定理証明器」とは何か？
たまたまですがゲーデルとつながってる感じ
あと言語について軽い説明があります
atomとかdefunとかCommon Lispの流れみたいですね
ACL2のページを見てみたら
"ACL2" denotes "A Computational Logic for Applicative Common Lisp".
って書いてありました
Applicativeってついてますがでも何かCommon Lispなんでしょう
sizeは値を組み立てるのに必要なconsの数
単純にリストの長さってことじゃないんだ
定理はdethmで定義します
defunと違って定理を再帰的に定義することはできません
ところで
atomは、空でないリストに対しては'tを、そうでなければ'nilを返します。
これ反対じゃないかなあ
あとがきはMatthias Felleisenさん
ちょっとメイキングみたいな話が出てます
なるほど
ゲーデルの不完全性定理の証明のアレをRacketで書いてみる (58)
大詰め
定義43 xはaとbの"直接の帰結"である
(define (IsConseq [x : GForm]
[a : GForm]
[b : GForm]) : Boolean
(or (= a (Implies b x))
(∃ v <= x (and (IsVar (gsymbol+ v))
(= x (ForAll (gsymbol+ v) a))))))定義44 xは"形式的証明"である
(define (IsAxiomAt [x : GSeqSeq]
[n : Natural]) : Boolean
(IsAxiom (gform+ (elm x n))))
(define (ConseqAt [x : GProof]
[n : Natural]) : Boolean
(∃ p q < n
(and (> p 0)
(> q 0)
(IsConseq (gform+ (elm x n))
(gform+ (elm x p))
(gform+ (elm x q))))))
(define (IsProof [x : GProof])
(and (> (len x) 0)
(∀ n <= (len x)
(⇒ (> n 0)
(or (IsAxiomAt x n)
(ConseqAt x n))))))定義45 pはxの"形式的証明"である
(define (Proves [p : GProof]
[x : GForm])
(and (IsProof p)
(IsEndedWith p x)))ラスボスを倒すには特別な装備が必要
(上限なしの∀と∃)
(define-syntax (define-equipment stx)
(syntax-parse stx
((_ name term notfound found)
#:with fname (format-id stx "_~a" #'name)
#'(begin
(define (fname [cmp : (-> Natural Natural Boolean)]
[max : Natural]
[f : (-> Natural Boolean)]) : Boolean
(let loop ((x : Natural 0))
(cond ((not (cmp x max)) (notfound x))
((term (f x)) (found x))
(else (loop (+ x 1))))))
(define-syntax (name stx)
(syntax-parse stx
[(_ v:id cmp:id max:expr body:expr)
#'(fname cmp max (λ (v) body))]
[(_ v:id ...+ vn:id cmp max:expr body:expr)
#'(name v (... ...) cmp max (fname cmp max (λ (vn) body)))]
[(_ v:id body:expr)
#'(fname (const #t) 0 (λ (v) body))]
[(_ v:id ...+ vn:id body:expr)
#'(name v (... ...)
(const #t)
0
(fname (const #t) 0 (λ (vn) body)))]))))))かなり適当なパターンマッチでギリギリたまたま動いてるって感じ
定義46 xには、"形式的証明"が存在する
(define (IsProvable [x : GForm])
(∃ p (Proves (gproof+ p) x)))終わり！
（終わったからといって特に何もなし）
（定理証明手習いにとりかかれる）
なにか語りかけ口調になる
自分の思いつきを書き留めているだけで誰かのために書いてるわけではないんですけどね
でもブログに書くんだと思うと言葉遣いが変わります
不思議ですね
ていうかアウトプットの練習と思って書きはじめたのに自分の思いつきを書き留めてるだけ、ってのは目的に合ってないですね
誰かのために書く文章であるべきなんだろうな
でもそこにたどり着くまでのステップ1ということで（誰に言い訳してるのか
