合金モデル代数群

Question

私は合金で代数群の構造をモデル化しようとしています。

グループには要素のセットと特定のプロパティを持つバイナリリレーションがありますので、合金に適していると思いました。

これは私が

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 

} 

Answer 1

は、合金中のグループをコードする1つの方法です：

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 

Answer 2

で開始するものである私はちょうど合金のビットを自分自身のことを学びましたが、あなたの問題は述語論理の観点から、簡単に見える「逆行列が存在します」。 eの数量詞の範囲で逆の特性を置くことによって

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 
} 

であなたの最初の2つのプロパティを置き換え、それは同じeを参照しています。

これはテストしていません。ここで