Preface: 前書き
これは「ソフトウェアの基礎」という、高信頼ソフトウェアの数学的基礎に関するシリーズの導入です。
このシリーズでは、論理、コンピュータによる定理証明、証明支援系Coq、関数型プログラミング、操作的意味論、プログラムの推論のための論理、そして静的型などの基礎を学ぶことができます。
読者は、学部生から博士課程の学生や研究者に至るまでの広範囲を想定しています。
論理学やプログラミング言語についての知識は仮定しませんが、ある程度の数学的素養は理解に有用です。
このシリーズの特徴は、取り扱う内容がすべて形式化されて、さらに機械によって確かめられることです。
これは、それぞれのテキストがCoqのスクリプトファイルそのものとなっていることで実現されています。
このシリーズでは、Coqのインタラクティブモードを横で動かしながら（またはエディタで一行ずつ進めながら）読み進めることを想定しています。
内容の細部まですべてCoqで形式化され、また演習もCoqを使って行うように設計されています。
それぞれの本は、主要部とそれ以外の「派生」からなります。
主要部は1学期分の講義として十分な量が、順序だって記述されています。
また、派生部分は主要部に関連する項目をカバーしています。
主要部は学部後半の学生や院生にちょうどいい内容でしょう。
この本「論理の基礎(Logical Foundations)」は 、シリーズの他の本の基盤であり、関数型プログラミング(functional programming)や構成的論理(constructive logic)、証明支援系 Coq に関する導入となっています。
信頼性の高いソフトウェアを構築することは実に困難です。
現代のシステムは大きく複雑に、関係者の数は膨大に、さらには要求も多岐にわたっています。
これらが原因で、100パーセント正しいもの以前に、ある程度うまく動くソフトウェアを構築することでさえも難しくなっています。
同時に、情報処理が社会の至る所に利用されることで、バグや不具合によるコストが増大し続けています。
計算機科学者やソフトウェア技術者は、これらの問題に対し、ソフトウェアの信頼性を向上させる技術として、プロジェクトチーム管理手法（例：extreme programming）、ライブラリの設計思想（例：モデル-ビュー-コントローラ、出版-購読(publish-subscribe)など）、プログラミング言語（例：オブジェクト指向プログラミング、アスペクト指向プログラミング、関数型プログラミングなど）、ソフトウェアの性質を表現する数学的手法、記述した性質を確かめるためのツール、と多岐にわたる技術を開発してきました。
「ソフトウェアの基礎」ではこれらのうち最後の技術群（数学的手法および性質検査）について学びます。
このテキストは次の3つのコンセプトから構成されています：
(1) 「論理」を基にして、プログラムに対する正確な言明を記述し、確かめる。
(2) 「証明支援系」により、厳格で論理的な主張を構成する。
(3) 「関数型プログラミング」によって、推論しやすいプログラミングを行い、さらに論理との橋渡しを行う。
この講義以降に読むとよい本については、Postscriptの章に記載しています。
これらの本の参照情報はBibファイルにあります。
論理とは、「証明」を対象とした学問領域です。
ここでいう証明とは、特定の命題が真実であることの、反証しようのない根拠を指します。
計算機科学において論理が果たす役割に関しては、非常にたくさんの文献で述べられています。
MonnaとWaldingerは、この役割を"計算機科学における微積分学"と呼び、またHalpernらの論文「On the Unusual Effectiveness of Logic in Computer Science」では論理から出てきたいくつもの重要な道具や洞察が紹介されています。
この論文にはこうあります。
"実際のところ、論理は数学においてよりはるかに計算機科学において有効活用されている。
特筆すべきなのは、このことが、論理が数学から生まれて100年における、論理の発展の大きな推進剤になっていることである。"
特に、帰納法の原理は計算機科学の世界においてあまねく存在します。
離散数学やアルゴリズムの解析において見てきたかもしれませんが、このコースではこれまでよりも深くまで利用することになるでしょう。
論理と計算機科学の間の影響は一方方向ではありません。
計算機科学もまた論理の発展に寄与してきました。
そのうちの一つが、論理命題に対する証明の構築を助けるソフトウェアの開発です。
これらのソフトウェアは大きく二種類に分類されます。
このコースは、Coqを用いて進めていきます。
Coqは1983年から開発されている証明支援系で、近年研究・工業両面で大きなコミュニティが形成されています。
Coqの提供する機能は、機械検証された形式推論の対話的な開発に有効です。
Coqの核(kernel)は、演繹が正しく進められているかを確かめるだけの、シンプルな証明検査器です。
Coqは、この核を基礎として、証明の構築に便利な機能を提供しています。
この機能には、例えばよく使われる定義や性質のライブラリ、複雑な証明を半自動で生成するタクティク、ある特定の証明を自動化するタクティックを記述することに特化したプログラミング言語、といったものがあります。
Coqは計算機科学と数学を通じて、多くのことを実現してきました。
ところで、このソフトウェア"Coq"という名前がどこから来たか疑問に思うかもしれません。
INRIA（Coqを主に開発しているフランスの国立研究機関）にあるオフィシャルのwebサイトでは次のように説明されています。
「一部のフランスの計算機科学者には、作ったソフトに動物の名前を付ける伝統があります。
例えばCaml（訳注：ラクダ・英語のcamel）、Elan（訳注：ヘラジカ）、Foc（訳注：アザラシ・フランス語のphoqueと音が同じ）、Phox（訳注：キツネ・英語のfox）などがこの暗黙の了解に従っています。
フランス語で'coq'は雄鶏を意味し、また音がCoqの基礎であるCalculus of Constructionsの頭文字(CoC)と似ています。」
なお、雄鶏はフランスのシンボルでもありますし、またCoqという並びはThierry CoquandというCoqの初期の開発者の名前の三文字でもあります。
- 「自動定理証明器」は"開始ボタン"によって証明の構築を行います。
証明器に命題を与えると、証明器はその命題について「真」か「偽」（場合によっては「不明：時間切れ」）を返します。
証明器の能力が発揮できる範囲はまだ限定されてはいますが、近年急速に発達し、様々な用途に使われています。
例としては、SATソルバー、SMTソルバー、モデル検査器が挙げられます。
- 「証明支援系」は単純な操作を自動化し、難しい部分を人間が指示するというハイブリッドなツールです。 広く使われている証明支援系には、Isabelle、Agda、Twelf、ACL2、PVS、Coqなどがあります。
- 「プログラミング言語をモデル化する基盤」として、複雑な言語の記述と推論に用いられています。
例えばJavaCardプラットフォームにおいて、Common Criteria Certificationの最高レベルを得るためにセキュリティの検査に利用されたり、x86やLLVMの命令セット、Cなどのプログラミング言語に対する形式仕様を与えたりしています。
（http://www.commoncriteriaportal.org/products/ や http://www.commoncriteriaportal.org/cc/ のPart.3を参照のこと。）
- 「検証付きソフトウェア・ハードウェアの開発環境」として、CompCertという最適化も含めたCの検証付きコンパイラの開発、CertiKosという検証付きハイパーバイザ、浮動小数点数を使った繊細なアルゴリズムの正しさの証明、また暗号化アルゴリズムのセキュリティ検査の環境CertiCryptの基盤として使われています。
また、オープンソースのRISC-Vプロセッサにおいて、検証付き実装を作るために使われています。
- 「現実的な依存型付きの関数型プログラミング環境」として、非常に多くの革新を起こしています。
例えば、ハーバード大学で行われたYnotシステムでは「関係ホーア推論(relational Hoare reasoning)」（このコースで説明する「ホーア論理」の拡張）をCoqに埋め込んでいます。
- 「高階論理の証明支援系」として、いくつもの数学における重要な性質を検証しました。 例えば、証明に複雑な計算を組み込めたので、四色定理(4-color theorem)の最初の形式検証された証明作ることができました。 この証明は一時議論を呼びました。 というのも、この証明にはプログラムを使った大量の背景の検証が含まれていたためです。 Coqによる検証では、計算部分を含む全てのものが検査されます。 最近では、Feit-Thompsonの定理のCoqによる定式化が行われました。 これは、有限単純群の分類における第一歩です。
「関数型プログラミング」という語には、どの言語でも使えるプログラミング手法としての用法と、これらの手法に重点を置いたプログラミング言語としての用法があります。
なお、後者における言語としては、HaskellやOCaml、Standard ML、F#、Scala、Scheme、Racket、Common Lisp、Clojure、Erlang、そしてCoqが挙げられます。
関数型プログラミングは数十年にわたって開発されてきました。
そのルーツは、1930年代初頭、最初の（少なくとも電気的なものとしての）コンピュータが開発されるより前、チャーチが提案したラムダ計算までさかのぼります。
しかし、1990年初めから、エンジニアや言語設計者の関心を引き、またJane St. CapitalやMicrosoft、Facebook、Ericssonなどの企業で重要な役割を担っています。
関数型プログラミングの基本となる信念は、可能な限り計算は「純粋(pure)」であるべき、というものです。
純粋であるとは、その実行が結果となる値を返すだけ、ということです。
つまり、計算には入出力や変数への代入、ポインタの書き換えなどといった「副作用(side effect)」を含まないようにすべき、ということを意味します。
例えば、「命令的(imperative)」ソートでは、受け取ったリスト内のポインタを張り替えてソートするでしょうが、純粋なソートでは受け取ったリストとは違う新しいリストをソートした上で返すでしょう。
関数型プログラミングのスタイルにおける大きな利点は、プログラムの理解を容易にすることです。
もし全ての操作が既存のデータから新しくデータを作り、既存のものに手を入れないなら、それがどこで保持されていて、そこで変更が影響を及ぼすのか、その影響で他が依拠している条件から逸脱しないか、などを気にする必要がありません。
こういった問題は特に並行システムにおいて顕著で、複数のスレッドから参照される変更可能な状態は、悪質なバグの原因になり得ます。
実際、現場での関数型プログラミングにおける関心の多くが並行性におけるこの単純な振る舞いに向いています。
関数型プログラミングの流行の理由の他の理由としては、（関数型プログラミングという語の）最初の用法と関連しますが、関数型プログラムはしばしば対応する命令的なものに比べて非常に容易に並列化可能です。
もし計算が結果を出すこと以外なにも影響を与えないならば、それは「どこで」計算しても構わないことになります。
同様に、データ構造が破壊的に変更されないならば、CPUのコア間やネットワーク間で自由にコピーできます。
実際、「MapReduce」というHadoopのような大規模分散クエリ処理系の核にある考え方は、関数型プログラミングで古くからある例の一つです。
関数型プログラミングには、非常に重要な役割がもう一つあります。
論理と計算機をつなぐという役割です。
Coqは小さく、しかし表現力豊かな関数型言語と、論理的表明を記述、証明するツールの組み合わせと言えます。
加えて、より詳細を見ていくと、その二つの側面が同一の機構、つまり「証明はプログラムである」というものであることがわかります。
この本は単体で読めるようにしてありますが、それぞれの内容でより進んだ話を見たければ、Postscript章に挙げた参考文献を見ると良いでしょう。
章と章の間の依存関係をまとめた図と、代表的な学習の流れを、deps.htmlにまとめてあります。
Coqは、WindowsやLinux、macOSで動きます。
以下のソフトを用意しましょう。
- Coqホームページにある最新版のCoq。
全てのサンプルソースはバージョン8.8.1でコンパイルできることが確認されています。
（訳注：翻訳チームは8.8.2でコンパイルできることを確認していますが、QuickChickの章は8.9や8.9.1でコンパイルできないことを確認しています。）
- Coqを対話的に操作するIDE。
現在、以下の二つから選択できます。
- ProofGeneralは、Emacs上に作られたIDEです。
すでにEmacsに慣れている人向けのものです。
Coqとは別にインストールする必要があります。
（詳しくはgoogleで"ProofGeneral"を検索してください）
冒険心のある人向けに、Coq用のEmacs拡張として company-coq や control-lock というものもあります。
- CoqIDEは、スタンドアロンで動作するシンプルなIDEです。
Coqと一緒に配布されているので、Coqをインストールすれば使えるはずです。
1からビルドし直すこともできますが、環境によってはGUIライブラリなどの追加パッケージをインストールする必要があります。
CoqIDEを選ぶ場合は、「非同期(asynchronous)モード」や「エラー復元(error resilience)モードを無効にした方がいいでしょう。 その場合は以下のように起動します。
coqide -async-proofs off -async-proofs-command-error-resilience off Foo.v &
- ProofGeneralは、Emacs上に作られたIDEです。
すでにEmacsに慣れている人向けのものです。
Coqとは別にインストールする必要があります。
（詳しくはgoogleで"ProofGeneral"を検索してください）
この資料の各章には、たくさんの練習問題がついています。
練習問題についている「スターレーティング」には、以下のような意味があります。
また、いくつかの練習問題には「advanced」や「optional」とついています。
これらの付いていない問題だけで広範囲の内容を学習できます。
「optional」な練習問題は重要な概念へのさらなる演習と、また主題とは少し異なる内容への導入となります。
「advanced」な練習問題は、さらに難しい問題がほしい読者へのものです。
結果として、この教材のより深い理解が得られるでしょう。
注意：
- ★：多くの読者が1～2分でできる簡単な問題。
読者は、この問題に取り組んで、このレベルの問題に慣れておくべきです。
- ★★： 素直で簡単な問題（5～10分でできるでしょう）
- ★★★： 少し考えないといけない問題（10～30分ほどかかるでしょう）
- ★★★★（または★★★★★）： さらに難しい問題（30分以上）
##############################################################################
### 絶対にこの教材の練習問題の解答を皆に見える場所には置かないでください！ ###
##############################################################################
ソフトウェアの基礎は自学用と講義用の側面があります。
講義の視点では、解答に安易に接することができるのは有効ではありませんし、またこれらの問題は単位認定に関わる課題となります。
これらの解答を、検索エンジンによって見つけられる場所に置いたりしないでください！
この教材のリリース版のソース（CoqスクリプトとHTMLファイル）をtarで固めたものが、 http://softwarefoundations.cis.upenn.edu から取得できます。
講義でこの本の一部だけを使用している場合、講師からリリース版の代わりに使う変更版について説明されると思います。
学期の途中で変更される可能性があるでしょうし、公開されている版ではなく、その変更版を利用してください。
Sample Exams
「論理の基礎」を元にした集中講義（DeepSpec summer schoolの一部）の様子が https://deepspec.org/event/dsss17/ と https://deepspec.org/event/dsss18/ から見られます。
2017年版の最初の方は画質が悪いのですが、後の講義になるに従って徐々に良くなっていきます。
この資料を自分のコースで使おうと思った場合、ほぼまちがいなく書き直しや追加したいところが出てくるでしょう。
そういった貢献は大歓迎です。
法的関係を容易にし、またライセンス条項や部分的なライセンスなどの調整などが必要なときの責任の所在を明確にするため、
全ての貢献者（開発者リポジトリへのアクセス権を持っている人）に対して、それぞれの貢献への著作権を以下の "author of record" へ割り当てることを求めます。
貢献するには、自己紹介、どのように利用するかと共に、(1) 上の著作権譲渡文（訳注：必ず原文です）、(2) githubのユーザ名、の二つをBenjamin Pierceまでemailで送ってください。
そうすれば、gitのリポジトリとメーリングリストへのアクセス権を設定します。
リポジトリには、INSTRUCTORSファイルがありますので、次にどうすべきかはそれを参照してください。
- I hereby assign copyright in my past and future contributions
to the Software Foundations project to the Author of Record of
each volume or component, to be licensed under the same terms
as the rest of Software Foundations. I understand that, at
present, the Authors of Record are as follows: For Volumes 1
and 2, known until 2016 as "Software Foundations" and from
2016 as (respectively) "Logical Foundations" and "Programming
Foundations," and for Volume 4, "QuickChick: Property-Based
Testing in Coq," the Author of Record is Benjamin C. Pierce.
For Volume 3, "Verified Functional Algorithms", the Author of
Record is Andrew W. Appel. For components outside of
designated volumes (e.g., typesetting and grading tools and
other software infrastructure), the Author of Record is
Benjamin Pierce.
（訳注：契約の条文であるため、原文をそのまま載せています。 参考のために以下に大まかな翻訳を載せていますが、もし条文を利用する立場になる（＝貢献者になる）場合は、原文をよく読み、原文の解釈を基に行動してください。 日本語翻訳チームはこの翻訳により発生したいかなる問題についても、一切の責任を負いません。）私は今後、Software Foundationsプロジェクトに対するこれまでとこれからの貢献について、著作権をそれぞれの分冊または一部のAuthor of Recordに譲渡します。 私は現在のAuthor of Recordが次の通りであることを理解しています。 ボリューム1と2、2016年までは"Software Foundations"（ソフトウェアの基礎）、2016年からはそれぞれ"Logical Foundnations"（論理の基礎）と"Programming Foundations"（プログラミングの基礎）と呼ばれるもの、そしてボリューム4 "QuickChick: Property-Based Testing in Coq"（Coqにおけるプロパティベーステスト）について、Author of RecordはBenjamin Pierceです。 ボリューム3 "Verified Functional Algorithms"については、Author of RecordはAndrew W. Appelです。 これらのボリューム以外の要素（例：組版、評価用ツール、その他のソフトウェア基盤）についてのAuthor of RecordはBenjamin Pierceです。
ボランティアによる翻訳のおかげで、「ソフトウェアの基礎」は http://proofcafe.org/sf から日本語で読めます。
中国語の翻訳も進行中で、状況を https://coq-zh.github.io/SF-zh/ から見られます。