プログラミング言語の形式的意味論入門

プログラミング言語の (形式的) 意味論とは、プログラムの動作を数学によって厳密に定義し、その性質について議論するための枠組みのことである。プログラムを数学の俎上に載せることにより、プログラムやプログラミング言語を厳密に理解し、解析し、これらについて推論することができるようになる。この分野は近年実用化に向けて進んでいる形式手法の礎となり、またそれ自体、様々な数学概念が飛び交う興味深い一分野を形成してきた。

本書は、Winskel によるプログラミング言語意味論の世界的標準教科書の邦訳である。前提知識をできるだけ少なくしつつ、プログラムの意味を数学的に定義・議論するための手法が解説されている。本書により、プログラミング言語理論関係の専門的な文献を読むための基礎を学ぶことができる。本書で身につけた基礎知識は、プログラミング言語研究の成果を理解し応用するために役立つはずである。

『プログラミング言語の形式的意味論入門』 (G.ウィンスケル 著、末永 幸平 監訳、勝股 審也、中澤 巧爾、西村 進、前田 敦司 訳、丸善出版、2023 年 1 月 30 日発売) は、プログラムの動作を数学で厳密に定義し、その性質を証明するための手法を扱う教科書の邦訳です。原タイトルは The Formal Semantics of Programming Languages: An Introduction です。版元の紹介文は、本書を Winskel によるプログラミング言語意味論の世界的標準教科書の邦訳と位置づけ、前提知識をできるだけ少なくしつつ、プログラムの意味を数学的に定義 / 議論するための手法を解説した本と説明しています。

全 12 章と付録の構成、集合論の基礎から情報システムまで

本論はまえがきに続く全 12 章と付録 A です。第 1 章「集合論の基礎」で論理の記法、集合、関係と関数を確かめ、第 2 章「入門: 操作的意味論」で簡易命令型言語 IMP の算術式とブール式の評価、コマンドの実行を規則として定めます。第 3 章「帰納法の原理」と第 4 章「帰納的な定義」は、数学的帰納法、構造帰納法、整礎帰納法、規則帰納法、最小不動点といった証明の道具を整える章です。続く第 5 章「IMP の表示的意味論」、第 6 章「IMP の公理的意味論」、第 7 章「ホーア規則の完全性」で、同じ IMP を別の 2 つの方法で意味づけます。第 8 章「領域理論入門」から後は、再帰方程式、再帰の技法、高階型を持つ言語、情報システムへ進み、付録 A「不完全性と決定不能性」で計算可能性と決定不能性、ゲーデルの不完全性定理を扱います。すべての章と付録の末尾に参考文献の節があり、巻末に参考文献、監訳者あとがき、索引が付きます。

操作的、表示的、公理的の 3 つの意味論で IMP を読む

操作的意味論は、プログラムがどう実行されるかを、状態の移り変わりや評価の規則として定めます。表示的意味論は、プログラムの各部分に数学的な対象を対応させ、IMP のコマンドであれば状態から状態への部分関数として、全体の意味を部分の意味から組み立てます。while ループの意味は、ループを 1 回展開した等式の解として定まり、その解を連続関数の最小不動点として取り出す道具が、第 5 章の節に並ぶ cpo と Knaster-Tarski の定理です。公理的意味論は、実行前に成り立つ条件と実行後に成り立つ条件の組でコマンドの性質を述べる方法で、第 6 章は表明言語 Assn と部分正当性のための証明規則、その健全性を扱います。第 5 章で操作的意味論と表示的意味論の等価性を示し、第 7 章はゲーデルの不完全性定理、最弱事前条件と表現可能性、検証条件、述語変換子を節に立ててホーア規則の完全性を論じます。

領域理論から再帰、値呼びと名前呼び、先行評価と遅延評価へ

後半は、関数が自分自身を呼び出す 再帰 による定義の意味を数学的に扱うための章が続きます。第 8 章は cpo の構成手法と連続関数を定義するためのメタ言語、第 9 章は言語 REC を題材に、値呼びと名前呼びのそれぞれについて操作的意味論と表示的意味論を与えてその等価性を示します。第 10 章は Bekić の定理、不動点帰納法、整礎再帰、第 11 章は先行評価と遅延評価の言語について 2 つの意味論の一致を確かめ、不動点演算子、観測と完全抽象性、直和を扱います。完全抽象性とは、表示的意味論で同じ意味を持つことと、どの文脈に置いても観測上区別できないこととが一致する性質です。第 12 章は再帰型と情報システム、閉集合族と Scott 前領域を扱います。

形式手法と静的解析を支える意味論、前提とする知識

版元の紹介文は、プログラミング言語の意味論を形式手法の礎となる分野と説明しています。プログラムを実行せずに性質を推論する 静的解析 や検証の技術は、何をもって正しいとするかをプログラムの意味の定義に拠っており、意味論はその定義を与える コンピューターサイエンス の一分野です。本書は第 1 章の集合と論理の記法から始まり、第 2 章で操作的意味論に入った後、帰納法の原理と帰納的な定義を独立した 2 つの章で整えます。

版元の紹介文は、本書でプログラミング言語理論の専門的な文献を読むための基礎を学べると述べています。小さな命令型言語 IMP に 3 つの意味論を与えて比べる前半と、領域理論から再帰、高階型を持つ言語へ進む後半が 1 冊に収まり、各章の末尾に参考文献の節が置かれています。