one限量で複数の変数を宣言する

Alloyの言語仕様をゴリゴリ読み進めていた。 非常に勉強になります。

Software Abstractions (1st ed., p.288):

So although a quantified constraint with multiple declarations may be regarded, for some quantifiers, as a shorthand for nested constraints, each with one declaration, this is not in general true. Thus

  all x:X, y:Y | F

is short for

  all x:X | all y:Y | F

but

  one x:X, y:Y | F

is not short for

  one x:X | all y:Y | F

なるほど。しかしoneという限量子は自分が知っている一階述語論理には出てこなかったので、馴染みがない。実際のところどう違うんだろう。

次のAlloyコードを基本として、ちょっと考える。

sig X {r : set Y}
sig Y {}
fact { #X=2 and #Y=2 }

run {}

sig宣言で、それぞれ2つの要素をもつ集合XとYを与える。 シグネチャX はフィールド r をもち、型は set Y と宣言されている。これは X と Y の間に2項関係 r がありますよというのと同等だ。 Alloy Analyzer で Execute すると、実際に図で確認できる。

次のファクトを考えよう。factはモデルに常に成り立つ制約を追加する。

fact {one x:X, y:Y | x->y in r}

ここでは x->yは 単に (x,y) と同等だ。 結局、このファクトは 関係rの要素になる(x,y)の組み合わせはただ1つだと述べている。

一方、上の制約のかわりに

fact {one x:X | one y:Y | x->y in r}

と書いた場合はどうだろうか。真理値表で確認してみるのもいいが、せっかくなので Alloy Analyzer に表示させてしまおう。

こういう図が出た。

たしかに、内側のone y:Y|x->y in r が偽になるには、x2->y1, x2->y2がrに入っていても良いわけか。

x	y	x->y in r	one y:Y | x->y in r
x1	y1	t	t
	y2	f	f
x2	y1	t	f
	y2	t	f

なるほど なぜかyの列がすべてy1になっていたので修正