たけをの日記@天竺から帰ってきたよ このページをアンテナに追加 RSSフィード

2014-04-20

Alloyで直積を考える

| 15:33 | Alloyで直積を考えるを含むブックマーク

前回の続きです。正確には、前回の続きの後の檜山さんのブログ記事に対する更なる「合いの手」です。

一連の記事を読んでいろいろ考えているうち、実は直和だけでなく直積も問題だということがわかりましたw

ということで、前回とほぼ同じノリで直積も考えてみます。今回も使ったAlloy記述全文はGistに貼りました。

あと、上記檜山さんの記事の「関係圏を観察してみる」以降を適時引用します。Alloyは関係をベースにした言語なので、関係圏とは相性がとてもいいのです。

お膳立て

さっき問題あるとは書いたものの、直積は直和と違い、Alloyにはちゃんと言語機能としてあります。集合A に対して A->A と書きます。

なんで直積なのに関数型みたいな書き方すんの?という方にはこちらを。関係圏では(翻ってAlloyも)集合の直積は冪とか関数(関係だけど)とほぼ同一視できるようです。

ということで、このAlloyの直積を議論の対象として扱います。檜山さんの記事に合わせると、テンソル積と呼ぶべきですかね。

単位元(単位対象)

関係圏Relでは、ホムセット Rel(A, {0, 1}) はAのベキ集合にはなりません。Rel(A, {0}) がAのベキ集合なのです。{0}は単元集合1です。1は、関係圏においては始対象でも終対象でもありません(始対象=終対象=空集合です)。1は、テンソル積(集合の直積でした)の単位対象として特徴付けられます。 個体と世界の関係:圏から論理半環を絞り出す − 檜山正幸のキマイラ飼育記

だ、そうなので、単元集合を持ってきましょう。

Alloyには特別特定の単元集合があるわけではないので、1からこさえます。と言っても1行で終了ですが。

one sig Unit {}

冒頭のoneで、必ず1個だけ存在する、すなわち単元集合であるという宣言をしております。

で、これがテンソル積の単位対象になってることを確かめてみます。

……といっても、単純じゃないんですよねこれ。要は、 Unit->A ないし A->Unit が Aと同型になっているって言えばいいんですけど。

同型であることの証明ってAlloyで書きづらい……*1

てなわけで、「集合のサイズが等しい」っていう、間接的な形で確認することにします。

ということで、以下のアサーションを。反例出ないと思います。

check {
  all a: set univ {
    #(Unit -> a) = #a
    #(a -> Unit) = #a
  }
}

対角、余対角

対角ですが、こんな感じで。直和の時とほとんど感覚は同じです。

fun diagP (a: univ): univ -> univ {
  a -> a
}

適当な集合Aに対して、A->Aを作って返してやるだけです。

一方余対角ですが、ないらしいので、

論理積∧は、p, q:A→1 に対して、δA;(p×q);ρ と定義する。ρ:1×1→1 は、テンソル積の単位法則に伴う自然同型。

にあるρ:1×1→1 (ここまでの書き方に沿えば、ρ:(Unit->Unit)->Unit)をこさえましょう。こんな感じです。

fun ro (r: Unit -> Unit): Unit {
  Unit.r
}

rの頭からUnitと結合して、r: Unit->Unitの後ろ側の成分(第二成分)だけを取り出して返します。

え?第一成分は要らないの?これでいいの?? とお思いになるかもしれませんが……一般的にはダメかもしれません。しかしAlloyの矢印型直積を使う分には、これで構いません。この理由は後で述べます。

で、せっかくなので、上記の論理積 δA;(p×q);ρ を作ってしまいましょう。 まずは δA と (p×q) を結合するために、次のような関数をこさえます。

fun joinL (a: univ->univ, r: (univ->Unit)->(univ->Unit)): Unit->Unit {
  (a.univ).(r.univ.univ) -> (univ.a).(univ.(univ.r))
}

aの第一成分とrの第一成分、第二成分と第二成分を結合して、改めて -> でつなぎなおします。これも、直和のときに考えた結合と、基本的な理屈は同じです。

以上の diagP(δA)とjoinL(結合子 ; )、ro(ρ)をつないで、さっきの論理積の定義を書き下します。

fun prodL (f,g: univ -> Unit): univ -> Unit {
  {x: univ, u: Unit | u = x.diagP.joinL [f -> g].ro }
}

こうして、論理積 f ∧ g が定義できたんですけども。

これって結局、やっぱり、Alloyでいうところの

f & g

と同じなんですよね。実際、以下のアサーションは反例出ないです。

equiv_product: check {
  all f, g: univ -> Unit | prodL[f, g] = f & g
}

ということで、直和の時とオチもほぼ同じでした。ちゃんちゃん。

ちなみに、以前紹介したドメイン付きクリーネ代数のAlloyモデルですが、命題をPropのべき集合(set Prop)で与え、論理積はその間の集合積 & で書いてました。この辺とややつながった感じ?

直積にもいろいろある

で、上記 ro の定義がなんであんないい加減でいいのか、というお話ですが。

実は、ひとくちに「直積」と言っても、ビミョーな差でいくつか種類があるのです。それで「Alloyの矢印型直積を使う分にはこれで構わない」なんてビミョーな表現をしたのです。


ro の引数 r: Unit -> Unit (=Unit×Unit)ですが、具体的に何種類の値があるかわかります?

Unitが単元集合だったので、Unit型の引数にはたかだか1要素しか入りません。なのでUnit×Unitなら、第一成分、第二成分それぞれに「ある」(Unitそのもの)か「ない」(空集合 none)かの2択しかなく、よって r は 4種類。

……と見せかけて、実はAlloyの場合、2種類しかありません。Alloyの直積はstrictな直積(スマッシュ直積とかいいます)になっていて、片方の成分が空集合なら、ただちに全体も空集合になります*2。なので、第一成分、第二成分とも「ある」か、両方ともなかったことになるかの2択なのです。

一方、一般的な集合の直積、集合圏の直積はstrictではなく、なので片方が空集合というだけで全体が空集合と完全にイコールにはなりません(同型にはなるけど)。ということで、ビミョーに違うんですね。

なので roは、本当なら「第一成分と第二成分がともに空でない場合に単元集合を返す、そうでなければ空集合を返す」と書くべきなんでしょうが。現実的には、どっちも空でないかどっちも空か、しか選択肢がないので、片方だけ参照する、という上の定義で成り立ってるわけです。

Alloyプリミティブの直積 -> じゃなくて、新たに一般的な直積を起こせばよかったのかもしれませんが、面倒くさかったのでした。はい。

*1天下りに同型射を与えればいいんですけどね。

*2スマッシュ直積云々はこちらでもちらっと書いてますが、って8年半も前の記事だよ。わーお。

2014-04-14

Alloyで直和を考える

| 00:18 | Alloyで直和を考えるを含むブックマーク

前回の記事に檜山さんが反応してくださいまして。いやレスつけにくい記事ですいません。

せっかくなので、檜山さんの記事をまんまAlloyに翻訳してみよう…と思ったのですが*1、実は大きな問題があって。

Alloyには、直和を直接扱う言語要素がないんですなー。

ということで前振りとして、Alloyで直和を書き下してみて、どうなるかってのを観察してみます。

今回使うAlloyの記述全文はGistに貼ったので、よろしければそちらを参照のこと。

えーまず

いきなりですが、直和をこさえます。どーん。

enum Tag { Fst, Snd }

fun prod1(a, b: univ): Tag -> univ {
  Fst -> a + Snd -> b
}

prod1が、適当な集合a, bを受け取って(univは何でもアリな型です。java.lang.Objectみたいな)、aとbの直和を返す関数。返り値の型 Tag -> univ が直和型です。脳内でそういう風にフィルタかけて読んで下さい。

やってることは見ての通り、1番め・2番め(Fst, Snd)ってタグを付けた上で集合和を取るんですね。

prod って書いてるのは、上記の檜山さんの記事にある「(圏論的)直積=(圏論的)直和」に倣ってるので、ここでは良いネーミングじゃないかもですが。

試しに

run prod1

とか打ってevaluate ... してみても、ビジュアル的にはあんまり面白くないものが出ます。Evaluatorボタンを押して、prod1に適当な引数渡して評価してみてください。

対角、余対角

さて、任意の要素を直和に持っていく対角Δは次のように書けます。

fun diag (a: univ): Tag -> univ {
  Fst -> a + Snd -> a
}

diagがΔに相当する関数です。Fstタグ、Sndタグに同じ要素を入れた直和を返します。

一方、直和から要素に潰す余対角∇は

fun codiag (a: Tag -> univ): univ {
  { b: univ | b in Fst.a or b in Snd.a }
}

とか書けます。直和のFstタグ側かSndタグ側か、どちらかにある要素の集合、です。

…ですがこれ、もっと簡単にかけて、

fun codiag (a: Tag -> univ): univ {
  Tag.a
}

です。ついてるタグを忘れる操作。


そして、対角と余対角を合成すると、idと同じになります。

これは以下のアサーションで反例が出ないことからわかっていただけるかと。

cmp_id: check {
  all x: univ | x.diag.codiag = x
}

単位元

さてここで、直和操作の単位元について考えてみます。これは、空集合Alloyでいう none)でございます。檜山さんの記事にあった、零対象がこれに当たります。

noneとの直和取ったものは元の要素と同型です。

これは、noneとの直和取って、タグ忘れたら元に戻る、という意味の以下のアサーションで反例が出ないことから確かめられます。

zero_is_unit1: check {
  all x: univ {
    prod1 [x, none].codiag = x
    prod1 [none, x].codiag = x
  }
}

2項関係に拡張

さてさて、集合(=単項関係=アリティ1の関係)について、直和を考えることができました。

次は、2項関係=アリティ2の関係の直和について。またいちいちこさえます。

fun prod2 (f, g: univ -> univ): Tag -> (univ -> univ) {
  Fst -> f + Snd -> g
}

prod1 とまったく理屈は同じです。

そして2項関係を考えたからには、他のものとの結合を考えたくなりますね。なりませんか?なるでしょ?

ということで。結合も作ります。(言語要素にないってめんどくさいねー)

fun join2 (x: Tag -> univ, r: Tag -> (univ -> univ)): Tag -> univ {
  Fst -> (Fst.x.(Fst.r)) + Snd -> (Snd.x.(Snd.r))
}

わかりますでしょうか。Fstタグ付きはFstタグ付き同士、Sndタグ付きはSndタグ付き同士で結合して、改めてタグを付け直しております。

直感的には x.r って操作をやりたい訳なんですが、直接は上手くいかないので、この関数で結合のドットを代用しようという腹です。

で、こうしてやると、元の檜山さんの記事にあった足し算の定義

Δ;(f×g);∇

ってのが書けるようになります。こんな↓感じ。

fun sum2 (f, g: univ -> univ): univ -> univ {
  { x, y: univ | y in x.diag.join2 [ prod2 [f, g] ].codiag }
}

diagがΔ、prod2[f,g] が f×g、codiagが∇。

適当なxに対して y ∈ x;Δ;(f×g);∇ となるようなyを集めて、ペア (x, y) の集合を作っているわけです。2項関係はペアの集合でできています。よってこれは、間に Δ;(f×g);∇ が成り立つような2項関係を作っているわけです。

これも run sum2 とかやって、Evaluatorで遊んでみてくださいな。


しかし、ですね。

Alloyでは、2項関係同士の足し算は直接書けて

f+g

なんですなー。

ということで、この2種類の足し算が同じもの、っていう、以下の様なアサーションを書いてみます。反例でないはずです。

sum_equiv: check {
  all f, g: univ -> univ | sum2 [f, g] = (f + g)
}

結論

以上、回りくどくなりましたが。

Alloyには表面上プリミティブに存在しない直和ですが、裏側に暗黙的に存在してて、立派に足し算を成立させることができているのです。

ということで、時間があったらこの結果を使って、Alloyで檜山さんの記事を書き直す試みをやってみます。時間があれば。

*1:実は前回も同じようなことを考えて途中でヘタれたのでした。

2014-04-06

ドメイン付きクリーネ代数をAlloyで

| 23:03 | ドメイン付きクリーネ代数をAlloyでを含むブックマーク

久々すぎて、はてなの書き方を忘れてしまいました。

さて(脈絡なし):

上記の記事を今更読んだのですが*1、そういや私め、昔テスト付きクリーネ代数…の拡張のドメイン付きクリーネ代数(Kleene Algebra with Domain, KAD)Alloyで書いてみたことがありまして。

cf. [cs/0310054] Kleene algebra with domain -- arXiv

GitHubに置いてあるので、とりあえずリンク貼っときます。

このモデルでは、クリーネ代数シグネチャProp上の2項関係 Prop->Prop で表現していて、ブール値はPropの集合で、乗法はドット結合、論理積は集合積で書いてました。たとえば、

(p∧q)・f = p・(q・f)

    (p & q).toKA.f = p.toKA.(q.toKA).f

と書けて(toKAはブールをクリーネ代数に持っていくおまじない)、こんな↓アサーションを書いてやっても反例は出ないようにはなっております。

def_and: check {
  all p, q: set Prop, f: Prop->Prop {
    (p & q).toKA.f = p.toKA.(q.toKA).f
  }
} for 10

以上、ほとんどメモ的な内容で具体的な説明なしで大変不親切なのですが。

最近またKADが自分内でリバイバルし始めてて、本当はがっつり解説書こうかと思ったんですが何かダレた。一部直観的でないところがあったり、今見るとイマイチだなーと思うところもあったりですが、とりあえず。

気分が乗ったら追加でまた書くかも。

*1:ちょうど自分がKATを知った頃に読んだのがこれで、そうかー檜山さん的にはイマイチなのかー、と思った記憶。

2012-05-15

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

| 07:53 |  シグネチャのフィールドにある関係の多重度 続きを含むブックマーク

昨日の日記 の続き。 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

koji8ykoji8y 2012/05/15 09:46 ありがとうございます(^^) lone か〜.すっきりしました.

ところで functional, bijective 等の記述をどこかで見たなと記憶をたどってみたら,alloy4.2-rc.jar の中,
(jar xf alloy4.2-rc.jar で展開して出てくる) models/util/relation.als にあるんですね.

pred functional [r: univ->univ, s: set univ] {
all x: s | lone x.r
}

みたいな形で.
# まあ Cheatsheet そのままですが :-)

bonotakebonotake 2012/05/15 20:00 はい。(ご存知かもですが)Alloy本の原著にも、その辺の説明があります(3章)。
日本語版だと、「関数的」「短射的」といった言葉をあてています。

2012-05-14

スタートAlloyやりました

| 21:53 | スタートAlloyやりましたを含むブックマーク

cf. http://atnd.org/events/27160

ヒジョーに適当な準備だけで(テキトーな資料でホントすいません)、しかも「習うより慣れろ」と吹いてAlloy言語のレクチャーほとんどなしに演習やってもらうという無謀な試みにも関わらず、(Alloy初心者の方々も含め)全体的に皆さん大健闘されまして、僕としてはうれしい誤算でした。

というか、やってみるもんだなぁ。僕もいろいろ勉強になりました。

当日の演習課題について

課題にしたのは「バージョン管理システムモデリング」。

  1. 1人だけで使う状況を考える
  2. 複数人で使う状況を考える
  3. 発展的課題

…と、3問用意していたのですが、実は1. だけでも半日〜数日は余裕で遊べる、ヒジョーに難しい課題でした*1

何が難しいかというとですね。

普通のOS上のファイルシステムなら、同一フォルダ内で同じファイルかどうか、というのは、同じファイル名かどうかで単純に区別がつきます。

ところが、バージョン管理システムでは、それ以外に

  • リポジトリ内とローカルファイルとで別々に存在するファイルが同一のものか否か
  • 同じリポジトリ内で、リビジョン違いの同一ファイルか否か

があり、「ファイル」という概念に3種類の同一性を導入しないといけないのです。

ということで、かなりハードだったはずです。でも皆さん、その全てではないにしても、問題の本質に気づいてそれなりにモデリングをこなされていたので、すばらしかったです。

AlloyモデリングTips

で、今回皆さんのさまざまな反応を見て思った、Alloyでのモデリングのコツ。自分のためにも残しておきます。

とにかくシンプルに、シンプルに。

設計対象の本質(「抽象」)だけをモデル化していくべし。

言い換えると、「それがなかったら、このシステムは実現不可能」な概念だけを導入してください。

たとえば、バージョン管理システムに「ファイルの差分」という概念は、必ずしも必要ではないですよね。

自分の中の「仕様」を疑え。

プログラミングAlloyを使ったモデリングは、似ているようで、決定的に違うところがあります。

それは、Alloyの出力結果が正しくて、自分の頭の中の仕様が間違ってるケースが多々あるということです。そもそも、元々ぼんやりとした要求しかないところから、仕様を考える作業をしているのだから、当たり前です。

だから、Alloyが変なインスタンスを出してきたからといって、すぐにバグ扱いしないでください。それ以前にまず、それをバグだとする判断が自分の思い込みではないのかを疑ってください。

想像力を働かせて、現実にそういう状況が起こりうるのか、起こっても大丈夫かが確認できたら、それはスルーして大丈夫なのです。むしろ積極的に、そういう状況を受け入れ可能なように、自分の脳内イメージを改めてください。

制約を緩めることも大事。

(上記を踏まえた上で)どう考えてもあってはならないインスタンスが出力されたら、それはモデルに制約を追加するときです。

一方、意図したようなインスタンスが出力されなかったら、それは十中八九モデル中の制約が強すぎるときです。なので、このときは逆に、制約を緩めないといけません。ここで更に制約を追加すると、おかしなことになります。

そして、注意すべきは、制約が少なければ少ないほど、システムは堅牢になるということです。制約とはシステムが正常動作する前提条件です。余計な前提条件があればあるほど、脆いシステムになってしまいます。

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

| 22:33 |  シグネチャのフィールドにある関係の多重度を含むブックマーク

さて、スタートAlloy中、頂いたテクニカルな質問のうち1つに、当日うまく答えられませんでした(すいません… orz)。

ちゃんと考え直したので(^^; ここに書いておきます。(thx to @masahiro_sakaiさん)

質問

以下のようなシグネチャ宣言があったとする。

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

ここで、Bのスコープを1にすると、任意の a: A から得られる a.r が全部同じになってしまう。

たとえば、以下のようなコマンドで反例が出ない。

check {
  all disj a1, a2: A | a1.r = a2.r
} for 3 but 1 B

たとえば a1.r は空で、a2.r は空でないような可能性があるように思うが、なぜないのか?

回答

まず、シグネチャのフィールドにある関係は、次のように解釈されます。(Alloy本 p.261)

…したがって、例えば

sig S {f: e}

という宣言によって導入される制約は、(fを通常の変数とした場合の)fが式eの部分集合であるという制約ではなく、以下のような制約になる。

all this: S | this.f in e

よって、先ほどのシグネチャA内のフィールドrの宣言は、

all a: A | a.r in B one -> one C

という制約だと解釈されます。(thisはaに置き換えました)

更に、関係の中の多重度についてですが、(Alloy本 p. 76)

多重度は単なる省略記法であり、標準的な制約に置き換えることができる。以下の多重度制約は、

r: A m -> n B

以下のように書き換えることができる。

all a: A | n a.r
all b: B | m r.b

とあります。コロンは in と読み替えても意味的には同じです。

ということで、先ほどの制約式を、更に展開すると

all a: A | all b: B | one b.(a.r)
all a: A | all c: C | one (a.r).c

となります。

なので、Bのスコープが1だと、B、C ともに空で a.r が常に空になるか、B、C ともにサイズ1で、aによらず a.r が存在して一意に定まるか、いずれかになります。

追記

続きを書きました → シグネチャのフィールドにある関係の多重度 続き - たけをの日記@天竺から帰ってきたよ

*1:実際のところ、難しすぎるなーと思って予備に回していたお題だったのですが、本命で考えていた課題が、自分でやってみると逆に単純すぎて、直前で取りやめざるを得なかったのでした。