Fwd: モデルのインスタンスの詳細を知りたーい (was Re: 献本送付先を教えてください)
Takeo Imai
今見ると結構な量（20通ほど）で、外にアナウンスする前にやるべきだったと思うのですが、一時的なものですのでご容赦下さい。
今井
---------- Forwarded message ----------
From: Masayuki Hiyama <m.hi...@gmail.com>
Date: 2011/7/18
Subject: モデルのインスタンスの詳細を知りたーい (was Re: 献本送付先を教えてください)
To: takeo...@gmail.com
たけをさん、
本とAlloyの感想はそのうちブログに書くつもりです。
んで、GUIでガックシだけど、気をとりなして少しAlloyで遊ぼうとかと。
とりあえず、モノイドの定義をまんま書いてみました。標準的定義を直訳した
つもりなんですが、、、こんなんんでいいんすか？
- - - - - - - - - - - - - - - - - - - - - - - - - - - - - -
-- モノイド
module mon1
sig Mon {
mult : Mon->one Mon // 乗法
}
one sig point {
unit : Mon // 単位
}
-- 結合律
fact assoc {
all x, y, z : Mon | (x.mult[y]).mult[z] = x.mult[y.mult[z]]
}
-- 単位律
fact unit {
all x : Mon | point.unit.mult[x] = x and x.mult[point.unit] = x
}
-- 可換律
pred comm {
all x, y: Mon | x.mult[y] = y.mult[x]
}
pred show {}
/* 以下にコマンド */
run comm for 2
- - - - - - - - - - - - - - - - - - - - - - - - - - - - - -
で、アナライザーの使い方でわかんないことが：
Executeすると、次のようなメッセージができます。
Executing "Run comm for 2"
Sig this/point scope <= 1
Sig this/Mon scope <= 2
Sig this/Mon in [[Mon$0], [Mon$1]]
Sig this/point == [[point$0]]
Solver=sat4j Bitwidth=4 MaxSeq=2 SkolemDepth=1 Symmetry=20
273 vars. 12 primary vars. 495 clauses. 21ms.
Instance found. Predicate is consistent. 5ms.
絵もでます。が、見つかったモデルインスタンスの詳細がわかりません。どう
やったら表示できるんでしょう？
僕が言っている「詳細」とは、可換モノイドの完全な記述です。
point = {point$0}, Mon = {Mon$0, Mon$1} という2つの集合があることはわか
ります。unit : point→Mon, mult:Mon→(Mon→Mon) という写像（関係の特別な
ものとしての写像）もあるはずです。
例えば、unitの可能性は、point$0 |→ Mon$0 と point$0 |→ Mon$1 の2つが
ありますが、具体的にどっちが選ばれたかを知りたいのです。同様に mult は、
Mon×Mon→Mon の演算表（乗積表）で表現できるはずなんで、その演算表を見
たいのです。それを見ないと、全然安心できません。
解決（solve）した解というのは、そういう具体的な有限構造のことなんじゃな
いかと思うのですが、「解があります」だけじゃなくて、どういう解かを具体
的に完全に知りたいのですけど、どうすりゃいいの？
--
檜山正幸 (HIYAMA Masayuki)
http://d.hatena.ne.jp/m-hiyama/
http://www.chimaira.org/
--
IMAI Takeo <takeo...@gmail.com>
Takeo Imai
このあと、連続して転送し続けますので、ご容赦を。
もちろん、気になるところに他の方からの質問・ツッコミなど歓迎です。
今井
---------- Forwarded message ----------
From: Masayuki Hiyama <m.hi...@gmail.com>
Date: 2011/7/18
Subject: Re: モデルのインスタンスの詳細を知りたーい (was Re: 献本送付先を教えてください)
To: takeo...@gmail.com
2011年7月18日13:01 Takeo Imai <takeo...@gmail.com>:
> Google Groups で公開のメーリングリストを作るのはアリかも、と思ったんですが、どうでしょう。
> アーカイブはWeb上で見られます。
>
>
僕は何でもいいですよ。せっかくだから、やり取りが共有できたほうがいい
な、ってだけです。
ところで、
モノイドの次は、カテゴリーを書いてみました。いいか悪いかわかりませんが、
余代数的に書くよりグローバル風シグネチャを使ったほうが普通の記述に近い
ようなので、単なる集合Obj, Morの外側に圏の構造を与える演算を書いてみま
した。
このモデル記述のインスタンスはあるようですが、やっぱりどんな構造が事例
なのかサッパリわからないので、正しいのかどうかもわかりませーん。
- - - - - - - - - - - - - - - - - - - - - - - - - - - - - -
-- 圏 : グローバルに定義するのが書きやすいようだ
module cat
-- 対象類と射類は単なる集合とする
sig Obj {}
sig Mor {}
-- 圏を定義するグローバルなシグネチャ
one sig cat {
-- 恒等
id: Obj ->one Mor,
-- 域と余域
dom, cod: Mor ->one Obj,
-- 結合、部分的二項演算
comp: Mor -> (Mor ->lone Mor)
}
-- 結合可能性
pred composable[f: Mor, g: Mor] {
cat.cod[f] = cat.dom[g]
}
-- dom, cod, id, compの関係（有向グラフ構造上の演算であること）
fact digraph {
-- 恒等のdom, codの定義
all a: Obj |
cat.dom[cat.id[a]] = a and cat.cod[cat.id[a]] = a
-- 結合射のdom, codの定義
all f, g: Mor |
cat.dom[cat.comp[f, g]] = cat.dom[f]
and
cat.cod[cat.comp[f, g]] = cat.cod[g]
}
-- 左結合可能な射の存在、確認用
assert lexist {
all g: Mor | some f: Mor | composable[f, g]
}
-- 右結合可能な射の存在、確認用
assert rexist {
all g: Mor | some h: Mor | composable[g, h]
}
-- 結合可能なら結合射が存在する、およびその逆
fact compexit {
all f, g: Mor | composable[f, g] <=> one cat.comp[f, g]
}
-- 結合律
fact assoc {
all f, g, h: Mor |
(composable[f, g] and composable[g, h]) =>
cat.comp[cat.comp[f, g], h] = cat.comp[f, cat.comp[g, h]]
}
-- 単位律
fact unit {
all a, b: Obj, f: Mor |
(cat.dom[f] = a and cat.cod[f] = b) =>
cat.comp[cat.id[a], f] = f and cat.comp[f, cat.id[b]] = f
}
pred show {}
/* 以下にコマンド */
check lexist
check rexist
run show
- - - - - - - - - - - - - - - - - - - - - - - - - - - - - -
--
Takeo Imai
From: Masayuki Hiyama <m.hi...@gmail.com>
Date: 2011/7/18
Subject: Re: モデルのインスタンスの詳細を知りたーい (was Re: 献本送付先を教えてください)
To: takeo...@gmail.com
2011年7月18日13:28 Masayuki Hiyama <m.hi...@gmail.com>:
> やっぱりどんな構造が事例
> なのかサッパリわからないので、正しいのかどうかもわかりませーん。
catだと絵も描かれなくなっちゃいました。
#1: No counterexample found. lexist may be valid.
#2: No counterexample found. rexist may be valid.
#3: Instance found. show is consistent.
「そういうのあります／ありません」だけ教えてもらっても、どうも自信も気
力も湧かないので、インスタンスの詳細が分かるまで中断。
Takeo Imai
From: Takeo Imai <takeo...@gmail.com>
Date: 2011/7/18
Subject: Re: モデルのインスタンスの詳細を知りたーい (was Re: 献本送付先を教えてください)
まだちゃんと見られてないんですが、絵が出ていれば、関係がどのアトムとの間に成立しているかは
絵でも確認できますし、あと絵を表示するパネルに「 Evaluator 」というボタンがあって、これを押すと
インタプリタ式の評価器が使えます。
2011/7/18 Masayuki Hiyama <m.hi...@gmail.com>:
> catだと絵も描かれなくなっちゃいました。
ちゃんと見れてないんですが、このツールは（OBJみたいなのとは違って）数学的対象をモデリングすると、
うまくいかないことが多いです。そのせいかも？
> assert lexist {
> all g: Mor | some f: Mor | composable[f, g]
> }
みたいなのは典型的で、このアサーションで言う f の存在を有限領域内で保証しようとすると、矛盾が発生するのです。
こういうプロパティをAlloy用語で「生成公理」と呼んでいます。（本には5.3節に書いています）
--
IMAI Takeo <takeo...@gmail.com>
--
IMAI Takeo <takeo...@gmail.com>
Takeo Imai
From: Masayuki Hiyama <m.hi...@gmail.com>
Date: 2011/7/18
Subject: Re: モデルのインスタンスの詳細を知りたーい (was Re: 献本送付先を教えてください)
2011年7月18日14:00 Takeo Imai <takeo...@gmail.com>:
> まだちゃんと見られてないんですが、絵が出ていれば、関係がどのアトムとの間に成立しているかは
> 絵でも確認できますし、
そのへんは実演付きじゃないと、やり方がよくわかんないなぁ。GUIの困る点は
（少なくとも僕には）、操作法の伝達を文章でするのが面倒・困難なところ。
> あと絵を表示するパネルに「 Evaluator 」というボタンがあって、これを押すと
> インタプリタ式の評価器が使えます。
おっ、これは便利だ。見つかったモデルインスタンスの評価環境内でタイプし
た式の評価をしてくれるんですね。がんばれば、インスタンスの細部まで式評
価でインスペクトできますね、がんばれば、だけど。
> 2011/7/18 Masayuki Hiyama <m.hi...@gmail.com>:
>> catだと絵も描かれなくなっちゃいました。
>
> ちゃんと見れてないんですが、このツールは（OBJみたいなのとは違って）数学的対象をモデリングすると、
> うまくいかないことが多いです。そのせいかも？
絵がでなくなったのは、Obj = Mor = {} （空集合） というインスタンスになっ
ていたからみたい。空な圏ですね。some を付けて非空にしたら、ObjもMorも単
元な自明な圏を見つけたみたい。
小さい基数に事例があればそれを見つけようとするわけだから、まー当然か。
非自明な例を見つけたいなら、シグネチャの基数を少し大きめに取らないとい
けないんですね。
>
>> assert lexist {
>> ?all g: Mor | some f: Mor | composable[f, g]
>> }
>
> みたいなのは典型的で、このアサーションで言う f の存在を有限領域内で保証しようとすると、矛盾が発生するのです。
> こういうプロパティをAlloy用語で「生成公理」と呼んでいます。（本には5.3節に書いています）
>
んん？ 「はじめに」と付録しか読んでないから、ワカンナイ。5章になにか書
いてあるのね、そのうち目を通します。
Takeo Imai
From: Takeo Imai <takeo...@gmail.com>
Date: 2011/7/18
Subject: Re: モデルのインスタンスの詳細を知りたーい (was Re: 献本送付先を教えてください)
2011/7/18 Masayuki Hiyama <m.hi...@gmail.com>:
> 絵がでなくなったのは、Obj = Mor = {} （空集合） というインスタンスになっ
> ていたからみたい。空な圏ですね。some を付けて非空にしたら、ObjもMorも単
> 元な自明な圏を見つけたみたい。
>
> 小さい基数に事例があればそれを見つけようとするわけだから、まー当然か。
>
> 非自明な例を見つけたいなら、シグネチャの基数を少し大きめに取らないとい
> けないんですね。
あるいは、インスタンス表示ウィンドウで Next ボタンを押すと、別解を出してくれます。
ポチポチ押してれば、制約を満たしている限りは非自明な解も出てくるはず。
Takeo Imai
From: Masayuki Hiyama <m.hi...@gmail.com>
Date: 2011/7/18
Subject: Re: モデルのインスタンスの詳細を知りたーい (was Re: 献本送付先を教えてください)
2011年7月18日16:28 Takeo Imai <takeo...@gmail.com>:
>
> あるいは、インスタンス表示ウィンドウで Next ボタンを押すと、別解を出してくれます。
> ポチポチ押してれば、制約を満たしている限りは非自明な解も出てくるはず。
>
おおー、なるほど。Prologインタプリタののセミコロンみたいなもんか（処理
系依存だったか？＞「;」）。
状態遷移の例だと、意図と絵とピッタリあうみたいですね。スタックの仕様を
書いてみたら、出てきた絵がバッチリな状態遷移図。故意に条件を緩めてあげ
ると、変な状態遷移図を探してくるので面白い。
- - - - - - - - - - - - - - - - - - - - - - - - - - - - - -
module stack
one sig stk {
empty: State,
full: State
}
sig Val {}
sig State {
push: Val ->lone State,
pop: lone State,
top: lone Val
}
/* 一時的に empty = full を許す
// empty = full をやられた
fact non_triv {
stk.empty != stk.full
}
*/
fact top {
all s: State |
(s != stk.empty => one s.top)
and
(s = stk.empty => no s.top)
}
fact pop {
all s: State |
(s != stk.empty => one s.pop and s.pop != s)
and
(s = stk.empty => no s.pop)
}
fact push {
all s: State, v: Val |
(s != stk.full => one s.push[v] and s.push[v] != s)
and
(s = stk.full => no s.push[v])
}
fact push_top {
all s: State, v: Val |
s != stk.full => s.push[v].top = v
}
fact push_pop {
all s: State, v: Val |
s != stk.full => (s.push[v]).pop = s
}
pred show {}
pred card {
#State >= 3
}
run show
run card for 5
- - - - - - - - - - - - - - - - - - - - - - - - - - - - - -
Takeo Imai
From: Masayuki Hiyama <m.hi...@gmail.com>
Date: 2011/7/18
Subject: Re: モデルのインスタンスの詳細を知りたーい (was Re: 献本送付先を教えてください)
To: takeo...@gmail.com
> 変な状態遷移図を探してくるので面白い。
いやー、おもろいなー、コレー。
最近、子供の相手しないから、休日の遊びがAlloyになってしまった。
どこが面白いか？というと、人間が一人（自分だけ）でもコンピュータ相手に
“エクソシストゲーム”ができる。
- http://d.hatena.ne.jp/m-hiyama/20060407/1144378577
- http://d.hatena.ne.jp/m-hiyama/20060408/1144479281
律儀に悪魔の役をやってくれる人間なんていないけど、Alloyアナライザーが悪
魔のターンを実行してくれるので、俺のターンでは仕様を詳細化してだんだん
追い詰める。インスタンスが一意になるほど追い込む必要はないけど、奇妙な
事例が出ない程度まではターンを続けないとね。
僕にとっては、これは完全に娯楽ソフトウェアだな。
Takeo Imai
From: Takeo Imai <takeo...@gmail.com>
Date: 2011/7/18
Subject: Re: モデルのインスタンスの詳細を知りたーい (was Re: 献本送付先を教えてください)
いやーしかし、さすがというか、既に使いこなしてるところがすごいですね（笑）
2011/7/18 Masayuki Hiyama <m.hi...@gmail.com>:
> 律儀に悪魔の役をやってくれる人間なんていないけど、Alloyアナライザーが悪
> 魔のターンを実行してくれるので、俺のターンでは仕様を詳細化してだんだん
> 追い詰める。インスタンスが一意になるほど追い込む必要はないけど、奇妙な
> 事例が出ない程度まではターンを続けないとね。
これがまさに、開発者が推奨するAlloyの使い方です。
悪魔が勝てないギリギリの仕様を見つけるのが目的と言うか。
> 僕にとっては、これは完全に娯楽ソフトウェアだな。
開発者も「ソフトウェアの設計を楽しくしたい」と常々言っていたので、
娯楽ツールにしてもらえたのなら、何よりだと思いますです。
Takeo Imai
From: Masayuki Hiyama <m.hi...@gmail.com>
Date: 2011/7/18
Subject: Re: モデルのインスタンスの詳細を知りたーい (was Re: 献本送付先を教えてください)
2011年7月18日17:21 Takeo Imai <takeo...@gmail.com>:
>
>> 僕にとっては、これは完全に娯楽ソフトウェアだな。
>
> 開発者も「ソフトウェアの設計を楽しくしたい」と常々言っていたので、
> 娯楽ツールにしてもらえたのなら、何よりだと思いますです。
「二人で対戦」を一人だけで出来るゲームソフトだね。そういうふうにプロモー
ションすると裾野がひろがるかも -- って、、？？ まー少なくとも証明責務が
伴うツールに比べると、格段に気楽だと思いますよ。
制約がゆるい段階で、（人間にとっては）思いがけない奇妙な例を律儀に探し
てくるのが可愛いなー。
ソフトウェアのほうを触ってみたので、本の続きも読みますよ、ハイ。付録を
読めば、3章、4章は飛ばしてもよさげだから（オィッ！＞自分）、5章からかな。
Takeo Imai
From: Takeo Imai <takeo...@gmail.com>
Date: 2011/7/18
Subject: Re: モデルのインスタンスの詳細を知りたーい (was Re: 献本送付先を教えてください)
2011/7/18 Masayuki Hiyama <m.hi...@gmail.com>:
> 「二人で対戦」を一人だけで出来るゲームソフトだね。そういうふうにプロモー
> ションすると裾野がひろがるかも -- って、、？？
なるほど。将棋ソフト（CPU対戦モードつき）みたいなもんですね、確かに。
> 制約がゆるい段階で、（人間にとっては）思いがけない奇妙な例を律儀に探し
> てくるのが可愛いなー。
ですです。
> ソフトウェアのほうを触ってみたので、本の続きも読みますよ、ハイ。付録を
> 読めば、3章、4章は飛ばしてもよさげだから（オィッ！＞自分）、5章からかな。
まぁ実際、そうなので（笑）
3，4章とも、付録を直接読み込めない人のための導入ですから。
5章はアナライザーのコンセプトから内部実装のさわり、みたいな話です。
既に概要は会得されてしまった気がするので、ご興味があるところだけ、お好みでどうぞ。