Structures
What Are Structures?
Structures define mathematical objects with their properties and operations. Think of them as “blueprints” for mathematical concepts.
structure Vector(n : ℕ) {
// Operations this structure supports
operation add : Vector(n) → Vector(n)
operation scale : ℝ → Vector(n)
operation dot : Vector(n) → ℝ
// Properties that must hold
axiom commutative : ∀(u : Vector(n))(v : Vector(n)).
add(u, v) = add(v, u)
}
Structure Syntax
structure Name(parameters) {
// Elements (constants)
element1 : Type1
// Operations (functions)
operation op1 : InputType → OutputType
// Axioms (properties)
axiom property : logical_statement
}
Structure Members
Structures contain three kinds of members:
The operation Keyword
The operation keyword declares a function that the structure provides:
structure Group(G) {
operation mul : G × G → G // Binary operation
operation inv : G → G // Unary operation
}
Operations declare the signature (types), not the implementation. The implementation is provided in an implements block (see Chapter 10).
The element Keyword
The element keyword declares a distinguished constant of the structure:
structure Monoid(M) {
element e : M // Identity element
operation mul : M × M → M
axiom identity : ∀(x : M). mul(e, x) = x
}
structure Field(F) {
element zero : F // Additive identity
element one : F // Multiplicative identity
}
Elements are constants that satisfy the structure’s axioms. You can also write elements without the element keyword:
structure Ring(R) {
zero : R // Same as "element zero : R"
one : R
}
The axiom Keyword
The axiom keyword declares a property that must hold:
structure Group(G) {
element e : M
operation mul : G × G → G
operation inv : G → G
axiom identity : ∀(x : G). mul(e, x) = x ∧ mul(x, e) = x
axiom inverse : ∀(x : G). mul(x, inv(x)) = e
axiom associative : ∀(x : G)(y : G)(z : G). mul(mul(x, y), z) = mul(x, mul(y, z))
}
Axioms are verified by Z3 when you use implements blocks or run kleis verify.
Example: Complex Numbers
structure Complex {
re : ℝ // real part
im : ℝ // imaginary part
operation add : Complex → Complex
operation mul : Complex → Complex
operation conj : Complex // conjugate
operation mag : ℝ // magnitude
axiom add_commutative : ∀(z : Complex)(w : Complex).
add(z, w) = add(w, z)
axiom magnitude_positive : ∀(z : Complex).
mag(z) ≥ 0
axiom conj_involution : ∀(z : Complex).
conj(conj(z)) = z
}
Parametric Structures
Structures can have type parameters:
structure Matrix(m : ℕ, n : ℕ, T) {
operation transpose : Matrix(n, m, T)
operation add : Matrix(m, n, T) → Matrix(m, n, T)
axiom transpose_involution : ∀(A : Matrix(m, n, T)).
transpose(transpose(A)) = A
}
// Square matrices have more operations
structure SquareMatrix(n : ℕ, T) extends Matrix(n, n, T) {
operation det : T
operation trace : T
operation inv : SquareMatrix(n, T)
axiom det_mul : ∀(A : SquareMatrix(n, T))(B : SquareMatrix(n, T)).
det(mul(A, B)) = det(A) * det(B)
}
Nested Structures
Structures can contain other structures. This enables compositional algebra — defining complex structures from simpler parts:
structure Ring(R) {
// A ring has an additive group
structure additive : AbelianGroup(R) {
operation add : R × R → R
operation negate : R → R
zero : R
}
// And a multiplicative monoid
structure multiplicative : Monoid(R) {
operation mul : R × R → R
one : R
}
// With distributivity connecting them
axiom distributive : ∀(x : R)(y : R)(z : R).
mul(x, add(y, z)) = add(mul(x, y), mul(x, z))
}
Nested structures can go arbitrarily deep:
structure VectorSpace(V, F) {
structure vectors : AbelianGroup(V) {
operation add : V × V → V
zero : V
}
structure scalars : Field(F) {
operation add : F × F → F
operation mul : F × F → F
}
operation scale : F × V → V
}
When using Z3 verification, axioms from nested structures are automatically available.
The extends Keyword
Structures can extend other structures:
structure Monoid(M) {
e : M
operation mul : M × M → M
axiom identity : ∀(x : M). mul(e, x) = x ∧ mul(x, e) = x
axiom associative : ∀(x : M)(y : M)(z : M).
mul(mul(x, y), z) = mul(x, mul(y, z))
}
structure Group(G) extends Monoid(G) {
operation inv : G → G
axiom inverse : ∀(x : G). mul(x, inv(x)) = e ∧ mul(inv(x), x) = e
}
structure AbelianGroup(G) extends Group(G) {
axiom commutative : ∀(x : G)(y : G). mul(x, y) = mul(y, x)
}
The over Keyword
Many mathematical structures are defined “over” a base structure. A vector space is defined over a field, a module over a ring:
// Vector space over a field
structure VectorSpace(V) over Field(F) {
operation add : V × V → V
operation scale : F × V → V
axiom scalar_identity : ∀(v : V). scale(1, v) = v
axiom distributive : ∀(a : F)(u : V)(v : V).
scale(a, add(u, v)) = add(scale(a, u), scale(a, v))
}
// Module over a ring (generalization of vector space)
structure Module(M) over Ring(R) {
operation add : M × M → M
operation scale : R × M → M
}
// Algebra over a ring
structure Algebra(A) over Ring(R) {
operation add : A × A → A
operation scale : R × A → A
operation mul : A × A → A
axiom bilinear : ∀(r : R)(a : A)(b : A).
scale(r, mul(a, b)) = mul(scale(r, a), b)
}
When you use over, Kleis automatically makes the base structure’s axioms available for verification. For example, when verifying VectorSpace axioms, Z3 knows that F satisfies all Field axioms.
Differential Geometry Structures
Kleis shines for differential geometry:
structure Manifold(M, dim : ℕ) {
operation tangent : M → TangentSpace(M)
operation metric : M → Tensor(0, 2)
axiom metric_symmetric : ∀(p : M).
metric(p) = transpose(metric(p))
}
structure RiemannianManifold(M, dim : ℕ) extends Manifold(M, dim) {
operation christoffel : M → Tensor(1, 2)
operation riemann : M → Tensor(1, 3)
operation ricci : M → Tensor(0, 2)
operation scalar_curvature : M → ℝ
// R^a_{bcd} + R^a_{cdb} + R^a_{dbc} = 0
axiom first_bianchi : ∀(p : M).
cyclic_sum(riemann(p)) = 0
}
What’s Next?
Learn how to implement structures!