多値で簡単パーサーコンビネーター（Shibuya.lisp TT#6）

Shibuya.lispのテクニカルトーク#6に参加しました。仕事半分以下、趣味半分以上です。

まず仕事の部分について、直売で書籍を購入いただいた皆さん、本当にありがとうございました。Lispそのものの本よりも『鉄道ダイヤの回復技術』や『日本のコンピュータ史』のような本が想定以上に売れてしまうあたり、さすがShibuya.lispだと思った。

ただ、前回も直販をしたのだけど、そのときの反省として、販売員をやるとどうも外野っぽくなってしまう。自分としては、普段からSchemeを使っているので、いちLispユーザーとしてもShibuya.lispに参加したい。それで今回はLTに応募した。LTのトピックはなんでもよかったのだけど、具体的にコードが見えるもののほうが面白かろうということで、個人プロジェクトの中で利用したアイデアを切り出して、多値を使って自分の目的にあったパーサーコンビネーターを簡単に作れるよ、という発表をさせてもらった。誤解を招くようにしたわけだけど、本の宣伝広告のほうはネタです。

多値で簡単パーサーコンビネーター

View more presentations from k16shikano.

Gaucheで実行できるコードもgithubにあげておきます。実質的には100行くらいの短いコードです。

k16shikano/tinypeg

肝心の発表では、思わずTeXについて語ってしまったおかげで時間がなくなってしまったけど、本当はスライド26枚目でParsecが出てくるあたりから面白くなるはずだった！ でも@khibinoさんに喜んでもらえたので本望です。なおかつフィードバックもたくさんもらえた。ありがとうございます。これについてはそのうちまとめてもうちょっと役に立ちそうな記事を書くつもり。

ちなみに、実際にこのアイデアを実装していたのは去年のいまごろの話。この原理を利用したパーサーコンビネーターを作ったおかげで、本来の開発対象であるTeX modokiがずいぶん前進した。

k16shikano/tex-modoki

TeX modokiはGaucheによるTeXの簡易実装です。TeXのソースをHTML/CSS2.1で出力します。

Lisperのためのゲーデルの不完全性定理の反証不可能性について考えてみた

Lisperのためのゲーデルの不完全性定理では、(g g)が証明も反証もできないことが示されていない。証明できないほうはいいとして、反証できないことがすぐに理解できなかった。unprovable-pとvalid-proof-pだけで反証不能なことが証明できるの？

ちょっと考えてみた。
(g g)の否定が証明可能だとすると、

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

の否定が証明可能ということなので、

(valid-proof-p
 (eval
  ((lambda
     (x)
     `(unprovable-p
       (eval
        (,x ',x))))
   '(lambda
      (x)
      `(unprovable-p
        (eval
         (,x ',x)))))))

ところがこれは、gの主張である

(unprovable-p (eval (,x ',x))))

と矛盾する。したがって(g g)は反証不可能。

こんな感じだろうか？

で、(g g)の形式的な決定不能性はいいとして、これをもってゲーデルの不完全性定理が証明できた、とは依然としていえないんじゃないだろうか。なぜなら、S式からなる形式的な系について、unprovable-pとvalid-proof-pがあるということ以上に何も情報がないから。それだけの情報では、この系が不完全性定理の前提条件を満たすかどうか確かめようがない。と思う。S式で自然数が作れるのは確かだけど、すべてのS式からなる系では当然無矛盾性を満たさないし。1階の述語論理に対応するS式のセットを再帰的に用意して、そこでunprovable-pとvalid-proof-pを（Lispの意味論を使わず形式的に）定義すればいいのだけど、簡単ではなさそう。（追記：Lispの実装にこだわらなければ、比較的わかりやすく形式化できるようです→howm wiki - 不完全性定理.改。Lispでゲーデルの不完全性定理が証明できる！のようなインパクトはないですが、「Lispを含む再帰的可算な公理系は不完全」の証明になってそう）

だからたぶんチャイティンの元記事は、不完全性定理のフレーバーをLispならS式で表せるぜ、という話であって、それは、不完全性定理のフレーバーを自然言語ならうそつきのパラドクスで表せるぜ、という話と大きく違わないのではないかと思った。