Alloyはモノを抽象的に記述したり、それらの関係を数学で言うところの「関係」でもって記述する言語です。
さらに、そこで記された制約を満足する例を見つけたり、制約に対する反例を見つけたりするための解析器がついてます。
プログラムの仕様をこれで記述して、それに対して見落しがないかを探すのに便利みたいです。
公式サイトhttp://alloy.mit.edu/alloy/の記述を引用すると、
Alloy is a language for describing structures and a tool for exploring them. It has been used in a wide range of applications from finding holes in security mechanisms to designing telephone switching networks.
ということになります。
以前http://ashiato45.hatenablog.jp/entry/2017/02/08/220148で、環に対する反例を見つけるのにAlloyを使おうと思ってこの本
で勉強していたのですが、ざっくり読んだので
id:qnighyさんが以前群でやっていたのを思い出しつつ
Alloyで群の性質を調べてみました。
できたコードはhttps://gist.github.com/ashiato45/b46837f5ff1237fa9c12e64ddaf4711eにあります。
sig Element{}
one sig Group{
elements: set Element,
unit: one elements,
mult: elements -> elements -> one elements,
inv: elements -> one elements
}
fact NoRedundantElements{
all e: Element | e in Group.elements
}まず元としてElementを宣言しておきます。これで、何らかの集合Elementが定義されます*1。
それで、群を定義します。群は要素を持ち、うち丁度1つが単位元で、2つの元に対して丁度1つ元を定めるmultがあり、1つの元に対してその逆元を求めるinvがあるということを記述します。いま1つの群についてのみ考えたいので、「one sig Group」とすることでGroupは群を丁度1つだけ含む集合ということにします*2。NoRedundantElementsというfactで、このモデルにあらわれる要素というのはすべて群で使うものとします。この制約がないと、特に意味のない元が例に現れてしまって邪魔です。
fact UnitLaw1{
all a: Group.elements | Group.mult [a] [Group.unit] = a
}
fact UnitLaw2{
all a: Group.elements |
Group.mult [Group.unit] [a] = a
}
fact AssociativeLaw{
all a: Group.elements | all b: Group.elements | all c:Group.elements |
Group.mult [Group.mult [a] [b]] [c] = Group.mult [a] [Group.mult [b] [c]]
}
fact InvLaw1{
all a: Group.elements | Group.mult [Group.inv[a]] [a] = Group.unit
}
assert InvLaw2 {
all a: Group.elements | Group.mult [a] [Group.inv[a]] = Group.unit
}
check InvLaw2さらに、群の制約を書き足します。単位元の制約、結合則はいいのですが、逆元について制約は、「任意の元aについて、aのinvは左からかけると単位元になる」ということしか言っていません。InvLaw2は同じことを右からで言っているのですが、こちらは制約ではなくただの成り立ってほしいと思っている命題です。ここで、最後の行でこの命題が成り立つかを検査します。結果、Alloyの検査器は「多分正しい」と教えてくれます。「多分」というのはAlloyは有限個の範囲でしか検査せず、デフォルトだとすべての集合が3つ以下しか元を持たないという制約のもとで(上手に)総当たりします*3。これで、「多分正しいだろう」と人間も予想できるので証明してみます。示すことは、「任意の元bについて、ここで定義した意味でのbのinvは右からかけると単位元になる」ということ。bのinvのことを、
と書くことにし、単位元はeで書きます。
aをいま考えている群の元とする。InvLaw1から、
となる。同様に、
となる。よって、結合則より
となる。よって、任意のaについて
が成立する。
bを群の元とする。先のことから、
となり、
となる。証明おわり。
ということでこのcheckはコメントアウトして先に進む。
次に、
run {}で、ここまでの制約をみたすような例を表示してみます。Executeを実行して、Showをクリックすると訳のわからん図が出てきます。ここで、図のなかにGroupが出てきてるのが邪魔なので、表示画面の「Theme」をクリックして、出てくる「sig Group」を選択し、「Project over this sig」をonにして「Close」すると
こんな感じで群が出てきます。Element1に「unit」と書いてあるので、これが単位元だとわかります。この群はもちろんZ/2Zで演算を和としたものです。
さらに、Nextをクリックすると他の例を探してくれます。いくらか押すと、位数3の群も出てきます。
若干演算がよく分からないので、「Evaluator」をクリックします。ここでは、対話型で出てきた例を調べることができます。
ここで、「Group.mult」と叩くと演算multがどうなっているかが見えます。
もう満足したので、このrunはコメントアウトして先に進みます。
assert Commutativity{
all a: Group.elements | all b: Group.elements | Group.mult [a] [b] = Group.mult [b] [a]
}
check Commutativity for 5このassertは群が可換であることを意味します。そして、checkでこれが本当に成立するかどうかを確かめます。「for 5」がついていて、位数5以内でこれを確かめます。Executeを押すと「多分正しい」と出てきます。これで、この命題は多分正しそうだということになり、「全ての群は可換である」という気がしてくるのですが*4、念の為もうちょっと大きく、
check Commutativity for 6
と変えて実行すると、「反例が見つかりました」と出てきます。すごい。
これで満足したのでcheckはコメントアウトして先に進みます。
今回私が本当に調べたかったのは、
Gを群とし、AをGの正規部分群、BはAの正規部分群とする。このとき、BはGの正規部分群か？
です。これは割と落とし穴でちょっと考えるぐらいだと分かりません。このためには、
pred subgroup (g: set Element, h: set Element){
(all a: g | a in h) and
(Group.unit in g) and
(all a, b: g | Group.mult [a] [b] in g) and
(all a: g | Group.inv[a] in g)
}
pred regularSubgroup(n: set Element, g: set Element){
subgroup [n, g] and
(all n0: n, g0: g | Group.mult [Group.mult [g0] [n0]] [Group.inv[g0]] in n)
}
pred main(n1: set Element, n2: set Element){
let g = Group.elements |
regularSubgroup [n1, g] and
(some g0: g | (not g0 in n1)) and
regularSubgroup [n2, n1] and
(some n10: n1 | (not n10 in n2)) and
(not regularSubgroup [n2, g])
}と書きます。subgroupは要素の集合2つをとる述語で、その範囲で演算が閉じているかを確かめます。
regularSubgroupも要素の集合2つをとって、正規部分群になっているかを調べます。
mainが調べたいことで、特に意味はないのですが真の正規部分群になっているという条件もついてます。これで
run main for 7
とすると「多分正しい」となります。さらに、「for 8」としてみると、今度は反例を見つけてくれます。
めでたしめでたし。
