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

発売日 : 2023年01月30日

著者／編集 : G.ウィンスケル/末永　幸平/勝股　審也/中澤　巧爾/西村　進/前田　敦司

出版社 : 丸善出版

発行形態 : 単行本

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

まえがき
第1章 集合論の基礎
1.1 論理に関する記法／1.2 集合／1.3 関係と関数／1.4 参考文献
第2章 入門：操作的意味論
2.1 IMP――簡易命令型言語／2.2 算術式の評価／2.3 ブール式の評価／2.4 コマンドの実行／2.5 簡単な性質の証明／2.6 別の操作的意味論／2.7 参考文献
第3章 帰納法の原理
3.1 数学的帰納法／3.2 構造帰納法／3.3 整礎帰納法／3.4 導出に関する帰納法／3.5 帰納的定義／3.6 参考文献
第4章 帰納的な定義
4.1 規則帰納法／4.2 特殊な規則帰納法／4.3 操作的意味論のための証明規則／4.4 演算とその最小不動点／4.5 参考文献
第5章 IMPの表示的意味論
5.1 動機／5.2 表示的意味論／5.3 二つの意味論の等価性／5.4 cpoと連続関数／5.5 Knaster-Tarskiの定理／5.6 参考文献
第6章 IMPの公理的意味論
6.1 基本的なアイデア／6.2 表明言語Assn／6.3 表明の意味論／6.4 部分正当性のための証明規則／6.5 健全性／6.6 ホーア規則の使い方の例／6.7 参考文献
第7章 ホーア規則の完全性
7.1 ゲーデルの不完全性定理／7.2 最弱事前条件と表現可能性／7.3 ゲーデルの不完全性定理の証明／7.4 検証条件／7.5 述語変換子／7.6 参考文献
第8章 領域理論入門
8.1 基本的な定義／8.2 例：ストリーム／8.3 cpoの構成手法／8.4 連続関数を定義するためのメタ言語／8.5 参考文献
第9章 再帰方程式
9.1 言語REC／9.2 値呼びの操作的意味論／9.3 値呼びの表示的意味論／9.4 値呼びの二つの意味論の等価性／9.5 名前呼びの操作的意味論／9.6 名前呼びの表示的意味論／9.7 名前呼びの二つの意味論の等価性／9.8 局所的な関数定義／9.9 参考文献
第10章 再帰の技法
10.1 Bekićの定理／10.2 不動点帰納法／10.3 整礎帰納法／10.4 整礎再帰／10.5 演習を一つ／10.6 参考文献
第11章 高階型を持つ言語
11.1 先行評価のための言語／11.2 先行評価の操作的意味論／11.3 先行評価の表示的意味論／11.4 先行評価の意味論の一致／11.5 遅延評価のための言語／11.6 遅延評価の操作的意味論／11.7 遅延評価の表示的意味論／11.8 遅延評価の意味論の一致／11.9 不動点演算子／11.10 観測と完全抽象性／11.11 直和／11.12 参考文献
第12章 情報システム
12.1 再帰型／12.2 情報システム／12.3 閉集合族とScott前領域／12.4 情報システムのなすcpo／12.5 情報システムの構成／12.6 参考文献
付録A 不完全性と決定不能性
A.1 計算可能性／A.2 決定不能性／A.3 ゲーデルの不完全性定理／A.4 万能プログラム／A.5 Matijasevicの定理／A.6 参考文献
参考文献
監訳者あとがき
索引

G.ウィンスケル

Winskel, G. (Glynn)

末永　幸平

末永, 幸平

勝股　審也

勝股, 審也

中澤　巧爾

中澤, 巧爾

西村　進

西村, 進

前田　敦司

前田, 敦司