不完全性定理の理解不完全性

大阪大学に赴任してから半年たったぐらいの2019年2月頃に、離散数学と計算の理論という題目の講義を4月から担当することに決まった。その理由は、その講義を元々担当していた当時研究室の准教授だった先生が、他大学の教授へとご栄転されることが決まったからである。

自分はネットワークシステム、分散・P2Pコンピューティング、ネットワークセキュリティが専門でどちらかというと実装よりなので、数学はあまりやってこなかったのだが、今はプログラミング言語理論を習得するために論理学や計算モデルを勉強していたので引き受けることにした。この講義は大阪大学のProSecというコースを申し込むと、社会人でも受講することができるようになっている(コースは有料だけど)ので、詳細は「大阪大学 prosec」で検索してほしい。(現5月時点で申し込むと、秋からの受講になるだろうが)

プログラミング言語を真面目に初めた理由は、最近はネットワーク業界でもソフトウェア定義や、プログラマブルスイッチなどと言われているため、数年後にはプログラミング言語理論の知識が必要になるのではないかと漠然と思っていたからであった。実際に活かせるかどうかはこれからの研究にかかっているので、乞うご期待といったところである。

そんなこんなで講義を担当することが決まり慌ててシラバスを決めたのだが、自分の担当は以下のようにした。

  1. 命題論理
  2. 述語論理
  3. 計算可能性
  4. 不完全性定理
  5. λ計算
  6. 型システム

4回で不完全性定理まで行くのはかなり駆け足な気がするが(2人の先生で15回なのでこんな感じに)、大阪大学の学生は優秀なので大丈夫だろう。問題は自分の方である。内容を決めたは良いが、勉強のし直しが大変だった。3月からは、家に帰ってからは数学の本を読むことに時間を使った気がする。今はゴールデンウィークだが、不完全性定理はめちゃくちゃ大変で、ゴールデンウィークの半分は不完全性定理で消えてしまった。なぜシラバスに入れたかと自分を恨んだりもしたものだ。ツライ。

不完全性定理を学ぶ上でいろいろな文献を参考にしたが、数年前に買った「コンピュータは数学者になれるのか?」という書籍がとてもためになった。しかし、この本は一般書の顔をしているが数学がある程度わかる人向けなので、誰得感が否めない。前半の1、2章で述語論理の導入から初めて不完全性定理まで行くというハイペースぶりである。自分はとてもためになったので、俺得ではあるのだが。まだ不完全性定理の理解は不完全なので、今後はもう少し落ち葉拾いをしていきたい。

この講義では簡単な原始帰納的関数Haskellで実装したり、型付λ計算で簡単な型推論エンジンを実装したりもする予定なので、内容的にはかなり面白いのではないかと思う。特にうちは工学部なので、数学をプログラミングに活かせたほうが学生にもよいだろう。

他にも、大阪大学のProSecでは、ファイアウォール演習、レジスタマシンのエミュレータ実装演習、多層防御の演習なども自分が担当する予定なので、こちらも準備しないといけない。無事に乗り切りたいところである。

ゴールドバッハ予想の反例を探索するJavaScript

ゴールドバッハ予想とは、2より大きい偶数は2つの素数の和で表せるという予想である。例えば、18 = 5 + 13 や、34 = 3 + 31 となる。

ゴールドバッハ予想が誤りであることを証明するには、その反例を示せば良い。というわけで、ゴールドバッハ予想の反例を求めるJavaScriptを作成したので、ここに公開する。なお、このプログラムは反例が見つかれば停止する。

ゴールドバッハ予想

f:id:ytakano:20190305234235p:plain

ゴールドバッハ予想の反例を求めるプログラムの実行例

プログラミング言語と論理学の狭間にてさけぶけもの

情報科学をやってきたのだから、死ぬまでに一度自作のプログラミング言語を作ろうと思ったのが2016年後半ぐらいである。プログラミング言語オペレーティングシステム情報科学を志した者は誰もが一度は目指す道である(たぶん)。

しかし、思い立ったは良いが、プログラミング言語の研究は論理学を基礎としており、その当時は論理学のろの字もわからなかった。実際には、JAISTの学生時代に小野先生の数理論理学の講義を受けたのだが、その当時は「ANDとOR計算ね」ぐらいの認識しかなかったという体たらくであった。当時は大堀先生もJAISTStandard MLの講義をしていたので、今にして思えば受講しておけばよかったと思う。

そんなこんなで基礎を習得するのに2年弱かかってしまって、今ようやく自作プログラミング言語の実装に取り掛かっているわけである。本報はプログラミングという情報科学にそびえ立つエベレスト、いやオリンポス山登頂を目指しているつもりが、論理学というジャングルへ踏み込むことになった結果得られた知見をまとめたものである。

論理学入り口

独習コンピュータ科学基礎II 論理構造

独習コンピュータ科学基礎II 論理構造

 
論理学をつくる

論理学をつくる

 

『独習コンピュータ科学基礎 II 論理構造』と『論理学をつくる』は初学者におすすめしたい本である。論理学の教科書というと記号の羅列になりがちで、これがどう情報科学に生きていくのは分かりづらい部分がある。一方、『独習コンピュータ科学基礎 II 論理構造』の方は、論理学的な証明もしつつ、プログラムを証明するとはどういうことかや、プログラムで自動推論するにはどうするかなどを解説しており、論理学が情報科学にどう結びつくかが強くわかるようになっている。この『独習コンピュータ科学基礎 II 論理構造』はポートランド州立大学のコンピュータ科学基礎論の教科書であり、内容も大学の講義に耐えうるものだ。

『独習コンピュータ科学基礎 II 論理構造』は、論理学をどう使うかということが主題で、論理学そのものについてはあまり深くはない。例えば、演繹体系は自然演繹法のみ利用しており、様相論理や直観主義論理などの非古典的論理の解説はなく、演繹体系の健全性や完全性の証明はおざなりな感じは否めない。『論理学をつくる』では、情報科学に活かすというよりも、より論理学になった感じの書籍であるが、内容は大変明快で初学者にもわかりやすい。『独習コンピュータ科学基礎 II 論理構造』では触れられていなかった様相論理や直観主義論理も解説されている。

数学や論理学を専攻するのでなければ、この2冊、もしくはどちらかを抑えておけばよいのではないかと思う。つまり、『独習コンピュータ科学基礎 II 論理構造』∨『論理学をつくる』である。

論理学の奥地へ

情報科学における論理 (情報数学セミナー)

情報科学における論理 (情報数学セミナー)

 
論理と計算のしくみ (岩波オンデマンドブックス)

論理と計算のしくみ (岩波オンデマンドブックス)

 

自分は『情報科学における論理』は、JAIST時代に小野先生の数理論理学の講義教科書として購入した。本書は『独習コンピュータ科学基礎 II 論理構造』に比べるとずっと理論よりとなり、プログラミング言語などの関わりよりも、論理そのものを学ぶ、まさに数理論理学という本である。内容は、古典的論理から様相論理、直観主義論理、λ計算まで幅広く書かれている。

『論理と計算のしくみ』は『情報科学における論理』よりもさらに広い範囲をカバーしている。例えば、ゲーデル不完全性定理や、型付きλ計算型推論まで含んでいる。しかし、本書は極めて理論的であるため、論理学の応用を目指す人にとっては幾分難解な箇所もあるように感じた。例えば、無限の論理式を含む式とか、無限という言葉がカジュアルに出てきて抽象度がかなりあがっている。

情報科学における論理』と『論理と計算のしくみ』は、論理学を応用として使ってみるうちに、その理論的背景を知りたくなった場合に読めばよいのではないかと思う。例えば、モデル検査の理論的背景にはクリプキ構造や様相論理があり、背景知識までを正確に理解するにはこれら書籍を参考にするしか無い。

そしてプログラミング言語

型システム入門 −プログラミング言語と型の理論−

型システム入門 −プログラミング言語と型の理論−

  • 作者: Benjamin C. Pierce,住井英二郎,遠藤侑介,酒井政裕,今井敬吾,黒木裕介,今井宜洋,才川隆文,今井健男
  • 出版社/メーカー: オーム社
  • 発売日: 2013/03/26
  • メディア: 単行本(ソフトカバー)
  • クリック: 68回
  • この商品を含むブログ (11件) を見る
 
Programming Distributed Computing Systems: A Foundational Approach (The MIT Press) (English Edition)

Programming Distributed Computing Systems: A Foundational Approach (The MIT Press) (English Edition)

 

プログラミング言語の定番本として挙げられる本といえば『型システム入門』、通称TaPLがあるが、個人的には論理学の教科書で基礎を学んだあとに読んだほうがわかりやすいのではないかと思う。例えば、本書の22章 型再構築には単一化と呼ばれる操作のアルゴリズムが載っており、単一化アルゴリズムは『独習コンピュータ科学基礎 II 論理構造』、『情報科学における論理』、『論理と計算のしくみ』にも載っているが、『型システム入門』の説明が一番わかりにくい。

『Programming Distributed Computing Systems: A Fundamental Approach』は英語の本だが、λ計算、π計算、アクターモデル、Join計算、アンビエント計算など並行計算モデル書かれた良書である。λ計算の説明は本書が一番わかりやすかった。前半の理論部分の解説は良いのだが、後半の実装部分がツール類が古くて動かないものばかりなので読まなくても良いかもしれない。

以上が2年弱勉強して得られたざっくりとした知見である。自分は論理学の専門家では無く、あくまでも論理学のユーザであるため異なっている箇所もあるかもしれないが、なにかの役に立つかもしれないと思い簡単にまとめた。それでは良いハッキングライフを。

ネットでホテルを誤って当日予約してしまい1分後に即キャンセルするもキャンセル料100%請求された件

状況

  • 2月前に楽天トラベルで来週のホテルの予約をしようとしたら、間違って当日に京王プレッソインの予約を取得してしまった
  • あわてて1分後に予約キャンセルする
  • 2月後の今になってキャンセル料100%全額請求されていることに気がついた

結論から言うと、楽天トラベルから予約しするも誤って当日予約してしまった場合は、ホテルに直接電話するとキャンセル料請求取り消しのチャンスが有ったようだ。

はじめに、京王プレッソインへ問い合わせてみた。

京王プレッソインの説明、その1

  • システム的に無理
  • 楽天トラベル側で無理と言っているので無理

楽天トラベル側で無理と言っていたので、楽天トラベルへ問い合わせてみた。

楽天トラベルの説明

  • 楽天トラベルでは、キャンセル料については関与しない
  • システム的には可能なので、ホテル側では可能

楽天トラベルでは可能と言われ、ホテル側と説明が食い違っていたので、再度ホテルに問い合わせてみた。

京王プレッソインの説明、その2

  • システム的に無理
  • 楽天トラベルで操作はできない

やはり説明が食い違っていたので、楽天トラベルに確認したが可能であると聞いたと問い合わせた。もう一度、楽天トラベル側へ問い合わせ、出来ると確認されればキャンセル料請求取消して頂けるという事でよいかと確認したら、担当が変更になる。

  • 楽天トラベルのシステムで取り消し出来るかどうかは問題ではない
  • 規約上、すでに契約は終えているので無理
  • 1分後に取り消していようが無理なものは無理
  • ただし、そういう場合は当日に連絡してくれれば可能であったかもしれない

という説明を受けた。規約上無理というのと、当日に連絡ならキャンセル料請求取り消し可能であるというのは矛盾している気もするが、どうも、間違って予約したらホテル側へ即電話を入れたほうが良いらしい。

最後に、消費者センターへ問い合わせてみた。

消費者センターの説明

  • インターネットで契約を完了してしまったら無理
  • 自分で契約に同意してしまっているから難しい

という説明を受けた。どうも、1万円払うしかないようだ。サンクコストであることが確定し、これ以上考えてもどうしようもないことであることが判明した。

楽天トラベルで日にちを当日に間違えて予約して即キャンセルするも全額請求された件

タイトルの通りのなんだけど、楽天トラベルで翌週の日にちを指定して検索してたら、いつの間にか当日にリセットされていた。そうとは気が付かず予約をしたら、なんと予約日が当日だった。慌てて予約キャンセルしたものの、今になって、あれは当日なので全額請求だよとのこと。

完全に自分が悪いのだが、悔しいのでホテルへ連絡してなんとかならないかと連絡したものの、楽天に問い合わせたが無理だと言われた。間違えて当日予約したものをキャンセルしたという数分のミスで1万円近く失ってしまい釈然としないが、規約をちゃんと読まなかった自分が悪いのだろう。

仕方ないので、今度1万円払ってくることにする。

【ネタバレ】翠星のガルガンティアと優生学

2018年の11月頃からNetflixで配信されている翠星のガルガンティアを少しづつ視聴していたが、12月頃末頃に観終わった。翠星のガルガンティアは2013年に放映されたアニメで、実は、当時もリアルタイムで観ていたのだが、再び視聴することで本作が傑作であることを再確認した。

翠星のガルガンティア コミック 1-3巻セット (角川コミックス・エース )

翠星のガルガンティア コミック 1-3巻セット (角川コミックス・エース )

 

本作には、優生学をテーマとしたシーンがあり、ちょうどそのときに読んでいた「RE:THINK: 答えは過去にある」という書籍で優生学について述べられていたので、いろいろ考えさせられた。

銀河宇宙同盟とヒディアーズ

細かいストーリ説明は割愛するが、翠星のガルガンティアの歴史背景としては、人類銀河同盟という主人公レドが所属する人間サイドの組織と、ヒディアーズという正体不明のエイリアンが大昔から激しい戦いを繰り広げているというものである。翠星のガルガンティアは、主人公レドがヒディアーズとの戦闘撤退時の亜空間航行に失敗し、人類の故郷たる地球へと迷い込むところから始まる。

人類銀河同盟における優生学

人類銀河同盟では、ヒディアーズとの激戦を生き残るため、資源の有効活用が至上命題とされていた。そこで、劣等な(ヒディアーズと戦闘できないと思われる)人類を切り捨ている。これはすなわち、優生学と呼ばれる考え方そのものである。優生学とは、優れた遺伝子のみを生存させることで社会構造を変革していこうという考え方であり、1883年にイギリスの科学者であるフランシス・ゴルトンが提唱した考え方である。

優生学とは、フランシス・ゴルトンのもともとの考えでは、進化とは即ち適者生存、不適者不生存であり、自然のランダムなふるまいに任せ、苦痛や死によってのみ起こる非常に残酷なものであるため、人工的に人に優しい進化を行おうというものであった。しかし、実際に優生学が実行された方法としては、ナチス・ドイツなどにみられる人権政策である。ヒトラー優生学の信奉者であり、優秀なアーリア人を残すためにホロコーストを行った。

銀河宇宙同盟では、不適格な人類は処分するという優生学的な考えで人類の選別を行っており、これは実のところホロコーストとかわりのないのではないだろうか。

ディアーズにおける優生学

ディアーズとはイカのような見目をした敵性エイリアンであるが、翠星のガルガンティアの話が進むに連れて、実は、人間が遺伝子操作によって進化し、宇宙空間でも生存できるようになった超人類であることが明らかになる。ヒディアーズはもともとはEvolverと呼ばれる革新団体で、地球滅亡を乗り切るために遺伝子操作によって超人類へ進化することで宇宙空間へ飛び出そうとしていた人間のことである。

おそらく、視聴者が翠星のガルガンティアを観て思うのは、遺伝子操作によって人間の形態を失いたくないというものであろう。しかし、レドの所属する人類銀河同盟では優生学的な考えのもと不適格な人類の切り捨てが日常的に行われていたらどうだろうか?もし、人類銀河同盟に切り捨てられる運命の人物がいて、Evolverに属して超人類に進化することで生存可能になるとしたらどうだろうか?

積極的優生学

人類の歴史を見てみると、ホロコーストなどのような消極的な優生学はすでに様々なところで実践され、今では禁忌とされている。しかし、遺伝子操作技術の革新により、遺伝子に改良を加えることでより適した遺伝子を持つ人類へと進化させることが可能になりつつある。

では、このような積極的に優勢な遺伝子を作り出していこうという行いについては、私達はどう考えるべきだろうか。遺伝的疾患を持つ胎児を治療することが許されるのならば、より知性の高く、肉体的に優れた人類を遺伝子操作によって作り出すことが許されるのではないか?

もし、優生学的な政策により切り捨てられるか、遺伝子操作によって生存の活路を見いだすかのどちらか一方を選択しなければならないとき、自分はどうするのだろうか。そのようなことを翠星のガルガンティアを観ながら考えていた。

しかし、チェインバーに搭乗できる可能性があるなら、人類銀河同盟も悪くないかもしれない。何故ならば、ラストのブリキ野郎のシーンはカッコ良すぎるのだ。

【読書メモ】RE:THINK: 答えは過去にある

過去のアイデアを再考する

新しいアイデアを生み出すことが技術や社会に革新をもたらすと私達は思うかもしれない。しかし、多くの場合、新規アイデアや新製品などは、過去に誰かが考案したものである。「RE:THINK: 答えは過去にある」ではそのような事実を指摘し、新規性も重要だが過去のアイデアを再考することも同様に重要であるとの気づきを与えてくれる。

ルネサンス期の新規性

古代ローマで哲学や科学や大きく進歩して、13世紀頃から16世紀頃にかけて、古代ローマの哲学や科学がヨーロッパに再輸入された。その頃の、最新科学と言えば古代ローマの知識のことであった。まさに、いにしえのファイナルファンタジーや、∀ガンダムの世界である。

ルネサンス時代、重力を発見した科学者がいた。かの有名なニュートンである。当時の先端科学と言えば、古代ローマ人の考えた知識のことであり、それこそが権威であったため、ニュートンは重力を自分の発見とするのではなく、古代ローマから考えられていたと嘘の説明しようとしていた。実際には、その説明はプリンキピアには載らなかったが、載せようといしていたそうだ。ニュートンは新たに発見を行ったが、昔は、過去のアイデアこそ最も考察すべき対象であった。

デモクリトス古代ローマの哲学者であり、原子論を提唱した人物でもある。しかしその原子論はデモクリトスの提唱後約2000年間も忘れ去られ、19世紀初頭になってようやくイギリスの科学者ドルトンが再び提唱し、20世紀頃に科学的に観測された。実は、この例のようなことが非常に多くある。

例えば、電子タバコや電気自動車などは、一度は失敗し頓挫したアイデアであるが、再考され広まったアイデアである。その他にも、ベーシックインカム、麻薬や覚醒剤の医療目的利用などなど、いろいろな物がある。アイデアは実は過去に様々考案されているが、それが重要かどうかは、その当時の社会規範、技術的限界、権力者などに依存して決定してしまう。新規性というのは、実は、過去にこそあるのかもしれない。

ここで、個人的に、本書の中でも特に面白かった民主主義について紹介しよう。

民主主義とは何なのか

現在の政治は、議会民主主義に則り代表者を選挙で選出して代表者が統治を行うものである。しかし、政府は裕福な利権団体の犬であり、専門職と化した政治家には2世、3世の議員が多く、自分たちの権力を永続化させることにしか興味がない。しかも、2〜4年周期で行われる選挙では、地球温暖化少子化といった長期にわたる政策はとれない。民主主義はすでに死んでいるのだ。実は、このような見解は、100年以上も前の19世紀頃から暗に陽に指摘されていたらしい。

ここで、古代アテネの考える民主主義についてみてみよう。古代アテネ(加えて大半のヨーロッパの時代)では、選挙は極めて貴族的な官僚選出方法だと考えられていた。貴族制とは即ち、人民なかで最良の人物に統治させることであり、選挙で最良の人物を選ぶことは貴族制に他ならなかった。

古代アテネでは主要な4つの都市のうち3つで、くじ引きによるランダムな選出を行って統治者を選んでいた。ランダムに複数人選べば、平均的には、人民の総意が政治に反映されると言えるのではないだろうか。そもそも、現代の議会民主主義は、貴族制なので再考すべきではないだろうか。

かなり過激な案ではあるが、民主主義というものをよく考えるためには面白い考えであると思う。この案ならば、大統領が暴走したり、ウォール街が利権を貪ったりはしないかもしれない。真実はわからないが、このように、過去には再考すべきアイデアが多く眠っている。温故知新である。

本書では、このように多くの過去のアイデアについて述べられており、なかなか楽しく読めた。他にも優生学については考えさせるところもあったので、また後日紹介したい。

炎と怒り トランプ政権の内幕 (早川書房)

炎と怒り トランプ政権の内幕 (早川書房)