Hatena::ブログ(Diary)

あどけない話

2010-11-12

Lisper のためのゲーデルの不完全性定理

注:この記事の内容には、問題があるようなので、勉強して書き直す予定です。

ゲーデルの不完全性定理を読んでも理解できない Lisper のために、Lisp のコードで不完全性定理を説明してみる。昨日と同様に Emacs Lisp を使うが、Common LispScheme でもコードはあまり変らない。

ゲーデル不完全性定理

ゲーデル不完全性定理とは、おおざっぱに言うと「(自然数論を含む帰納的に記述できる)公理系が無矛盾であれば、証明も反証もできない命題が存在する」と言うことだ。これは嘘つきのパラドックスと似ていると言われている。

嘘つきのパラドックスとは、「この文は嘘である」という文は、正しいとも間違っていると言えないということ。この文が正しいと仮定すると、この文は嘘となり、仮定と一致しない。一方、この文が間違っていると仮定すると、この文は嘘ではなくなり、文の内容と一致しない。矛盾の根源は、この文がこの文自体について述べている自己言及にある。

ゲーデルは少し内容を変えて、「この文は証明できない」という命題を考えた。可能性としては二つある。証明可能な定理であるか、証明不可能な定理でないものであるか。この文が証明可能であると仮定すると、この文は証明できないことになり、仮定と一致しない。つまり、公理系が矛盾していることになる。そこでこの可能性を捨てて、この文は証明不可能であると仮定する。すると、仮定と文の内容が一致するので、この公理系には証明できない命題が存在することになる。つまり、この公理系は不完全だ。

後述の「知の限界」の著者チャイティンは以下のように述べている。

ゲーデルは「xがyを証明する」ということを算術的に表現するのです。これは非常に巧妙な方法ですが、数学的叙述が正の整数とも考えられるという基本的な考えは、今日では、さほど驚くことには思えません。結局、すべての記号列が、現代のコンピュータでは数値で表されているからです。... ゲーデル数は、1930年代よりも今の方がずっと理解しやすいのです。

Lisp による不完全性定理の証明

不完全性定理Lisp で証明するには、「このS式は証明できない」と主張するS式が構成できればよい。

まず最初にS式が妥当な証明か判断する valid-proof-p という関数を考える。この関数は、引数が妥当な証明なら証明された定理を返し、そうでないなら nil を返す。この関数は実際には実装しないけれど、S式を走査して妥当かを判定するアルゴリズムはあるとする。

つぎに、unprovable-p という関数を考える。この関数は、与えられたS式が証明できないことを主張する。実装としては、与えられたS式 a が、すべてのS式 b に対して (valid-proof-p b) と等しくないこと言えばよい。

次に以下のような関数 g を考える。

(set 'g '(lambda (x) `(unprovable-p (eval (,x ',x)))))
(fset 'g g)

関数 g は、`(,x ',x) を eval しているので、`(,x ',x) という名前から値を取り出し、その値が証明不可能だと主張していることになる。

では、g に g を与えた場合、何が証明不可能だと主張していることになるだろう?

(pp (g g))(unprovable-p
 (eval
  ((lambda
     (x)
     `(unprovable-p
       (eval
	(,x ',x))))
   '(lambda
      (x)
      `(unprovable-p
	(eval
	 (,x ',x)))))))

eval より後ゴチャゴチャしている部分が名前である。この名前は値はなんだろう?それを知るには、(g g) から名前を取り出して、eval すればよい。

(pp (eval (cadr (cadr (g g)))))(unprovable-p
 (eval
  ((lambda
     (x)
     `(unprovable-p
       (eval
	(,x ',x))))
   '(lambda
      (x)
      `(unprovable-p
	(eval
	 (,x ',x)))))))

さっきと同じものが出てきた。Lisp に同じだと確認させてみよう。

(equal (g g) (eval (cadr (cadr (g g)))))t

結局どういうことだろう?

(g g) は、ある名前が指すS式が証明不可能だと主張しているS式である。ある名前が指すものを取り出してみると (g g) であった。すなわち (g g)は、「自分自身が証明不可能だ」と主張するS式である。

くどいようだが、この意味を考えてみる。(g g) が証明可能なら、証明不可能を肯定したことになるので、公理系が矛盾していることになる。(g g) が証明不可能なら、(g g) の主張と一致する。証明不可能な問題があることになり、公理系は不完全である。

なにか騙されたような気も拭いきれないが、これがLispによるゲーデル不完全性定理の証明である。

参考文献

昨日の記事と今日の記事の元ネタは、「知の限界」という本である。この本は、内容は素晴らしいが、言葉が足りないため読破するのは難しい。私は、不完全性定理のLisp, Mathematicaによる記述を参考にこの本を読んだが、2年ぐらい意味不明だった。最近ようやく分かった気になったので、忘れないように記事にまとめてみた次第である。

知の限界

知の限界

2010-11-11

Lisper のためのチューリングマシンの停止性問題

停止性問題を読んでも、意味が分からなかった Lisper のために、Lisp のコードで停止性を解説してみる。使用する Lisp としては、SchemeCommon LispEmacs Lisp を検討したが、Emacs Lisp が一番よいと分かったので、Emacs Lisp を使う。

名前を使った概略

halt-p というプログラムは、入力としてプログラム p とデータ d を取る。Lisp なので、p も d も S 式である。halt-p は、p と d を検査し、p に d を与えたときに、停止するか否かを有限時間で判断する。停止するなら t、停止しないなら nil を返す。

machine というプログラムは、入力 x に対して以下のような動作をする。

  • (halt-p x x) が t なら、(machine x) を呼び出すことで同じ作業を繰り返す
    • つまり、x に x 自身を与えたときに、停止すると判断した場合
  • (halt-p x x) が nil なら、nil を返して停止する
    • つまり、x に x 自身を与えたときに、停止しないと判断した場合

では、machine に machine を与えたときはどうなるだろう?

halt-p は、入力に関わらず、必ず t を返す場合:

(defun halt-p (p d) t)
(defun machine (x)
  (if (halt-p x x) (machine x) nil))
(machine 'machine) → 停止しない

machine というプログラムに、machine を与えたときは停止すると、halt-p が判断したにも関わらず、(machine 'machine) は停止しない。

halt-p は、入力に関わらず、必ず nil を返す場合:

(defun halt-p (p d) nil)
(defun machine (x)
  (if (halt-p x x) (machine x) nil))
(machine 'machine)nil を返して停止する

machine というプログラムに、machine を与えたときは停止しないと、halt-p が判断したにも関わらず、(machine 'machine) は停止する。

という訳で、矛盾が導けた。「それだけ?」と思うかもしれないが、チューリングマシンの停止性問題とは、単にこんなものである。つまり、プログラムを走らせる前に、そのプログラム無限ループに陥るか否かをあらかじめ知る一般的な方法はないということ。「当たり前だ」と思うかもしれないが、あなたが「当たり前だ」としか感じれない素地を作ったのがすごいのだ。

この証明は分かりやすいが、たくさんつっこみどころがあるので、以下ではそれを解決して行く。

ちゃんと自分自身を与える

問題の一つ目は、machine に 'machine というシンボルを渡しているところ。ちゃんとプログラム自体を渡したい。Emacs Lisp のシンボルには、プログラムとデータが別々に束縛されているので、以下のように両方に同じ S 式を束縛することで、この問題を解決できる。

停止するはずなのに停止しない場合:

(defun halt-p (p d) t)
(set 'machine
     (lambda (x) (if (halt-p x x) (machine x) nil)))
(fset 'machine machine)
(machine machine) → 停止しない

停止しないはずなのに停止する場合:

(defun halt-p (p d) nil)
(set 'machine
     (lambda (x) (if (halt-p x x) (machine x) nil)))
(fset 'machine machine)
(machine machine)nil を返して停止する

halt-pをインライン化する

次に問題なのが、名前を使っていることである。名前を定義したりする機能は、公理の一部と考えていいのだろうか? よくわからないので、名前を消すことにする。

まず、halt-p をいう名前を消そう。そのためには、halt-p をインライン化すればよい。

停止するはずなのに停止しない場合:

(set 'machine
     (lambda (x)
       (if ((lambda (p d) t) x x) (machine x) nil)))
(fset 'machine machine)
(machine machine)

停止しないはずなのに停止する場合:

(set 'machine
     (lambda (x)
       (if ((lambda (p d) nil) x x) (machine x) nil)))
(fset 'machine machine)
(machine machine)

自己言及

次は、machine という名前を消すべきである。しかし、machine という名前は、再帰するために使われているので、消すのは厄介だ。名前なしで再帰するための技として、Yコンビネータが知られている。その本質は、自己言及である。

詳細は述べないが、以下のように自分自身に自分自身を適用すると、全体として同じものが返るS式が知られている。

((lambda (x) `(,x ',x)) '(lambda (x) `(,x ',x)))((lambda (x) `(,x ',x)) '(lambda (x) `(,x ',x)))

この技を使って、名前なしで再帰する。

名無しでループ

以下では、自己言及した値を y としている。これを eval すれば、再帰できる。また、プログラムにデータを適用した形になっているので、halt-p に相当するラムダ式引数が一つになっている。(halt-p は、引数を使わないのでどうでもいいとも言える。)

停止するはずなのに停止しない場合:

(set 'machine
     (lambda (x)
       (let ((y `(,x ',x)))
	 (if ((lambda (p) t) y) (eval y) nil))))
(fset 'machine machine)
(machine machine) → 停止しない

停止しないはずなのに停止する場合:

(set 'machine
     (lambda (x)
       (let ((y `(,x ',x)))
	 (if ((lambda (p) nil) y) (eval y) nil))))
(fset 'machine machine)
(machine machine)
(machine machine)nil を返して停止する

evalだけの世界

machine という名前も不要なので、使わずにやってみよう。

停止するはずなのに停止しない場合:

((lambda (x)
   (let ((y `(,x ',x)))
     (if ((lambda (p) t) y) (eval y) nil)))
 (lambda (x)
   (let ((y `(,x ',x)))
     (if ((lambda (p) t) y) (eval y) nil))))
→ 停止しない

停止しないはずなのに停止する場合:

((lambda (x)
   (let ((y `(,x ',x)))
     (if ((lambda (p) nil) y) (eval y) nil)))
 (lambda (x)
   (let ((y `(,x ',x)))
     (if ((lambda (p) nil) y) (eval y) nil))))nil を返して停止する

これで、S式とevalだけで、チューリングマシンの停止性問題を説明できた。

(let で y という名前を付けているじゃんと突っ込みたい人は、let が lambda への糖衣構文だということを勉強しましょう。)

2010-10-21

祝 「Scheme 手習い」復刻

めでたい! 「Scheme 手習い」が復刻しました。正確に言うと、復刻ではなく、新しい版に基づいた新しい訳です。

Scheme手習い

Scheme手習い

以前、マグロウヒル出版から出版されていた「Scheme手習い―直感で学ぶLisp」は、"The Little Lisper" の訳です。内容が、Common Lisp でもなく、Scheme でもない Lisp の方言によって書かれているのに、邦題に Scheme が入っていたのは、この本の唯一の欠点だと僕は感じていました。

今回は、"The Little Schemer" の訳です。原書も訳書も名実共に Scheme に基づいています。現在では、Lisp と言えば、Common LispScheme のことを指すようになりました。Scheme の実装も簡単に手に入ります。また、Lisp の価値も見直されています。よい時代に、よい翻訳書が現れました!

学ぶのは再帰

この本で学ぶのは「再帰プログラミング」です。

世界的に有名な Joel Spolsky 氏のエッセイの一つに「Java スクールの危険」があります。一部を引用します。

私のささやかな経験から言わせてもらうと、伝統的に大学のコンピュータサイエンスカリキュラムで教えられているもので、多くの人がうまく理解できないものが2つあった: ポインタ再帰だ。

優秀なプログラマーとそうでないプログラマーを分ける指標の一つが、再帰を理解しているか否かです。優秀なプログラマーを目指すなら、再帰的な考え方を学ぶ必要があります。本書は、再帰を学ぶための最高の入門書です。

解説

Scheme 手習いは、習うより慣れろという感じで書かれているので、パズルを解くような楽しさがあるのですが、一方で、その背景や目的を理解しないまま読んでしまう恐れがあります。そこで、各章を少し解説しておきます。何をやっているのか分からなければ、以下を読んでみて下さい。

第1章

Scheme の基本的な関数 car、cdr、cons、null?、atom?、および eq? を学びます。Lisp を知らない人は、新鮮な感じで読めるでしょう。注意していただきたいのは、Lisp を中途半端に知っている人です。第1章を立ち読みして「なんだ知っていることばかりで、つまらない」と思って買うのを止めないで下さい。再帰が出てくるのは2章以降です。

分かっている人から見れば、これらの基本関数と(さらに cond と quote と)関数を定義する環境があれば、ピュアな Lisp が作れるという厳選された関数ばかりです。10章で、Schemeインタープリターを作る際は、第1章に立ち返ってみて下さい。これらが珠玉のプリミティブだということが分かるでしょう。

第2章

いよいよ再帰を学びます。再帰は、基底部(null?)と再帰部(自分自身を呼び出す)から構成されることを理解しましょう。

第3章

入力のリストから出力として新しいリストを生成します。入力のリストは破壊されません。これが関数プログラミングの流儀です。リストを生成するには cons を使います。cons は、オブジェクト指向言語でいう new、C 言語でいう malloc() にあたります。大切なので、も一度言います。新しい値が作り出されるので、古い値は破壊されないのです。(不要になった古い値は、ゴミとして自動的に回収されます。)

第4章

自然数演算再帰で扱います。自然数再帰で扱えるのは、自然数帰納的(再帰的)に定義されているからです。

第5章

リストのリストに対して、深く再帰します。見方を変えれば、これは木構造に対する再帰です。リストは、木構造も表現できるのです。

第6章

影法師とは、補助関数のことです。補助関数というインターフェイスを定義して、データを抽象化します。(プログラムは理解しやすくなりますが、Scheme にはアクセス制御がないので、安全にはなりません。)

第7章

リストで集合を表現して、集合演算を実装します。

第8章

ついに、引数として関数が指定されるようになります。関数型言語では、関数が第一級の値であり、その素晴らしさが実感できるでしょう。継続も登場します。

第9章

とても難しい内容です。前半は、未解決問題である Collatz の関数、原始帰納的関数でない帰納的関数の代表例である Ackermann 関数チューリングマシンの停止性問題がさりげなく登場します。

後半では、Yコンビネータを作ります。Yコンビネータとは、関数名を使わずに再帰を可能にする補助関数のことです。Yコンビネータ自体も、名前を使って再帰していないことに注意して下さい。(この Y コンビネータBML であることが、いつか分かるかもしれません。)

第10章

Schemeインタープリターを Scheme で実装します。このインタープリターはかなり優秀で、第9章で作った Y コンビネータを動かすこともできます。

あわせて読みたい

原書 ”The Little Schemer” の解説記事も書いていますので、あわせてどうぞ。

2008-11-17

Emacs補完候補の選択を便利に

今話題のauto-complete.elを使ってみましたが、以下の点が使いづらく、使うのを止めてしまいました。

  • 候補が最大10個しか出ない
    • 10個以上の候補がある場合、次に打つべき文字が分らない
  • バッファの最下部でメニューが表示されると、勝手にスクロールされる

個人的には、Emacsが提供する標準の Completion List モードを拡張する方がいいなぁと思いました。Completion List モードが使いにくいのは、以下の点です。

  • C-f/C-b/C-n/C-pはカーソルの移動であって、候補間の移動ではない
  • RETで選ぶと、候補のリストを表示する前の状態に戻れない
    • Emacs 22では、カーソルが他のバッファに行ってしまう
    • Emacs 23では、元のバッファにカーソルが戻るが、余計なバッファが表示されたまま

という訳で、これらを解決するコードを書いてみました。最後に付けているコードを

".emacs" に入れるだけです。

こういう使い方を想定しています。

  • TAB や M-TAB で補完の候補を表示
  • C-xo で補完の候補のバッファへ移動
  • C-f/C-b/C-n/C-p あるいは C-s/C-r で候補を選択
  • RET で候補を選ぶと、元々の状態に戻り、選んだ候補が挿入される
(define-key completion-list-mode-map "\C-n" 'next-completion)
(define-key completion-list-mode-map "\C-f" 'next-completion)
(define-key completion-list-mode-map "\C-p" 'previous-completion)
(define-key completion-list-mode-map "\C-b" 'previous-completion)
(define-key completion-list-mode-map "\C-m" 'my-choose-completion)

(defun my-choose-completion ()
  "Choose the completion that point is in or next to."
  (interactive)
  (let (beg end completion (buffer completion-reference-buffer)
	(base-size completion-base-size))
    (if (and (not (eobp)) (get-text-property (point) 'mouse-face))
	(setq end (point) beg (1+ (point))))
    (if (and (not (bobp)) (get-text-property (1- (point)) 'mouse-face))
	(setq end (1- (point)) beg (point)))
    (if (null beg)
	(error "No completion here"))
    (setq beg (previous-single-property-change beg 'mouse-face))
    (setq end (or (next-single-property-change end 'mouse-face) (point-max)))
    (setq completion (buffer-substring-no-properties beg end))
    (delete-completion-window)
    (choose-completion-string completion buffer base-size)))

候補数の問題もないし、検索もできます。

P.S.

Mew では、フォルダ名を入力するときに、C-s/C-r/TAB を組み合わせて使うと、より快適に候補が選択できます。大昔に実装したけど、使っている人はいるでしょうか?