抽象によるソフトウェア設計 付録A 練習問題 その5

付録A 練習問題続きます。

• A.1.9 閉包推移を公理化してみる
  • 閉包推移は一階論理で公理化できない。のでできないのだけどやろうとして失敗してみるというもの

-- 推移被覆
pred transCover (R, r: univ -> univ) {
   r in R       -- R は r を含む
   R.R in R     -- R は推移的
  }

-- 推移閉包
pred transClosure (R, r: univ -> univ) {
  transCover [R, r]   -- R は r の推移被覆であり
  no x, y: univ | x -> y in R and transCover [R - x -> y, r]
                      -- R から取り除いても推移被覆であるようなタプルがない
  }

assert Equivalence {
  all R, r: univ -> univ | transClosure [R, r] iff R = ^r
  }

check Equivalence for 3

• • r が2つの部分グラフに分割されるような関係で R が両者を繋ぐタプルを含んでいるような時に上記の記述では「最小の推移被覆である」ことをうまく表現できません

今日は試行錯誤で時間を使ってしまってここまでです。
解説によると、「有限領域における推移閉包は一階論理で公理化できる」そうです。