合金模型代数群答案

【问题标题】：Alloy model an algebraic group合金模型代数群
【发布时间】：2012-03-23 13:19:31
【问题描述】：

我正在尝试用 Alloy 对代数群的结构进行建模。

一个组只有一组元素和具有某些属性的二元关系，所以我认为它非常适合合金。

这就是我的开始

sig Number{}
/* I call it Number but this is really just a name for some objects that are going to be in the group */

sig Group{
member: set Number,
product: member->member->member, /*This is the part I'm really not sure about the Group is supposed to have a a well-defined binary relation so I thought maybe I could write it like this, sort of as a Curried function...I think it's actually a ternary relation in Alloy language since it takes two members and returns a third member */
}{//I want to write the other group properties as appended facts here.

 some e:member | all g:member| g->e->g in product //identity element
all g:member | some i:member| g->i->e in product /* inverses exist I think there's a problem here because i want the e to be the same as in the previous line*/
all a,b,c:member| if a->b->c and c->d->e and b->c->f then a->f->e //transitivity
all a,b:member| a->b->c in product// product is well defined

}

【问题讨论】：

标签： algebra alloy

【解决方案1】：

我自己只学了一点Alloy，但是从谓词逻辑的角度来看，您的“逆存在”问题看起来很简单；将前两个属性替换为

some e:member {
  all g:member | g->e->g in product //identity element
  all g:member | some i:member | g->i->e in product // inverses exist
}

通过将inverse属性放在e的量词范围内，它指的是同一个e。

我还没有测试过。

【讨论】：

【解决方案2】：

这是在 Alloy 中编码组的一种方式：

module group[E]

pred associative[o : E->E->E]{  all x, y, z : E | (x.o[y]).o[z] = x.o[y.o[z]]   }

pred commutative[o : E->E->E]{  all x, y : E | x.o[y] = y.o[x]  }

pred is_identity[i : E, o : E->E->E]{   all x : E | (i.o[x] = x and x = x.o[i]) }

pred is_inverse[b : E->E, i : E, o : E->E->E]{  all x : E | (b[x].o[x] = i and i = x.o[b[x]])   }

sig Group{
op : E -> E->one E, inv : E one->one E, id : E
}{
associative[op] and is_identity[id, op] and is_inverse[inv, id, op] }

sig Abelian extends Group{}{    commutative[op] }

unique_identity: check {
all g : Group, id' : E | (is_identity[id', g.op] implies id' = g.id)
} for 13 but exactly 1 Group

unique_inverse: check {
all g : Group, inv' : E->E | (is_inverse[inv', g.id, g.op] implies inv' = g.inv)
} for 13 but exactly 1 Group

【讨论】：