日々の流転

λ. 推移閉包が一階述語論理では表現できないことをAlloyで確認する

Alloy - 言語ゲーム(2009-05-27) にコメントした話から。

以前「推移閉包は一階述語論理では表現できないのね」と書いたが、 Alloyは一階述語論理に推移閉包を加えて拡張した論理なので、推移閉包の機能を使わずに書いた関係と、推移閉包の機能を使って書いた関係が等しいかをAlloy上で検査すれば、イメージしやすくなるのではないかと思った。

まず、集合UとU上の二項関係R1,R2を定義。

sig U {
  R1 : set U,
  R2 : set U
}

次に、R2がR1の推移閉包であることを、推移閉包の機能を使わずに記述してみようとする。

fact {
  all x, y : U {
    y in x.R2 <=> (y in x.R1 || (some z : U | z in x.R2 && y in z.R2))
  }
  //// 関係演算を直接使った書き方
  // R2 = R1 + R2.R2
}

そして、Alloyの推移閉包の機能を使うと、R1 の推移閉包は ^R1 と書けるので、R2 が ^R1 と一致するかを検査してみる。 ただし、あまりに trivialな例でも面白くないので、R1が空でないという制約を追加しておく。

fact { some R1 }

assert R2_is_TC_of_R1 {
  R2 = ^R1
}

check R2_is_TC_of_R1

で、検査してみると、例えば以下の図が反例として出てくる。

R2はR1を含む推移的関係になっているけど、推移閉包すなわち「R1を含む最小の推移的関係」にはなっていない。 こういった最小性や最大性は一般に一階述語論理では表現できない。