Alloy による群のモデリング

alloy_group.als

// ************************************
//   群のモデル
// ************************************

// ------------------------------------
//   群の公理
// ------------------------------------

// 群の元
sig Element {
    action : Element -> one Element  // 自身への右作用
}

// (左) 単位元
sig Unit extends Element {}

// 作用を二項演算子風にシュガー
fun op (x, y : Element) : Element {
    y.(x.action)
}

// (左) 逆元を関数として呼び出し可能に
fun inv (x : Element) : Element {
    { y : Element | op[y, x] = Unit }
}

// 少なくとも 1 個の元が存在
fact nonempty {
    some Element
}

// 結合律
fact associativity {
    all x, y, z : Element | op[x, op[y, z]] = op[op[x, y], z]
}

// 左単位元律
fact leftUnitLaw {
    all x : Element | op[Unit, x] = x
}

// 左逆元律
fact leftInverseLaw {
    all x : Element | some inv[x]
}


// ------------------------------------
//   導出できる性質
// ------------------------------------

// (左) 単位元の一意性
assert uniqUnit {
    one Unit
}
check uniqUnit for 5 Element

// (左) 逆元の一意性
assert uniqInv {
    all x : Element | one inv[x]
}
check uniqInv for 5 Element

// 右単位元律
assert rightUnitLaw {
    all x : Element | op[x, Unit] = x
}
check rightUnitLaw for 5 Element

// 右逆元律
assert rightInvLaw {
    all x : Element | op[x, inv[x]] = Unit
}
check rightInvLaw for 5 Element


// ------------------------------------
//   群構造の例
// ------------------------------------

// 巡回群
pred cyclic {
    // gen は生成元
    some gen : Element | all x : Element | x in Unit.^(gen.action)
}
run cyclic for exactly 4 Element
run cyclic for exactly 5 Element
run cyclic for exactly 6 Element

// 二面体群
pred dihedral {
    some s, t : Element {
        // s は回転、t は鏡映
        Unit in Unit.^(s.action)
        op[t, t] = Unit
        op[s, t] = op[t, inv[s]]
        // s と t とが全体を生成
        all x : Element | x in (Unit + t).*(s.action)
    }
}
run dihedral for exactly 6 Element
run dihedral for exactly 7 Element  // 奇数位数の二面体群は存在しない
run dihedral for exactly 8 Element

// 四元数群
pred quaternion {
    // n は 通常 -1 と表記される元で、任意の元と可換
    some disj n, i, j, k : Element - Unit {
        all x : Element | op[n, x] = op[x, n]
        op[i, i] = n
        op[j, j] = n
        op[k, k] = n
        op[i, j] = k
        op[j, k] = i
        op[k, i] = j
        op[j, i] = op[n, k]
        op[k, j] = op[n, i]
        op[i, k] = op[n, j]
        Element = (iden + n.action).(Unit + i + j + k)
    }
}
run quaternion for 8 Element