Skip to content

浦島太郎への憧れ

おもしろいことをしていると、一息つく間に二時間くらい経ってしまう。ガスコンロを使っているときはおもしろいことをしないように気をつけている。浦島太郎は竜宮城から帰ったあとに、あけてはならないと言われた玉手箱を開けたとたんに年をとって周囲も時代がうつっているという話である。玉手箱にはおもしろい数学の本が入っていて、おもしろがっていたらあっというまに年をとってしまったのだと考えると、つじつまがあう。

個人的な信条――演繹の力

帰納ではなく演繹の力を信じる。演繹の力とは、経験を集めて知識を引き出すのではなく、いったん世界をほうって引きこもり、エディタなりノートなりにごにょごにょ書いてからこうなるはずだと言い切る力である。目的に関していえば、人が欲しいものを聞いてまわるのではなく、ひきこもって、これが欲しいはずだと考えることである。手段に関していえば、もうある道具を漸次改良するのではなく、原理に戻って根本を断つことである。

あ、たぶん人間は帰納するようにできているので、目の前で起きていることから直接学ぶのは、健康だし社会的だし成功への道だと思う。帰納への反感はない。

それでも演繹にこだわるのはなぜか。地球の歴史を通じて、生物の進化は、経験を糧として遺伝子を選別する帰納の過程であった。しかしつい最近になって人間が証明を書き始めた。もっと最近になって書いたものが動くようになった。これはおもしろい。なので、ソフトウェアに証明をつけたり証明を動かしたりしている。

追記: Knuthが喋っている

 

Coqでゲーム(1)

Theorem Proving Advent Calendar 18日目

このまえCoqで超現実数(1)を書いたときにMamameさんの研究をみてみたら、ゲームの比較の推移律の証明が構成的でないと書いてあって、たいへん不満をおぼえました。ゲームの比較の推移律は、Aを取ってBを返す関数と、Bを取ってCを返す関数とを合成してAを取ってCを返す関数を作る、ということをゲームでやる話なので、戦略と戦略から戦略を構成しないとおもしろくありません。というわけで、有限なゲームに限ってでもいいから、それをやろうということになりました。

ソースコードはgithubにあります。

ゲームは二人でやることにします。LとRです。

Inductive player := L | R.

で、ゲームというのは、空っぽの何もできないゲームemptyか、プレイヤーpがmというゲームに移れるaddMove p mというゲームかどちらかということにします。

Inductive game: Set :=
| empty: game
| addMove: player -> game -> game (* original *) -> game
.

次に、ゲームgでプレイヤーpが先手必勝なwinningStrategy g pというものと、先手必敗であるlosingFate g pというものを定義します。

Inductive winningStrategy: game -> player -> Set :=
| take: forall p m o, losingFate m (opponent p)
                      -> winningStrategy (addMove p m o) p
| pass: forall p m o q, winningStrategy o p
                        -> winningStrategy (addMove q m o) p
with losingFate: game -> player -> Set :=
| stuck: forall p, losingFate empty p
| whichever: forall m p o, winningStrategy m (opponent p) ->
                  losingFate o p -> losingFate (addMove p m o) p
| wait: forall p q o m, losingFate o p -> q = opponent p ->
                  losingFate (addMove q m o) p
.

この手のゲームでは、両者ゲームのことがぜんぶわかっててかしこければ先手必勝か先手必敗かどちらかになるので、それを示しました。

Definition decision (g: game) (p: player):
  winningStrategy g p + losingFate g p.
Proof with auto.
generalize p.
clear p.
induction g.
  intro p.
  right.
  apply stuck.

  rename p into mover.
  intro p.
  destruct IHg1 with (opponent p);
    destruct IHg2 with p;
    clear IHg1 IHg2;
    destruct mover; destruct p; simpl in *.

  left.
  apply pass...

  left.
  apply pass...

  left.
  apply pass...

  left.
  apply pass...

  right.
  apply whichever...

  right.
  apply wait...

  right.
  apply wait...

  right.
  apply whichever...

  left.
  apply pass...

  left.
  apply pass...

  left.
  apply pass...

  left.
  apply pass...

  left.
  apply take...

  right.
  apply wait...

  right.
  apply wait...

  left.
  apply take...
Defined.

ただ、同時に先手必勝と先手必敗になることはありえない、ということを証明していないので、それはこんどにしましょう。



				

Coqで超現実数(1)

Theorem Proving Advent Calendar 6日目

超現実数というものがあります。それをネタにKnuthが小説を書きました(日本語訳)。ConwayのOn Numbers and Gamesという本もむかし読みました。これをCoqで実装して修論を書いたMamameさんという人がいる(TYPESのMamameさん論文)のは知っていたけれども、中身はまだ見てなくて、で、見ないまま自分でやってみると、少し違うものができました(github)。

まずゲームを定義してから、数は特殊なゲームだと言います。

ここでいうゲームは二人ゲームです。左の人と右の人が勝負します。なにもできなくなったほうがまけ。ゲームを決めるには、左の人が先手で何かした結果どういうゲームにできるかと、右の人が先手で何かした結果どういうゲームにできるかとが決まればよいです。ここで問題はゲームを定義するためにゲームを使っていることですが、なんとかなります。残り何手以内のゲームかでもって話を切れば、残り0手のゲームを定義するためにゲームを使う必要がないので、めでたくゲームを定義していくことができる(ちなみにMamameさんはもっとエレガントなことをしています)。

それで残りn+1手以内のゲームとは何か。まず、残りn手以内のゲームは、残りn+1手以内のゲームでもありますね。めでたい。それから、左の人が移れる行けるゲームと右の人が移れるゲームを決めてもいいですね。この、nからn+1にうつるところを、ゲームどもからゲームどもを決めるしかけとして実装してみましょう。

Inductive step (orig: Type): Type :=
 | inherit: orig -> step orig (* もともとゲームだったものはゲームのまま *)
 | compose: (orig -> Prop) -> (orig -> Prop) -> step orig
   (* 左が動ける先のゲームを定義する述語と、右が動ける先のゲームを定義する述語があればよい *)
.

あとは、空の型から始めて、順々につくっていけばいいです。証明をCoqに通したい人はgithubから持っていってください。

Fixpoint game (m: nat): Type :=
 match m with
 | O => empty
 | S m' => step (game m')
 end.

game 0という型のものはないはずなので、game 0という型のものについての述語は簡単に定義できます。どんなgame 0のものを持ってこられても「にゃー」とか言っておけばいいのです。どうせ何も持ってこられないはずなので。

Definition charm: game 0 -> Prop.
intro.
destruct X.
Defined.

ひとたび「にゃー」と言えればゲームを作るのは簡単です。

Definition zero: game 1 := compose _ charm charm.
Definition one : game 2 := compose _ (fun _ => True) (fun _ => False).
Definition half: game 3 := compose _ (fun x => x = inherit _ zero) (fun y => y = one).

ついでにゲーム同士を比べるgleという関係を定義してみます。どっちのほうが左に有利、というのを比べます。擬順序になるつもりです。

 

Inductive gle: forall m n, game m -> game n -> bool -> Prop (* 定義は略 *)

これを使うと、さっき定義した3つのゲーム同士を比較できます。

Lemma zero_one: gle _ _ zero one true.
Lemma one_zero: gle _ _ one zero false.
Lemma zero_half: gle _ _ zero half true.

擬順序のつもりですから、たとえばreflexivityが成り立ちます。

refl : forall (m : nat) (g : game m), gle m m g g true (* 証明は略 *)

推移律も成り立つはずです、えーと、まだ証明していません。次回以降にやります。反射律と推移律があるなら、すくなくともpreorderとして圏になりますね。でも、ゲームがゲーム以下というのは、あっちのゲームの勝ち方がわかればこっちのゲームの勝ち方もわかるということで、戦略から戦略を計算する仕掛けと捉えることもできますから、もっと豊かな構造を持っていてもいいはずです…ということを考えている先人はたくさんいます。Joyal (1997)の英訳

いまのところ、m手以下のゲームというのを考えてきました。しかし、一手進めると、残り何手なのか決まるゲームというのを考えてもいいでしょう。どうせ終わるのですから。残りω手のゲームと言えるでしょう。残りn手のnのところに、自然数に限らず順序数を許しておけば、最初からこの手のゲームも扱えて幸せになれそうですね。いまは、ωのところだけ、書いておきましょう。

Inductive ogame : Type :=
| o_inherit: forall m, game m -> ogame
| o_compose: (forall m, game m -> Prop) -> (forall m, game m -> Prop) -> ogame
.

ぴらんだ

オランダに来て一週間だ。

日本との違いはたくさんあるけれども、わからないことはインターネットでだいたい解決できてしまう。たとえばハムを買って、生で食べていいのかよくわかんないというときも、包装を見ながら、Google Translateに”Het product kan overhit als broodbeleg geconsumeerd worden”と打ち込むと、どうやらそのまま何かに乗せて食べてもいいらしいとわかってしまう。ただし大学のこのへやから印刷するにはどうすればいいのか、とか、そのてのローカルなことは、人に聞かないとわかんなくて、ありがたいので、そろそろ日本からやってくるおみやげをみんなにわたそう。

オランダと日本の差よりも、個人的に避けてきたことをやってみているギャップのほうが、大きい気がしている。

避けてきたこと「普通のコンピュータサイエンス」

なんだかロジックがらみのことばかりやってきたので、ぼちぼち、普通に役に立つことをやってみてはどうかねという気分になって、やってみている。まあ、ロジックがらみでやってみたことと、今回やることと使うテクニックは似ているので、悪い順番ではないのだろう。単純な対象でさんざん遊んでからややこしい対象に手をつけているのだから。

避けてきたこと「自炊」

本郷でも一人暮らしはしていたが、部屋には食べ物を持ち込まないというポリシーがあって、自炊はしていなかった。幼稚園時代から、正しいタイミングで正しい動きをすることに苦手意識があった。筆頭は音楽で次が体操とか。料理もなんとなくそっち側に分類していたらしい。

もともと動くことが苦手になったのは、もともと人の動きを真似するのが苦手な上に、間違ったことをするといちいち指摘して直させられたあたりが、元凶であろうと思う。歌ったり踊ったりも楽しくすればいいじゃないのと言ってくれればよかったであろうに。

それで動くのは苦手なので、途中結果はともあれ最後にできたものがよければいいような、証明とかプログラムとかを書くほうに、力をいれてきた。

15年かかってわかってきたことがある。結果さえよければいいといっても、それなりに早く結果を上げるには、正しいタイミングで正しいことをしないといけない。バグがあるときに次にどこをみるべきかとか、いつまで作業したら依頼してきた人に報告するべきかとか。さいわい、損得勘定はできたので、いつのまにか、より正しいタイミングで正しいことをするのに慣れてきたようだ。そして、損得勘定で正しいタイミングがきまるのは、料理も似たようなものだ。

オランダと日本とのギャップが気にならない理由

日本にいても頭でっかちな感じで、あまり周囲のことがよくわからず、考え考え暮らしていたので、オランダに来て周囲のことがよくわからなくても、あまり方法に変化がないのかもしれない。今後も考え考えやっていくのであろう。

ぽんぽこり〜ん

強風。大学のピロティの自転車が半分くらい倒れていた。しかし風が当たらないところはまだ空いていた。

床屋に行った。床屋の鼻息が荒くて怖かった。

論文を書いている。ふだん定義定理補題証明補題証明定理の証明ばかりなので、そうでない論文になにを書けばいいのかよくわからない。しかし、目の前にある紙切れの変なところはわかるので、そこに印をつけておいて、エディタに向かって書き足したり並べ替えたりする。

3日で作ったiPhoneアプリがランキング入りした

iPhoneアプリってどういうものかと思って、3日かけて調べながら作ってみた。someoneradarという名前を付けて出した。6,000ダウンロードくらいに達して、一日2,000ダウンロードくらい。AppBankさんに取り上げられた影響が大きい。

そうするとApp Storeの無料のエンターテインメント部門で14位に達してから、ずるずると順位が下がってきている。

現実世界と数学

人と喋りながら横断歩道を渡ろうとして自転車にぶつかられると、現実世界というものがあることがわかる。そんなに頑張って何の話をしているかというと、数学の話とか数学以前の話とかをしている。そういうところに耽溺しているのもいいのだが、現実世界も相手にしたいものだ。行ったり来たりしたい。

現実世界には数学にしたがうものがたくさんある。化学とか物理とかやれば、数学と現実世界と両方を相手にできる。もんだいは、勝手に数学をこしらえても物理とか化学の実験結果は変わってくれないということである。人間の勝手な数学にしたがって変わってくれるものは現実世界にはないものかと探してみると、筆頭は人間である。人間に数学の話をすると、おもしろがったりあきれたり無視したりする。こまるのは、人間は同じ話をなんども聞かせると反応が変わってしまったり、おなかがすいてくると反応が変わってしまったりして、よくわからないことである。そこで、人間以外に、勝手な数学にしたがって変わってくれるものはないかしらんと探してみると、計算機というのがあって、もちろん結局物理法則に従って動いているけれど、顕著に楽しい現象は人間の勝手な都合で動いているようにみえる。これは楽しい。

計算機だって結局物理法則にしたがうなら、人間の勝手に決めた数学にしたがうことにならないという人は、この文章を読めないはずである。あなたの目の前には、明るい点とか暗い点とかが並んでいるだけで、文章などというものはないはずだ。ここに文章があるなら、計算機は人間が勝手に決めた数学に従っている。

博士課程に入った反省をする

今月は論文を二本も投稿してしまった。といっても粗製濫造しているわけではなく、片方は一年前から解けずにうなっていた問題が解けたものだし、もう片方は二人がかりで三ヶ月かかっている(山本和彦さんとの共著)。いわば収穫の秋である。

ここらで、どうして博士課程に入ったんだっけと思い出し、その目的は果たせそうか、これからどうしようかと考えてみる。

どうして博士課程に入ったんだっけ。博士課程に進むのを決めたのは去年の春から夏にかけてのことであった。当時はなにやら、自分しか気づいていないことがあるから書き下そうと思っていたようだ。自分で真面目に書き下さなければ、こんご五十年くらいは他に誰も書いてくれない気がした。わりと世の中のプログラマがめんどくさがっていることを楽にできるようになる気配も感じた。

この目的は果たせそうだろうか。今思うに、放っておけば十五年くらい誰も書かなかっただろうというのは、やはりもっともだ。この分野とこの分野をまたぐ必要があるのに、片方の分野には20,000人くらいいても、もう片方の分野にはたぶん50人くらいしかいない感じ。ぜんぜん難しい話ではないのだが。それで自分で書いてみたし、出版物にも載るし、おもしろがってくれた人もいる。

世の中のプログラマをちょぴっとでも楽にできるかは予断を許さない。できあがるまでのうちまだ一割か二割。

できあがったところで、使ってもらえるかどうかわからない。もちろん使ってもらえなければ自分で使ってみせるまでであるし、そういう覚悟でなければなんにもできないものであろう。もちろん、どんどん人を巻き込んでいかなければ世の中を変えることは叶わないけれども、中庸に、「国に道なきときも死に至るまで変ぜず」とある…と、このように孤立志向なのは危険な徴候だ。今年の前半は、本題が行き詰っていた上に、孤独にわけのわからないことをしていて、危うかった。われながら偉いのは、わけがわからないところからふと覚めて、志とは別に、コンビニ研究者的な行動を開始したことである。ふわふわとそのへんを漂っていて、そこにいる人だけでは解決するまで大変そうだけど自分が手伝えば早いということを発見し、解いてみる。研究テーマの決まるのはいつも偶然という言葉通りにできたのが共著の論文である。この具体的な問題を堅実に解いているうちに気分が変わり、行き詰っていた本題にも堅実な方法を取り入れて、突破することができた。 こうしてできたのが、今月もう一本投稿した論文である。

これからどうしようか。本題で、次にすることがみえているので、それを進める。いろいろな人を待たせている。次の論文の潜在的読者も、一緒に何かしようと言ってくださる方々も。もうちょっと芋を掘ってから、また見晴らしのいい、人がたくさんいるところに行こう。見晴らし台から面白いところに急転直下、また穴掘りをしよう。詩に云う「鳶飛んで天に戻り、魚淵に踊る」と。

未来日記

なるほど未来日記というのを書く人もいるのかと思って書いてみる。とはいえ彼ほど先が見えるわけではない。しかし、前回書いたものは、作戦通りに書きあがって投稿できたので、起こらないことばかりが見えるわけでもない。

10月

役立ち論文を仕上げて投稿。共著者はじめ、たくさんの人たちの協力を得られている。

何か通知を受け取る。

決定不能の会の準備。自分の発表の準備もあれば、イベントとしての準備もある。それにしても変な集まりだ。

11月

中庸を読み終える。

おもしろい論文を投稿。

講演会のお手伝い。

申請をまじめに書く。

名古屋でCoq人に話を聞いてもらう。

12月

何か通知を受け取る。イスタンブール以外の初のヨーロッパ成るか。

運転免許を取る(?)。

役立ち論文がどうなったかわかる(?)。

1月

次のネタを探してごそごそ計算