数学的基礎を徹底解説！ ――近刊『コンピュータサイエンスにおける様相論理』まえがき公開
2022年1月下旬発行予定の新刊書籍、『コンピュータサイエンスにおける様相論理』のご紹介です。
同書の「まえがき」の一部を、発行に先駆けて公開します。
＊＊＊
〈 本書の目的 〉
様相論理とは、たとえば「真の可能性がある」「将来にわたってずっと偽」「それが真であることを花子は知っている」のように、単に真か偽かだけでなく状況に依存した真偽や複雑化された真偽概念を表現できる論理です。さまざまな動機から生まれたさまざまな様相論理がありますが、コンピュータサイエンスにおいてはCTL(computation tree logic)、様相ミュー計算(modal μ-calculus)、PDL(propositional dynamic logic)といった様相論理がよく研究されています。CTLは、たとえば「Aが起こればその後いつかはBが起こる」のような、時間とともに変化する真偽を細かく記述できるので、システムの振る舞いを記述してその成否を調べるモデル検査という技術に用いられています。様相ミュー計算は、不動点という仕組みを使うことで、CTLをはるかに超える記述力を実現している様相論理です。PDLは「このプログラムの実行が終了したら真」などプログラムに依存した真偽を表現できる様相論理です。プログラム検証を行う論理としてホーア論理というのがよく知られていますが、PDLはホーア論理と密接な関係があります。
本書の目的は、コンピュータサイエンスにおけるこれらの様相論理に関して、その数学的な基礎部分をわかりやすくかつ正確に説明することです。
〈 本書の特徴 〉
上記の様相論理をまとめて詳細に説明した本書のような教科書は他にほとんどないと思います。とくに、既存の教科書には証明まで載せられることが少ない下記の定理について、本書では証明を与えました。
証明体系の完全性
数理論理学における重要な定理が証明体系の完全性定理です。Lを様相論理としたとき、Lの証明体系の完全性定理は「論理式φがLの真偽概念のもとで恒真である」と「Lの証明体系によってφを導くことができる」という二つの条件の同値性、すなわち真理と証明との一致を表しています。これはLの定式化が妥当であることの証拠といえ、Lの分析にモデル論的な手法と証明論的な手法の両方を自在に使えることを保証する、研究の土台となる定理であるともいえます。本書にはCTLとPDLの証明体系の完全性定理の証明を載せました。さらに、Geach論理（モデルの状態遷移関係の合流性を網羅的に公理化した様相論理）についても証明を載せました。
計算可能性
コンピュータサイエンスにおける様相論理の意義には二つの方向があります。一つは先述のようにシステムやプログラムに関わる真偽を論理式で表現できること、そして、もう一つはそのように表現した論理式の真偽がコンピュータで計算可能であることです。本書では各様相論理について、論理式とモデルが与えられたときの真偽が計算可能であることの証明を載せました。さらに、CTLとPDLについては、「論理式が与えられたときにそれが恒真であるか否か（充足可能であるか否か）」が計算可能であることの証明も載せました。
様相ミュー計算のゲーム意味論の妥当性
ゲーム意味論とは、特殊なゲームの必勝戦略の有無で論理式の真偽を定義する方法です。多くの論理に適用できますが、とくに様相ミュー計算で威力を発揮し、これを用いることで不動点の扱いが著しく簡単になります。ゲーム意味論と従来の意味論で論理式の真偽が一致する、という事実をゲーム意味論の妥当性といいますが、この重要な基本性質の証明を載せました。
〈 本書の読み方 〉
本書は命題論理の基本を学んだことのある読者を想定しています。第1章で命題論理に関する必要事項をまとめて説明しますが、そこでは丁寧な説明や詳細な証明は省略するので、必要に応じて他の教科書などを参照してください。
第2章では、Kという様相論理とその周辺の基本事項を丁寧に説明します。本書の様相論理はすべてKを拡張したものなので、この章の内容は後の章を読むために必要です。ただし、最後の三つの節（2.9節以降）は後の章にほとんど関わらないので、飛ばして後の章に進むこともできます。また逆に、後の章には進まずに第2章だけを完結した様相論理の入門として読むこともできます。
第3、第4、第5章では、それぞれCTL、様相ミュー計算、PDLを扱います。これらの章の内容は互いに独立なので、別々に読むことができます。
第6章では、ホーア論理（これは様相論理ではありません）の基本部分を説明します。この章は第5章に付随したものですが、様相論理に関わらない部分を単独にホーア論理の解説として読むこと、つまり他の章は読まずに6.1～6.3節だけを読むこともできます。
本書をコンピュータサイエンス専攻あるいは数理論理学、数学、哲学などを専攻する大学3年～大学院の講義やセミナーの教科書として使用することもできると思います。実際に本書は、筆者が大学や大学院で行ったいくつかの講義の資料に基づいて作成されています。
＊＊＊
著：鹿島 亮（ 東京工業大学 准教授 ）
基本となる様相論理Kから始め、コンピュータサイエンス（計算機科学）において重要である、CTL（計算木論理）、様相ミュー計算、PDL（命題動的論理）について、その数学的な基礎をわかりやすく、かつ厳密に説明する。
また、様相論理ではないもののPDLとの関係が深く、プログラム検証を行う際に活躍するホーア論理についても詳しく解説する。
各論理については、定義や基本的な定理はもちろん、証明が難解で省略されがちな「証明体系の完全性」「計算可能性」「様相ミュー計算のゲーム意味論の妥当性」の証明も掲載しており、本書一冊で基礎を徹底的に学ぶことができる。
【目次】
第1章 準備：命題論理
1.1 論理式
1.2 真理値，恒真
1.3 真偽・恒真性の計算可能性
1.4 証明体系，完全性
第2章 K
2.1 様相論理とは
2.2 論理式，状態遷移系，モデル
2.3 モデルの実例
2.4 恒真
2.5 基本性質
2.6 カノニカルモデルによる完全性の証明
2.7 ▢*の追加
2.8 完全性と有限モデル性の証明
2.9 シークエント計算
2.10 遷移の合流性と論理式の対応
2.11 Geach論理の完全性の証明
第3章 CTL
3.1 定義
3.2 モデル検査
3.3 様相記号の相互関係と再帰的定義
3.4 基本性質
3.5 周辺の論理
3.6 完全性と有限モデル性の証明
第4章 様相ミュー計算
4.1 不動点
4.2 論理式
4.3 論理式の解釈
4.4 代入について
4.5 基本性質
4.6 ゲーム意味論：論理式
4.7 ゲーム意味論：定義
4.8 ゲーム意味論：使用例
4.9 ゲーム意味論：妥当性の証明
第5章 PDL
5.1 ホーア論理，DL，PDL
5.2 定義
5.3 基本性質
5.4 Fischer-Ladner閉包
5.5 完全性と有限モデル性の証明
第6章 ホーア論理
6.1 whileプログラム
6.2 ホーアトリプルと証明体系
6.3 健全性，相対完全性
6.4 PDLとの関係
演習問題の解答
参考文献
索引
この記事が気に入ったらサポートをしてみませんか？