C90: 「簡約!? λカ娘 9」 が出ます

C90の三日目(2016/08/14(日))に、サークル「参照透明な海を守る会」から『簡約!? λカ娘 9』が出ます。場所は「西地区f32a」です。

<簡約!? λカ娘 9> 内容紹介
第 1 章 λカ娘探索ファイナル (@ark_golgo)
第 2 章 変態する昆虫の観察 (@master_q)
第 3 章 IST(Internal Set Theory) 入門 (前編) (@dif_engine)

第 3 章の『 IST(Internal Set Theory) 入門 (前編) 』が私の記事です。

以下、いくつかの記事について簡単な紹介をします。自分が書いた記事以外はどれも「ちゃんと理解できていない」ので、自分の理解の程度に応じた紹介となります。ご了承ください。

第1章 λカ娘探索ファイナル
AlphaGo が凄いということはみなさんもご存知かと思いますが、では一体どこがどのように凄いのでしょうか?この記事ではコンピュータ囲碁の研究をしている荒木さんによって、コンピュータ囲碁の歴史とAlphaGoの強さの本質、そして将来のコンピュータ囲碁の展望が語られています。

第2章 変態する昆虫の観察
組み込み系のChibiOS/RT というOSは独自の(非POSIXの)スレッド機構を持ち、グローバルロック状態に応じて呼び出せるシステムAPIが変わるのだそうです。間違ったシステムAPIの呼び出しは未定義の挙動を引き起こすのですが、このたぐいのコーディングミスは実行時ではなく、コンパイル時にわかってほしいものです。そのための方法の一つはプログラムの静的なチェックを強化することです。岡部さんの方針は、この静的なチェックのためにATSを使うというものです。(この場合、ATSは最終的にC言語のソースコードを生成します。)

第3章 IST(Internal Set Theory) 入門 (前編)
Edward Nelson によって創始された超準集合論であるInternal Set Theory (以下、IST)という理論があります。
「ふつうの」超準解析、例えば齋藤正彦やM・デービスや中村徹の超準解析の本では、通常の集合論宇宙の超積を使って超準宇宙を作ります。
これに対し、NelsonによるISTにおいては、通常の集合論宇宙が超準宇宙に該当します。この宇宙の中に、一種のミニチュア宇宙が存在し、そこには空集合からスタートして集合論公理を有限回使って到達できるもの全てが含まれています。ISTでは、その意味で超準化という手続きは「すでに終わっている」ので超準宇宙の構成の議論は必要ありません。また、ISTはZFCの保存拡張になっているため、ZFC集合論での全ての定理はISTの定理でもあります。
(超積による超準宇宙の構成では正則性公理(基礎の公理)が省かれることがあります。したがって、ZFC集合論における議論を修正しないとZFC宇宙における定理を超準宇宙に輸入できないことがあります。)

このように言うとISTには良いことしかないようですが、NelsonのIST論文は若干読みにくいところがあります。それは、(1)読者に数理論理学の基礎的教養を要求している (2)ZFCにおける有限性のやや深い理解を要求している ところから来ているのではないかと思います。

(1)に関して言えば、ISTの公理図式は、量化子を「St付き」に変更するような操作を要求しており、論理式をオブジェクトとみなす視点が必要です。(2)に関して言えば、”直観的には”無限集合にしかなり得ない巨大な集合が有限集合であることがISTでは示されたりします。そして、そのようなことがISTにおける議論において有効に利用されたりする場面があります。このため、ISTを学ぶ人は「有限性とはなんだったのか」と悩むことになるでしょう。ISTにおける「有限性」の奇妙さに関連して、Nelson自身は次のような言葉を残しています:

—Perhaps it is fair to say that “finite” does not mean what we have always thought it to mean. What have we always thought it to mean?
I used to think that I knew what I had always thought it to mean, but I no longer think so. In any case, intuition changes with experience.

(1)も(2)もそれぞれ数理論理学と公理的集合論の基本的な教科書を読めば済む話なのですが、なかなか大変です(大変でした)。この章を読みこなせばNelsonによるISTの論文を読むための最低限の知識が得られる、そんな線を狙って執筆しました。なお、この(1)(2)を丁寧に説明しすぎて、肝心のISTの解説には入ることができなかったので「前編」とさせて頂きました。(後編は来年の予定です)。

表紙
久しぶりに表紙絵を描きました。「このすば」のめぐみんの衣装を着たイカ娘です。

簡約!? λカ娘 9 表紙

簡約!? λカ娘 9 表紙

簡約!? λカ娘 Go! (C84)

C84の三日目(2013/08/12(月))に、サークル「参照透明な海を守る会」から『簡約!? λカ娘 Go!』が出ます。C82の『簡約!? λカ娘(算)』に引き続き、この本にも記事を書かせて頂きました。元々はこの一つ前のC83(2012年冬)のために用意していた記事ですが、諸事情により期限までに書くことができませんでした。今回の記事は去年の冬のために用意していた原稿に大幅に書き足して完成させたものです。

<簡約!? λカ娘 Go!> 内容紹介
第1章 めたせぴ☆ふぁうんでーしょん
第2章 jhcコピペ
第3章 侵略者と転校生とアイドルとイカが再帰を学ぶそうですよ!
第4章 殺物語  ←私の記事です
第5章 λカ娘探索?
第6章 ロマンティック・パージング
第7章 HaskEll Shaddai

第四章の『殺物語』が私の記事です。ストーリー部分は『簡約!? λカ娘(算)』に書いた『蓮物語』の続編になっていますが、数学やプログラミングの話題に関する部分は、『蓮物語』を読んでいなくても問題なく読めるように書いてあります。

『殺物語』 内容紹介
Haskellや圏論についてある程度理解している「私」が、モナドについて質問しにきた下級生に説明する話です。内容をもう少し具体的に要約すると、圏を導入し、Haskellの圏Haskを導入し、その上でKleisli圏に関連付けてモナドを説明しています。圏論は自然変換のあたりまで説明しています。こう要約すると短い記事になりそうなものだと思えてくるのですが、会話形式で書いたためか予想外にページが増えました(約50ページ)。圏Haskを圏論の議論の動機付けや理由付けとしてとりあげ、圏論を学ぶ際の「例が簡単すぎるか(数学的な前提知識が)高度すぎるかのどちらかになりがち」というハードルをいくらかでも緩和しようと試みています。

想定した読者
C82の『簡約!? λカ娘(算)』に私が書いた『蓮物語』は、数学科の平均的な大学二年生に期待されている程度の理解力を持つ「僕」が、はじめてHaskellと圏論に触れ、Haskellのアプリカティブファンクターの振る舞いを理解しようとする話でした。これはこれで一貫した姿勢で書いたものであり、自分では気に入っています。しかし、わかりにくいという読者も多かったようです。プログラミングという話題そのものが特殊ですから、誰にもわかる、というのはそもそも望むべきではないかもしれませんが、もう少し多くの人に理解してもらえる記事を書きたくなりました。反省してみると『数学科の平均的な大学二年生に期待されている程度の理解力を持つ「僕」』のあたりがハードルを高くしていたらしいので、今回は読者に要求する数学のレベルをやや下げました。そのかわりにHaskellの入門書(具体的には『すごいHaskellたのしく学ぼう!』ぐらいの本)を一冊はなんとなく読んだ、というぐらいのレベルの理解を前提としました。

なんでタイトルがモナドと関係無さそうな『殺物語』なの?
数学やプログラミングとは関係ない理由です。前回の『蓮物語』は、西尾維新の『化物語』の二次創作という体裁になっていました。『化物語』の主人公である阿良々木暦は原作でも数学が得意だという設定なので、『数学ガール』の「僕」の役割を果たすのに丁度良かったのです。タイトルはHaskellから取って『蓮物語』に決めていましたが、Haskellだから蓮、という以外に何か欲しくなり、記事を書いたときに大流行していた(そしてまだ流行している)近未来を舞台にしたサイバーパンクニンジャ活劇小説『ニンジャスレイヤー』の主役を改変した「ハスケルスレイヤー」を登場させました。本家の主人公・ニンジャスレイヤーのメンポ(面頬)に「忍」「殺」と刻まれているのが印象的だったので、ハスケルスレイヤーのメンポには「蓮」「殺」と刻まれていることにしました。『蓮物語』では構成上、いきなり出てきていきなり倒されるキャラクターだということもあり、『ニンジャスレイヤー』の主人公そのものを登場させたくはなかったというのも改変キャラにした理由です。というわけで、『蓮物語』の続編であることから、ハスケルスレイヤーのメンポの二文字目「殺」をタイトルに入れました。

☆追記(2013/08/24) 若干の誤記がありました。お詫びと訂正→『殺物語』 正誤表

他の記事について
『簡約!? λカ娘 Go!』は全部で168ページもあります。あまり薄い本じゃない感じですね。執筆者による自記事紹介がすでにいくつかあります:

“簡約!? λカ娘 Go!”の紹介とAjhcプロジェクト近況
簡約!? λカ娘 Go!に「きつねさんでも分かるLR構文解析」書きました

以下、いくつかの記事について簡単な紹介をします。自分が書いた記事以外はどれも「ちゃんと理解できていない」ので、自分の理解の程度に応じた紹介となります。ご了承ください。

第1章 めたせぴ☆ふぁうんでーしょん
あまり有名ではありませんが、jhcというHaskellコンパイラが存在します。著者の @master_q さんはこのコンパイラに非常に強い関心を持ち、UnixライクなフリーOSをHaskellで実装するという野心的なプロジェクトを立ち上げています。野心的、というのは少々の工夫で片付くレベルではないからです。しかしながら、まったく無謀な試みというわけでもないことが、今回の @master_q さんの記事を読めばわかるかもしれません。記事の著者の @master_q さんは組み込み系の仕事をなさっていた方で、デバイスドライバのようなものを書くために必要な kernel ドメインでのプログラミングに強く型付けされた言語を使えないかと数年間考え(過去に @master_q さんが『λカ娘』に書いた記事の全てにこのような問題意識が関わっています)、スナッチ設計というアプローチにたどり着きました。このスナッチ設計が上手く行けば、漸進的にUnixライクなOSをHaskellでリライトでき、めでたく kernel ドメインのプログラミングに強く型付けされた言語を使えるはずです。この記事の議論の詳細を理解するためには低レイヤの部分で何が起こっているかをよく知っている必要があると思います。(というわけで、私には議論の細部を理解することができませんでした。)

タイトルに含まれる「ふぁうんでーしょん」は『銀河帝国興亡史』という通称で親しまれているアイザック・アシモフの有名な未来史のSFシリーズに由来します。『銀河帝国興亡史』は、統計力学と心理学を合わせたような「歴史心理学」を発展させた数学者ハリ・セルダンが銀河帝国の崩壊を予見し、帝国の崩壊後の文明再生の核となる組織「ファウンデーション」を作るところから話が始まります。(型付けが弱い)C言語を基礎としたUnix帝国の崩壊後の、kernelレベルプログラミング再生のための礎を築こうという意気込みが反映されたタイトルです。

第3章 侵略者と転校生とアイドルとイカが再帰を学ぶそうですよ!
リストのように、型そのものが再帰的な構成によって定義される事があります。このような構成を一般化したものとして、再帰スキームというものがあるのだそうです。このような再帰スキームが、たとえば foldr のような再帰関数の高レベルな一般化であることや、再帰スキームを利用して型を定義したときにテストをする方法などが紹介されています。

第4章 殺物語
「——それで翼さん、Haskell のモナドって何でそんなにすごいんですか?」
突然の訪問者は、忍野扇だった。圏論とモナドの解説のあと、忍者が出て殺す!

第5章 λカ娘探索?
囲碁というゲームがありますね。見かけはよく似ている(?)オセロなどと違い、囲碁をコンピュータで解析するのは難しいのだそうです。この記事では囲碁を解析するためになされてきたいくつかの工夫が解説されています。

第6章 ロマンティック・パージング
コンパイラの教科書には LL だとか LR だとか LALR のような術語が登場します。そんなわけで、コンパイラの授業を受けた人はこれらの用語やオートマトンについてよく知っていることが期待されるわけです。現実には、これらの話はなかなか面倒で、ただ本を眺めているだけでは身につきません。(身につきませんでした。)この記事では二人(二匹?)のきつねさんが会話しながらLR構文解析について勉強します。きつねでもわかるのだから人間である自分にもわかるはずだ、そんな希望と期待を抱かせてくれる記事です。

第7章 HaskEll Shaddai
オブジェクト指向プログラミングでは、しばしば個々のオブジェクトの属性を setter/getter 関数で読み書きします。このようなプログラミングスタイルは、オブジェクトが状態を持つ事を前提としています。したがって、参照透明性を基礎とするHaskellで setter/getter のようなものを書くには工夫が必要です。Lensはそのような工夫の一つです。この記事の著者である@fumieval さんのブログ記事『Freeモナドでゲームを作ろう!第2回: 本当に動かす 』でもこのLensについての概観が与えられていますが、『HaskEll Shaddai』ではもう少し深く掘り下げて機能が説明されており、Webスクレイピングのサンプルなどが与えられています。

表紙
今回は、表紙の絵も書かせて頂きました:
pixiv: λカ娘c84表紙絵  簡約!? λカ娘 Go!
表紙絵は裏表ひとつづきになっています。