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

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

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

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

論理学入り口

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

論理学をつくる

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

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

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

論理学の奥地へ

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

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

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

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

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

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

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

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

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

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

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