プログラミング言語の形式的意味論入門(プログラミングゲンゴノケイシキテキイミロンニュウモン)

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

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

「このプログラムは正しく動く」と主張するとき、その「動く」は何によって定義されているのか。この問いに数学で答えるのがプログラミング言語の形式的意味論で、本書はその分野で世界的な標準教科書と目される G.ウィンスケルの著作の邦訳です。末永幸平氏をはじめとするプログラミング言語理論の研究者たちの手で訳され、丸善出版から 2023 年 1 月に刊行されました。プログラムの動作を厳密に定義し、その性質を証明の対象にするための道具立てを、腰を据えて学ぶための本です。

内容は、プログラムの意味を数学的に定義するための代表的な手法を、できるだけ少ない前提知識から積み上げていく構成です。操作的意味論・表示的意味論・公理的意味論という主要なアプローチを軸に、帰納法による定義と証明の技法が繰り返し登場します。「入門」と冠されてはいるものの、集合と論理の記法に耐性があり、定義と定理を一行ずつ追う読み方を厭わないことが実質的な前提で、コード例で学ぶタイプの技術書とは読書体験がまったく違います。

この投資が効くのは、 Coq や Agda といった定理証明支援系に触れて背後の理論を知りたくなった人、プログラム検証や形式手法を仕事や研究で扱う人です。読み通せば、プログラミング言語理論の専門的な論文や文献が「読める記号の列」に変わる地点まで到達できます。急がば回れを地で行く、基礎体力づくりのための教科書です。