反射的推移的閉包の演算子「*」がよくわからない
Masayuki Hiyama
以下のモデル記述は、http://d.hatena.ne.jp/m-hiyama/20110720/1311129932
に晒したやつをわずかに変更したものです。
- - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - [begin]
-- 自然数の区間 {0, 1, 2, ..., n}
module interv_why
one sig Foo {} // univ を大きくするため
sig Interv {
-- 後者
next: lone Interv,
-- 順序
private gt : set Interv, //ビジュアライズのとき邪魔だからprivate
ge : set Interv
}
-- ゼロと最後の数
-- この定義により、ゼロと最後の数は異なることになる。
one sig zero, last extends Interv {}
-- nextに関する公理
fact next {
{
-- lastのnextは存在しない
no last.next
-- last以外ではnextが一意に定義されている
all x: (Interv - last) |
one x.next
-- ゼロからの可達性
zero.*next = Interv
}
}
-- gt, geに関する公理（定義）
fact order {
{
gt = ^next
ge = *next // ダメ
// ge = ^next + Interv<:iden // これならOK
// ge = ^next + iden // ダメ
}
}
pred show {}
/* 以下にコマンド */
run show
- - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - [end]
実行すると失敗します（モデルインスタンスは見つかりません）：
- - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - [begin]
Executing "Run show"
...
No instance found. Predicate may be inconsistent. 0ms.
- - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - [end]
コメントアウトしてますが、ge （等号付き大小のつもり）の定義が3つありま
して：
1. ge = *next
2. ge = ^next + Interv<:iden
3. ge = ^next + iden
1番目はダメです。が、2番目ならちゃんと成功します。3番目もダメです。
nextはInterv上の二項関係なので、2番目の定義は正しいと思います。
僕は、(1番目) ⇔ (2番目） だと予想してたし、それが真っ当な「*」の定義だ
と思うのですが、(1番目) と (2番目) で挙動が違うってことは、(1番目) ⇔
(2番目） ってことはありえず、むしろ (1番目) ⇔ (3番目）の可能性がありま
す。
なんか勘違いしてますかね？ もし僕の勘違いじゃないとすれば、反射的推移的
閉包の演算子「*」はチトおかしいのでは？
--
檜山正幸 (HIYAMA Masayuki)
Takeo Imai
2011/7/20 Masayuki Hiyama <m.hi...@gmail.com>:
> 1. ge = *next
> 2. ge = ^next + Interv<:iden
> 3. ge = ^next + iden
（snip）
> 僕は、(1番目) ⇔ (2番目） だと予想してたし、それが真っ当な「*」の定義だ
> と思うのですが、(1番目) と (2番目) で挙動が違うってことは、(1番目) ⇔
> (2番目） ってことはありえず、むしろ (1番目) ⇔ (3番目）の可能性がありま
> す。
>
> なんか勘違いしてますかね？ もし僕の勘違いじゃないとすれば、反射的推移的
> 閉包の演算子「*」はチトおかしいのでは？
残念ですが、勘違いではありません。
本のp62にその事実と、あとその質問に対する著者からの反論が書かれています。
反論を素直に受け入れられるかどうかはわかりませんが（＾＾； ← 自分も過去にハマったクチ
--
IMAI Takeo <takeo...@gmail.com>
Masayuki Hiyama
Takeo Imai
> うっ、第3章を読んでないのがバレた。
ふっふっふ。
ついでに私見を加えると、これは計算効率追究の産物ではないかと思ってます（勝手な推測）。
閉包の計算そのものに、定義域の制限（に必要な制約）を含ませたくなかったのでしょう。
なぜなら、演算子で定義域の制限をかけなくても、実用上は結合などの他の演算との合成で自然に定義域に制限がかかることが多いからです。無駄な制約を裏で追加して計算効率を落とすようなことはしたくなかったのかなーと。
…てなことを、本文ではいかにも当然だというごとく正当化して書いてますが、本心はこんなトコロだったのではないでしょうか。
SATソルバがすごく賢くなった今からAlloyを設計し始めていたら、もう少し状況は変わっていたかも。
それとも、ある世界ではAlloy流の定義が自然なのかもしれないので、そういう世界を知ってる方おられたら反論下さい。
--
IMAI Takeo <takeo...@gmail.com>
Masayuki Hiyama
ですが、意味的には承服できないなー。「*」って、関係のクリーネスターです
よね。関係のクリーネスターが台集合をはみ出すとか、ありえないでしょ。
2011年7月20日22:03 Takeo Imai <takeo...@gmail.com>:
Takeo Imai
とりあえず、反射推移閉包を使う場合は、必要に応じて意識的に定義域制限を使ってください、としか言えないです。（この場合は、 Interv<:*next ）
2011/7/21 Masayuki Hiyama <m.hi...@gmail.com>:
--
IMAI Takeo <takeo...@gmail.com>
Masahiro Sakai
On 7月21日, 午前8:21, Masayuki Hiyama <m.hiy...@gmail.com> wrote:
> 「効率のためだ」と言われると、「あーそうですか」としか言いようがないの
> ですが、意味的には承服できないなー。「*」って、関係のクリーネスターです
> よね。関係のクリーネスターが台集合をはみ出すとか、ありえないでしょ。
台集合として何が意図されているかが処理系からは分からないんですよ。
分かんないので、台集合として最も汎用的なunivが仮定されるという。
台集合を適当に推論する方法や、明示的に台集合を指定する構文にする
方法もあったとは思いますが、前者は皆が納得出来るルールは難しそう
だし、後者は構文が煩雑になりそうだし、現在の設計は個人的にはまあ
妥当な design decision だと思ってます。
On 7月20日, 午後10:03, Takeo Imai <takeo.b...@gmail.com> wrote:
> ついでに私見を加えると、これは計算効率追究の産物ではないかと思ってます（勝手な推測）。
> 閉包の計算そのものに、定義域の制限（に必要な制約）を含ませたくなかったのでしょう。
> なぜなら、演算子で定義域の制限をかけなくても、実用上は結合などの他の演算との合成で自然に定義域に制限がかかることが多いからです。無駄な制約を裏で追加し て計算効率を落とすようなことはしたくなかったのかなーと。
>
> …てなことを、本文ではいかにも当然だというごとく正当化して書いてますが、本心はこんなトコロだったのではないでしょうか。
> SATソルバがすごく賢くなった今からAlloyを設計し始めていたら、もう少し状況は変わっていたかも。
少なくとも Partial Model の機能が利用出来るような場合には、
その方がSATに落としたときの効率は良さそうな気がします。
Partial Model の機能が利用できないような場合や、Kodkod以前の
Alloy3だとどちらが効率が良いかは微妙なところですが。
-- 酒井 政裕
Takeo Imai
2011/7/21 Masahiro Sakai <masahir...@gmail.com>:
> Alloyは型がなくても解釈できる言語として設計されているので、
> 台集合として何が意図されているかが処理系からは分からないんですよ。
> 分かんないので、台集合として最も汎用的なunivが仮定されるという。
結局、どの関係もuniv上の部分関係、という解釈なんですよね。
「定義域」はunivの中で、全域的な定義がある部分集合、という。
> 台集合を適当に推論する方法や、明示的に台集合を指定する構文にする
> 方法もあったとは思いますが、前者は皆が納得出来るルールは難しそう
> だし、後者は構文が煩雑になりそうだし、現在の設計は個人的にはまあ
> 妥当な design decision だと思ってます。
ただ、素人にとって直観的でないのも事実なんですよね。
関連して、p45の議論にも、定義域や値域の話がありますけど…こういう話を
議論に書くということ自体、初心者がハマる箇所だ、ということの裏返しでもある
と。
# まぁ元々、「定義域」「値域」という言葉は慣用的なもので、定義がいい加減
# だなぁと普段から思わなくもないですが。
> 今のKodkodベースのAlloyなら、適当な規則で台集合を限定しても、
> 少なくとも Partial Model の機能が利用出来るような場合には、
> その方がSATに落としたときの効率は良さそうな気がします。
KodKodの仕様をちゃんと覚えてないのですが、Partial Modelって何でしたっけ？
--
IMAI Takeo <takeo...@gmail.com>
Masayuki Hiyama
事情を聞けば「しょうがない」気もするのですが、関係rに対して *r が広がり
すぎていることは、なかなか気がつかないです。落とし穴になりますね。
むしろ、「*」演算は組み込みで入れないほうがいいのではないでしょうか。
^r + iden とか ^r + a<:iden とユーザーが明示的に書くなら、idenがuniv上
に広がっていることは意識できるでしょう。ひとつの演算子に閉じ込めてしま
うと、idenの広がりを忘れてしまいがち（つうか、気づきもしない）。
2011年7月21日11:59 Takeo Imai <takeo...@gmail.com>:
--
Masahiro Sakai
>> 少なくとも Partial Model の機能が利用出来るような場合には、
>> その方がSATに落としたときの効率は良さそうな気がします。
>
> KodKodの仕様をちゃんと覚えてないのですが、Partial Modelって何でしたっけ？
Kodkodの仕様はkodkod.instance.Boundsあたりを見てください。
http://alloy.mit.edu/kodkod/docs/kodkod/instance/Bounds.html
各関係変数に対して上界値および下界値の形で指定するようになってます。
指定すると、SATにエンコードする際のビット変数行列の一部分が、
0,1に決まるので、それらは定数として扱い、SATの変数を割り当てなくなります。
-- 酒井 政裕