抽象によるソフトウェア設計 第3章 論理系 その2

「論理系」の3つの側面について

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

だいぶ抽象的な説明が続きますが頑張ります。