先日の記事に書いたように KOKIA にハマりまして、 とりあえず片っ端から聴いてみることにしました。まずは 1st アルバムの 『songbird』 から …
…４曲目の "白い雪" ヤバい。超ヤバい。なんだこれ。ツボすぎる。 ベスト盤を聴いたとき感じた揺らぎなく落ち着いた歌唱力的な曲を期待して聴きはじめたら、 予想外の声質の歌が飛び込んできてびっくりしました。もちろん抜群に巧いのに かわりはないんですが、ずっと儚げな、ガラス細工みたいなイメージの、ああ、その、 つまり白い雪みたいな雰囲気の綺麗な声で。その声と奇跡的にマッチしたメロディ。 すごいなあ。９曲目の "ありがとう…" もベスト盤でのリテイクと比べて同じ印象で、 Amazonのreview で TenderBerry さんという方が近いことを書いておられました。 しかし書いてて自分の語彙のなさが悲しくなってきたよ。 『trip trip』 も買ってあるのであとで聴こうと思います。
たつをさんによる 「次」と「前」の意味と並び順 という調査記事。面白い。
しかしこれ、なんでどのサービスも「次」「前」なんていうわっかりにくい言葉を 選んでいるんでしょう。例えば「新しい記事へ」「古い記事へ」 って表示すれば紛れがなくてよいと思うんですが…。
それでも「次」「前」よりはマシではないかなあ。 ちなみに、この日記のナビゲーションは上のようなことをしばし考えた結果、 「一つ過去のページ」「一つ未来のページ」に落ち着いています。これはこれで 日本語として斬新すぎて自分でもちょっと笑えるのが最大の問題。
『pearl ～The Best Collection～』 を聴きまくっています。 このアルバムだと15曲目の「ありがとう」をBGM…というか効果音に使ってる動画を見かけて、 いい歌だなーと思って購入。調べてみたら有名なflashにも使われてたらしい。知らんかった。
ベスト盤だからというのはあるにしても、自分にとってハズレが一曲もないアルバムというのは とても珍しい。ほとんどの場合はよくても一、二曲は肌に合わないのがあるもんなんですが、 これは全曲好きです。知るきっかけとなった "ありがとう…" も勿論いいし、 "Desperado" も…最初聴いたときはオリジナルと比べて 薄い感じ？とか思ったけどこれもいいかと１分で思い直したり… いいし、 リズミカルな "So much love with you" も素晴らしい。
（ブラウザなりテキストエディタなりの）文字コードの自動判別を学習型の ベイジアンフィルタでやったら便利なのでは、と、さっきふと思ったりしました。
よくある実装は、「ある文字コードだと仮定したときにちゃんと読めるバイト列かどうか判定」 と「各文字コードごとのバイト値出現頻度表を用意しといて比較」と、あと適当に幾つか 場当たり的なチェックを組み合わせる感じだと思います。 auto_ef や Mozilla はそんな雰囲気。IEのはどうなんだろう。ちなみに GreenPad のはもっとずっと手抜き。 実はもっと洗練された判別アルゴリズムがあるのかも。まあいいや。
そういうのと比べると、「文字コードに関する静的な知識を持っていなくても、適当に その文字コードの文書をかき集めてきて学習させれば判別エンジンが作れる、ような気がする」 （"読み書きはもっとたくさんの対応しているけど、自動判定は ShiftJIS/EUC-JP/ISO-2022-JP/UTF-8 のみ対応です、他を含めると精度良い判別ができないので" みたいなことを言わなくて済む、ような気がする。）「いざ判定をミスったときにも、 ユーザーが指示して学習させれば次開くときはその文書（およびそれと似た内容かつ同じ 文字コードの文書）については判定を間違わないようにする、のが簡単そう」 （自動判別ミスをバグ報告されたりしたときに判定アルゴリズムを手動で改良してみたり、 無理ですごめんなさいと言ったりしなくていい。）（別にミスったときでなくても、 ユーザーの扱う文書の傾向に合わせて学習できたりするかも？）といった辺りが便利かな、と。 精度がどのくらい出るものかはよくわかりませんが…。
書いてて激しく既出な気がしてきたので検索してみると、 mikioさんの開発メモが引っかかりました。言語の自動判別まで含めてのお話ですが、 近いものは色々ありそう…。文字コードの判別だけに特化したらもっと簡単に精度あがったり しないかな。
そういえば先週のサナギさんでブラウワーがネタになっていて笑。
ヲタ漫画経験値 やってみました。×127 △42 ○23 ◎8。うへ、全然知らない…。 ちなみに◎は、山名沢湖、鬼頭莫宏、吉崎観音、あずまきよひこ、鳥山明、冨樫義博、 久米田康治、小畑健。なんというか、エニックス系の人が数人しかリストになくて これはきついというか、自分の買う漫画はとてもそっち方面に偏りすぎなことを改めて認識。
結城さんのコメント。
ところで「ゲーデルの不完全性定理」とか「チューリングマシンの停止問題」なども、
プログラミング的に「証明」できたりするのでしょうか。
できたりします。…たぶん。
そういえば、やったことも見たこともなかったので、 ちょっと調べてみました。まずはAgdaで停止問題！という "Formalizing the Halting Problem in a Constructive Type Theory" （ソースコード）から。 Agdaというのはとてもいい加減に言うと、Haskellに証明に向いたハイパワーな型システムを 振りかけたような雰囲気の関数型言語です。以下が、停止問題の証明…つまり、 「停止性は決定可能ではない」という命題=型を持つプログラム=証明 らしいです。関数型言語としてみると、abstract_haltp という別の関数に構造体(?)を 何個か渡して呼び出しているコードです。証明としてみると、何か別の抽象化した補題 abstract_haltp を、具体的に停止問題の話に応用して証明しているところだと思います。
pHaltProb :: Not (decidable terminates)
= abstract_haltp terminates
(struct {
fst = const True;
snd = True;})
(struct {
fst = loop;
snd = True;})
(struct {
fst = True;
snd = pConst True True;})
(pLoop True)
(\(c1::computation) ->
\(c2::computation) ->
\(pEq::kleeneEq c1 c2) ->
\(pc1::terminates c1) ->
struct {
fst = (pEq (Inl@_ pc1)).fst;
snd = (pEq (Inl@_ pc1)).snd.snd;})
次にCoqで不完全性定理！という "Essential Incompleteness of Arithmetic Verified by Coq" （リンク先のA constructive proof of ... というリンクがソースコード）。 Coqというのはとてもいい加減に言うと、Camlに証明に向いたハイパワーな型システムを 振りかけたような雰囲気の関数型言語です。不完全性定理の証明を見てみます。 「体系Tがω無矛盾なら、Tで証明も反証もできない、自由変数を持たない論理式fが存在する」 という型をもつ関数 Godel'sIncompleteness1st のプログラム…
Theorem Godel'sIncompleteness1st : wConsistent T -> exists f : Formula, ~ SysPrf T f /\ ~ SysPrf T (notH f) /\ (forall v : nat, ~ In v (freeVarFormula LNN f)). Proof. intros. assert (con : (forall f:Formula, SysPrf T f) -> False). intros. induction (wCon2Con T). apply H1. apply H0. ...(略)... Qed.
こちらはあまりプログラムっぽくなくて、どちらかというといわゆる証明に 近そうに見えます。実はCoqもAgdaも、ただプログラミング言語=証明言語がドカンと あるだけではなくて、プログラムとして証明を書くことを支援してくれる開発環境で もあります。実際には全証明を手でプログラムとして書き下すことは少なくて、 補完機能や対話型の証明/プログラム書き支援シェルを使って開発していきます。 （cf.Agdaでの証明風景）上にあげたのはCoqの対話型シェルに入力されたコマンド列で、 このスクリプトを実行してやれば最終的になにやらプログラムっぽい物がでてくるはず。 試してませんが。
「プログラム⇔証明」であるならば、AgdaやCoqのような証明に特化した言語を 使わなくても、もう少し普通の関数型言語…例えばHaskellやOCamlで "証明" できるべきでは？という疑問がわきます。
実際、簡単な"証明"なら、HaskellやOCamlの処理系があれば十分です。 例えば下であげた例「(a かつ (aならばb)) ならば b」を証明したければ、 そういう型を持つプログラムを書いて、コンパイラやインタプリタに通して、 型チェックが通れば、証明完了！終わり！です。基本的には。
ところが不完全性定理や停止問題になると、…これはなかなか難しい。
不完全性定理を述べるためには、「こういう論理式が存在する」みたいな命題を 表現しないといけません。つまり、"論理式"のような命題ではないデータ構造に ついて、「このデータはこれこれこういう性質をもってます」ていうことが 書ける論理システムを持ってこないと、そもそも不完全性定理について 語ることすらできない、と。"ならば" や "かつ" だけだと、どこまでいっても 扱うものは命題だけで、どうにも力が足りません。 そして、HaskellやOCamlの基本的な型システムは、この "ならば" や "かつ" しかないような論理システムに対応しています。
論理学の世界では、「伝統的な論理学じゃ、そういう、命題以外のデータを扱う論理に ついて何も考えられてないじゃん！」 と気づいた フレーゲ という人が大革命を起こして、「述語論理」という新しい論理を 作りました。それが後のラッセルやゲーデルの成果に繋がっています。そしてこの 「述語論理」という論理に一対一対応するのが、AgdaやCoqの備えている 「Dependent Type (依存型)」という型システムだったりします。
余談の余談ですが、この Dependent Type というのは、単に命題記述のためだけの型システムと いうわけでもなくて、普通にプログラムを組むときにも便利なので、そっち方面でも 研究開発が進んでいる型システムでもあります。便利さの一例として、例えば C++ の テンプレートは型/命題でないデータである、"整数"を型の中に含むことができる、 ある意味整数限定なんちゃって Dependent Type で（…とかいうと各方面から 怒られそうですが…）
template<int N>
class IntArray { ... };
template<int A, int B>
IntArray<A+B> concat( IntArray<A> x, IntArray<B> y ) { ... }
IntArray<3> x = {{1,2,3}};
IntArray<4> y = {{4,3,2,1}};
IntArray<7> z = concat(x,y); // OK
IntArray<8> w = concat(x,y); // コンパイルエラー!
コンパイル時に配列の長さチェックしてくれる配列演算ライブラリが書けます。 行列計算ライブラリに適用すれば、(2×3) の行列に (3×4) の行列をかけ算したかったのに、 うっかり間違えて逆に (3×4) に (2×3) をかけちゃってました～なんていうバグは コンパイル時に全部検出できちゃいます。
これが整数以外のいろんなデータも扱えて、ある程度型推論してくれちゃったりすると、 さらに用途が広がるわけで。これまたいろいろと面白い分野であります。
そういえば昨日 「三角関数と複素数を知ってるのに極座標表示を知らないようなもったいなさ」 という表現を使ったら、教師をしている親から「高校数学の新課程では極座標表示を 扱わないって知ってた？」って突っ込みをもらいました。課程が変わるたびに 出たり入ったりしている項目らしいです。な、なんだってー！ そんなまるで論理とラムダ計算を教わってCurry-Howard同型対応を教わらないような！
他人のひとに言及して日記を書く日々が続いております。今日は、 さかいさん や 住井さん の素晴らしい記事を見てて、ふと、前々から思っていた愚痴を書いてみようと思い立ちました。
一言で言うと、 論理学 を教えてくれて、 λ計算 を教えてくれて、 Curry-Howard 対応 を教えてくれなかったうちの学科のカリキュラムはどうかと思うということ。 （もしかしたら今は触れてるのかもしれませんが…。） 大学生にもなって教えてもらうとか言うな自分で調べろむしろ気づけ、というのは 実に正論です。実際私は自分で勉強したわけですが、でも、元々この手の分野に 興味のない人はそこまでしないしする必要もないでしょう。にも関わらず、元々λ計算などには あまり興味はなかった -- けれどコンピュータ系の学科に来てる程度には近い -- 学生の一部を 振り向かせるには十分興味深い話題だし、一言述べるだけで論理とλ計算に対する理解が簡単に 一段深まる話題だと思うのです。なので、もったいないなあ、と。
例えて言い過ぎるならば、前二者を知っているのにCurry-Howardを知らないのは、 三角関数と複素数を知ってるのに 極座標表示 を 知らないようなもったいなさだと思うのですけど、どんなもんでしょうか。
そしてここから紹介を書き始めようとしたのですけども、「前二者を知っている」人でないと 全然面白くない気がしてきた…orz。まあいいや、適当に書き散らします。 書きたかったことはここまでで全部書いたので、あとは正直完全に戯れ言です。 数理論理やλ計算からはじめて一から解説してる文章としては、英語ですけど 『Lectures on the Curry-Howard Isomorphism』 があります。
さて、Curry-Howard 対応とは何か。
あとで詳しく説明しますが、一言で言うと「命題 ⇔ 型」 という一対一の対応関係、 そして 「証明 ⇔ プログラム」という一対一の対応関係のことをいいます。 命題や証明というのが論理学の概念ですね（"命題"というのはtrueかfalseなのかを議論できる ような対象のことで…例えば "1" は命題じゃないですが "1+1=2" は命題、みたいな。 "証明"はみなさんご存じのいわゆる証明です）。型やプログラムというのがλ計算などなど、 プログラミング言語の世界の用語です。この二つの一見あんまり関係なさそうな 世界に見事な対応関係がある、というのがCurry-Howard 対応です。
例をあげてみましょう。"命題"の例です。
(a かつ (aならばb)) ならば b
まあ、直感的に見て明らかにtrueな命題ですよね。 本当にtrueだということは"証明"してみないとわかりませんが、 それはひとまず置いておいて、この命題と一対一に対応する"型"はなんでしょう？
(a, a->b) -> b
論理式の"かつ"は、型でいう"pair"と対応すると考えます。aかつbは、(a,b)というpair型。 論理式の"ならば"は、関数の型と対応することにします。aならばbは、a型の値を受け取ってb型 の値を返す関数の型になります。"aかつb"って"a and b"であってつまり"aとb"なわけで、 pairだと思うのは悪くない気がしませんか。論理学の流儀によっては "aならばb" は "a→b" と表記しますから、もう、関数の型の表記そのものです。強引すぎ？
さてここで唐突ですが、(a, a->b) -> b という型になるような
プログラムを書いてみます。aやbは特に決めてませんでしたので、なんでもいいので
適当にどうぞ。私が考えたのは次のようなものです。OCamlで書くと上のコード、
Haskellで書くと下のコード。
# fun x -> (snd x) (fst x);;
- : 'a * ('a -> 'b) -> 'b = <fun>
Prelude> :t \x -> (snd x) (fst x) \x -> (snd x) (fst x) :: (a, a -> t) -> t
型変数の名前とか微妙に違いますけど、ここは気にしない方向で。 …いや、うそ、型推論とか多相型がまじると説明が面倒なので気にする方向で。 ちょっと明示的に型を書いてやることにします。
# type a;; # type b;; # fun (x : a*(a->b)) -> ((snd x) (fst x) : b);; - : a * (a -> b) -> b = <fun>
で、この"プログラム"が実は"証明"と対応している、((a かつ (aならばb)) ならば b) の証明を表しているのだ！というのがCurry-Howardの主張なのです。Let's Go。
fun (x: a*(a->b)) -> (* aかつ(aならばb) が成り立つと仮定する … x *)
((snd x) (* 仮定xが成り立つので、"かつ"の右手側の aならばb も成り立つ *)
(fst x) (* 仮定xが成り立つので、"かつ"の左手側の a も成り立つ *)
: b) (* aならばb と a が同時に成り立っているので、bも成り立つ *)
(* OK、要するに「aかつ(aならばb)が成り立つと仮定するとbも成り立つ」が証明できた。
これはつまり「(aかつ(aならばb))ならばb」ということだ。証明完了！ *)
ちと証明がまわりくどいですかね？ 実はここでは、数学的にきちんと"証明"というものを 定式化したシステムの一つである 自然演繹 に従って証明をしました。証明の各ステップごとに使ってよい規則の種類は、 誰でも"正しい"とすぐに認められる最小限のセットにとどめておいて、その組み合わせのみで 証明を構築することで、厳密に正しい"証明"を得ようというものです。 ここではリンク先の記事に列挙されている中で、∧(かつ) 除去を２発に →(ならば) 除去、 とどめに → 導入則を使いました。
狭い意味では、「直観主義命題論理という論理体系の命題 ⇔ 単純型付きλ計算の型」そして 「自然演繹という証明システムでの証明 ⇔ 単純型付きλ計算のプログラム」の間の対応関係の ことが Curry-Howard 対応 と呼ばれています。ここまでに示した例も、まさにその例です。
「命題⇔型」については、「かつ⇔pair」で「ならば⇔関数」であって、 ついでにもう一つ有名な論理演算子については「または⇔variant」という対応関係が 成り立ちます。住井さんの説明をお借りすると、
type ('a, 'b) sum = InLeft of 'a | InRight of 'b
という型を考えておいて、「aまたはb ⇔ (a,b) sum」ってところですね。
「証明⇔プログラム」については、 「"かつ"除去則(1) : aかつbが証明できてるならaが証明できてるとしてOK」に対しては fst というプリミティブが、「"かつ"除去則(2) : 略」については snd というプリミティブが 対応します。「"ならば"除去則 : aならばb と a が証明できてるなら b が証明できてる としてOK」は関数適用ですね。「"ならば"導入則 : aを仮定してbが証明できたらそれは aならばb の証明」は、λ抽象／関数定義です。「"または"導入則(1) : aが証明できてる ならaまたはbも証明できる」はInLeft、「"または"導入則(2) : 略」はInRight。 「"または"除去則 : aまたはbが証明できてて、aを仮定するとcが証明できてbを仮定 してもcが証明できるなら、cが証明できる」は複雑ですけど、match式というかcase式というか。
match s with InLeft x -> hoge | InRight y -> fuga
と、全部すみからすみまで対応しているすげー！というのが、 とりあえずCurry-Howard対応の概略です。ちなみに これだけでも知っていると、プログラマな学生が論理学の試験を受けるとき に結構役立ちます（実体験）。「この命題の自然演繹での証明を書け」って言われても 知らねーよって感じですが、「この型を持つ関数をなんでもいいから一個書け」なら 気合いでなんとかなりますので、あとはそこから同型対応で必死に引き戻し。
狭い意味でのCurry-Howard対応とは、「直観主義命題論理＆自然演繹 ⇔ 単純型付きλ計算」 の一対一関係のことでした。驚くべきは、この「命題⇔型」 「証明⇔プログラム」という対応関係は、論理システムや証明システム、そして 型システムやプログラミング言語をいろいろ取っ替え引っ替えしても当てはまるのです。 論理学の重要な概念や定理が、ことごとく（というと言い過ぎですが）プログラミング言語の 側の重要な概念や定理に綺麗に対応して、逆もまた然り…と。幾つかご紹介しましょう。
"かつ"はpairで、"ならば"は関数で、"または"はvariantでした。
でも、まだ一つ重要な論理演算子が抜けていますね。"ではない"、否定、"not"。 こいつに対応するプログラミング言語側の型の概念はなんでしょう？ pairと関数とvariantで、HaskellやMLの型システムの構成要素は全部出尽くしている 気がしますが…。
実は、"aではない" は "aを受け取る継続" という型に対応すると言われています。 「継続」といっても言語によって色々あるかもですが、継続に値を突っ込んだらその 継続先にジャンプしてしまってその場所には返ってこないような、Schemeの継続 みたいな多分一番普通なやつです。
(aならばb) ならば ((bではない)ならば(aではない))
に対応する型は、(a→b)型の関数をうけとると(bをとる継続→aをとる継続)型の関数を 返す関数型です。ややこしいかも…。この型のプログラムを作ってみると、例えばSchemeで 書いちゃうとこんなので
(lambda (f) (lambda (k) (lambda (x) (k (f x)))))
対応する証明もなんかそんな感じのものです。
否定 "not a" は、"a ならば 矛盾" の省略形だ、と考えることもよくあって、 その方が継続っぽく見えるかもしれません。"a ならば 矛盾" に対応する型は
a -> ⊥
a型の値を渡すと、返ってこない( ⊥ )ような関数の型を表しています。 こっちの方が個人的に読みやすいので、以降では「not a⇔a->⊥」で行きます。
否定に関する自然演繹の規則もいくつかありまして、大部分は問題ないのですが、 １個だけ、論理学の歴史的に、大議論を巻き起こしてきた規則があります。 それが "二重否定除去則"
not not a が証明できているならば、a が証明できたことにしてOK
「あったり前じゃん、そりゃ論理的に not not a == a でしょ？」 と思いますか？
しかし、今世紀20世紀のはじめに、「この規則を
証明ステップとして認めてしまうのには重大な問題がある！」と強烈に主張した
Brouwer という数学者がいます。
二重否定除去則を認めないBrouwerの立場を「直観主義」といい、認める立場を「古典」と
言ったりします。なぜどのように問題なのかを書くにはこのスペースは
あまりにも狭すぎますが…
『無限論の教室』
という本が超おすすめです。よく書けた一般向けの本なので、ここまでの私の文章が
意味わからんかったという方でも面白く読めると思います。
まあそんないわくつきの二重否定除去則ですが、証明規則ということは、 何かしら対応がつくプログラミング言語側のプリミティブがあるはずです。それが…
call/cc
（…なのだ！と、この記事の最初のバージョンでは書いていたのですが、実はやっぱり ちょっと違うので、以下は つっこみ を受けてごにょごにょと書き直したバージョンです。）
call/cc が引数にとるのは、「何かしら継続 a -> ⊥ を受け取ると、
その継続に何か値を突っ込んで返してくる関数」です。継続を使わずに
普通に直接a型の値を返してくることもあるので、引数の型は
(a -> ⊥) -> a ですね。次に call/cc の結果の型を考えると、
こいつはその継続に突っ込まれてくる値の型なので、要するに、a です。
つまり、(a -> ⊥) -> a 型の値をうけとると a 型になっちゃうヤツ、それが
call/cc なわけですね。
「プログラムを書くときにcall/ccを使ってよい」つまり「(a -> ⊥) -> a 型の値が あったらそれをcall/ccを使ってa型の値に変換してOK」ってことはすなわち…論理の話として 言い直すと、「証明を書くときに、(not a ならば a)が証明できたら、aが証明できたことに してよい」という証明ステップを認めていることになります。この証明技法はよく使われるので、 とても有名な名前がついてます。いわゆる 背理法 の一種ですね。「(not a ならば a)」は要するに、「not aを仮定したら aが証明できちゃう、つまり仮定と矛盾した結論がでてきてしまう」ってことで、そこから 「そういう矛盾がでるということは最初の仮定not aがそもそも間違っていたのだ、実はaは真」 と論証を進めるのが背理法(の一種)です。つまりおおよそ、「背理法⇔call/cc」、と。
※背理法と呼ばれる証明には実際には２パターンあって、 「aを仮定したら矛盾が出た。よってnot aである」というパターンと 「not aを仮定したら矛盾がでた。よってaである」というパターンです。 前者の背理法はなにも問題なくて、call/cc に対応するのは、後者の背理法の方です。 詳細略しますが、後者の背理法をよくみると、言っていることはほとんど二重否定除去則 そのまんまで、どちらかを認めればもう片方も認めざるを得ないという関係にあります。 背理法や二重否定除去の他にもこれらと等価な証明の規則はいろいろ存在していて、 そして「そのあたりの証明規則は全部問題あり！」と叫んだのが、Brouwerの直観主義なの でした。上の２パターンの背理法の区別について、直観主義を知ってる人が相手なら、 "ヤバくない方の背理法" と "ヤバい方の背理法" で通じるかもしれません。 同様の用例として、"ヤバい方のド・モルガン" などがあります。(笑)
論理学の話だけ聞いていても「二重否定除去や背理法(の一種)って、なんかキモい」 と主張した Brouwer の気持ちは私にはあんまりわからなかったのですが、「call/cc って なんかわけわからんしキモい」なら理解できる気がします。でも、Curry-Howard対応の 示すところによれば、この二つは要するに同じ物。どっちかがヤバいならもう片方もヤバいの です。逆に言うと、「call/ccなんて二重否定除去と同じくらい感覚的には当たり前だよ」とも 言えるのかもしれませんが。
Brouwerの感覚を理解するためには、二重否定除去則を認めないと証明できないような 命題、例えば (aまたはnot a) を証明してみるのが一番です。論理的には正しそうですよね？ どんな命題もtrueかfalseかのどっちかなはずですから。 もちろん、証明してみる＝その型がつくプログラムを書いてみるです。 (a,a->⊥) sum 型のつくプログラム。
…
call/cc なしでは、書けません(aが具体的にたとえばboolと決まっていれば書けるんですが、 一般のaについて成り立つようなものは書けないことが"証明"されています)。書けません どころか、私の場合そんなプログラム、まったく書ける気すら起きないと 感じます。最終的に (a,a->⊥) sum 型の値を作るには、InLeft するか InRight するかの どっちかしかないですが、そのInLeftするa型の値やInRightするa->⊥型の関数はいったい どこから湧いてくるのか？その「まったく書ける気すら起きない」がBrouwerに 「それはいかん」と感じさせた点でもあります。さて、 住井さんの例 を再度お借りします。
callcc (
fun (k: (a, a->⊥) sum -> ⊥) ->
InRight (fun (x:a) -> k (InLeft x)))
)
何をやってるかわからねーですが、要は、いったん "not (aまたはnot a) ならば (aまたはnot a)" という型のつくプログラム（これは頑張れば作れます）を作って、それに callccを適用しておしまい、という寸法でした。
call/ccや継続がない言語でも、「プログラム変換によってcall/ccと継続を完全に エミュレートできる」ことが知られています。その変換を "CPS(Continuation Passing Style)変換" といいます。 全ての関数適用を末尾適用にしてくれる変換でもあるので、 コンパイラの内部表現として使われていたりもするらしいです。
一方で、あちらのコメント欄に酒井さんが書いておられましたが、「二重否定除去則を認めないと 証明できないような命題であっても、"not not" をつけて回れば二重否定除去則なしで 証明できる命題に変換できる」という有名な定理があります。プログラムと型の世界の 話である "CPS変換" は、実はどうみてもこの "命題と証明に二重否定つけて回る変換" です。 本当に
といった対応関係などもありまして。なんかnotと継続の話ばっかりですね。他…
数理論理学の世界で定式化された証明のスタイルには、大きく分けて３種類があります。 適当にGoogleったらこの辺がひっかかりました。
関数型言語の世界でのプログラミング言語の定式化には大きく分けて２種類があります。
いままで見てきたように、「自然演繹⇔λ計算」なのでした。そして、他のシステムにも
ちゃんと対応関係が成り立っています。まず「ヒルベルトスタイル⇔コンビネータ」。
ヒルベルト流というのは、"いったん仮定を置いてからそれを消して…" みたいな証明技法を
使わない定式化で、プログラミング言語というかλ計算の世界での
fun x -> みたいにいったん仮定xをおいてそれを後で束縛みたいな
やり方はしない方法で、「SとKとIと関数適用しか使わない！λ抽象なんかいらん！」という
SKIコンビネータ
まさにそのものだったり。
「シーケント計算」も、λ計算とだいたい対応しますが、 「自然演繹」とはちょっと違ったやり方でpairやvariantを扱います。 一番最初にあげた例を思い出してください。こんなプログラム=証明でした。
# fun x -> (snd x) (fst x);;
- : 'a * ('a -> 'b) -> 'b = <fun>
これが自然演繹の証明でありプログラムです。 …しかし、まともな OCamlプログラマ / Haskellプログラマなら、 同じことをする関数を書くにしても、もっと別の書き方をしますよね、普通。
# fun (x,f) -> f x;;
- : 'a * ('a -> 'b) -> 'b = <fun>
そう、pairから値を取り出すのにfstやsndなんて使いません。パターンマッチします。 んで、fstやsndをやめて、代わりにパターンマッチ（っぽいもの）を使うのが 「シーケント計算」です…って、書いててなんかパターンマッチは流石に違う気が してきたんですけど！どうしよう。まあ近いものはあるということにしておく（いい加減）。 本当は、厳密にシーケント計算の推論規則に一対一対応する関数を書くと、だいたい
fun p ->
let (x,_) = p in
let (_,f) = p in
f x
こんな雰囲気のものになります。「自然演繹」ではpairを"壊す"規則＝"除去"規則と、 それに対応するfst,sndというプリミティブが用意されていましたが、「シーケント計算」 では、証明規則の中に演算子を"壊す"規則,除去規則はありません。その代わり、 自然演繹ではλ抽象で束縛する時以外基本的にさわらなかった、"仮定"に演算子を入れる、 "左導入規則"ていうのを使います。λ計算でいうと、ペアの第一成分を取るときはfstを 使ってペアを壊すのではなくて、新しい変数(=仮定)を使いはじめるときに、 「このペアの右手側を指す変数です」みたいな感じに変数定義の側にpairなどなどの構造を 入れることで対処する感じ。
さて、勢いだけで書き始めたらだんだん自分でも書いてることが激しくあやふやに なってきましたので、適当に色々列挙してごまかしつつ終わることにします。 「帰納法 ⇔ fold」 だとか 、「二階命題論理 ⇔ 多相型」、「一階述語論理 ⇔ Dependent Type」、 「線形論理 ⇔ 線形型」 などなど。
あとそうだ、最初の方に "1+1=2" が例えば命題っていいましたけど、じゃあ当然、"1+1=2" に 対応する型ってなんだ、その型のプログラムってなんだ、という話になるわけですが…。そういう "1+1=2" のような型を表現できるなんとも強烈な型システムを持つプログラミング言語が、 いわゆる定理証明系の、例えば Coq の表現言語 であるGallinaだったり、 Isabelle だったり、 Agda は実は全く知らないのですが多分そう、だったりするそうな。
といったところで、このお話は終わりにします。 さてさて、何人か見ていそうな気がする専門家の目から見てボロボロな予感がして怖いのですが、 間違いがあったらきっと突っ込みまくってくれるはず！と期待！ しかし、書いてみると、こんなやたら長い記事誰も読まない気がしてきた…。
ある日記サイトで読んだ文章が記憶に残っています。
中学生のころ、何の時間だったか、先生が黒板に小ぶりな円を描いた。
「いろんなことをたくさん勉強すれば物知りになって、知らないことやわからないことが少なくなると思いますか」
先生は一拍おいた。
「まったく反対です。勉強すればするほど、知らないことやわからないことがどんどん増えていきます」
そこで先生は、黒板の円を指した。
続きは 「日々是好日」 ２００４年１０月２０日 をどうぞ。"無知の知" 的なよくある話かもしれません。 しかし、印象に残るたとえだと思いました。どこまでスケールするかはともかく、 これを読んで以来、"知識" を漠然と "円" としてイメージする癖がついてしまっています。
トラックバック受信のかわりの手動逆リンク集。
くるるさんによる証明 と、 山形さんによるそのメモ。Moore の方法を (m2,m1,m3)
で回すと本質的にほとんど同じになるのかもしれません。「自然数の範囲で
考えればOK」という観察が -min(x,y,z) で、あとはmaxで外側の帰納法 →
yが大きい場合は自明 → そうでない場合は中でxで内側の帰納法、という形になっているので。
確かに言われてみれば、xの帰納法には上限がありました。
住井さんによるMcCarthyの証明の紹介。すみませんScienceDirectにアクセス できるIPアドレスを得にいくのが面倒で手抜きしてました…(汗。ありがとうございます。
DTAK0(X,Y,Z) = DTAK00(X-Y,Z-Y)
ここまでは、x-y や z-y 辺りを指標として使うのはありに思えました（nucさんもその方向をイメージして らしたみたい。）が、その先が物凄いですね。もう少しはなんとかなりそうな…確かに、 表現を変えればもっとわかりやすい帰納法だったりするのかもしれません。
D言語の開発者である Walter Bright 氏への Bitwise誌によるインタビュー に、何度も Ruby が登場してて面白かったのでご紹介。 一部訳出してみますと
Huw: つい先日、Ruby と D が同時に TIOBEのプログラミング言語 'トップ20' にランクインしました。構文の見た目は、Ruby と D では随分と違いますが、共通の特徴がいくつもあるのも確かです（例えば、かなり'純粋な'オブジェクト指向、簡潔な構文、GC、モジュールとmixin、クロージャ)。こういった Ruby と D の類似には、表面的なもの以上の何かがあるのでしょうか？
Walter Bright: Ruby と D には、興味深い共通項がたくさんあります。Ruby は Perl の reengineering として開発が始まっていて、Perl は C++ と ある意味でよく似ています（訳注: D は C++ の reengineering、という触れ込みの言語）。 Ruby は一人の開発者の、純粋にプログラミング言語が好きだという気持ちから生まれた言語であって、これも D と同じです。Ruby も D も、"プログラマの必要に応えるため" 以外の隠れた開発意図はありません ‐ だから、大企業がバックについて予算を投入したりせずとも、広くプログラマに受け入れられました。おそらく、この二つの言語の間の根本的な違いは、Rubyはインタプリタ系の、動的型の言語であることで、D はネイティブコンパイルの、静的型の言語であることでしょう。
色々突っ込みたい… D が fairly 'pure' OOP ? …ところはありますけど、それは おくとして。私も D の "template を mixin" する設計を見たとき真っ先に 思い出したのが "module を mixin" する Ruby だったりして、近いところはあるなあと いう気はしていました。
Huw: D は除くとすると、いまどきのプログラミング言語の中で、一番面白い、あるいは一番可能性を秘めていると思うのはどれですか？
Walter Bright: 疑問の余地はないですね。注目すべきは Ruby です。
だそうですよ。
ちなみにこの紹介を書いた私の隠された意図は、Rubyを褒めている記事を 引用することでRubyistの目をD言語に惹きつけてみるテスト、という下心なのですが、 そんなことをしている暇があったらむしろ自分がRubyを勉強せねば、とつい 数日前に思ったのだった…。
いえいえバッチリOKです。
ということで、検索してみました。Boyer&Moore の定理証明系Nqthmを使った証明
（Moore, 1979）
が一発目ですね。その論文自体はちょっと見つからなかったのですが、実際の証明デモの
サンプル(PDF)を発見。
三種類のメジャー m1, m2, m3 を定義して、(m1(x,y,z), m2(x,y,z), m3(x,y,z))
で超限帰納法してるみたいです。方針はそれしかないとは思ったのですが…
m1(x,y,z) = if x≦y then 0 else 1 m2(x,y,z) = max(x,y,z) - min(x,y,z) m3(x,y,z) = x - min(x,y,z)
2ω2。これどうやって思いつくんだろう…。Moore 以前にも、 McKarthy が別の（もっと複雑な）順序を入れて証明しているらしい。
そして上記の結果を引用している論文を眺めていたら、 Tom Bailey, John Cowles, "Knuth's Generalization of Takeuchi's Tarai Function: Preliminary Report" (2000) がなかなか面白いです。Knuthが、たらいまわし関数のN引数に一般化バージョンを提唱して いるらしく。
t(x[1], x[2], ..., x[N]) =
if x[1] <= x[2] then x[2]
else t(t(x[1]-1, x[2], ..., x[N]),
t(x[2]-1, x[3], ..., x[1]),
t(x[3]-1, x[4], ..., x[2]),
...,
t(x[N]-1, x[1], ..., x[N-1]))
こういうもの。N=3の場合がいわゆる竹内/たらい/tak/tarai関数ですね。さて問題。
まず１番目は…昨日向井さんに教えていただいたような、「大小関係に応じて引数の どれかを返す関数」の一般化バージョンになるんじゃないの？と予想できます。
λ(x[1], ..., x[N]).
if x[1]≦x[2] then x[2] else
if x[2]≦x[3] then x[3] else
...
if x[N-1]≦x[N] then x[N] else
x[1]
実際これは N=3 では正しかったし、N=4 でも正しい。ところが N=5 では成立しない。 t(5,3,2,0,1) が反例らしいです。これに気づいたKnuthは、↑の関数を一段複雑にしたような 関数を定義して、それが等式を満たすことを… "手ではたぶん証明できたと思うが、二度と チェックする気が起きない。誰か計算機で機械証明して欲しい" …という形でOpen Problemと して記します。しかしそのKnuthバージョンにも9年後、N=6での反例 が 発見されているとのこと。
Knuthは1と同時に、call-by-needなら止まる、という証明も与えていたそうなのですが、 反例が見つかってしまった誤った定式化に基づいていたので、これも一旦白紙に戻って、 Open Problem。
call-by-value ではどうか？ N=3 のときは、今日の記事の一番上に上げたような証明で、 止まることが知られている。しかし、N=4 のとき call-by-value では止まらない という例が2000年に示されているそうな。t(3,2,1,5) が無限ループするそうです。
と、こんな風な絶妙な境界線上に載っている楽しいテーマなんだそうな。 この論文自体は、1.にKnuthバージョンとは別の「今度こそ正しいはず」解を与えて、 2.については、「止まる」というConjectureを主張しているもの。 ACL2 を使って完全な機械証明を与えようとしている途中とのこと。手では証明できている つもりで何度もチェックしているけれど、Knuthの例もあるから…みたいな雰囲気で。
またこの話ですすみません。
f(x,y,z) =
if x <= y then y
else f(f(x-1,y,z), f(y-1,z,x), f(z-1,x,y))
この計算は、経験的には、どんな整数３つを引数にしても停止するようです。 で、前からずっと気になっていたのが、これの停止性ってどうやって証明すればいいんだろう？ という疑問。あと、経験的には返値はx,y,zのどれかなんですけど、これもなんでだろう。 fの返値を再度fに与えてるので、両方同時に解かないといけない問題な気はする。
という感じで、いい考えが思いつきません。 エレガントな証明が知られてそうな予感がすごくするのですが。
なるほど！ でも、例えばちと無理矢理ですが
g n = if n <= 0 then 1 else g (n+1) - g (n-1)
この等式は普通のフィボナッチ関数を当てはめると成り立ちますが、 この g は1以上の値を喰わせると停止しません。つまりある等式が
(\x y z -> if x <= y then y else if y <= z then z else x)
を当てはめると成り立つとしても、それがちゃんと停止してこの関数を 計算してくれるかどうかはただちに明らかではないような…。
…そういう閉鎖的なスタイルは、誰にとっても得がない上に誰にとっても損があるのでは ないかと。自分は、ACM会員だけ見られるページに論文があればそこにリンクするし、 dat落ちした2chスレにも必要なら言及するし、もし仮に全てのchatのlogやpersonal conversationにURIが振られる日が来たら、そのURIを全て貼り付けながら日記を書くでしょう。 （そもそもの前提として、「誰もが見られる情報のみに依存しているか、もしくは完全に 自己完結した記事しか書かない」という縛りは面白くないと思う。） そうしないことによる"損"とは、敢えてそうしていないこのエントリが示しているように、 閲覧者に無駄にネタ元を憶測させる手間でありググらせる手間であり。