79 lines
1.9 KiB
Plaintext
79 lines
1.9 KiB
Plaintext
|
// Monoid: a set with an associative binary operation and identity element
|
|||
|
|
//
|
|||
|
|
// This is the simplest algebraic structure with interesting axioms.
|
|||
|
|
// Note: geolog uses postfix function application.
|
|||
|
|
|
|||
|
|
theory Monoid {
|
|||
|
|
M : Sort;
|
|||
|
|
|
|||
|
|
// Binary operation: M × M → M
|
|||
|
|
mul : [x: M, y: M] -> M;
|
|||
|
|
|
|||
|
|
// Identity element: we use a unary function from M to M that
|
|||
|
|
// "picks out" the identity (any x maps to e)
|
|||
|
|
// A cleaner approach would use Unit → M but that needs product support.
|
|||
|
|
id : M -> M;
|
|||
|
|
|
|||
|
|
// Left identity: id(x) * y = y (id(x) is always e)
|
|||
|
|
ax/left_id : forall x : M, y : M.
|
|||
|
|
|- [x: x id, y: y] mul = y;
|
|||
|
|
|
|||
|
|
// Right identity: x * id(y) = x
|
|||
|
|
ax/right_id : forall x : M, y : M.
|
|||
|
|
|- [x: x, y: y id] mul = x;
|
|||
|
|
|
|||
|
|
// Associativity: (x * y) * z = x * (y * z)
|
|||
|
|
ax/assoc : forall x : M, y : M, z : M.
|
|||
|
|
|- [x: [x: x, y: y] mul, y: z] mul = [x: x, y: [x: y, y: z] mul] mul;
|
|||
|
|
|
|||
|
|
// id is constant: id(x) = id(y) for all x, y
|
|||
|
|
ax/id_const : forall x : M, y : M.
|
|||
|
|
|- x id = y id;
|
|||
|
|
}
|
|||
|
|
|
|||
|
|
// Trivial monoid: single element, e * e = e
|
|||
|
|
instance Trivial : Monoid = {
|
|||
|
|
e : M;
|
|||
|
|
|
|||
|
|
// Multiplication table: e * e = e
|
|||
|
|
// Using positional syntax: [a, b] maps to [x: a, y: b]
|
|||
|
|
[e, e] mul = e;
|
|||
|
|
|
|||
|
|
// Identity: e is the identity element
|
|||
|
|
e id = e;
|
|||
|
|
}
|
|||
|
|
|
|||
|
|
// Boolean "And" monoid: {T, F} with T as identity
|
|||
|
|
// T and T = T, T and F = F, F and T = F, F and F = F
|
|||
|
|
instance BoolAnd : Monoid = {
|
|||
|
|
T : M;
|
|||
|
|
F : M;
|
|||
|
|
|
|||
|
|
// Identity: T is the identity element
|
|||
|
|
T id = T;
|
|||
|
|
F id = T;
|
|||
|
|
|
|||
|
|
// Multiplication table for "and":
|
|||
|
|
[x: T, y: T] mul = T;
|
|||
|
|
[x: T, y: F] mul = F;
|
|||
|
|
[x: F, y: T] mul = F;
|
|||
|
|
[x: F, y: F] mul = F;
|
|||
|
|
}
|
|||
|
|
|
|||
|
|
// Boolean "Or" monoid: {T, F} with F as identity
|
|||
|
|
// T or T = T, T or F = T, F or T = T, F or F = F
|
|||
|
|
instance BoolOr : Monoid = {
|
|||
|
|
T : M;
|
|||
|
|
F : M;
|
|||
|
|
|
|||
|
|
// Identity: F is the identity element
|
|||
|
|
T id = F;
|
|||
|
|
F id = F;
|
|||
|
|
|
|||
|
|
// Multiplication table for "or":
|
|||
|
|
[x: T, y: T] mul = T;
|
|||
|
|
[x: T, y: F] mul = T;
|
|||
|
|
[x: F, y: T] mul = T;
|
|||
|
|
[x: F, y: F] mul = F;
|
|||
|
|
}
|