抽象によるソフトウェア設計 第3章 論理系 その2
「論理系」の3つの側面について
- 論理の記述形式
- 述語論理
- 自然言語で「全ての○○が□□ならば〜」というのに似た形式
- 述語論理形式は内包表記で使うことが多い
- ナビゲーション形式
- 関係計算
- 難しいけど短く書けるのでイディオムとして使えるところがある
- 同じ意味の制約を3通りの記述のしかたで表現できる
- 基本的にナビゲーション形式を使う
- 多重度の制約はよく使うので別の構文が用意されている
- 表現能力(表現できる論理の範囲)はナビゲーション形式が最も高い
- 述語論理
- アトム - 不可分、不変、非解釈という性質を持つ構成要素
- 関係 - タプル(アトムの並び)の集合。RDB のテーブルのようなもの。タブルが行
- 行の数(タプルの数)を関係のサイズと呼ぶ
- 列の数(タプルのアトム数)をアリティと呼ぶ
- タプルを持たない関係(サイズが0)は「空」
- 高々1個(0 or 1) のタプルを持つ関係を「オプション」と呼ぶ
- Alloy ではタプルを生のまま扱うことはなくて、タプル1つだけの一元関係として扱う
だいぶ抽象的な説明が続きますが頑張ります。