bonotakeの日記

元・ソフトウェア工学系研究者、今・AI系エンジニア

シグネチャのフィールドにある関係の多重度 続き

昨日の日記 の続き。 id:koji8y さんから、トラックバック

じゃあ,昨日のスタート Alloy の演習中に僕らが表現したかったこと,

sig A {
	r: B -> C
}

で,各 A の各 r が one to one の関係 (functional かつ injective な関係) となること*1を表現するにはどう記述したらいいでしょうね?
(略)

sig A {
	r: B -> C
}{
	// functional (left-unique)
	all b: B, c1, c2: C {
		(b->c1 in r and b->c2 in r) => c1 = c2
	}
	// injective (right-unique)
	all b1, b2: B, c: C {
		(b1->c in r and b2->c in r) => b1 = b2
	}
}

とすると,表示したインスタンスは求めている形になっていそう.

でももっと簡単に記述できるるのではないかと...

と追加質問いただいたんですが…これって

  sig A {
    r: B lone -> lone C
  }

では?シグネチャファクト中の

  all b: B, c1, c2: C {
    (b->c1 in r and b->c2 in r) => c1 = c2
  }

って制約は

  all b: B {
    lone b.r
  }

と同じ意味に読めます。

実際、下記のように書いたアサーションで反例は(スコープをいくつにしても)出ないです。
アサーションを記述するため、シグネチャファクトや宣言制約を述語内に書き下しています)

sig A {
	r: B -> C
}
sig B, C {}

pred p1 {
  all a: A {
	// functional (left-unique)
	all b: B, c1, c2: C {
		(b->c1 in a.r and b->c2 in a.r) => c1 = c2
	}
	// injective (right-unique)
	all b1, b2: B, c: C {
		(b1->c in a.r and b2->c in a.r) => b1 = b2
	}
  }
}

pred p2 {
  all a: A | a.r in B lone -> lone C
}

assert equivalence {
  p1 <=> p2
} 

check equivalence for 6
注:bonotakeは、amazon.co.jpを宣伝しリンクすることによってサイトが紹介料を獲得できる手段を提供することを目的に設定されたアフィリエイト宣伝プログラムである、 Amazonアソシエイト・プログラムの参加者です。