The Kleis Manual

“Mathematics is the language with which God has written the universe.” — Galileo Galilei

Welcome to The Kleis Manual, the official guide to the Kleis mathematical specification language.

What is Kleis?

Kleis is a structure-oriented mathematical formalization language with Z3 verification and LAPACK numerics.

Philosophy: Structures — the foundation of everything.

Core Capabilities

• 🏗️ Structure-first design — define mathematical objects by their axioms, not just their data
• ✅ Z3 verification — prove properties with SMT solving
• 🔢 LAPACK numerics — eigenvalues, SVD, matrix exponentials, and more
• 📐 Symbolic mathematics — work with expressions, not just numbers
• 🔬 Scientific computing — differential geometry, tensor calculus, control systems
• 🔄 Turing complete — a full programming language, not just notation

Computational Universality: Kleis is Turing complete. This was demonstrated by implementing a complete LISP interpreter in Kleis (see Appendix: LISP Interpreter). The combination of algebraic data types, pattern matching, and recursion enables arbitrary computation.

Domain Coverage

Kleis has been used to formalize:

Who is This For?

Kleis is for anyone who thinks in terms of structures and axioms:

• Mathematicians — formalize theorems, verify properties, explore number theory
• Physicists — tensor algebra, differential geometry, dimensional analysis
• Engineers — control systems, protocol specifications, verified designs
• Security architects — authorization policies (Zanzibar, OAuth2)
• Researchers — formalize new theories with Z3 verification
• Functional programmers — if you enjoy Haskell or ML, you’ll feel at home

If you’ve ever wished you could prove your specifications are consistent, Kleis is for you.

Why Kleis Now?

Modern systems demand formal verification:

Universal verification — same rigor for mathematics, business rules, and beyond.

How to Read This Guide

Each chapter builds on the previous ones. We start with the basics:

1. Starting Out — expressions, operators, basic syntax
2. Types — naming and composing structures
3. Functions — operations with laws

Then we explore core concepts:

4. Algebraic Types — data definitions and constructors
5. Pattern Matching — elegant case analysis
6. Let Bindings — local definitions
7. Quantifiers and Logic — ∀, ∃, and logical operators
8. Conditionals — if-then-else

And advanced features:

9. Structures — the foundation of everything
10. Implements — structure implementations
11. Z3 Verification — proving things with SMT

Philosophy: In Kleis, structures define what things are through their operations and axioms. Types are names for structures. A metric tensor isn’t “a 2D array” — it’s “something satisfying metric axioms.”

A Taste of Kleis

Here’s what Kleis looks like:

// Define a function
define square(x) = x * x

// With type annotation
define double(x : ℝ) : ℝ = x + x

// Create a structure with axioms
structure Group(G) {
    operation e : G                    // identity
    operation inv : G → G              // inverse
    operation mul : G × G → G          // multiplication
    
    axiom left_identity : ∀ x : G . mul(e, x) = x
    axiom left_inverse : ∀ x : G . mul(inv(x), x) = e
}

// Numerical computation
example "eigenvalues" {
    let A = Matrix([[1, 2], [3, 4]]) in
    out(eigenvalues(A))  // Pretty-printed output
}

Getting Started

Ready? Let’s dive in!

→ Start with Chapter 1: Starting Out

Starting Out

Your First Kleis Expression

The simplest things in Kleis are expressions. An expression is anything that has a value:

define answer = 42              // A number
define pi_approx = 3.14159      // A decimal
define sum(x, y) = x + y        // An arithmetic expression
define angle_sin(θ) = sin(θ)    // A function call

The REPL

The easiest way to experiment with Kleis is the REPL (Read-Eval-Print Loop):

$ cargo run --bin repl
🧮 Kleis REPL v0.1.0
   Type :help for commands, :quit to exit

λ> 2 + 2
2 + 2

λ>  let x = 5 in x * x
times(5, 5)

Basic Arithmetic

Kleis supports the usual arithmetic operations:

define add_example = 2 + 3       // Addition: 5
define sub_example = 10 - 4      // Subtraction: 6
define mul_example = 3 * 7       // Multiplication: 21
define div_example = 15 / 3      // Division: 5
define pow_example = 2 ^ 10      // Exponentiation: 1024

Variables and Definitions

Use define to create named values:

define pi = 3.14159
define e = 2.71828
define golden_ratio = (1 + sqrt(5)) / 2

Functions are defined similarly:

define square(x) = x * x
define cube(x) = x * x * x
define area_circle(r) = pi * r^2

Comments

Kleis uses C-style comments:

// This is a single-line comment
define x = 42  // Inline comment

/* 
   Multi-line comments
   use slash-star syntax
*/

Unicode Support

Kleis embraces mathematical notation with full Unicode support:

// Greek letters
define α = 0.5
define β = 1.0
define θ = π / 4

// Mathematical symbols in axioms
axiom reflexivity : ∀(x : ℝ). x = x           // Universal quantifier
axiom positive_exists : ∃(y : ℝ). y > 0       // Existential quantifier

You can use ASCII alternatives too:

What’s Next?

Now that you can write basic expressions, let’s learn about the type system!

→ Next: Types and Values

Types and Values

Why Types Matter

Types are the foundation of Kleis. Every expression has a type, and the type system catches errors before they become problems.

define answer = 42                // 42 is an integer
define pi_val = 3.14              // 3.14 is a real number
define flag = True                // True is a boolean

Built-in Types

Numeric Types

Other Basic Types

Parameterized Primitive Types

// Boolean values
define flag = True
define not_flag = False

// Boolean in quantified expressions (inside structures)
structure BoolExamples {
    axiom reflexive_unicode : ∀(p : 𝔹). p = p
    axiom reflexive_full    : ∀(q : Bool). q = q
}

The Unit Type

The Unit type represents “no meaningful value” — like void in C or () in Rust/Haskell. It has exactly one value: ().

When to use Unit:

1. Result types that can fail but return nothing on success:

// A validation that succeeds with () or fails with an error message
data ValidationResult = Ok(Unit) | Err(String)

define validate_positive(x : ℝ) : ValidationResult =
    if x > 0 then Ok(()) else Err("must be positive")

2. Optional values where presence matters, not content:

// Option type - Some(value) or None
data Option(T) = Some(T) | None

// A flag that's either set or not (no associated value)
define flag_set : Option(Unit) = Some(())
define flag_unset : Option(Unit) = None

3. Proof terms with no computational content:

// A theorem that x = x (the proof itself carries no data)
structure Reflexivity {
    axiom refl : ∀(x : ℝ). x = x
}
// The "witness" of this axiom would have type Unit

Type Annotations

You can explicitly annotate types with ::

// Variable annotation
define typed_let = let x : ℝ = 3.14 in x * 2

// Function parameter and return types
define f(x : ℝ) : ℝ = x * x

// Expression-level annotation (ascription)
define sum_typed(a, b) = (a + b) : ℝ

Type Aliases

Type aliases give a new name to an existing type, making your code more readable and self-documenting.

The type Keyword

type Probability = ℝ
type Temperature = ℝ
type Velocity = ℝ

Now you can use Probability instead of ℝ to make your intent clear:

define coin_flip : Probability = 0.5
define boiling_point : Temperature = 100.0

Why Use Type Aliases?

1. Readability — Probability is clearer than ℝ
2. Documentation — the type name explains what the value represents
3. Refactoring — change the underlying type in one place

Function Type Aliases

Type aliases are especially useful for complex function types:

type RealFunction = ℝ → ℝ
type BinaryOp = ℝ → ℝ → ℝ
type Predicate = ℝ → Bool

Now instead of writing (ℝ → ℝ) → ℝ, you can write:

type Integrator = RealFunction → ℝ

Parameterized Type Aliases

Type aliases can have parameters:

type Pair(T) = T → T → T
type Endomorphism(T) = T → T

Aliases for Data Types and Structures

Type aliases work with user-defined types too:

// Alias for a data type (sum type)
data Option(T) = Some(value : T) | None
type MaybeInt = Option(ℤ)
type MaybeString = Option(String)

// Alias for a structure (product type)
structure Point {
    x : ℝ
    y : ℝ
}
type Coordinate = Point

// Alias for nested ADTs
data Result(T, E) = Ok(value : T) | Err(error : E)
type IntResult = Result(ℤ, String)

Note: Type aliases create a synonym — Probability and ℝ are interchangeable. They don’t create a distinct new type.

Function Types

Functions have types too! The notation A → B means “a function from A to B”:

// square takes a Real and returns a Real
define square(x : ℝ) : ℝ = x * x
// Type: ℝ → ℝ

// add takes two Reals and returns a Real
define add(x : ℝ, y : ℝ) : ℝ = x + y
// Type: ℝ × ℝ → ℝ (or equivalently: ℝ → ℝ → ℝ)

Higher-Order Function Types

Functions can take other functions as arguments or return functions. These are called higher-order functions:

// A function that takes a function as an argument
define apply_twice(f : ℝ → ℝ, x : ℝ) : ℝ = f(f(x))
// Type: (ℝ → ℝ) × ℝ → ℝ

// A function that returns a function
define make_adder(n : ℝ) : ℝ → ℝ = ???
// Type: ℝ → (ℝ → ℝ)

The parentheses matter! Compare:

• (ℝ → ℝ) → ℝ — takes a function, returns a number
• ℝ → (ℝ → ℝ) — takes a number, returns a function
• ℝ → ℝ → ℝ — curried function (associates right: ℝ → (ℝ → ℝ))

Function Type Examples

Set Types

Kleis provides a built-in Set(T) type backed by Z3’s native set theory. Sets are unordered collections of unique elements:

// Declare a set type
define S : Set(ℤ)

// Set operations (see stdlib/sets.kleis for full structure)
in_set(x, S)              // Membership: x ∈ S → Bool
union(A, B)               // Union: A ∪ B → Set(T)
intersect(A, B)           // Intersection: A ∩ B → Set(T)
difference(A, B)          // Difference: A \ B → Set(T)
complement(A)             // Complement: ᶜA → Set(T)
subset(A, B)              // Subset test: A ⊆ B → Bool
insert(x, S)              // Add element: S ∪ {x} → Set(T)
remove(x, S)              // Remove element: S \ {x} → Set(T)
singleton(x)              // Singleton set: {x} → Set(T)
empty_set                 // Empty set: ∅

Set Theory Axioms

Sets come with a complete axiomatization (see stdlib/sets.kleis):

structure SetTheory(T) {
    // Core operations
    operation in_set : T → Set(T) → Bool
    operation union : Set(T) → Set(T) → Set(T)
    operation intersect : Set(T) → Set(T) → Set(T)
    element empty_set : Set(T)
    
    // Extensionality: sets are equal iff they have the same elements
    axiom extensionality: ∀(A B : Set(T)). 
        (∀(x : T). in_set(x, A) ↔ in_set(x, B)) → A = B
    
    // Union definition
    axiom union_def: ∀(A B : Set(T), x : T). 
        in_set(x, union(A, B)) ↔ (in_set(x, A) ∨ in_set(x, B))
    
    // De Morgan's laws
    axiom de_morgan_union: ∀(A B : Set(T)). 
        complement(union(A, B)) = intersect(complement(A), complement(B))
}

Using Sets in Verification

Sets are particularly useful for specifying properties involving collections:

structure MetricSpace(X) {
    operation d : X → X → ℝ
    operation ball : X → ℝ → Set(X)
    
    // Open ball definition
    axiom ball_def: ∀(center : X, radius : ℝ, x : X).
        in_set(x, ball(center, radius)) ↔ d(x, center) < radius
}

Parametric Types

Types can have parameters:

// Parametric type examples:
List(ℤ)           // List of integers
Matrix(3, 3, ℝ)   // 3×3 matrix of reals
Vector(4)         // 4-dimensional vector
Set(ℝ)            // Set of real numbers

Dimension Expressions

When working with parameterized types like Matrix(m, n, ℝ), the dimension parameters are not just simple numbers — they can be dimension expressions. This enables type-safe operations where dimensions depend on each other.

Supported Dimension Expressions

Why Dimension Expressions Matter

Consider the realification functor from control theory, which embeds a complex n×n matrix into a real 2n×2n matrix:

// Complex matrix represented as (real_part, imag_part)
type ComplexMatrix(m: Nat, n: Nat) = (Matrix(m, n, ℝ), Matrix(m, n, ℝ))

// Realification: embed C^(n×n) into R^(2n×2n)
structure Realification(n: Nat) {
    operation realify : ComplexMatrix(n, n) → Matrix(2*n, 2*n, ℝ)
    operation complexify : Matrix(2*n, 2*n, ℝ) → ComplexMatrix(n, n)
}

The 2*n dimension expression captures the invariant that the output dimension is always twice the input dimension.

How Dimension Unification Works

When Kleis type-checks your code, it must verify that dimension expressions match. This uses a built-in dimension solver that can handle common arithmetic constraints.

What the Solver Can Unify

What the Solver Rejects

Examples in Practice

Matrix multiplication requires matching inner dimensions:

// Matrix(m, n) × Matrix(n, p) → Matrix(m, p)
structure MatrixMultiply(m: Nat, n: Nat, p: Nat) {
    operation matmul : Matrix(m, n, ℝ) → Matrix(n, p, ℝ) → Matrix(m, p, ℝ)
}

The n dimension must match on both sides — the solver verifies this.

SVD decomposition produces matrices with min(m, n) dimensions:

// Illustrative — tuple return types in structures are aspirational
structure SVD(m: Nat, n: Nat) {
    // A = U * Σ * Vᵀ where Σ is min(m,n) × min(m,n)
    operation svd : Matrix(m, n, ℝ) → 
        (Matrix(m, min(m,n), ℝ), Matrix(min(m,n), min(m,n), ℝ), Matrix(min(m,n), n, ℝ))
}

Simplification

The dimension solver simplifies expressions before comparing them:

This means Matrix(1*n, n+0, ℝ) correctly unifies with Matrix(n, n, ℝ).

Design Philosophy

The dimension solver is deliberately bounded:

• It handles practical cases (linear arithmetic, powers, min/max)
• It fails clearly on complex constraints it cannot solve
• It doesn’t require external dependencies (no SMT solver needed for type checking)

If you need more advanced constraint solving, use the :verify command with Z3 at the value level.

Type Inference

Kleis often infers types automatically:

define double(x) = x + x
// Kleis infers: double : ℝ → ℝ (or more general)

define square_five = let y = 5 in y * y
// Kleis infers: y : ℤ

But explicit types make code clearer and catch errors earlier!

The Type Hierarchy

                    Any
         /     |      \       \
     Scalar  String  Collection  Set(T)
     /    \              |
    ℂ    Bool          List
    |                 /    \
    ℝ            Vector   Matrix
    |
    ℚ
    |
    ℤ
    |
    ℕ

Note: ℕ ⊂ ℤ ⊂ ℚ ⊂ ℝ ⊂ ℂ (naturals ⊂ integers ⊂ rationals ⊂ reals ⊂ complex)

Set(T) is parameterized by its element type. Set(ℤ) is a set of integers, Set(ℝ) is a set of reals, etc.

Type Promotion (Embedding)

When you mix numeric types in an expression, Kleis automatically promotes the smaller type to the larger one. This is called type embedding, not subtyping.

Embedding vs Subtyping

The difference is subtle but important:

// Embedding: Integer 3 is lifted to Rational before the operation
rational(1, 2) + 3
// Becomes: rational_add(rational(1, 2), lift(3))
// Result: rational(7, 2) — exact!

How Promotion Works

1. Type inference determines the result type (the “common supertype”)
2. Lifting converts arguments to the target type
3. Operation executes at the target type

Int + Rational
    ↓ find common supertype
  Rational
    ↓ lift Int to Rational
  lift(Int) + Rational
    ↓ execute operation
  rational_add(Rational, Rational)
    ↓
  Rational result

The Promotes Structure

Type promotion is defined by the Promotes(From, To) structure:

structure Promotes(From, To) {
  operation lift : From → To
}

// Built-in promotions
implements Promotes(ℕ, ℤ) { operation lift = builtin_nat_to_int }
implements Promotes(ℤ, ℚ) { operation lift = builtin_int_to_rational }
implements Promotes(ℚ, ℝ) { operation lift = builtin_rational_to_real }
implements Promotes(ℝ, ℂ) { operation lift = builtin_real_to_complex }

Defining Your Own Promotions

You can define promotions for your own types. Unlike built-in types (which use builtin_* functions), you must write the conversion function yourself:

data Percentage = Pct(value: ℝ)

// Step 1: Define the conversion function
define pct_to_real(p: Percentage) : ℝ =
  match p { Pct(v) => divide(v, 100) }

// Step 2: Register the promotion, referencing YOUR function
implements Promotes(Percentage, ℝ) {
  operation lift = pct_to_real   // References the function above
}

Now this works in the REPL:

λ> :eval 0.5 + pct_to_real(Pct(25))
✅ 0.75

Key difference from built-in types:

Important: For concrete execution (:eval), you must provide an actual define for the lift function. Without it:

• :verify (symbolic) — Works (Z3 treats lift as uninterpreted)
• :eval (concrete) — Fails (“function not found”)

Precision Considerations

Warning: Promotion can lose precision!

// Exact in Rational
define third : ℚ = rational(1, 3)  // Exactly 1/3

// Approximate in Real (floating-point)
define approx : ℝ = 1.0 / 3.0      // 0.333333...

// If you promote:
define promoted = third + 0.5      // third lifted to ℝ, loses exactness!

Recommendation: When precision matters, be explicit about types:

// Keep it in Rational for exact arithmetic
define exact_sum : ℚ = rational(1, 3) + rational(1, 6)  // Exactly 1/2

// Or use type annotations to prevent accidental promotion
define result(x : ℚ, y : ℚ) : ℚ = x + y

No LSP Violations

Because Kleis uses embedding (not subtyping), operations are always resolved at the target type after lifting. This means:

• Int + Int uses integer addition
• Int + Rational lifts the Int first, then uses rational addition
• You never accidentally get integer truncation when you expected rational division

5 / 3           // Integer division → 1 (if both are Int)
rational(5, 1) / rational(3, 1)   // Rational division → 5/3 (exact)

What’s Next?

Types are the foundation. Now let’s see how to define functions!

→ Next: Functions

Functions

Defining Functions

Functions are defined with define:

define square(x) = x * x
define cube(x) = x * x * x
define add(x, y) = x + y

Functions with Type Annotations

For clarity and safety, add type annotations:

define square(x : ℝ) : ℝ = x * x

define distance(x : ℝ, y : ℝ) : ℝ = sqrt(x^2 + y^2)

define normalize(v : Vector(3)) : Vector(3) = v / magnitude(v)

Multi-Parameter Functions

Functions can take multiple parameters:

define add(x, y) = x + y
define volume_box(l, w, h) = l * w * h
define dot_product(a, b, c, x, y, z) = a*x + b*y + c*z

Recursive Functions

Functions can call themselves:

define factorial(n : ℕ) : ℕ =
    if n = 0 then 1
    else n * factorial(n - 1)

define fibonacci(n : ℕ) : ℕ =
    if n ≤ 1 then n
    else fibonacci(n-1) + fibonacci(n-2)

Built-in Mathematical Functions

Kleis includes standard mathematical functions:

Trigonometric

sin(x)      cos(x)      tan(x)
asin(x)     acos(x)     atan(x)
sinh(x)     cosh(x)     tanh(x)

Exponential and Logarithmic

exp(x)      // e^x
ln(x)       // natural log
log(x)      // base-10 log
log(b, x)   // log base b of x

Other

sqrt(x)     // square root
abs(x)      // absolute value
floor(x)    // round down
ceil(x)     // round up
min(x, y)   // minimum
max(x, y)   // maximum

Lambda Expressions (Anonymous Functions)

Lambda expressions allow you to create anonymous functions inline:

define square_lambda = λ x . x * x
define increment = lambda x . x + 1
define add_lambda = λ x . λ y . x + y
define square_typed = λ (x : ℝ) . x^2
define curried_add = λ x . λ y . x + y

Lambda expressions are first-class values - you can pass them to functions:

// Pass lambda to higher-order function
define doubled_list = map(λ x . x * 2, [1, 2, 3])

// Or define inline
define result = apply(λ x . x + 1, 5)

Higher-Order Functions

Functions can take functions as arguments:

// Apply a function twice
define apply_twice(f, x) = f(f(x))

// Example usage:
define inc(x) = x + 1
define result = apply_twice(inc, 5)   // Result: 7

Partial Application and Currying

With lambda expressions, you can create curried functions:

// Curried addition
define add = λ x . λ y . x + y

// Partial application creates specialized functions
define add5 = add(5)           // λ y . 5 + y
define eight = add5(3)         // Result: 8

Named Arguments (v0.96)

For plotting and numeric functions, Kleis supports named arguments (keyword arguments):

// Named arguments come after positional arguments
diagram(
    bar(xs, ys, offset = -0.2, width = 0.4, label = "Data"),
    plot(x, y, color = "blue", yerr = errors),
    width = 10,
    height = 7,
    title = "My Chart"
)

Syntax

Named arguments use = (not ==) and must come after all positional arguments:

// ✅ Valid: positional first, then named
f(a, b, x = 1, y = 2)

// ✅ Valid: all named
f(x = 1, y = 2)

// ❌ Invalid: positional after named
f(x = 1, a, b)      // Error!

Parser Transformation

Named arguments are syntactic sugar. The parser transforms them into a record expression:

// You write:
bar(xs, ys, offset = -0.2, width = 0.4)

// Parser produces:
bar(xs, ys, record(
    field("offset", -0.2),
    field("width", 0.4)
))

Limitations: Numeric Only

Important: Named arguments are designed for concrete numeric computation (plotting, configuration). They cannot be used in:

• structure definitions
• axiom declarations
• implements blocks
• Z3 verification proofs

// ❌ Does NOT work in axioms
structure Bad {
    axiom wrong: f(x = 1)  // ERROR: named args not for axioms
}

// ✅ Works in plotting/computation
let xs = [0, 1, 2, 3]
let ys = [10, 20, 15, 25]
diagram(bar(xs, ys, color = "blue"))

Why This Design?

Named arguments are opaque to the type system:

1. Type inference sees record as an opaque type
2. Unification doesn’t look inside records
3. Z3 never receives record expressions
4. Built-in functions consume records at runtime

This ensures named arguments don’t interfere with symbolic mathematics while providing convenient syntax for plotting and configuration.

What’s Next?

Learn about algebraic data types for structured data!

→ Next: Algebraic Types

Algebraic Data Types

What Are ADTs?

Algebraic Data Types (ADTs) let you define custom data structures by combining simpler types. There are two main kinds:

• Product types — “this AND that” (records, tuples)
• Sum types — “this OR that” (variants, enums)

Product Types

A product type combines multiple values:

// A point has an x AND a y
structure Point {
    x : ℝ
    y : ℝ
}

// A person has a name AND an age
structure Person {
    name : String
    age : ℕ
}

Sum Types (Variants)

A sum type represents alternatives — a value that can be one of several different forms.

The data Keyword

In Kleis, you define sum types using the data keyword:

data TypeName = Constructor1 | Constructor2 | Constructor3

Syntax breakdown:

• data — keyword that introduces a new type definition
• TypeName — the name of your new type (starts with uppercase)
• = — separates the type name from its constructors
• Constructor1, Constructor2, etc. — the possible variants (each starts with uppercase)
• | — read as “or” — separates the alternatives

Constructors with Data

Constructors can carry data (fields):

data TypeName = Constructor1(field1 : Type1) | Constructor2(field2 : Type2, field3 : Type3)

Each constructor acts like a function that creates a value of the type.

Parameterized Types (Generics)

Types can have parameters, making them work with any type:

data Option(T) = Some(value : T) | None

Here T is a type parameter. You can use Option(ℕ) for optional natural numbers, Option(String) for optional strings, etc. The type is generic — it works for any T.

Examples

// A shape is a Circle OR a Rectangle OR a Triangle
data Shape = Circle(radius : ℝ) | Rectangle(width : ℝ, height : ℝ) | Triangle(a : ℝ, b : ℝ, c : ℝ)

// An optional value is Some(value) OR None
data Option(T) = Some(value : T) | None

// A result is Ok(value) OR Err(message)
data Result(T, E) = Ok(value : T) | Err(error : E)

Pattern Matching with ADTs

ADTs shine with pattern matching:

define area(shape) =
    match shape {
        Circle(r) => π * r^2
        Rectangle(w, h) => w * h
        Triangle(a, b, c) => 
            let s = (a + b + c) / 2 in
            sqrt(s * (s-a) * (s-b) * (s-c))
    }

Recursive Types

Types can refer to themselves:

// A list is either empty (Nil) or a value followed by another list (Cons)
data List(T) {
    Nil
    Cons(head : T, tail : List(T))
}

// A binary tree
data Tree(T) {
    Leaf(value : T)
    Node(left : Tree(T), value : T, right : Tree(T))
}

The Mathematical Perspective

Why “algebraic”?

• Product types correspond to multiplication: Point = ℝ × ℝ
• Sum types correspond to addition: Option(T) = T + 1

The number of possible values follows algebra:

• Bool has 2 values
• Bool × Bool has 2 × 2 = 4 values
• Bool + Bool has 2 + 2 = 4 values

Practical Example: Expression Trees

ADTs are perfect for representing mathematical expressions:

data Expression = 
    ENumber(value : ℝ)
  | EVariable(name : String)
  | EOperation(name : String, args : List(Expression))

// Helper constructors for cleaner syntax
define num(n) = ENumber(n)
define var(x) = EVariable(x)
define e_add(a, b) = EOperation("plus", Cons(a, Cons(b, Nil)))
define e_mul(a, b) = EOperation("times", Cons(a, Cons(b, Nil)))
define e_neg(a) = EOperation("neg", Cons(a, Nil))

define eval_expr(expr, env) =
    match expr {
        ENumber(v) => v
        EVariable(name) => lookup(env, name)
        EOperation("plus", Cons(l, Cons(r, Nil))) => 
            eval_expr(l, env) + eval_expr(r, env)
        EOperation("times", Cons(l, Cons(r, Nil))) => 
            eval_expr(l, env) * eval_expr(r, env)
        EOperation("neg", Cons(e, Nil)) => 
            -eval_expr(e, env)
        _ => 0
    }

What’s Next?

Let’s dive deeper into pattern matching!

→ Next: Pattern Matching

Pattern Matching

The Power of Match

Pattern matching is one of Kleis’s most powerful features. It lets you destructure data and handle different cases elegantly:

define describe(n) =
    match n {
        0 => 0
        1 => 1
        _ => 2
    }

Basic Patterns

Literal Patterns

Match exact values:

define describe_literal(x) =
    match x {
        0 => "zero"
        1 => "one"
        42 => "the answer"
        _ => "something else"
    }

Variable Patterns

Bind matched values to names:

define sum_point(point) =
    match point {
        Point(x, y) => x + y
    }

Wildcard Pattern

The underscore _ matches anything:

define describe_pair(pair) =
    match pair {
        (_, 0) => "second is zero"
        (0, _) => "first is zero"
        _ => "neither is zero"
    }

Nested Patterns

Patterns can be nested arbitrarily:

define sum_tree(tree) =
    match tree {
        Leaf(v) => v
        Node(Leaf(l), v, Leaf(r)) => l + v + r
        Node(left, v, right) => v + sum_tree(left) + sum_tree(right)
    }

Guards

Add conditions to patterns with if:

define sign(n) =
    match n {
        x if x < 0 => "negative"
        x if x > 0 => "positive"
        _ => "zero"
    }

As-Patterns

Bind the whole match while also destructuring:

define filter_head(list) =
    match list {
        Cons(h, t) as whole => 
            if h > 10 then whole
            else t
        Nil => Nil
    }

Pattern Matching in Let

Destructure directly in let bindings:

define distance_squared(origin) =
    let Point(x, y) = origin in x^2 + y^2

define sum_first_two(triple) =
    let (first, second, _) = triple in first + second

Pattern Matching in Function Parameters

With lambda expressions now available, you can combine them with match:

// Pattern matching with lambdas
define fst = λ pair . match pair { (a, _) => a }
define snd = λ pair . match pair { (_, b) => b }

Alternative workaround:

define fst(pair) = 
    match pair {
        (a, _) => a
    }

Exhaustiveness

Kleis checks that your patterns cover all cases:

// ⚠️ Warning: non-exhaustive patterns
define incomplete(opt) =
    match opt {
        Some(x) => x
    }

// ✓ Complete
define complete(opt) =
    match opt {
        Some(x) => x
        None => 0
    }

Real-World Example: Symbolic Differentiation

Pattern matching makes symbolic math elegant:

define diff(expr, var) =
    match expr {
        Const(_) => Const(0)
        
        Var(name) => 
            if name = var then Const(1)
            else Const(0)
        
        Add(f, g) => 
            Add(diff(f, var), diff(g, var))
        
        Mul(f, g) =>
            Add(Mul(diff(f, var), g), 
                Mul(f, diff(g, var)))
        
        Neg(f) => 
            Neg(diff(f, var))
    }

Note: This diff function computes derivatives by pattern matching on expression trees. Kleis also provides D(f, x) and Dt(f, x) operations in stdlib/calculus.kleis for verifying derivative properties with Z3. See Applications: Symbolic Differentiation for a detailed comparison.

What’s Next?

Learn about let bindings for local definitions!

→ Next: Let Bindings

Let Bindings

Introduction

Let bindings introduce local variables with limited scope. They’re essential for breaking complex expressions into readable parts.

define square_five = let x = 5 in x * x
// Result: 25

Basic Syntax

let <name> = <value> in <body>

The variable name is only visible within body:

define circle_area = let radius = 10 in π * radius^2
// Result: 314.159...
// 'radius' is not visible outside the let binding

With Type Annotations

Add explicit types for clarity:

define typed_example1 = let x : ℝ = 3.14 in x * 2
define typed_example2 = let n : ℕ = 42 in factorial(n)
define typed_example3 = let v : Vector(3) = [1, 2, 3] in magnitude(v)

Nested Let Bindings

Chain multiple bindings:

define nested_example =
    let x = 5 in
    let y = 3 in
    let z = x + y in
        x * y * z
// Result: 5 * 3 * 8 = 120

Shadowing

Inner bindings can shadow outer ones:

define shadowing_example =
    let x = 1 in
    let x = x + 1 in
    let x = x * 2 in
        x
// Result: 4  (not 1!)

Each let creates a new scope where x is rebound.

Pure Substitution Semantics

In Kleis, let x = e in body is equivalent to substituting e for x in body:

define substitution_demo = let x = 5 in x + x
// is the same as:
define substitution_result = 5 + 5

This is pure functional semantics — no mutation, no side effects.

Practical Examples

Quadratic Formula

define quadratic_roots(a, b, c) =
    let discriminant = b^2 - 4*a*c in
    let sqrt_d = sqrt(discriminant) in
    let denom = 2 * a in
        ((-b + sqrt_d) / denom, (-b - sqrt_d) / denom)

Heron’s Formula

define triangle_area(a, b, c) =
    let s = (a + b + c) / 2 in
        sqrt(s * (s - a) * (s - b) * (s - c))

Complex Calculations

define schwarzschild_metric(r, M) =
    let rs = 2 * G * M / c^2 in
    let factor = 1 - rs / r in
        -c^2 * factor

Let vs Define

// Global constant
define pi = 3.14159

// Local temporary in a function
define circumference(radius) = let two_pi = 2 * pi in two_pi * radius

What’s Next?

Learn about quantifiers and logic!

→ Next: Quantifiers and Logic

Quantifiers and Logic

Universal Quantifier (∀)

The universal quantifier expresses “for all”:

// Quantified propositions (used inside axioms)
axiom reflexivity : ∀(x : ℝ). x = x
axiom additive_identity : ∀(x : ℝ). x + 0 = x
axiom commutative : ∀(x : ℝ)(y : ℝ). x + y = y + x

ASCII alternative: forall x . ...

Existential Quantifier (∃)

The existential quantifier expresses “there exists”:

// Existential quantifiers
axiom positive_exists : ∃(x : ℝ). x > 0
axiom sqrt2_exists : ∃(y : ℝ). y * y = 2
axiom distinct_exists : ∃(x : ℝ)(y : ℝ). x ≠ y

ASCII alternative: exists x . ...

Combining Quantifiers

Build complex statements:

// Every number has a successor
axiom successor : ∀(n : ℕ). ∃(m : ℕ). m = n + 1

// Density of rationals: between any two reals is a rational
axiom density : ∀(x : ℝ)(y : ℝ). x < y → ∃(q : ℚ). x < q ∧ q < y

Logical Connectives

Conjunction (∧ / and)

define in_range(x) = x > 0 ∧ x < 10     // x is between 0 and 10
define false_example = True ∧ False     // False

Disjunction (∨ / or)

define is_binary(x) = x = 0 ∨ x = 1    // x is 0 or 1
define true_example = True ∨ False     // True

Implication (→ / implies)

define positive_square(x) = x > 0 → x * x > 0   // If positive, square is positive
define implication(P, Q) = P → Q                // If P then Q

Negation (¬ / not)

define nonzero(x) = ¬(x = 0)     // x is not zero
define not_true = ¬True          // False

Biconditional (↔ / iff)

define zero_iff_square_zero(x) = x = 0 ↔ x * x = 0  // x is zero iff x² is zero

Type Constraints in Quantifiers

Restrict the domain:

axiom naturals_nonneg : ∀(x : ℕ). x ≥ 0
axiom det_inverse : ∀(M : Matrix(n, n)). det(M * M⁻¹) = 1

The where Clause

Add conditions to quantified variables using the where keyword:

structure Field(F) {
    element zero : F
    element one : F
    operation inverse : F → F
    
    // Multiplicative inverse only for non-zero elements
    axiom multiplicative_inverse:
        ∀(x : F) where x ≠ zero. inverse(x) * x = one
}

The where clause restricts the domain before the quantified body is evaluated. This is essential for axioms that don’t apply universally.

More examples:

structure Analysis {
    // Division only defined for non-zero denominator
    axiom division: ∀(a : ℝ)(b : ℝ) where b ≠ 0. a / b * b = a
    
    // Logarithm only for positive numbers
    axiom log_exp: ∀(x : ℝ) where x > 0. exp(log(x)) = x
}

Using Quantifiers in Axioms

Quantifiers are essential in structure axioms:

structure Group(G) {
    e : G                      // Identity element
    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))
}

Nested Quantifiers (Grammar v0.9)

Quantifiers can appear inside logical expressions:

structure Analysis {
    // Quantifier inside conjunction
    axiom bounded_positive: (x > 0) ∧ (∀(y : ℝ). abs(y) <= x)
    
    // Quantifier inside implication
    axiom dense_rationals: ∀(a b : ℝ). a < b → (∃(q : ℚ). a < q ∧ q < b)
    
    // Deeply nested quantifiers
    axiom limit_def: ∀(L : ℝ, ε : ℝ). ε > 0 → 
        (∃(δ : ℝ). δ > 0 ∧ (∀(x : ℝ). abs(x) < δ → abs(f(x) - L) < ε))
}

Epsilon-Delta Limit Definition

The classic analysis definition now parses correctly:

structure Limits {
    axiom epsilon_delta: ∀(f : ℝ → ℝ, L a : ℝ). 
        has_limit(f, a, L) ↔ 
        (∀(ε : ℝ). ε > 0 → (∃(δ : ℝ). δ > 0 ∧ 
            (∀(x : ℝ). abs(x - a) < δ → abs(f(x) - L) < ε)))
}

Function Types in Quantifiers (Grammar v0.9)

Quantify over functions using the arrow type:

structure FunctionProperties {
    // Quantify over a function ℝ → ℝ
    axiom continuous: ∀(f : ℝ → ℝ, x : ℝ). 
        is_continuous(f, x)
    
    // Quantify over multiple functions
    axiom composition: ∀(f : ℝ → ℝ, g : ℝ → ℝ). 
        compose(f, g) = λ x . f(g(x))
    
    // Higher-order function types
    axiom curried: ∀(f : ℝ → ℝ → ℝ, a b : ℝ). 
        f = f
}

Topology with Function Types

structure Topology {
    axiom continuity: ∀(f : X → Y, V : Set(Y)). 
        is_open(V) → is_open(preimage(f, V))
    
    axiom homeomorphism: ∀(f : X → Y, g : Y → X). 
        (∀(x : X). g(f(x)) = x) ∧ (∀(y : Y). f(g(y)) = y) → 
        bijective(f)
}

Verification with Z3

Kleis uses Z3 to check quantified statements:

// Z3 can verify this is always true:
axiom add_zero : ∀(x : ℝ). x + 0 = x

// Z3 can find a counterexample for this:
axiom all_positive : ∀(x : ℝ). x > 0
// Z3 finds counterexample: x = -1

Truth Tables

What’s Next?

Learn about conditional expressions!

→ Next: Conditionals

Conditionals

If-Then-Else

The basic conditional expression:

if condition then value1 else value2

Examples:

define positive_check(x) = if x > 0 then "positive" else "non-positive"

define factorial(n) = if n = 0 then 1 else n * factorial(n - 1)

define abs(x) = if x ≥ 0 then x else -x

Conditionals Are Expressions

In Kleis, if-then-else is an expression that returns a value:

define doubled_abs(x) =
    let result = if x > 0 then x else -x in
    result * 2

// Both branches must have compatible types!
// if True then 42 else "hello"  // ❌ Type error!

Nested Conditionals

define sign(x) =
    if x > 0 then 1
    else if x < 0 then -1
    else 0

define grade(score) =
    if score ≥ 90 then "A"
    else if score ≥ 80 then "B"
    else if score ≥ 70 then "C"
    else if score ≥ 60 then "D"
    else "F"

Guards vs If-Then-Else

Pattern matching with guards is often cleaner:

// With if-then-else
define classify_if(n) =
    if n < 0 then "negative"
    else if n = 0 then "zero"
    else "positive"

// With pattern matching and guards
define classify_match(n) =
    match n {
        x if x < 0 => "negative"
        0 => "zero"
        _ => "positive"
    }

Piecewise Functions

Mathematicians love piecewise definitions:

// Absolute value
define abs_fn(x) =
    if x ≥ 0 then x else -x

// Heaviside step function
define heaviside(x) =
    if x < 0 then 0
    else if x = 0 then 0.5
    else 1

// Piecewise polynomial
define piecewise_f(x) =
    if x < 0 then x^2
    else if x < 1 then x
    else 2 - x

Boolean Expressions

Conditions can be complex:

define quadrant(x, y) =
    if x > 0 ∧ y > 0 then "first quadrant"
    else if x < 0 ∧ y > 0 then "second quadrant"
    else if x < 0 ∧ y < 0 then "third quadrant"
    else if x > 0 ∧ y < 0 then "fourth quadrant"
    else "on an axis"

Short-Circuit Evaluation

Kleis uses short-circuit evaluation for ∧ and ∨:

// If x = 0, division is never evaluated
define check_ratio(x, y) =
    if x ≠ 0 ∧ y/x > 1 then "big ratio" else "safe"

What’s Next?

Learn about structures for defining mathematical objects!

→ Next: Structures

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!

→ Next: Implements

Implements

From Structure to Implementation

A structure declares what operations exist. An implements block provides the actual definitions:

structure Addable(T) {
    operation add : T × T → T
}

implements Addable(ℝ) {
    operation add(x, y) = x + y
}

implements Addable(ℤ) {
    operation add(x, y) = x + y
}

Full Example: Complex Numbers

// Declare the structure
structure Complex {
    re : ℝ
    im : ℝ
    
    operation add : Complex → Complex
    operation mul : Complex → Complex
    operation conj : Complex
    operation mag : ℝ
}

// Implement the operations
implements Complex {
    operation add(z, w) = builtin_complex_add
    operation mul(z, w) = builtin_complex_mul
    operation conj(z) = builtin_complex_conj
    operation mag(z) = sqrt(z.re^2 + z.im^2)
}

Parametric Implementations

Implement structures with type parameters:

structure Stack(T) {
    operation push : T → Stack(T)
    operation pop : Stack(T)
    operation top : T
    operation empty : Bool
}

implements Stack(ℤ) {
    operation push = builtin_stack_push
    operation pop = builtin_stack_pop
    operation top = builtin_stack_top
    operation empty = builtin_stack_empty
}

Multiple Implementations

The same structure can have multiple implementations:

structure Orderable(T) {
    operation compare : T × T → Ordering
}

// Natural ordering
implements Orderable(ℤ) {
    operation compare = builtin_int_compare
}

Implementing Extended Structures

When a structure extends another, implement all operations:

structure Monoid(M) {
    operation e : M
    operation mul : M × M → M
}

structure Group(G) extends Monoid(G) {
    operation inv : G → G
}

// Must implement both Monoid and Group operations
implements Group(ℤ) {
    operation e = 0
    operation mul(x, y) = x + y
    operation inv(x) = -x
}

Builtin Operations

Some operations can’t be defined in pure Kleis — they need native code. The builtin_ prefix connects Kleis to underlying implementations:

implements Matrix(m, n, ℝ) {
    operation transpose = builtin_transpose
    operation add = builtin_matrix_add
    operation mul = builtin_matrix_mul
}

How Builtins Work

When Kleis sees builtin_foo, it:

1. Looks up foo in the native runtime
2. Calls the Rust/C/hardware implementation
3. Returns the result to Kleis

This enables:

• Performance: Native BLAS for matrix operations
• Hardware access: GPUs, network cards, sensors
• System calls: File I/O, networking, threading
• FFI: Calling existing libraries

The Vision: Hardware as Structures

Imagine:

structure NetworkInterface(N) {
    operation send : Packet → Result(Unit, Error)
    operation receive : Unit → Result(Packet, Error)
    
    axiom delivery : ∀(p : Packet).
        connected → eventually(delivered(p))
}

implements NetworkInterface(EthernetCard) {
    operation send = builtin_eth_send
    operation receive = builtin_eth_receive
}

The axioms define the contract. The builtins provide the implementation. Z3 can verify that higher-level protocols satisfy their specifications given the hardware axioms.

This is how Kleis becomes a universal verification platform — not just for math, but for any system with verifiable properties.

Verification of Implementations

Kleis + Z3 can verify that implementations satisfy axioms:

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))
}

implements Monoid(String) {
    element e = ""
    operation mul = builtin_concat
}

// Kleis can verify:
// 1. concat("", s) = s for all s ✓
// 2. concat(s, "") = s for all s ✓
// 3. concat(concat(a, b), c) = concat(a, concat(b, c)) ✓

What’s Next?

Learn about Z3 verification in depth!

→ Next: Z3 Verification

Z3 Verification

What is Z3?

Z3 is a theorem prover from Microsoft Research. Kleis uses Z3 to:

• Verify mathematical statements
• Find counterexamples when statements are false
• Check that implementations satisfy axioms

Basic Verification

Use verify to check a statement:

axiom commutativity : ∀(x : ℝ)(y : ℝ). x + y = y + x
// Z3 verifies: ✓ Valid

axiom zero_annihilates : ∀(x : ℝ). x * 0 = 0
// Z3 verifies: ✓ Valid

axiom all_positive : ∀(x : ℝ). x > 0
// Z3 finds counterexample: x = -1

Verifying Quantified Statements

Z3 handles universal and existential quantifiers:

axiom additive_identity : ∀(x : ℝ). x + 0 = x
// Z3 verifies: ✓ Valid

axiom squares_nonnegative : ∀(x : ℝ). x * x ≥ 0
// Z3 verifies: ✓ Valid (squares are non-negative)

axiom no_real_sqrt_neg1 : ∃(x : ℝ). x * x = -1
// Z3: ✗ Invalid (no real square root of -1)

axiom complex_sqrt_neg1 : ∃(x : ℂ). x * x = -1
// Z3 verifies: ✓ Valid (x = i works)

Checking Axioms

Verify that definitions satisfy axioms:

structure Group(G) {
    e : G
    operation mul : G × G → G
    operation inv : G → G
    
    axiom identity : ∀(x : G). mul(e, x) = 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))
}

// Define integers with addition
implements Group(ℤ) {
    element e = 0
    operation mul = builtin_add
    operation inv = builtin_negate
}

// Kleis verifies each axiom automatically!

Implication Verification

Prove that premises imply conclusions:

// If x > 0 and y > 0, then x + y > 0
axiom sum_positive : ∀(x : ℝ)(y : ℝ). (x > 0 ∧ y > 0) → x + y > 0
// Z3 verifies: ✓ Valid

// Triangle inequality
axiom triangle_ineq : ∀(x : ℝ)(y : ℝ)(a : ℝ)(b : ℝ).
    (abs(x) ≤ a ∧ abs(y) ≤ b) → abs(x + y) ≤ a + b
// Z3 verifies: ✓ Valid

Counterexamples

When verification fails, Z3 provides counterexamples:

axiom square_equals_self : ∀(x : ℝ). x^2 = x
// Z3: ✗ Invalid, Counterexample: x = 2 (since 4 ≠ 2)

axiom positive_greater_than_one : ∀(n : ℕ). n > 0 → n > 1
// Z3: ✗ Invalid, Counterexample: n = 1

Timeout and Limits

Complex statements may time out:

// Very complex statement
verify ∀ M : Matrix(100, 100) . det(M * M') ≥ 0
// Result: ⏱ Timeout (statement too complex)

Verifying Nested Quantifiers (Grammar v0.9)

Grammar v0.9 enables nested quantifiers in logical expressions:

structure Analysis {
    // Quantifier inside conjunction - Z3 handles this
    axiom bounded: (x > 0) ∧ (∀(y : ℝ). y = y)
    
    // Epsilon-delta limit definition
    axiom limit_def: ∀(L a : ℝ, ε : ℝ). ε > 0 → 
        (∃(δ : ℝ). δ > 0 ∧ (∀(x : ℝ). abs(x - a) < δ → abs(f(x) - L) < ε))
}

Function Types in Verification

Quantify over functions and verify their properties:

structure Continuity {
    // Z3 treats f as an uninterpreted function ℝ → ℝ
    axiom continuous_at: ∀(f : ℝ → ℝ, a : ℝ, ε : ℝ). ε > 0 →
        (∃(δ : ℝ). δ > 0 ∧ (∀(x : ℝ). abs(x - a) < δ → abs(f(x) - f(a)) < ε))
}

Note: Z3 treats function-typed variables as uninterpreted functions, allowing reasoning about their properties without knowing their implementation.

What Z3 Can and Cannot Do

Z3 Excels At:

• Linear arithmetic
• Boolean logic
• Array reasoning
• Simple quantifiers
• Algebraic identities
• Nested quantifiers (Grammar v0.9)
• Function-typed variables

Z3 Struggles With:

• Non-linear real arithmetic (undecidable in general)
• Very deep quantifier nesting (may timeout)
• Transcendental functions (sin, cos, exp)
• Infinite structures
• Inductive proofs over recursive data types

Practical Workflow

1. Write structure with axioms
2. Implement operations
3. Kleis auto-verifies axioms are satisfied
4. Use verify for additional properties
5. Examine counterexamples when verification fails

// Step 1: Define structure
structure Ring(R) {
    zero : R
    one : R
    operation add : R × R → R
    operation mul : R × R → R
    operation neg : R → R
    
    axiom add_assoc : ∀(a : R)(b : R)(c : R).
        add(add(a, b), c) = add(a, add(b, c))
}

// Step 2: Implement for integers
implements Ring(ℤ) {
    element zero = 0
    element one = 1
    operation add = builtin_add
    operation mul = builtin_mul
    operation neg = builtin_negate
}

// Step 3: Auto-verification happens!

// Step 4: Check additional properties
axiom mul_zero : ∀(x : ℤ). mul(x, zero) = zero
// Z3 verifies: ✓ Valid

Solver Abstraction Layer

While this chapter focuses on Z3, Kleis is designed with a solver abstraction layer that can interface with multiple proof backends.

Architecture

User Code (Kleis Expression)
         │
    SolverBackend Trait
         │
   ┌─────┴──────┬───────────┬──────────────┐
   │            │           │              │
Z3Backend  CVC5Backend  IsabelleBackend  CustomBackend
   │            │           │              │
   └─────┬──────┴───────────┴──────────────┘
         │
  OperationTranslators
         │
   ResultConverter
         │
User Code (Kleis Expression)

The SolverBackend Trait

The core abstraction is defined in src/solvers/backend.rs:

#![allow(unused)]
fn main() {
pub trait SolverBackend {
    /// Get solver name (e.g., "Z3", "CVC5")
    fn name(&self) -> &str;

    /// Get solver capabilities (declared upfront, MCP-style)
    fn capabilities(&self) -> &SolverCapabilities;

    /// Verify an axiom (validity check)
    fn verify_axiom(&mut self, axiom: &Expression) 
        -> Result<VerificationResult, String>;

    /// Check if an expression is satisfiable
    fn check_satisfiability(&mut self, expr: &Expression) 
        -> Result<SatisfiabilityResult, String>;

    /// Evaluate an expression to a concrete value
    fn evaluate(&mut self, expr: &Expression) 
        -> Result<Expression, String>;

    /// Simplify an expression
    fn simplify(&mut self, expr: &Expression) 
        -> Result<Expression, String>;

    /// Check if two expressions are equivalent
    fn are_equivalent(&mut self, e1: &Expression, e2: &Expression) 
        -> Result<bool, String>;

    // ... additional methods for scope management, assertions, etc.
}
}

Key design principle: All public methods work with Kleis Expression, not solver-specific types. Solver internals never escape the abstraction.

MCP-Style Capability Declaration

Solvers declare their capabilities upfront (inspired by Model Context Protocol):

#![allow(unused)]
fn main() {
pub struct SolverCapabilities {
    pub solver: SolverMetadata,      // name, version, type
    pub capabilities: Capabilities,   // operations, theories, features
}

pub struct Capabilities {
    pub theories: HashSet<String>,              // "arithmetic", "boolean", etc.
    pub operations: HashMap<String, OperationSpec>,
    pub features: FeatureFlags,                 // quantifiers, evaluation, etc.
    pub performance: PerformanceHints,          // timeout, max axioms
}
}

This enables:

• Coverage analysis - Know what operations are natively supported
• Multi-solver comparison - Choose the best solver for a program
• User extensibility - Add translators for missing operations

Verification Results

#![allow(unused)]
fn main() {
pub enum VerificationResult {
    Valid,                              // Axiom holds for all inputs
    Invalid { counterexample: String }, // Found a violation
    Unknown,                            // Timeout or too complex
}

pub enum SatisfiabilityResult {
    Satisfiable { example: String },    // Found satisfying assignment
    Unsatisfiable,                      // No solution exists
    Unknown,
}
}

Why Multiple Backends?

Different proof systems have different strengths:

Current Implementation

Currently implemented in src/solvers/:

Solver Discovery

#![allow(unused)]
fn main() {
use kleis::solvers::discovery;

// List all available backends
let solvers = discovery::list_solvers();  // ["Z3"]

// Check if a specific solver is available
if discovery::is_available("Z3") {
    let backend = Z3Backend::new()?;
}
}

Benefits of Abstraction

1. Solver independence - Swap solvers without code changes
2. Unified API - Same methods regardless of backend
3. Capability-aware - Know what each solver supports before using it
4. Extensible - Add custom backends by implementing the trait
5. Future-proof - New provers can be integrated without changing Kleis code

This architecture makes Kleis a proof orchestration layer with beautiful notation, not just another proof assistant.

What’s Next?

Try the interactive REPL!

→ Next: The REPL

The REPL

What is the REPL?

The REPL (Read-Eval-Print Loop) is an interactive environment for experimenting with Kleis:

$ cargo run --bin repl

🧮 Kleis REPL v0.1.0
   Type :help for commands, :quit to exit

λ>

Basic Usage

Enter expressions to evaluate them symbolically:

λ> 2 + 2
2 + 2

λ> let x = 5 in x * x
times(5, 5)

λ> sin(π / 2)
sin(divide(π, 2))

Note: The REPL performs symbolic evaluation, not numeric computation. Expressions are simplified symbolically, not calculated to numbers.

Loading Files

The REPL prompt evaluates expressions. For definitions (define, structure, etc.), use :load:

λ> :load examples/protocols/stop_and_wait.kleis
✅ Loaded: 1 files, 5 functions, 0 structures, 0 data types, 0 type aliases

λ> :env
📋 Defined functions:
  next_seq (seq) = ...
  valid_ack (sent, ack) = ...
  sender_next_state (current_seq, ack_received) = ...
  receiver_accepts (expected, received) = ...
  receiver_next_state (expected, received) = ...

More examples to load:

λ> :load examples/business/order_to_cash.kleis
✅ Loaded: 1 files, 21 functions, 0 structures, 4 data types, 0 type aliases

λ> :load examples/authorization/zanzibar.kleis
✅ Loaded: 1 files, 13 functions, 0 structures, 0 data types, 0 type aliases

The import Keyword

In Kleis source files, use import to include definitions from other files:

import "stdlib/prelude.kleis"
import "stdlib/matrices.kleis"

// Now you can use definitions from those files
define my_matrix = identity(3)

Import syntax:

• import "path/to/file.kleis" — includes all definitions from that file

Imports are processed at parse time. Relative paths are resolved from the importing file’s directory.

Common imports:

import "stdlib/prelude.kleis"     // Basic types and operations
import "stdlib/matrices.kleis"    // Matrix operations
import "stdlib/complex.kleis"     // Complex number support

Standard Library Resolution

Imports starting with stdlib/ are handled specially:

1. KLEIS_ROOT environment variable — If set, Kleis looks for $KLEIS_ROOT/stdlib/... first
2. Project directory — Kleis walks up from the current file looking for a stdlib/ folder
3. Current working directory — Falls back to ./stdlib/...

Setting KLEIS_ROOT:

# Add to your shell profile (~/.bashrc, ~/.zshrc, etc.)
export KLEIS_ROOT=/path/to/kleis

# Now stdlib imports work from anywhere
kleis run my_project/main.kleis

This is useful when:

• Working on projects outside the Kleis repository
• Running Kleis from arbitrary directories
• Sharing code that uses the standard library

Note: In the REPL, use :load instead of import. The :load command loads a file interactively, while import is for use inside .kleis source files.

Verification with Z3

Run verifications interactively with :verify:

λ> :verify x + y = y + x
✅ Valid

λ> :verify x > 0
❌ Invalid - Counterexample: x!2 -> 0

Satisfiability with Z3

Use :sat to find solutions (equation solving):

λ> :sat ∃(z : ℂ). z * z = complex(-1, 0)
✅ Satisfiable
   Witness: z_re = 0, z_im = -1

λ> :sat ∃(x : ℝ). x * x = 4
✅ Satisfiable
   Witness: x = -2

λ> :sat ∃(x : ℝ). x * x = -1
❌ Unsatisfiable (no solution exists)

λ> :sat ∃(x : ℝ)(y : ℝ). x + y = 10 ∧ x - y = 4
✅ Satisfiable
   Witness: x = 7, y = 3

:verify vs :sat:

Lambda Expressions

Lambda expressions work at the prompt:

λ> λ x . x * 2
λ x . times(x, 2)

λ> λ x y . x + y
λ x y . x + y

Type Inference

Check types with :type:

λ> :type 42
📐 Type: Int

λ> :type 3.14
📐 Type: Scalar

λ> :type sin
📐 Type: α0

Note: Integer literals (42) type as Int, real literals (3.14) type as Scalar. This enables proper type promotion (e.g., Int + Rational → Rational).

Concrete Evaluation with :eval

The :eval command performs concrete evaluation — it actually computes results, including recursive functions:

λ> :load examples/meta-programming/lisp_parser.kleis
✅ Loaded: 60 functions

λ> :eval run("(+ 2 3)")
VNum(5)

λ> :eval run("(letrec ((fact (lambda (n) (if (<= n 1) 1 (* n (fact (- n 1))))))) (fact 5))")
VNum(120)

:eval vs :sat vs :verify:

Key insight: Z3 cannot symbolically unroll recursive functions over unbounded data types. Use :eval for concrete computation, :sat/:verify for symbolic reasoning.

This is what makes Kleis Turing complete — the combination of ADTs, pattern matching, recursion, and concrete evaluation enables arbitrary computation. See Appendix: LISP Interpreter for a complete example.

The Verification Gap (Important!)

Users must understand this fundamental limitation.

The three REPL modes operate on different systems:

The gap:

When you run :verify ∀(a b : ℕ). a + b = b + a, Z3 proves this using its built-in integer arithmetic theory.

When you run :eval 2 + 3, Rust’s + operator computes 5.

We never verify that Rust’s + matches Z3’s +.

The Trusted Computing Base:

These components are assumed correct, never verified:

• Rust compiler
• Builtin implementations (builtin_add, builtin_mul, etc.)
• LAPACK (for matrix operations)
• IEEE 754 floating point

What Kleis provides:

Example:

structure AdditiveMonoid(M) {
    operation add : M → M → M
    axiom add_comm: ∀(a b : M). add(a, b) = add(b, a)
}

implements AdditiveMonoid(ℕ) {
    operation add = builtin_add  // Rust's + operator
}

• :verify add_comm → Z3 checks its integer model ✅
• :eval 2 + 3 → Rust’s builtin_add runs ✅
• Connection between them → Trusted, not verified ⚠️

This is the pragmatic trade-off Kleis makes: trust the implementation, verify the mathematics.

Value Bindings with :let

Use :let to bind values to names that persist across REPL commands:

λ> :let x = 2 + 3
x = 5

λ> :eval x * 2
✅ 10

λ> :let matrix = Matrix(2, 2, [1, 2, 3, 4])
matrix = Matrix(2, 2, [1, 2, 3, 4])

λ> :eval det(matrix)
✅ -2

:let vs :define:

The it Magic Variable

After each :eval, the result is stored in it for quick chaining:

λ> :eval 2 + 3
✅ 5

λ> :eval it * 2
✅ 10

λ> :eval it + 1
✅ 11

This is inspired by GHCi and OCaml REPLs. Use :env to see all bindings including it:

λ> :env
📌 Value bindings:
  x = 5

📍 Last result (it):
  it = 11

📋 Defined functions:
  double (x) = ...

REPL Commands

Tip: Use it in any expression to refer to the last :eval result.

Multi-line Input

For complex expressions, end lines with \ or use block mode:

λ> :verify ∀(a : R, b : R). \
   (a + b) * (a - b) = a * a - b * b
✅ Valid

Or use :{ ... :} for blocks:

λ> :{
   :verify ∀(x : R, y : R, z : R).
     (x + y) + z = x + (y + z)
   :}
✅ Valid

Example Session

λ> :load examples/authorization/zanzibar.kleis
✅ Loaded: 1 files, 13 functions, 0 structures, 0 data types, 0 type aliases

λ> :env
📋 Defined functions:
  can_share (perm) = ...
  can_edit (perm) = ...
  can_delete (perm) = ...
  effective_permission (direct, group) = ...
  inherited_permission (child_perm, parent_perm) = ...
  can_comment (perm) = ...
  is_allowed (perm, action) = ...
  doc_access (doc_perm, folder_perm, action) = ...
  has_at_least (user_perm, required_perm) = ...
  can_read (perm) = ...
  multi_group_permission (perm1, perm2, perm3) = ...
  can_grant (granter_perm, grantee_perm) = ...
  can_transfer_ownership (perm) = ...

λ> :verify ∀(x : ℝ). x * x ≥ 0
✅ Valid

λ> :quit
Goodbye! 👋

Tips

1. Press Ctrl+C to cancel input
2. Press Ctrl+D or type :quit to exit
3. Use :symbols to copy-paste Unicode math symbols
4. Use :help <topic> for detailed help (e.g., :help quantifiers)

What’s Next?

For a richer interactive experience with plots and visualizations:

→ Jupyter Notebook

Or explore practical applications:

→ Applications

Jupyter Notebook

Kleis provides Jupyter kernel support, allowing you to write and execute Kleis code in Jupyter notebooks. This is ideal for:

JupyterLab launcher with Kleis and Kleis Numeric kernels

• Interactive exploration of mathematical concepts
• Teaching mathematical foundations
• Documenting proofs and derivations
• Numerical computation with LAPACK operations
• Publication-quality plotting with Lilaq/Typst integration

Quick Start

cd kleis-notebook
./start-jupyter.sh

This will:

1. Create a Python virtual environment (if needed)
2. Install JupyterLab and the Kleis kernel
3. Launch JupyterLab in your browser

Installation

Prerequisites

1. Python 3.8+ with pip
2. Kleis binary compiled with numerical features:

cd /path/to/kleis
export Z3_SYS_Z3_HEADER=/opt/homebrew/opt/z3/include/z3.h  # macOS Apple Silicon
cargo install --path . --features numerical

Note: The --features numerical flag enables LAPACK operations for eigenvalues, SVD, matrix inversion, and more.

Install the Kernel

cd kleis-notebook

# Option 1: Use the launcher script (recommended)
./start-jupyter.sh install

# Option 2: Manual installation
python3 -m venv venv
source venv/bin/activate
pip install -e .
pip install jupyterlab
python -m kleis_kernel.install
python -m kleis_kernel.install_numeric

Using Kleis in Jupyter

Creating a Notebook

1. Start JupyterLab: ./start-jupyter.sh
2. Click New Notebook
3. Select Kleis or Kleis Numeric kernel

Example: Defining a Group

structure Group(G) {
    operation (*) : G × G → G
    element e : G
    
    axiom left_identity: ∀(a : G). e * a = a
    axiom right_identity: ∀(a : G). a * e = a
    axiom associativity: ∀(a b c : G). (a * b) * c = a * (b * c)
}

Example: Testing Properties

example "group identity" {
    assert(e * e = e)
}

Output:

✅ group identity passed

Example: Numerical Computation

eigenvalues([[1.0, 2.0], [3.0, 4.0]])

Output:

[-0.3722813232690143, 5.372281323269014]

REPL Commands

Use REPL commands directly in notebook cells:

Jupyter Magic Commands

Numerical Operations

When Kleis is compiled with --features numerical, these LAPACK-powered operations are available:

Eigenvalue Decomposition

// Compute eigenvalues
eigenvalues([[4.0, 2.0], [1.0, 3.0]])
// → [5.0, 2.0]

// Full decomposition (eigenvalues + eigenvectors)
eig([[4.0, 2.0], [1.0, 3.0]])
// → [[5.0, 2.0], [[0.894, 0.707], [-0.447, 0.707]]]

Matrix Factorizations

// Singular Value Decomposition
svd([[1.0, 2.0], [3.0, 4.0], [5.0, 6.0]])
// → (U, S, Vt)

// QR Decomposition
qr([[1.0, 2.0], [3.0, 4.0]])
// → (Q, R)

// Cholesky Decomposition (symmetric positive definite)
cholesky([[4.0, 2.0], [2.0, 5.0]])
// → Lower triangular L where A = L * L^T

// Schur Decomposition
schur([[1.0, 2.0], [3.0, 4.0]])
// → (U, T, eigenvalues)

Linear Algebra

// Matrix inverse
inv([[1.0, 2.0], [3.0, 4.0]])
// → Matrix(2, 2, [-2, 1, 1.5, -0.5])

// Determinant
det([[1.0, 2.0], [3.0, 4.0]])
// → -2

// Solve linear system Ax = b
solve([[3.0, 1.0], [1.0, 2.0]], [9.0, 8.0])
// → [2.0, 3.0]

// Matrix rank
rank([[1.0, 2.0, 3.0], [4.0, 5.0, 6.0], [7.0, 8.0, 9.0]])
// → 2

// Condition number
cond([[1.0, 2.0], [3.0, 4.0]])
// → 14.933...

// Matrix norms
norm([[1.0, 2.0], [3.0, 4.0]])
// → Frobenius norm

Matrix Exponential

// e^A (useful for differential equations)
expm([[0.0, 1.0], [-1.0, 0.0]])
// → rotation matrix

Built-in Functions Reference

Important: These functions perform concrete numeric computation. They cannot be used in symbolic contexts such as structure definitions, axiom declarations, or abstract proofs. They are designed for interactive exploration, plotting, and numerical analysis.

Math Functions

Sequence Generation

Random Number Generation

These use a deterministic pseudo-random number generator (LCG) for reproducibility.

Vector Operations

List Manipulation

Pair Operations

Why Numeric-Only?

These functions are implemented in Rust for performance and produce concrete values:

// ✅ Works: Concrete computation
let xs = linspace(0, 6.28, 10)
let ys = list_map(λ x . sin(x), xs)
diagram(plot(xs, ys))

// ❌ Does NOT work: Cannot use in axioms
structure MyStructure(T) {
    axiom bad: sin(x) = cos(x - pi()/2)  // ERROR: sin/cos/pi are numeric
}

For symbolic mathematics, define your own abstract operations:

// ✅ Correct: Define sin symbolically
structure Trigonometry(T) {
    operation sin : T → T
    operation cos : T → T
    constant π : T
    
    axiom shift: ∀(x : T). sin(x) = cos(x - π/2)
}

Matrix Syntax

Matrices can be specified using nested list syntax:

// 2×2 matrix (row-major order)
[[1, 2], [3, 4]]

// 3×3 identity matrix concept
[[1, 0, 0], [0, 1, 0], [0, 0, 1]]

// Column vector as 3×1 matrix
[[1], [2], [3]]

// Row vector as 1×3 matrix
[[1, 2, 3]]

Session Persistence

Definitions persist across cells within a session:

Cell 1:

define square(x) = x * x

Cell 2:

example "use square" {
    assert(square(3) = 9)
}

Output:

✅ use square passed

Use %reset to clear all definitions and start fresh.

Tips for Effective Notebooks

1. Start with imports and definitions at the top
2. Use example blocks for testable assertions
3. Use :eval for quick numerical calculations
4. Use :verify for Z3-backed proofs
5. Document with markdown cells between code
6. Save frequently - Kleis notebooks are standard .ipynb files

Troubleshooting

“kleis binary not found”

Install Kleis with:

cd /path/to/kleis
export Z3_SYS_Z3_HEADER=/opt/homebrew/opt/z3/include/z3.h
cargo install --path . --features numerical

Numerical operations return symbolic expressions

Make sure Kleis was compiled with --features numerical:

cargo install --path . --features numerical

Kernel dies unexpectedly

Check the terminal for error messages. Common causes:

• Z3 timeout on complex verification
• Memory issues with large matrices

Imports fail (stdlib not found)

When running Jupyter from a directory other than the Kleis project root, stdlib imports may fail:

Error: Cannot find file: stdlib/prelude.kleis

Solution: Set the KLEIS_ROOT environment variable to point to your Kleis installation:

export KLEIS_ROOT=/path/to/kleis
jupyter lab

Or add it to your shell profile (~/.bashrc, ~/.zshrc):

export KLEIS_ROOT="$HOME/git/cee/kleis"

The Kleis kernel automatically searches for stdlib in:

1. $KLEIS_ROOT/stdlib/ (if KLEIS_ROOT is set)
2. Current working directory
3. Parent directories (up to 10 levels)

Unicode input

Use standard Kleis Unicode shortcuts:

• \forall → ∀
• \exists → ∃
• \in → ∈
• \R → ℝ
• \N → ℕ
• \Z → ℤ

Example Notebook

Here’s a complete example exploring matrix properties:

Cell 1: Setup

// Define a 2×2 matrix
let A = [[1.0, 2.0], [3.0, 4.0]]

Cell 2: Basic properties

det(A)        // → -2
trace(A)      // → 5 (not yet implemented, use 1+4)

Cell 3: Eigenvalues

eigenvalues(A)
// → [-0.372..., 5.372...]

Cell 4: Verify Cayley-Hamilton

// A matrix satisfies its characteristic polynomial
// For 2×2: A² - trace(A)*A + det(A)*I = 0
// This is verified numerically by the eigenvalue product

Cell 5: Matrix inverse

let Ainv = inv(A)
// Verify: A * Ainv should be identity
// (Matrix multiplication coming soon!)

Plotting

Kleis integrates with Lilaq (Typst’s plotting library) to generate publication-quality plots directly in Jupyter notebooks. The API mirrors Lilaq’s compositional design, making it easy to create complex visualizations.

Requirements

• Typst CLI must be installed: brew install typst (macOS) or see typst.app
• Lilaq 0.5.0+ is automatically imported

Compositional API

Kleis uses a compositional plotting API where:

• Individual functions (plot, scatter, bar, etc.) create PlotElement objects
• The diagram() function combines elements and renders to SVG
• Named arguments (key = value) configure options

diagram(
    plot(xs, ys, color = "blue"),
    scatter(xs, ys, mark = "s"),
    bar(xs, heights, label = "Data"),
    title = "My Chart",
    xlabel = "X-axis",
    theme = "moon"
)

Plot Functions

Data Generation Functions

Example: Grouped Bar Chart with Error Bars

let xs = [0, 1, 2, 3]
let ys1 = [1.35, 3, 2.1, 4]
let ys2 = [1.4, 3.3, 1.9, 4.2]
let yerr1 = [0.2, 0.3, 0.5, 0.4]
let yerr2 = [0.3, 0.3, 0.4, 0.7]

let xs_left = list_map(λ x . x - 0.2, xs)
let xs_right = list_map(λ x . x + 0.2, xs)

diagram(
    bar(xs, ys1, offset = -0.2, width = 0.4, label = "Left"),
    bar(xs, ys2, offset = 0.2, width = 0.4, label = "Right"),
    plot(xs_left, ys1, yerr = yerr1, color = "black", stroke = "none"),
    plot(xs_right, ys2, yerr = yerr2, color = "black", stroke = "none"),
    width = 5,
    legend_position = "left + top"
)

Example: Bar Chart with Dynamic Annotations

let xs = [0, 1, 2, 3, 4, 5, 6, 7, 8]
let ys = [12, 51, 23, 36, 38, 15, 10, 22, 86]

// Dynamic annotations using list_map and conditionals
let annotations = list_map(λ p . 
    let x = fst(p) in
    let y = snd(p) in
    let align = if y > 12 then "top" else "bottom" in
    place(x, y, y, align = align, padding = "0.2em")
, list_zip(xs, ys))

diagram(
    bar(xs, ys),
    annotations,
    width = 9,
    xaxis_subticks = "none"
)

Example: Climograph with Twin Axes

let months = ["Jan", "Feb", "Mar", "Apr", "May", "Jun", 
              "Jul", "Aug", "Sep", "Oct", "Nov", "Dec"]
let precipitation = [56, 41, 53, 42, 60, 67, 81, 62, 56, 49, 48, 54]
let temperature = [0.5, 1.4, 4.4, 9.7, 14.4, 17.8, 19.8, 19.5, 15.5, 10.4, 5.6, 2.2]
let xs = range(12)

diagram(
    yaxis(
        bar(xs, precipitation, fill = "blue.lighten(40%)", label = "Precipitation"),
        position = "right",
        axis_label = "Precipitation in mm"
    ),
    plot(xs, temperature, label = "Temperature", color = "red", stroke = "1pt", mark_size = 6),
    width = 8,
    title = "Climate of Berlin",
    ylabel = "Temperature in °C",
    xlabel = "Month",
    xaxis_ticks = months,
    xaxis_tick_rotate = -90,
    xaxis_subticks = "none"
)

Example: Koch Snowflake Fractal

// Complex number operations
define complex_add(c1, c2) = Pair(fst(c1) + fst(c2), snd(c1) + snd(c2))
define complex_sub(c1, c2) = Pair(fst(c1) - fst(c2), snd(c1) - snd(c2))
define complex_mul(c1, c2) = Pair(
    (fst(c1)*fst(c2)) - (snd(c1)*snd(c2)),
    (fst(c1)*snd(c2)) + (snd(c1)*fst(c2))
)

define triangle_vertex(angle) = Pair(cos(radians(angle)), sin(radians(angle)))
define base_triangle() = [triangle_vertex(90), triangle_vertex(210), triangle_vertex(330)]

define koch_edge(p1, p2) = 
    let d = complex_sub(p2, p1) in
    [p1, complex_add(p1, complex_mul(d, Pair(1/3, 0))),
     complex_add(p1, complex_mul(d, Pair(0.5, 0 - sqrt(3)/6))),
     complex_add(p1, complex_mul(d, Pair(2/3, 0)))]

define koch_iter(pts) = 
    let n = list_length(pts) in
    list_flatten(list_map(λ i . 
        koch_edge(list_nth(pts, i), list_nth(pts, mod(i + 1, n)))
    , range(n)))

let n0 = base_triangle()
let n3 = koch_iter(koch_iter(koch_iter(n0)))  // 192 vertices

diagram(
    path(n3, fill = "blue", closed = true),
    width = 6, height = 7,
    xaxis_ticks_none = true,
    yaxis_ticks_none = true
)

Example: Scatter Plot with Colormap

let xs = linspace(0, 12.566370614, 50)  // 0 to 4π
let ys = list_map(lambda x . sin(x), xs)
let noise = random_normal(50, 33, 0.1)
let xs_noisy = vec_add(xs, noise)
let colors = random(50, 42)

diagram(
    plot(xs, ys, mark = "none"),
    scatter(xs_noisy, ys, 
        mark = "s",
        colors = colors,
        map = "turbo",
        stroke = "0.5pt + black"
    ),
    theme = "moon"
)

Example: Stacked Area Chart

let xs = [0, 1, 2, 3, 4, 5, 6, 7, 8, 9]
let y1 = [0, 1, 3, 9, 5, 4, 2, 2, 1, 0]
let y2 = [5, 3, 2, 0, 1, 2, 2, 2, 3, 2]
let y3 = [0, 0, 0, 0, 1, 2, 4, 5, 5, 9]

diagram(
    stacked_area(xs, y1, y2, y3),
    theme = "moon"
)

Themes

Kleis supports Lilaq’s built-in themes:

diagram(
    plot(xs, ys),
    theme = "moon"
)

Axis Customization

Complete Example Notebook

Cell 1: Import stdlib

import "stdlib/prelude.kleis"

Cell 2: Generate data with linspace

let xs = linspace(0, 6.28, 50)
let ys = list_map(lambda x . sin(x), xs)

Cell 3: Plot with theme

diagram(
    plot(xs, ys, color = "blue", stroke = "2pt"),
    title = "Sine Wave",
    xlabel = "x",
    ylabel = "sin(x)",
    theme = "moon"
)

Logarithmic Scales

For exponential or power-law data, use logarithmic scales:

// Semi-log plot (linear x, logarithmic y)
diagram(
    plot([0, 1, 2, 3, 4], [1, 10, 100, 1000, 10000]),
    title = "Exponential Growth",
    yscale = "log"   // "linear", "log", or "symlog"
)

// Log-log plot (both axes logarithmic)
diagram(
    plot([1, 10, 100, 1000], [1, 100, 10000, 1000000]),
    title = "Power Law",
    xscale = "log",
    yscale = "log"
)

Available scales:

• "linear" - Default linear scale
• "log" - Logarithmic scale (base 10)
• "symlog" - Symmetric log (linear near 0, log elsewhere; handles negative values)

Next Steps

• Learn to create PDFs, theses, and papers: Document Generation
• Explore the REPL chapter for more interactive features
• See Matrices for symbolic matrix operations
• Check Z3 Verification for formal proofs

Creating Documents with Kleis

Kleis provides a complete document generation system for creating publication-quality theses, dissertations, and papers. Unlike traditional approaches where documents are separate from code, in Kleis your document IS a program.

The Philosophy: Document = Program

Traditional academic writing separates:

• Code (Jupyter notebooks, Python scripts)
• Equations (LaTeX, copy-pasted)
• Plots (matplotlib, exported as images)
• Document (Word, LaTeX, Google Docs)

This separation causes problems:

• Copy-paste errors between code and paper
• Equations that can’t be re-edited
• Plots that can’t be regenerated
• No verification of mathematical claims

Kleis unifies everything into a single program:

┌─────────────────────────────────────────────────────────────┐
│               Your Document (.kleis file)                   │
├─────────────────────────────────────────────────────────────┤
│  Template Import   │ import "stdlib/templates/mit_thesis"   │
│  Metadata          │ Title, author, date, abstract          │
│  Equations         │ MITEquation("label", "$ E = mc^2 $")   │
│  Diagrams          │ MITDiagram("fig1", "caption", code)    │
│  Tables            │ MITTable("tab1", "caption", typst)     │
│  Chapters          │ MITChapter(1, "Introduction", "...")   │
│  Compile Function  │ compile_mit_thesis(my_thesis)          │
└─────────────────────────────────────────────────────────────┘
                              ↓
                   kleis test my_thesis.kleis
                              ↓
                        Typst Output
                              ↓
                   typst compile → PDF

Quick Start

Prerequisites

1. Kleis compiled and in PATH
2. Typst for PDF generation: brew install typst

Your First Document (5 minutes)

Create a file my_paper.kleis:

import "stdlib/templates/arxiv_paper.kleis"

// Define your paper
define my_paper = arxiv_paper(
    "My Amazing Research",                    // title
    ["Alice Smith", "Bob Jones"],             // authors
    ["MIT", "Stanford"],                      // affiliations
    "We present groundbreaking results...",   // abstract
    ["machine learning", "verification"],     // keywords
    [
        ArxivSection("Introduction", "We begin by..."),
        ArxivEquation("eq:main", "$ f(x) = x^2 + 1 $"),
        ArxivSection("Methods", "Our approach uses..."),
        ArxivSection("Conclusion", "We have shown...")
    ]
)

// Compile and output
example "compile" {
    let typst = compile_arxiv_paper(my_paper)
    // REQUIRED: typst_raw() makes output unquoted (no "..." around strings)
    // Without it, Typst would see quoted strings and fail to parse
    out(typst_raw(typst))
}

Generate PDF:

# --raw-output suppresses banners (✅/❌), typst_raw() in code produces unquoted output
kleis test --raw-output --example compile my_paper.kleis > my_paper.typ
typst compile my_paper.typ my_paper.pdf
open my_paper.pdf

That’s it! Your document is a Kleis program.

Emit clean Typst (no quotes, no banners)

• Required: Wrap your compiled document in typst_raw(...) before calling out(...). This is what makes the output unquoted - without it, strings are printed with quotes ("...") which breaks Typst parsing.
• Use table_typst_raw(...) for tables so Typst code is emitted directly (no ASCII boxes).
• Run kleis test --raw-output --example <compile_example> your_doc.kleis to suppress test banners (✅/❌) and summary lines.
• Then pipe to typst compile.

Important: The --raw-output flag only suppresses banners. The typst_raw() wrapper is what produces unquoted output suitable for Typst.

What --raw-output Suppresses

The --raw-output flag suppresses all test framework output:

• Per-example status lines (passed/failed/skipped)
• Error messages after failed examples
• The summary line (“N examples passed” or “N/M examples passed”)

It does not suppress:

• Output from out() calls in your example blocks (this is what you want to capture)
• Exit code 1 on failure (so CI pipelines still detect errors)

Available Templates

Kleis includes three professionally-styled templates:

Each template includes:

• Proper page margins and fonts per institution guidelines
• Title page, abstract, table of contents
• Chapter/section formatting
• Figure, table, and equation support
• Bibliography formatting
• Appendices

Template Gallery

MIT Thesis:

University of Michigan Dissertation:

arXiv Paper:

MIT Thesis Template

The MIT thesis template follows the official MIT Libraries thesis specifications.

Document Structure

import "stdlib/templates/mit_thesis.kleis"

// Define thesis metadata
define my_thesis = mit_thesis(
    "Formal Verification of Knowledge Production Systems",  // title
    "Jane Smith",                                            // author
    "Department of EECS",                                    // department
    "May 2026",                                              // date
    PhD,                                                     // degree: SB, SM, or PhD
    "This thesis presents Kleis, a formal verification...", // abstract
    "Prof. Alice Chen",                                      // supervisor
    "Professor of Computer Science",                         // supervisor title
    "I thank my advisor...",                                 // acknowledgments
    "To my family...",                                       // dedication
    all_elements                                             // document content
)

Content Elements

// Chapters
define ch1 = MITChapter(1, "Introduction", "Knowledge production relies on...")

// Sections within chapters
define sec1 = MITSection("Motivation", "The need for formal verification...")

// Subsections
define subsec1 = MITSubsection("Historical Context", "Early work in...")

// Equations
define eq_einstein = MITEquation("eq:einstein", "$ E = m c^2 $")

// Figures (with Typst code)
define fig_arch = MITFigure("fig:arch", "System architecture",
    "#rect(width: 80%, height: 3cm, fill: luma(240))[Architecture diagram]")

// Diagrams using NATIVE KLEIS data
define iterations = [1.0, 2.0, 3.0, 4.0, 5.0]
define accuracy = [10.0, 25.0, 40.0, 55.0, 70.0]
define fig_perf = MITDiagram("fig:perf", "Performance comparison",
    export_typst_fragment(plot(iterations, accuracy, mark = "o"),
        xlabel = "Iterations", ylabel = "Accuracy (%)"))

// Tables using NATIVE KLEIS data
define headers = ["Method", "Accuracy", "Runtime"]
define rows = [["Baseline", "72%", "1.2s"], ["Ours", "89%", "0.8s"]]
define tab_results = MITTable("tab:results", "Experimental results",
    table_typst_raw(headers, rows))

// References
define ref1 = MITReference("demoura2008", 
    "de Moura, L. Z3: An Efficient SMT Solver. TACAS 2008.")

// Appendices
define app_a = MITAppendix("Proofs", "Detailed proofs of theorems...")

// Acknowledgments and dedication
define ack = MITAcknowledgments("I thank my advisor...")
define ded = MITDedication("To my family...")

Complete MIT Thesis Example

See the full working example: examples/documents/jane_smith_thesis.kleis

import "stdlib/prelude.kleis"
import "stdlib/templates/mit_thesis.kleis"

// ============================================================================
// JANE SMITH'S PHD THESIS
// ============================================================================

// Chapter 1: Introduction
define ch1 = MITChapter(1, "Introduction", 
    "Knowledge production in science relies on precise notation and rigorous 
    verification. Traditional approaches separate these concerns...")

// Key equation
define eq_einstein = MITEquation("eq:einstein", "$ E = m c^2 $")

// Performance diagram using NATIVE KLEIS data
define loc = [100.0, 500.0, 1000.0, 5000.0, 10000.0]
define kleis_time = [0.1, 0.3, 0.5, 1.2, 2.1]
define other_time = [0.2, 0.8, 2.0, 12.0, 45.0]

define fig_performance = MITDiagram("fig:perf", "Type inference performance",
    export_typst_fragment(plot(loc, kleis_time, mark = "o", label = "Kleis"),
        xlabel = "Lines of Code", ylabel = "Time (seconds)"))

// Results table using NATIVE KLEIS data
define feature_headers = ["Feature", "Kleis", "Lean", "Coq"]
define feature_rows = [
    ["SMT Integration", "✓", "Partial", "✗"],
    ["Type Inference", "✓", "✓", "✓"],
    ["Typst Export", "✓", "✗", "✗"]
]
define table_features = MITTable("tab:features", "Feature comparison",
    table_typst_raw(feature_headers, feature_rows))

// Assemble all elements in order
define all_elements = [
    ack,           // Acknowledgments (front matter)
    ded,           // Dedication (front matter)
    ch1,           // Chapter 1
    eq_einstein,
    fig_performance,
    ch2,           // Chapter 2
    table_features,
    ch3,           // Chapter 3
    ref1, ref2,    // References
    app_a          // Appendix
]

// Create the thesis
define my_thesis = mit_thesis_full(
    "Formal Verification of Knowledge Production Systems",
    "Jane Smith",
    "Department of Electrical Engineering and Computer Science",
    "May 2026",
    PhD,
    "This thesis presents Kleis, a formal verification system...",
    "Prof. Alice Chen",
    "Professor of Computer Science",
    "I thank my advisor Prof. Chen for her guidance...",
    "To my parents, who taught me to question everything.",
    all_elements
)

// Compile to Typst
example "compile_thesis" {
    let typst = compile_mit_thesis(my_thesis)
    // Emit raw Typst so there are no quotes/escapes
    out(typst_raw(typst))
}

Running the example without banners/quotes: use the raw output mode so the Typst stream is clean and can be piped directly to typst compile:

./target/release/kleis test examples/documents/jane_smith_thesis.kleis > /tmp/mit_thesis.typ
typst compile /tmp/mit_thesis.typ /tmp/mit_thesis.pdf

What the MIT Template Produces

The compiled thesis includes:

1. Title Page - Centered title, author, department, degree, date
2. Signature Page - For PhD: supervisor signature block
3. Abstract - Formatted per MIT specifications
4. Acknowledgments - Optional dedication to advisors, family
5. Dedication - Optional short dedication
6. Table of Contents - Auto-generated from chapters
7. List of Figures - Auto-generated from figures
8. List of Tables - Auto-generated from tables
9. Chapters - Numbered chapters with sections
10. References - Bibliography section
11. Appendices - Lettered appendices (A, B, C…)

Table of Contents (auto-generated):

Chapter Content with Equations and Diagrams:

University of Michigan Rackham Template

The UofM template follows Rackham Graduate School formatting guidelines.

Document Structure

import "stdlib/templates/uofm_thesis.kleis"

// Committee members
define committee = [
    committee_member("Prof. Alice Chen", "Computer Science"),
    committee_member("Prof. Bob Smith", "Mathematics"),
    committee_member("Prof. Carol Davis", "Statistics")
]

// Define dissertation
define my_dissertation = umich_dissertation(
    "Deep Learning Theory and Applications",      // title
    "Alex Chen",                                  // author
    "Computer Science and Engineering",           // program
    "2026",                                       // year
    PhD,                                          // degree
    "This dissertation investigates...",          // abstract
    "Prof. Alice Chen",                           // committee chair
    "Computer Science and Engineering",           // chair affiliation
    committee,                                    // committee list
    "achen@umich.edu",                           // email
    "0000-0001-2345-6789",                       // ORCID
    "I thank the Rackham Graduate School...",    // acknowledgments
    "To my mentors...",                          // dedication
    "This work began as...",                     // preface
    all_elements                                 // content
)

UofM-Specific Features

• Double spacing throughout (Rackham requirement)
• Identifier page with ORCID and email
• Committee page with full committee list
• Preface section (optional)
• 2-inch top margin on chapter openings
• Roman numerals for front matter pages

Complete UofM Example

See: examples/documents/alex_chen_dissertation.kleis

Run the provided compile block with raw output to get Typst ready for typst compile:

./target/release/kleis test examples/documents/alex_chen_dissertation.kleis > /tmp/umich.typ
typst compile /tmp/umich.typ /tmp/umich.pdf

arXiv Paper Template

The arXiv template follows common academic paper conventions for preprints.

Document Structure

import "stdlib/templates/arxiv_paper.kleis"

define my_paper = arxiv_paper_full(
    "Attention Is All You Need",                          // title
    ["Ashish Vaswani", "Noam Shazeer", "Niki Parmar"],   // authors
    ["Google Brain", "Google Brain", "Google Research"], // affiliations
    "The dominant sequence transduction models...",       // abstract
    ["transformers", "attention", "neural networks"],    // keywords
    all_elements                                          // content
)

arXiv Content Elements

// Sections (no chapters in papers)
ArxivSection("Introduction", "Recent advances in...")
ArxivSection("Related Work", "Prior work includes...")

// Equations
ArxivEquation("eq:attention", "$ \\text{Attention}(Q, K, V) = \\text{softmax}(QK^T / \\sqrt{d_k})V $")

// Algorithms (using Typst's algo package)
ArxivAlgorithm("alg:train", "Training procedure", "
#import \"@preview/algorithmic:0.1.0\"
#algorithmic.algorithm({
  algorithmic.For(cond: [epoch in 1..N])[
    algorithmic.For(cond: [batch in data])[
      Compute loss and update
    ]
  ]
})
")

// Figures, tables, diagrams (same as MIT)
ArxivFigure("fig:model", "Model architecture", "...")
define result_headers = ["Method", "Accuracy", "Runtime"]
define result_rows = [["Baseline", "72%", "1.2s"], ["Ours", "89%", "0.8s"]]
ArxivTable("tab:results", "Experimental results",
    table_typst_raw(result_headers, result_rows))
ArxivDiagram("fig:loss", "Training loss", "...")

// Acknowledgments
ArxivAcknowledgments("We thank the Google Brain team...")

// References
ArxivReference("vaswani2017", "Vaswani et al. Attention Is All You Need. NeurIPS 2017.")

// Appendices
ArxivAppendix("Implementation Details", "We used PyTorch...")

Complete arXiv Example

See: examples/documents/sample_arxiv_paper.kleis

Diagrams and Plots

Kleis integrates with the Lilaq plotting library for creating beautiful diagrams directly in your document.

Native Kleis Data (Recommended)

The most powerful approach uses native Kleis lists with export_typst_fragment():

// Define your data as Kleis lists
define epochs = [1.0, 2.0, 3.0, 4.0, 5.0]
define accuracy = [10.0, 25.0, 45.0, 70.0, 90.0]

// Create a plot using Kleis's native plot() function
define my_plot = plot(epochs, accuracy, mark = "o", label = "Training")

// Convert to Typst code for embedding in a figure
define typst_code = export_typst_fragment(my_plot,
    title = "Model Performance",
    xlabel = "Epoch",
    ylabel = "Accuracy (%)"
)

// Use in your thesis/paper
define fig_training = MITDiagram("fig:training", "Training curves", typst_code)

Note: When piping to typst:

1. Use --raw-output to suppress test banners (✅/❌)
2. Use --example compile to run only the compile example
3. Ensure your example uses out(typst_raw(...)) for unquoted output

./target/release/kleis test --raw-output --example compile examples/documents/sample_arxiv_paper.kleis > /tmp/paper.typ
typst compile /tmp/paper.typ /tmp/paper.pdf

Why use native data?

• Your data is Kleis—it can be computed, verified, and reused
• No manual Typst syntax errors
• Data can flow from experiments to figures seamlessly
• Easier to update when results change

Available Plot Functions

Each function accepts optional parameters: label, mark, stroke, etc.

Example: Complete Workflow

// Raw experimental data
define x_data = [0.1, 0.5, 1.0, 5.0, 10.0, 25.0]
define method_a = [150.0, 120.0, 100.0, 80.0, 60.0, 40.0]
define method_b = [180.0, 140.0, 110.0, 85.0, 65.0, 45.0]

// Create plots
define plot_a = plot(x_data, method_a, mark = "o", label = "Method A")
define plot_b = plot(x_data, method_b, mark = "x", label = "Method B")

// Combine into diagram
define comparison_typst = export_typst_fragment(plot_a,
    title = "Performance Comparison",
    xlabel = "Problem Size",
    ylabel = "Time (ms)"
)

// Embed in thesis
define fig_comparison = MITDiagram("fig:comparison",
    "Performance comparison between methods",
    comparison_typst
)

Fallback: Raw Typst Strings

For complex diagrams not yet supported by native functions, you can use raw Typst strings:

define fig_complex = MITDiagram("fig:complex", "Complex diagram", "
import \"@preview/lilaq:0.5.0\" as lq
lq.diagram(
    lq.plot((1, 2, 3, 4), (10, 20, 35, 50), stroke: blue, mark: \"o\"),
    lq.plot((1, 2, 3, 4), (15, 30, 42, 55), stroke: red, mark: \"x\"),
    xlabel: \"Iteration\",
    ylabel: \"Value\"
)")

Tables

Native Kleis Data with table_typst_raw() (Recommended)

The cleanest approach uses Kleis lists with table_typst_raw(), which emits Typst directly (no quotes, no ASCII boxes):

// Define table data as Kleis lists
define headers = ["Method", "Accuracy", "F1 Score"]
define rows = [
    ["Baseline", "72.3%", "0.71"],
    ["Ours", "89.7%", "0.88"],
    ["SOTA", "87.1%", "0.86"]
]

// Generate Typst table code (raw Typst)
define table_code = table_typst_raw(headers, rows)

// Use in your thesis/paper
define tab_results = MITTable("tab:results", "Benchmark results", table_code)

Why use table_typst_raw()?

• Data as Kleis lists—can be computed, imported, or transformed
• No manual Typst table syntax
• Rows can come from experiments or external data
• Easy to add/remove rows programmatically
• Produces clean Typst for piping to typst compile

Example: Complete Workflow

// Data from experiments
define methods = ["CNN", "ResNet", "Transformer", "Kleis-Net"]
define accuracy = ["72.3%", "85.1%", "87.4%", "89.7%"]
define f1_scores = ["0.71", "0.84", "0.86", "0.88"]
define memory = ["128 MB", "256 MB", "512 MB", "192 MB"]

// Build table from data
define headers = ["Method", "Accuracy", "F1", "Memory"]
define rows = [
    ["CNN", "72.3%", "0.71", "128 MB"],
    ["ResNet", "85.1%", "0.84", "256 MB"],
    ["Transformer", "87.4%", "0.86", "512 MB"],
    ["Kleis-Net", "89.7%", "0.88", "192 MB"]
]

define tab_comparison = MITTable("tab:comparison",
    "Comparison of deep learning methods",
    table_typst_raw(headers, rows)
)

Fallback: Raw Typst Strings

For styled tables, you can use raw Typst syntax:

define tab_styled = MITTable("tab:styled", "Styled table", "
#table(
    columns: 4,
    stroke: 0.5pt,
    fill: (col, row) => if row == 0 { luma(230) },
    [Feature], [Kleis], [Lean], [Coq],
    [SMT], [✓], [Partial], [✗],
    [Types], [HM], [Dependent], [Dependent]
)")

Equations

Equations use Typst math syntax (similar to LaTeX):

// Simple equation
MITEquation("eq:simple", "$ x = \\frac{-b \\pm \\sqrt{b^2 - 4ac}}{2a} $")

// Multi-line equation
MITEquation("eq:multi", "$
\\nabla \\cdot E &= \\frac{\\rho}{\\epsilon_0} \\
\\nabla \\cdot B &= 0 \\
\\nabla \\times E &= -\\frac{\\partial B}{\\partial t} \\
\\nabla \\times B &= \\mu_0 J + \\mu_0 \\epsilon_0 \\frac{\\partial E}{\\partial t}
$")

// Inline math in text - just use $...$
MITSection("Methods", "A function $f: RR^n -> RR^m$ maps inputs to outputs.")

// Literal dollar sign - use \$
MITSection("Cost", "The price is \\$100 per unit.")

Common Math Symbols

💡 Tip: Use the Equation Editor

You don’t have to type Typst syntax manually!

The Kleis Equation Editor is a visual, WYSIWYG tool for building equations. Instead of memorizing frac(a, b) or mat(delim: "[", ...), you:

1. Build visually — Click buttons to create fractions, matrices, integrals
2. See live preview — The equation renders as you build (powered by Typst)
3. Copy and paste — Click “📋 Copy Typst” and paste into your thesis

The Equation Editor showing a type-checked matrix multiplication with rotation matrix. The type indicator confirms: Matrix(2, 2, Scalar).

The workflow:

Visual Editor → 📋 Copy Typst → Paste into thesis.kleis → PDF

Example: Building let A = [1 2 3; 4 5 6] × R_z(θ) × [1 0; 2 1; 2 1] takes seconds visually — versus minutes of typing and debugging Typst syntax.

Note: The Equation Editor requires kleis server running:

kleis server
# Server running at http://localhost:3000

Then open http://localhost:3000 in your browser. Full documentation coming in a future chapter.

Generating PDFs

Command Line

# Compile Kleis to Typst
# --raw-output: suppresses ✅/❌ banners
# --example compile: runs only the "compile" example block
# Your example must use out(typst_raw(...)) for unquoted output
kleis test --raw-output --example compile my_thesis.kleis > my_thesis.typ

# Compile Typst to PDF  
typst compile my_thesis.typ my_thesis.pdf

# Open PDF (macOS)
open my_thesis.pdf

One-liner

kleis test --raw-output --example compile my_thesis.kleis > my_thesis.typ && typst compile my_thesis.typ && open my_thesis.pdf

From Jupyter

Jupyter is the recommended environment for writing your thesis. Here’s a complete workflow:

Cell 1: Setup and check templates

from kleis_kernel import compile_to_pdf, compile_to_typst, list_templates, validate

# See available templates
print("Available templates:", list_templates())
# Output: ['mit_thesis', 'uofm_thesis', 'arxiv_paper']

Cell 2: Validate your document

# Check for parse errors before compiling
validate("my_thesis.kleis")
# Output: ✓ my_thesis.kleis is valid

Cell 3: Generate PDF

# Compile Kleis → Typst → PDF
compile_to_pdf("my_thesis.kleis", "my_thesis.pdf")
# Output: ✓ PDF created: my_thesis.pdf

Cell 4: Display in notebook

from IPython.display import IFrame
IFrame("my_thesis.pdf", width=800, height=600)

Alternative: View Typst output

# See the generated Typst code (useful for debugging)
typst_code = compile_to_typst("my_thesis.kleis")
print(typst_code[:500])  # First 500 chars

Complete Jupyter Workflow Example

# ============================================================
# Thesis Writing Workflow in Jupyter
# ============================================================

from kleis_kernel import compile_to_pdf, validate
from IPython.display import IFrame
import os

# 1. Your thesis file (edit this in VS Code or any text editor)
THESIS_FILE = "my_thesis.kleis"

# 2. Validate before compiling
if validate(THESIS_FILE):
    
    # 3. Generate PDF
    compile_to_pdf(THESIS_FILE, "thesis_draft.pdf")
    
    # 4. Display inline
    display(IFrame("thesis_draft.pdf", width=800, height=600))
    
else:
    print("Fix the errors above, then re-run this cell")

Tips for Jupyter Users

1. Edit .kleis files externally - Use VS Code with syntax highlighting
2. Use Jupyter for compilation - Quick feedback loop
3. Version control - Git works great with .kleis files (they’re plain text)
4. Hot reload - Re-run the cell after editing your .kleis file

Creating Custom Templates

To create a new template (e.g., for IEEE or Nature), create a .kleis file:

// stdlib/templates/ieee_paper.kleis

import "stdlib/prelude.kleis"

// Template metadata
define template_name = "IEEE Paper"
define template_version = "1.0"
define template_type = "paper"

// Data types for document elements
data IEEEDocExpr = 
    IEEESection(title: String, content: String)
  | IEEEEquation(label: String, typst_code: String)
  | IEEEFigure(label: String, caption: String, typst_code: String)
  | IEEETable(label: String, caption: String, typst_code: String)
  | IEEEReference(key: String, citation: String)

// Document container
data IEEEPaper = IEEEPaper(
    title: String,
    authors: List(String),
    affiliations: List(String),
    abstract_text: String,
    keywords: List(String),
    elements: List(IEEEDocExpr)
)

// Typst styling
define typst_ieee_page_setup = "#set page(
    paper: \"us-letter\",
    margin: (top: 0.75in, bottom: 1in, left: 0.625in, right: 0.625in),
    columns: 2
)"

define typst_ieee_text_setup = "#set text(
    font: \"Times New Roman\",
    size: 10pt
)"

// ... more styling definitions ...

// Compile function
define compile_ieee_paper(paper) = 
    match paper {
        IEEEPaper(title, authors, affiliations, abstract_text, keywords, elements) =>
            concat(typst_ieee_page_setup,
            concat(typst_ieee_text_setup,
            // ... assemble document ...
            ))
    }

No Rust code changes needed! Just add the template file.

Tips for Thesis Writing

1. Save frequently — Your .kleis file is the source of truth
2. Use version control — .kleis files are text, perfect for git
3. Label everything — Use meaningful labels for cross-references
4. Test incrementally — Compile often to catch errors early
5. Use Lilaq for plots — Regenerable, not static images
6. Store in one file — Keep related content together

Troubleshooting

“Typst not found”

# macOS
brew install typst

# Linux
curl -fsSL https://typst.app/install.sh | sh

“Parse error in .kleis file”

Check for:

• Unescaped quotes in strings (use \")
• Missing commas in lists
• Unclosed parentheses

“Figure not rendering”

Ensure Lilaq import is correct in your diagram code:

import "@preview/lilaq:0.5.0" as lq

“Cross-reference not found”

Labels must match exactly:

MITEquation("eq:main", "...")  // Define
"See Equation @eq:main"         // Reference

Next Steps

• See how documents combine with verification: Applications
• See full examples in examples/documents/
• Explore Typst documentation: typst.app/docs
• Learn Lilaq plotting: Lilaq on Typst Universe

Applications

Kleis is designed for mathematical verification, but its power extends far beyond pure mathematics. This chapter showcases applications across multiple domains.

Note: Many examples in this chapter use example blocks with assert statements for testing and verification. See Example Blocks for details on this syntax.

AI/ML Verification

Kleis aligns with the research agenda outlined in “Toward Verified Artificial Intelligence” (Seshia et al., Communications of the ACM, 2022) — a seminal paper from UC Berkeley on using formal methods to verify AI systems.

The Verified AI Challenge

The paper identifies five key challenges for AI verification:

Neural Network Properties

Kleis can express and verify properties of neural networks:

// Robustness: Small input changes → small output changes
structure RobustnessProperty {
    axiom local_robustness: ∀ x : Input . ∀ δ : Input .
        norm(δ) < ε → 
        abs(network(x + δ) - network(x)) < bound
}

// Monotonicity: Larger input → larger output (for certain features)
structure MonotonicityProperty {
    axiom monotonic_feature: ∀ x1 : Input . ∀ x2 : Input .
        x1.feature ≤ x2.feature → 
        network(x1) ≤ network(x2)
}

// Safety envelope: Output always in safe region
structure SafetyProperty {
    axiom output_bounded: ∀ x : Input .
        valid_input(x) → 
        min_safe ≤ network(x) ∧ network(x) ≤ max_safe
}

Safe Reinforcement Learning

// Safety envelope for learning-based controllers
structure SafeController(state_dim: Nat, action_dim: Nat) {
    // Pre-computed safety region
    element safe_set : Set(State)
    
    // Learned policy
    operation policy : State → Action
    
    // Safety invariant: policy never leaves safe set
    axiom safety_invariant: ∀ s : State .
        s ∈ safe_set → 
        next_state(s, policy(s)) ∈ safe_set
    
    // Backup controller for edge cases
    operation backup : State → Action
    
    axiom backup_safe: ∀ s : State .
        next_state(s, backup(s)) ∈ safe_set
}

Compositional Verification

The paper emphasizes assume-guarantee reasoning — exactly what Kleis structures provide:

// Perception module contract
structure PerceptionContract {
    operation detect : Image → List(BoundingBox)
    
    // Guarantee: no false negatives within sensor range
    axiom no_miss_close: ∀ img : Image . ∀ obj : Object .
        distance(obj) < sensor_range ∧ visible(obj, img) →
        ∃ box : BoundingBox . box ∈ detect(img) ∧ contains(box, obj)
}

// Planning module contract
structure PlanningContract {
    // Assume: perception is correct within range
    // Guarantee: plan avoids all detected obstacles
    axiom collision_free: ∀ boxes : List(BoundingBox) . ∀ plan : Trajectory .
        plan = plan_path(boxes) →
        ∀ t : Time . ∀ box : BoundingBox . 
            box ∈ boxes → ¬intersects(plan(t), box)
}

// System-level property emerges from composition
structure SystemSafety {
    axiom no_collision: ∀ img : Image .
        let boxes = PerceptionContract.detect(img) in
        let plan = PlanningContract.plan_path(boxes) in
        collision_free(plan)
}

Why Kleis for AI Verification?

Further Reading

• Paper: Toward Verified Artificial Intelligence (CACM 2022)
• VerifAI: Toolkit for formal AI verification (same authors)
• Scenic: Domain-specific language for scenario specification

Kleis provides a general-purpose substrate for expressing the same verification concepts in a unified, mathematically rigorous framework.

Hardware Verification

Kleis can formally verify hardware designs using Z3’s bitvector theory. This section explains how Kleis compares to the industry-standard Universal Verification Methodology (UVM) defined in IEEE 1800.2-2020.

Kleis vs UVM: Different Approaches to the Same Goal

What Kleis Proves

Kleis can formally prove properties for ALL possible inputs:

// Bitvector operations (maps to SystemVerilog bit[7:0])
operation bvadd : BitVec8 × BitVec8 → BitVec8
operation bvxor : BitVec8 × BitVec8 → BitVec8
operation bv_zero : BitVec8

// PROVE: Addition is commutative for ALL 2^16 input pairs
example "ADD is commutative" {
    assert(∀ a : BitVec8 . ∀ b : BitVec8 . bvadd(a, b) = bvadd(b, a))
}

// PROVE: XOR of same value always yields zero
example "XOR self is zero" {
    assert(∀ a : BitVec8 . bvxor(a, a) = bv_zero)
}

// PROVE: Subtraction inverts addition
example "SUB inverts ADD" {
    assert(∀ a : BitVec8 . ∀ b : BitVec8 . bvsub(bvadd(a, b), b) = a)
}

A UVM testbench would run random tests and hope to find bugs. Kleis proves correctness mathematically.

Reachability Analysis (Related to Coverage)

UVM coverage answers: “Did our tests exercise this state?”

Kleis reachability answers: “Is this state possible at all?”

// Can ADD ever produce zero? (Yes: 0+0, or 128+128 with overflow)
example "Zero is reachable via ADD" {
    assert(∃ a : BitVec8 . ∃ b : BitVec8 . bvadd(a, b) = bv_zero)
}

// Can ADD produce non-zero? (Yes: 1+0, etc.)
example "Non-zero is reachable via ADD" {
    assert(∃ a : BitVec8 . ∃ b : BitVec8 . bvadd(a, b) ≠ bv_zero)
}

Kleis Complements UVM, Not Replaces It

Kleis and UVM solve related but different problems:

┌─────────────────────────────────────────────────────────────┐
│                    VERIFICATION WORKFLOW                    │
├─────────────────────────────────────────────────────────────┤
│                                                             │
│   KLEIS (Pre-RTL)              UVM (With RTL)               │
│   ┌────────────────┐           ┌────────────────┐           │
│   │ Define ALU     │           │ Verilog ALU    │           │
│   │ specification  │    →      │ implementation │           │
│   └────────────────┘           └────────────────┘           │
│          ↓                            ↓                     │
│   ┌────────────────┐           ┌────────────────┐           │
│   │ PROVE correct  │           │ SIMULATE with  │           │
│   │ for ALL inputs │           │ random tests   │           │
│   └────────────────┘           └────────────────┘           │
│          ↓                            ↓                     │
│   Mathematical                 "Probably correct"           │
│   certainty                    (statistical)                │
│                                                             │
└─────────────────────────────────────────────────────────────┘

Use Kleis FIRST: Prove your algorithm is correct before writing HDL.

Use UVM AFTER: Validate your Verilog/VHDL implements the algorithm correctly.

What UVM Has That Kleis Doesn’t

Example: ALU Verification

See examples/hardware/alu_verification.kleis for a complete example that proves:

• ADD/AND/OR/XOR commutativity
• Addition associativity
• Subtraction inverts addition
• AND idempotence
• XOR self produces zero
• Additive inverse
• Reachability of zero and non-zero results

All properties are proven for all 65,536 possible 8-bit input pairs — not sampled, but exhaustively verified.

When to Use Kleis for Hardware

Business Process Modeling

Model and verify business workflows with formal guarantees:

// Order-to-Cash (O2C) Business Process
// Models the complete lifecycle from order to payment

// Order lifecycle states
data OrderStatus = 
    Draft | Pending | CreditApproved | CreditDenied 
  | Allocated | Fulfilled | Shipped | Invoiced 
  | Paid | Complete | Cancelled

// Credit check decision based on utilization
define credit_check_decision(utilization) =
    if utilization <= 100 then 1      // Approved
    else if utilization < 125 then 2  // PendingReview
    else 0                            // Denied

// Can order be cancelled from current state?
define can_cancel(status) = match status {
    Draft => 1
  | Pending => 1
  | CreditApproved => 1
  | Allocated => 1
  | _ => 0  // Can't cancel after fulfillment
}

// INVARIANT: No shipment without credit approval
define shipment_requires_credit(order_status, credit_approved) =
    if order_status = 6 then credit_approved = 1 else true

// INVARIANT: Order completion requires full payment
define completion_requires_payment(order_status, payment_status) =
    if order_status = 9 then payment_status >= 2 else true

Network Protocol Verification

Verify protocol correctness with formal methods:

// Stop-and-Wait Protocol - Reliable Data Transfer

// Sequence numbers alternate between 0 and 1
define next_seq(seq) = if seq = 0 then 1 else 0

// ACK is valid if it matches sent sequence
define valid_ack(sent, ack) = if ack = sent then 1 else 0

// Sender advances state only on valid ACK
define sender_next_state(current_seq, ack_received) = 
    if valid_ack(current_seq, ack_received) = 1 
    then next_seq(current_seq) 
    else current_seq

// VERIFIED: Double alternation returns to original
// next_seq(next_seq(0)) = 0  ✓
// next_seq(next_seq(1)) = 1  ✓

// SAFETY: No duplicate delivery when synchronized
// LIVENESS: Progress guaranteed when channel delivers

IPv4 Packet Validation

// IPv4 Header Validation (RFC 791)

// Version must be 4 for IPv4
define valid_version(v) = if v = 4 then 1 else 0

// IHL (Internet Header Length): 5-15 words
define valid_ihl(ihl) = ihl >= 5 and ihl <= 15

// Header length in bytes
define header_length(ihl) = ihl * 4

// Common protocols: 1=ICMP, 6=TCP, 17=UDP
define is_tcp(proto) = proto = 6
define is_udp(proto) = proto = 17

// Private address ranges
define is_private_class_a(o1) = o1 = 10
define is_private_class_c(o1, o2) = o1 = 192 and o2 = 168

// Full packet validation
define valid_packet(version, ihl, total, ttl, proto) = 
    valid_version(version) = 1 and
    valid_ihl(ihl) = 1 and
    ttl > 0 and
    total >= header_length(ihl)

Authorization & Access Control

Model Zanzibar-style relationship-based access control (like Google Drive):

// Permission Levels: 0=None, 1=Viewer, 2=Commenter, 3=Editor, 4=Owner

define has_at_least(user_perm, required_perm) = user_perm >= required_perm

define can_read(perm) = has_at_least(perm, 1)
define can_edit(perm) = has_at_least(perm, 3)
define can_delete(perm) = has_at_least(perm, 4)

// Folder inheritance (like Google Drive)
define inherited_permission(child_perm, parent_perm) = 
    if child_perm > 0 
    then child_perm      // Explicit permission overrides
    else parent_perm     // Inherit from parent

// Multi-group permission: take highest
define effective_permission(direct, group) = 
    if direct >= group then direct else group

// Security invariant: can_edit implies can_read
// ∀ p . can_edit(p) = 1 → can_read(p) = 1

Security Analysis

Use Z3 string theory for static security analysis:

// SQL Injection Detection using String Operations

// Vulnerable pattern: string concatenation + SQL execution
// :verify and(
//   contains("SELECT * FROM users WHERE id=" + userId, "+ userId"),
//   contains(code, "executeQuery")
// )
// If Valid → VULNERABLE!

// Safe pattern: parameterized queries
// :verify and(
//   contains(code, "PreparedStatement"),
//   not(contains(code, "+ userId +"))
// )
// If Valid → SAFE

// XSS Detection: innerHTML with user input
// :verify and(
//   contains(code, "innerHTML"),
//   contains(code, "userData")
// )

Control Systems Engineering

Design optimal controllers with verified stability:

// LQG Controller: Linear Quadratic Gaussian

structure LinearSystem(n: Nat, m: Nat, p: Nat) {
    element A : Matrix(n, n, ℝ)   // State dynamics
    element B : Matrix(n, m, ℝ)   // Input matrix
    element C : Matrix(p, n, ℝ)   // Output matrix
    element W : Matrix(n, n, ℝ)   // Process noise covariance
    element V : Matrix(p, p, ℝ)   // Measurement noise covariance
}

// LQR: Optimal state feedback
operation lqr_gain : LQRProblem(n, m) → Matrix(m, n, ℝ)

axiom lqr_stability:
    ∀ prob : LQRProblem(n, m) .
    let K = lqr_gain(prob) in
    let A_cl = prob.A - prob.B · K in
    is_stable(A_cl)

// Kalman Filter: Optimal state estimation
operation kalman_gain : KalmanProblem(n, p) → Matrix(n, p, ℝ)

// LQG combines LQR + Kalman via Separation Principle
structure LQGController(n: Nat, m: Nat, p: Nat) {
    element K : Matrix(m, n, ℝ)   // LQR gain
    element L : Matrix(n, p, ℝ)   // Kalman gain
}

Dimensional Analysis (Physical Units)

Prevent unit mismatch bugs at compile time - like the Mars Climate Orbiter disaster ($327M lost due to imperial/metric confusion):

// Physical dimensions as exponent tuples [Length, Mass, Time]
structure Dimension(L : ℤ, M : ℤ, T : ℤ) {
    axiom equal : ∀(d1 d2 : Dimension). 
        d1 = d2 ↔ (L(d1) = L(d2) ∧ M(d1) = M(d2) ∧ T(d1) = T(d2))
}

// Named dimensions
define Length = Dimension(1, 0, 0)
define Mass = Dimension(0, 1, 0)
define Time = Dimension(0, 0, 1)
define Velocity = Dimension(1, 0, -1)      // L·T⁻¹
define Force = Dimension(1, 1, -2)         // M·L·T⁻²
define Energy = Dimension(2, 1, -2)        // M·L²·T⁻²

// Physical quantity = value + dimension
structure Quantity(value : ℝ, dim : Dimension) {
    // Addition: dimensions must match
    axiom add_same_dim : ∀(q1 q2 : Quantity)(d : Dimension).
        dim(q1) = d ∧ dim(q2) = d → dim(q1 + q2) = d
    
    // Multiplication: dimensions compose
    axiom mul_composes : ∀(q1 q2 : Quantity).
        dim(q1 * q2) = Dimension(
            L(dim(q1)) + L(dim(q2)), 
            M(dim(q1)) + M(dim(q2)), 
            T(dim(q1)) + T(dim(q2)))
}

// Unit constructors
define meter(x : ℝ) = Quantity(x, Length)
define kilogram(x : ℝ) = Quantity(x, Mass)
define second(x : ℝ) = Quantity(x, Time)
define newton(x : ℝ) = Quantity(x, Force)

// Physics axioms verify dimensional consistency
structure Mechanics {
    // F = ma: [M·L·T⁻²] = [M] × [L·T⁻²] ✓
    axiom newton_second_law : ∀(m : Quantity)(a : Quantity).
        dim(m) = Mass ∧ dim(a) = Dimension(1, 0, -2) →
        dim(m * a) = Force
    
    // E = ½mv²: [M·L²·T⁻²] = [M] × [L·T⁻¹]² ✓
    axiom kinetic_energy : ∀(m : Quantity)(v : Quantity).
        dim(m) = Mass ∧ dim(v) = Velocity →
        dim(m * v * v) = Energy
}

Type-safe physics:

• meter(100) + meter(50) → Quantity(150, Length) ✓
• meter(100) / second(10) → Quantity(10, Velocity) ✓
• meter(100) + second(10) → ❌ Type error: Length ≠ Time

See examples/physics/dimensional_analysis.kleis for the full example.

Differential Geometry

Kleis excels at differential geometry calculations:

// Christoffel symbols for spherical coordinates
structure SphericalMetric {
    operation metric : (ℝ, ℝ) → Matrix(2, 2, ℝ)
    operation christoffel : (ℝ, ℝ) → Tensor(1, 2)
}

implements SphericalMetric {
    // Metric tensor: ds² = r²(dθ² + sin²θ dφ²)
    operation metric(r, θ) = Matrix [
        [r^2, 0],
        [0, r^2 * sin(θ)^2]
    ]
    
    // Christoffel symbols Γⁱⱼₖ
    operation christoffel(r, θ) = 
        let g = metric(r, θ) in
        let g_inv = inverse(g) in
        // ... compute from metric derivatives
}

Tensor Calculus

// Einstein field equations
structure EinsteinEquations {
    // Ricci tensor
    operation ricci : Manifold → Tensor(0, 2)
    // Scalar curvature
    operation scalar : Manifold → ℝ
    // Einstein tensor
    operation einstein : Manifold → Tensor(0, 2)
    
    axiom einstein_tensor : ∀(M : Manifold).
        einstein(M) = ricci(M) - (scalar(M) / 2) * metric(M)
}

Symbolic Differentiation

Kleis supports differentiation in two fundamentally different ways:

Computational Differentiation: diff

The diff function computes derivatives by pattern matching on expression trees. It’s implemented in pure Kleis and returns a new expression:

data Expression = 
    ENumber(value : ℝ)
  | EVariable(name : String)
  | EOperation(name : String, args : List(Expression))

// Helper constructors
define num(n) = ENumber(n)
define var(x) = EVariable(x)
define e_add(a, b) = EOperation("plus", Cons(a, Cons(b, Nil)))
define e_mul(a, b) = EOperation("times", Cons(a, Cons(b, Nil)))
define e_pow(a, b) = EOperation("power", Cons(a, Cons(b, Nil)))

define diff(e, var_name) =
    match e {
        ENumber(_) => num(0)
        EVariable(name) => if str_eq(name, var_name) then num(1) else num(0)
        EOperation(op_name, args) => diff_op(op_name, args, var_name)
    }

define diff_op(op_name, args, var_name) = match op_name {
    "plus" => match args {
        Cons(f, Cons(g, Nil)) => e_add(diff(f, var_name), diff(g, var_name))
        | _ => num(0)
    }
    "times" => match args {
        Cons(f, Cons(g, Nil)) => 
            e_add(e_mul(diff(f, var_name), g), e_mul(f, diff(g, var_name)))
        | _ => num(0)
    }
    "power" => match args {
        Cons(f, Cons(ENumber(n), Nil)) => 
            e_mul(e_mul(num(n), e_pow(f, num(n - 1))), diff(f, var_name))
        | _ => num(0)
    }
    "sin" => match args {
        Cons(f, Nil) => e_mul(e_cos(f), diff(f, var_name))
        | _ => num(0)
    }
    "cos" => match args {
        Cons(f, Nil) => e_neg(e_mul(e_sin(f), diff(f, var_name)))
        | _ => num(0)
    }
    _ => num(0)
}

Usage: Call diff(e_mul(var("x"), var("x")), "x") and get back an expression representing 2x.

Axiomatic Differentiation: D and Dt

The D and Dt operations are declared in stdlib/calculus.kleis with axioms that describe derivative properties. They don’t compute anything — Z3 uses these axioms to verify that equations involving derivatives are consistent:

// From stdlib/calculus.kleis
structure Differentiable(F) {
    operation D : F → Variable → F      // Partial derivative
    operation Dt : F → Variable → F     // Total derivative
    
    axiom D_product: ∀(f g : F, x : Variable). 
        D(f * g, x) = D(f, x) * g + f * D(g, x)
    
    axiom Dt_chain: ∀(f : F, x y : Variable). 
        Dt(f, x) = D(f, x) + D(f, y) * Dt(y, x)
}

Usage: Write D(f * g, x) = D(f, x) * g + f * D(g, x) and Z3 confirms it’s valid (it matches the D_product axiom).

When to Use Each

Analogy:

• diff is like a calculator — it gives you answers
• D axioms are like mathematical theorems — Z3 uses them to check proofs

See examples/calculus/derivatives.kleis for more examples of both approaches.

Linear Algebra

structure LinearSystem(n : ℕ) {
    operation solve : Matrix(n, n, ℝ) × Vector(n, ℝ) → Vector(n, ℝ)
    
    // Solution satisfies Ax = b
    axiom solution_correct : ∀(A : Matrix(n, n, ℝ))(b : Vector(n, ℝ)).
        det(A) ≠ 0 → mul(A, solve(A, b)) = b
}

// Eigenvalue problem
structure Eigen(n : ℕ) {
    operation eigenvalues : Matrix(n, n, ℂ) → List(ℂ)
    operation eigenvectors : Matrix(n, n, ℂ) → List(Vector(n, ℂ))
    
    axiom eigenpair : ∀(A : Matrix(n, n, ℂ))(i : ℕ).
        let lam = nth(eigenvalues(A), i) in
        let v = nth(eigenvectors(A), i) in
            mul(A, v) = scale(lam, v)
}

Quantum Mechanics

structure QuantumState(n : ℕ) {
    operation amplitudes : Vector(n, ℂ)
    
    // States must be normalized
    axiom normalized : ∀(psi : QuantumState(n)).
        sum(map(λ a . abs(a)^2, amplitudes(psi))) = 1
}

structure Observable(n : ℕ) {
    operation matrix : Matrix(n, n, ℂ)
    
    // Observables are Hermitian
    axiom hermitian : ∀(O : Observable(n)).
        matrix(O) = conjugate_transpose(matrix(O))
}

// Expectation value
define expectation(psi, O) =
    real(inner_product(amplitudes(psi), mul(matrix(O), amplitudes(psi))))

Category Theory

structure Category(Obj, Mor) {
    operation id : Obj → Mor
    operation compose : Mor × Mor → Mor
    operation dom : Mor → Obj
    operation cod : Mor → Obj
    
    axiom identity_left : ∀(f : Mor).
        compose(id(cod(f)), f) = f
        
    axiom identity_right : ∀(f : Mor).
        compose(f, id(dom(f))) = f
        
    axiom associativity : ∀(f : Mor)(g : Mor)(h : Mor).
        compose(compose(h, g), f) = compose(h, compose(g, f))
}

structure Functor(C, D) {
    operation map_obj : C → D
    operation map_mor : C → D
    
    axiom preserves_id : ∀(x : C).
        map_mor(id(x)) = id(map_obj(x))
        
    axiom preserves_compose : ∀(f : C)(g : C).
        map_mor(compose(g, f)) = compose(map_mor(g), map_mor(f))
}

Physics: Classical Mechanics

structure LagrangianMechanics(n : ℕ) {
    // Generalized coordinates and velocities
    operation q : ℕ → ℝ     // Position
    operation q_dot : ℕ → ℝ  // Velocity
    operation t : ℝ          // Time
    
    // Lagrangian L = T - V
    operation lagrangian : ℝ
    
    // Euler-Lagrange equations
    // Using Mathematica-style: Dt for total derivative, D for partial
    axiom euler_lagrange : ∀ i : ℕ . i < n →
        Dt(D(lagrangian, q_dot(i)), t) = D(lagrangian, q(i))
}

Language Implementation

Kleis can serve as a meta-language — a language for implementing other languages. See the complete LISP interpreter in Kleis:

λ> :load examples/meta-programming/lisp_parser.kleis

λ> :eval run("(letrec ((fib (lambda (n) (if (< n 2) n (+ (fib (- n 1)) (fib (- n 2))))))) (fib 10))")
✅ VNum(55)

λ> :eval run("(letrec ((fact (lambda (n) (if (<= n 1) 1 (* n (fact (- n 1))))))) (fact 5))")
✅ VNum(120)

The complete implementation (parser + evaluator) is ~560 lines of pure Kleis code.

→ Appendix: LISP Interpreter — Full source code with explanation

What’s Next?

Check out the reference appendices!

→ Appendix A: Grammar Reference → Appendix B: Operators → Appendix C: Standard Library → Appendix D: LISP Interpreter

Example Blocks (v0.93)

Kleis v0.93 introduces example blocks — executable documentation that serves as tests, debugging entry points, and living examples.

Syntax

example "descriptive name" {
    let x = 5
    let y = double(x)
    assert(y = 10)
}

An example block contains:

• Let bindings — bind values to names
• Assert statements — verify expected results
• Expressions — any valid Kleis expression

Why Example Blocks?

Example blocks serve three purposes:

1. Documentation — Show how to use your functions
2. Testing — Verify behavior with assertions
3. Debugging — Set breakpoints and step through

Running Examples

Use the kleis test command:

$ kleis test examples/math/complex_demo.kleis

✅ complex arithmetic basics
✅ euler's formula
✅ quadratic roots

3/3 examples passed

Failed assertions show details:

$ kleis test broken.kleis

❌ my test
   Assertion failed: expected Const("20"), got Const("15")

0/1 examples passed (1 failed)

Assert Statement

The assert statement verifies a condition. Kleis distinguishes between two types:

Concrete Assertions (Computation)

When both sides of an assertion can be fully evaluated to values, Kleis computes them directly:

example "concrete assertions" {
    // Arithmetic
    assert(1 + 2 = 3)
    
    // Transcendental functions
    assert(sin(0) = 0)
    assert(cos(0) = 1)
    assert(exp(0) = 1)
    assert(log(1) = 0)
    
    // Variables with bound values
    let x = 5
    assert(x + x = 10)
    assert(pow(x, 2) = 25)
}

Kleis uses eval_concrete() to fully evaluate both sides (including functions like sin, cos, exp, etc.), then compares. Floating-point comparisons use a relative tolerance of 1e-10.

When an assertion contains free (unbound) variables, it becomes a theorem proof using Z3:

structure CommutativeRing(R) {
    operation (+) : R × R → R
    axiom commutativity: ∀(a b : R). a + b = b + a
}

example "algebraic properties" {
    // Z3 verifies this using the commutativity axiom!
    assert(x + y = y + x)
    
    // Z3 proves associativity if the axiom is defined
    assert((a + b) + c = a + (b + c))
}

When an assertion contains unbound variables (like x, y), Kleis:

1. Detects the expression is symbolic
2. Loads axioms from defined structures
3. Passes the claim to Z3 for verification
4. Reports: Verified, Disproved (with counterexample), or Unknown

example "z3 finds counterexamples" {
    // Z3 disproves this with: "Counterexample: y!1 -> 1, x!0 -> 0"
    // assert(x + y = y + y)  // Would fail!
}

This enables theorem proving in your tests:

structure Field(F) {
    operation (*) : F × F → F
    operation inverse : F → F
    
    axiom inverse_right: ∀(x : F). x * inverse(x) = 1
    axiom inverse_left: ∀(x : F). inverse(x) * x = 1
}

example "inverse properties" {
    // Z3 verifies using field axioms
    assert(a * inverse(a) = 1)
    assert(inverse(inverse(a)) = a)  // Derived property!
}

How Kleis Chooses: Concrete vs Symbolic

The decision flow:

1. Try eval_concrete() on both sides
2. If both reduce to values → compare (with floating-point tolerance)
3. If either contains free variables → invoke Z3 with loaded axioms
4. Z3 returns: Verified, Disproved (with counterexample), or Unknown

Example Blocks as Entry Points

Example blocks are the entry points for debugging. Unlike function definitions which are just declarations, example blocks contain executable code:

// Function definition (not executable on its own)
define fib(n) = 
    if n <= 1 then n 
    else fib(n - 1) + fib(n - 2)

// Example block (executable, can set breakpoints)
example "fibonacci test" {
    let f5 = fib(5)      // ← Set breakpoint here
    let f10 = fib(10)    // ← Or here
    assert(f5 = 5)
    assert(f10 = 55)
}

When debugging:

1. Set a breakpoint on a line in an example block
2. Launch the debugger
3. Execution stops at your breakpoint
4. Step through, inspect variables, step into functions

Cross-File Debugging

Example blocks work with imports. When you step into a function from an imported file, the debugger opens that file:

// main.kleis
import "stdlib/complex.kleis"

example "complex math" {
    let z = complex(3, 4)
    let mag = abs(z)        // ← Step into this
    assert(mag = 5)         // Opens complex.kleis, shows abs definition
}

The debugger tracks source locations across files, showing you exactly where you are.

Source Location Tracking

Every expression in Kleis carries its source location (line, column, file). This enables:

• Accurate error messages
• Precise debugger breakpoints
• Cross-file stepping
• Stack traces with file paths

The location travels with the expression through evaluation, so even after function application, the debugger knows the original source.

Best Practices

1. One Concept Per Example

// Good: focused examples
example "addition is commutative" {
    assert(2 + 3 = 3 + 2)
}

example "multiplication distributes" {
    assert(2 * (3 + 4) = 2 * 3 + 2 * 4)
}

// Bad: too much in one example
example "all arithmetic" {
    assert(2 + 3 = 3 + 2)
    assert(2 * 3 = 3 * 2)
    assert(2 * (3 + 4) = 2 * 3 + 2 * 4)
    // ... many more assertions
}

2. Descriptive Names

// Good: describes what's being tested
example "negative numbers square to positive" { ... }

// Bad: vague
example "test1" { ... }

3. Use Let Bindings for Clarity

// Good: intermediate values have names
example "quadratic formula" {
    let a = 1
    let b = -5
    let c = 6
    let discriminant = b * b - 4 * a * c
    let root1 = (-b + sqrt(discriminant)) / (2 * a)
    assert(root1 = 3)
}

// Bad: one big expression
example "quadratic formula" {
    assert((-(-5) + sqrt((-5) * (-5) - 4 * 1 * 6)) / (2 * 1) = 3)
}

Grammar Reference

exampleBlock    ::= "example" string "{" exampleBody "}"
exampleBody     ::= { exampleStatement }
exampleStatement ::= letBinding 
                   | assertStatement 
                   | expression ";"

assertStatement ::= "assert" "(" expression ")"

letBinding      ::= "let" identifier [":" type] "=" expression

What’s Next?

Explore the functions and structures available in the standard library:

→ Standard Library

Learn how to set up VS Code for debugging:

→ Appendix: VS Code Debugging

Standard Library Types

Self-Hosting: Kleis Defines Kleis

One of Kleis’s most elegant features is meta-circularity: the type system is defined in Kleis itself.

// From stdlib/types.kleis - loaded before anything else
data Type =
    Scalar
    | Vector(n: Nat, T)
    | Matrix(m: Nat, n: Nat, T)
    | Complex
    | Set(T: Type)
    | List(T: Type)
    | Tensor(dims: List(Nat))

This means:

• Types aren’t hardcoded in the Rust compiler
• Users can extend the type system without recompiling
• The type checker can reason about types as data

Core Types

Bool

The fundamental boolean type:

data Bool = True | False

Operations:

define not(b) = match b {
    True => False
    | False => True
}

define and(b1, b2) = match b1 {
    False => False
    | True => b2
}

define or(b1, b2) = match b1 {
    True => True
    | False => b2
}

Option(T)

For values that might not exist (like Haskell’s Maybe):

data Option(T) =
    None
    | Some(value: T)

Operations:

define isSome(opt) = match opt {
    None => False
    | Some(_) => True
}

define isNone(opt) = match opt {
    None => True
    | Some(_) => False
}

define getOrDefault(opt, default) = match opt {
    None => default
    | Some(x) => x
}

Usage:

// Safe division that doesn't crash on zero
define safeDivide(a, b) =
    if b = 0 then None
    else Some(a / b)

// Use with pattern matching
define showResult(result) =
    match result {
        None => "undefined"
        Some(x) => x
    }

Result(T, E)

For operations that can succeed or fail with an error (like Rust’s Result):

data Result(T, E) =
    Ok(value: T)
    | Err(error: E)

Usage:

define parseNumber(s) =
    if isNumeric(s) then Ok(toNumber(s))
    else Err("not a number")

define processInput(input) =
    match parseNumber(input) {
        Ok(n) => n * 2
        Err(msg) => 0
    }

List(T)

Recursive linked list:

data List(T) =
    Nil
    | Cons(head: T, tail: List(T))

Operations:

define isEmpty(list) = match list {
    Nil => True
    | Cons(_, _) => False
}

define head(list) = match list {
    Nil => None
    | Cons(h, _) => Some(h)
}

define tail(list) = match list {
    Nil => None
    | Cons(_, t) => Some(t)
}

Note: For numeric computation, use the [1, 2, 3] list literal syntax with built-in functions like list_map, list_filter, etc. The Cons/Nil form is for symbolic reasoning and pattern matching.

Unit

The type with only one value (like void in C, but safer):

data Unit = Unit

Usage:

// A function that returns nothing meaningful
define printAndReturn(x) = Unit

// Flags without associated data
define flagSet : Option(Unit) = Some(Unit)
define flagUnset : Option(Unit) = None

Ordering

For comparison results:

data Ordering = LT | EQ | GT

Usage:

define compareNumbers(a, b) =
    if a < b then LT
    else if a > b then GT
    else EQ

Numeric Types

Scalar

The base numeric type (real numbers ℝ):

// Part of the Type data type
Scalar

Complex

Complex numbers with real and imaginary parts:

// Part of the Type data type  
Complex

See Chapter 14: Complex Numbers for operations.

Vector(n, T)

Fixed-length vectors:

Vector(n: Nat, T)

Example: Vector(3, ℝ) is a 3D real vector.

Matrix(m, n, T)

Matrices with row and column dimensions:

Matrix(m: Nat, n: Nat, T)

Example: Matrix(2, 3, ℝ) is a 2×3 real matrix.

Delimiter Variants:

Matrix(m, n, T)   // [a b; c d] - square brackets
PMatrix(m, n, T)  // (a b; c d) - parentheses
VMatrix(m, n, T)  // |a b; c d| - vertical bars (determinants)
BMatrix(m, n, T)  // {a b; c d} - braces

See Chapter 19: Matrices for operations.

Tensor Types (xAct-style)

Kleis includes types for differential geometry with xAct-style tensor notation.

IndexVariance

Whether an index is upper (contravariant) or lower (covariant):

data IndexVariance = Contravariant | Covariant

TensorIdx

A single tensor index:

data TensorIdx = TIdx(name: String, variance: IndexVariance)

Example: TIdx("μ", Contravariant) represents the upper index μ.

TensorRank

Tensor rank as (contravariant, covariant) pair:

data TensorRank = Rank(upper: Nat, lower: Nat)

Example: Rank(1, 2) for a (1,2)-tensor like Γ^μ_{νρ}.

TensorType

Full tensor type with explicit index structure:

data TensorType = TensorT(name: String, indices: List(TensorIdx))

Usage in physics:

// Christoffel symbol Γ^λ_μν
let christoffel = TensorT("Gamma", [
    TIdx("lambda", Contravariant),
    TIdx("mu", Covariant),
    TIdx("nu", Covariant)
])

// Riemann tensor R^ρ_σμν
let riemann = TensorT("R", [
    TIdx("rho", Contravariant),
    TIdx("sigma", Covariant),
    TIdx("mu", Covariant),
    TIdx("nu", Covariant)
])

The Prelude: Core Structures

After types load, minimal_prelude.kleis defines the fundamental structures that make operations work.

Arithmetic(T)

Basic math operations for any type:

structure Arithmetic(T) {
    operation plus : T → T → T
    operation minus : T → T → T
    operation times : T → T → T
    operation divide : T → T → T
    operation frac : T → T → T
}

// Implementation for real numbers
implements Arithmetic(ℝ) {
    operation plus = builtin_add
    operation minus = builtin_sub
    operation times = builtin_mul
    operation divide = builtin_div
    operation frac = builtin_div
}

Equatable(T)

Equality comparison:

structure Equatable(T) {
    operation equals : T → T → Bool
    operation not_equals : T → T → Bool
}

implements Equatable(ℝ) {
    operation equals = builtin_eq
    operation not_equals = builtin_neq
}

// Matrices have component-wise equality
implements Equatable(Matrix(m, n, ℝ)) {
    operation equals = builtin_matrix_eq
    operation not_equals = builtin_matrix_neq
}

Ordered(T)

Comparison operations (only for types with natural ordering):

structure Ordered(T) {
    operation less_than : T → T → Bool
    operation greater_than : T → T → Bool
    operation less_equal : T → T → Bool
    operation greater_equal : T → T → Bool
}

// Only scalars are ordered - matrices are NOT!
implements Ordered(ℝ) {
    operation less_than = builtin_lt
    operation greater_than = builtin_gt
    operation less_equal = builtin_le
    operation greater_equal = builtin_ge
}

Note: Matrices don’t implement Ordered because matrix comparison isn’t well-defined (is [[1,2],[3,4]] < [[5,6],[7,8]]?).

Numeric(N)

Advanced numeric operations:

structure Numeric(N) {
    operation abs : N → N
    operation floor : N → N
    operation sqrt : N → N
    operation power : N → N → N
}

implements Numeric(ℝ) {
    operation abs = builtin_abs
    operation floor = builtin_floor
    operation sqrt = builtin_sqrt
    operation power = builtin_pow
}

Calculus Structures

For symbolic differentiation and integration:

structure Differentiable(F) {
    operation derivative : F → F
    operation partial : F → F
}

structure Integrable(F) {
    operation integral : F → ℝ
    operation int_bounds : F → ℝ → ℝ → F → ℝ
}

Other Standard Library Files

The stdlib contains domain-specific modules:

Import what you need:

import "stdlib/complex.kleis"
import "stdlib/tensors.kleis"

Loading Order

The standard library loads in a specific order:

1. types.kleis - Core type definitions (Bool, Option, etc.)
2. minimal_prelude.kleis - Core structures (Arithmetic, Equatable, etc.)
3. Domain modules - As imported by user

This ensures types are defined before they’re used in structures.

Extending the Type System

Because types are defined in Kleis, you can add your own:

// Physics domain
data Particle = Electron | Proton | Neutron | Photon
data Spin = SpinUp | SpinDown

// Chemistry domain  
data Element = H | He | Li | Be | B | C | N | O

// Business domain
data Currency = USD | EUR | GBP | JPY

Your custom types work with pattern matching, axioms, and Z3 verification just like built-in types.

What’s Next?

Explore specific type domains in depth:

→ Complex Numbers
→ Matrices
→ Set Theory

Complex Numbers

Kleis has first-class support for complex numbers (ℂ), enabling symbolic reasoning about complex arithmetic, verification of identities, and theorem proving in complex analysis.

Natural Arithmetic Syntax ✨ NEW

Kleis now supports natural arithmetic operators for complex numbers!

You can write expressions using +, -, *, / with complex numbers, just like you would with real numbers:

// Natural syntax (NEW!)
:verify complex(1, 2) + complex(3, 4) = complex(4, 6)
// ✅ Valid

:verify complex(1, 2) * complex(3, 4) = complex(-5, 10)
// ✅ Valid

// The classic: 3 + 4i
:verify 3 + 4*i = complex(3, 4)
// ✅ Valid

// Mixed real and complex
:verify 5 + complex(1, 2) = complex(6, 2)
// ✅ Valid

Kleis automatically converts these to the appropriate complex operations via semantic lowering:

This works transparently in the REPL and for verification.

Concrete Evaluation with :eval

For direct computation with complex numbers, use the :eval command:

:eval complex_add(complex(1, 2), complex(3, 4))
// → complex(4, 6)

:eval complex_sub(complex(10, 20), complex(3, 4))
// → complex(7, 16)

:eval complex_mul(complex(1, 2), complex(3, 4))
// → complex(-5, 10)

:eval complex_conj(complex(3, 4))
// → complex(3, -4)

:eval complex_abs_squared(complex(3, 4))
// → 25  (|3+4i|² = 9 + 16 = 25)

Extracting Parts

:eval real(complex(5, 7))
// → 5

:eval imag(complex(5, 7))
// → 7

Mixed Symbolic/Concrete

:eval supports partial symbolic evaluation:

:eval complex_add(complex(a, 2), complex(3, 4))
// → complex(a + 3, 6)

:eval complex_mul(complex(a, 0), complex(0, b))
// → complex(0, a * b)

The Imaginary Unit

The imaginary unit i is predefined in Kleis:

// i is the square root of -1
define i_squared = i * i
// Result: complex(-1, 0)  — that's -1!

In the REPL, you can verify this fundamental property:

:verify i * i = complex(-1, 0)
// ✅ Valid

// Or using the explicit function:
:verify complex_mul(i, i) = complex(-1, 0)
// ✅ Valid

Scoping Rules for i

The imaginary unit i is a global constant. However, it can be shadowed by:

1. Quantified variables with explicit type annotations
2. Lambda parameters

Scoping examples:

// Quantified variable i : ℝ shadows the global imaginary unit
// Here i is a real number, so i + 1 uses regular addition
verify ∀(i : ℝ). i + 1 = 1 + i

// Quantified variable i : ℕ is a natural number
verify ∀(i : ℕ). i + 0 = i

// Quantified variable i : ℂ is explicitly complex
verify ∀(i : ℂ). complex_add(i, complex(0, 0)) = i

In the REPL, you can also check types:

λ> :type i
📐 Type: Complex

λ> :type i + 1  
📐 Type: Complex

λ> :type λ x . x + i
📐 Type: Complex

λ> :type λ i . i + 1
📐 Type: Scalar

Note: λ x . x + i uses global i, while λ i . i + 1 has parameter i shadowing global.

Best practice: Avoid using i as a variable name to prevent confusion with the imaginary unit. Use descriptive names like idx, index, or iter for loop-like variables.

// Clear: using i as imaginary unit
verify ∀(z : ℂ). complex_mul(z, i) = complex(neg(im(z)), re(z))

// Clear: using idx as index variable  
verify ∀(idx : ℕ). idx + 0 = idx

Creating Complex Numbers

Method 1: Using arithmetic (recommended)

define z1 = 3 + 4*i           // 3 + 4i
define z2 = 1 - 2*i           // 1 - 2i
define pure_real = 5 + 0*i    // 5 (a real number)
define pure_imag = 0 + 3*i    // 3i (pure imaginary)

Method 2: Using the complex(re, im) constructor

// complex(real_part, imaginary_part)
define z1 = complex(3, 4)       // 3 + 4i
define z2 = complex(1, -2)      // 1 - 2i
define pure_real = complex(5, 0)     // 5 (a real number)
define pure_imag = complex(0, 3)     // 3i (pure imaginary)

Extracting Parts

Use re and im to extract the real and imaginary parts:

define z = complex(3, 4)

// Extract real part
define real_part = re(z)        // 3

// Extract imaginary part  
define imag_part = im(z)        // 4

Verification examples:

:verify re(complex(7, 8)) = 7
// ✅ Valid

:verify im(complex(7, 8)) = 8
// ✅ Valid

:verify ∀(a : ℝ)(b : ℝ). re(complex(a, b)) = a
// ✅ Valid

Type Ascriptions with ℂ

Type ascriptions tell Kleis (and Z3) that a variable is a complex number. The syntax is : ℂ (or : Complex).

Quantifier Variables

The most common use is in universal quantifiers:

// z is a complex variable
:verify ∀(z : ℂ). conj(conj(z)) = z
// ✅ Valid

// Multiple complex variables
:verify ∀(z1 : ℂ)(z2 : ℂ). z1 + z2 = z2 + z1
// ✅ Valid

// Mixed types: real and complex
:verify ∀(r : ℝ)(z : ℂ). r + z = complex(r + re(z), im(z))
// ✅ Valid

When you write ∀(z : ℂ), the Z3 backend creates a symbolic complex variable with unknown real and imaginary parts. This lets Z3 reason about all possible complex numbers.

Definition Annotations

You can annotate definitions for clarity:

define z1 : ℂ = complex(1, 2)
define z2 : ℂ = 3 + 4*i
define origin : ℂ = complex(0, 0)

Why Type Ascriptions Matter

Without type information, Z3 wouldn’t know how to handle operations:

// With `: ℂ`, Z3 knows z is complex and creates appropriate constraints
:verify ∀(z : ℂ). z * complex(1, 0) = z
// ✅ Valid

// Z3 can reason symbolically about the real and imaginary parts
:verify ∀(z : ℂ). re(z) * re(z) + im(z) * im(z) = abs_squared(z)
// ✅ Valid

Equivalent Type Names

For complex numbers, these are all equivalent:

For comparison, here are the equivalent forms for other numeric types:

Arithmetic Operations

Addition and Subtraction

define z1 = 1 + 2*i    // 1 + 2i
define z2 = 3 + 4*i    // 3 + 4i

// Addition: (1 + 2i) + (3 + 4i) = 4 + 6i
define sum = z1 + z2

// Subtraction: (1 + 2i) - (3 + 4i) = -2 - 2i
define diff = z1 - z2

Verify concrete arithmetic:

// Natural syntax
:verify (1 + 2*i) + (3 + 4*i) = 4 + 6*i
// ✅ Valid

:verify (5 + 3*i) - (2 + 1*i) = 3 + 2*i
// ✅ Valid

// Explicit function syntax (also works)
:verify complex_add(complex(1, 2), complex(3, 4)) = complex(4, 6)
// ✅ Valid

Multiplication

Complex multiplication follows the rule: (a + bi)(c + di) = (ac - bd) + (ad + bc)i

define z1 = 1 + 2*i    // 1 + 2i
define z2 = 3 + 4*i    // 3 + 4i

// (1 + 2i)(3 + 4i) = 3 + 4i + 6i + 8i² = 3 + 10i - 8 = -5 + 10i
define product = z1 * z2

Verification:

// Natural syntax
:verify (1 + 2*i) * (3 + 4*i) = complex(-5, 10)
// ✅ Valid

// The fundamental property: i² = -1
:verify i * i = complex(-1, 0)
// ✅ Valid

// Multiplication by i rotates 90°
:verify ∀(z : ℂ). z * i = complex(neg(im(z)), re(z))
// ✅ Valid (where neg is negation)

Division

define z1 = 1 + 0*i    // 1
define z2 = 0 + 1*i    // i

// 1 / i = -i
define quotient = z1 / z2

Verification:

// Natural syntax
:verify (1 + 0*i) / (0 + 1*i) = 0 - 1*i
// ✅ Valid

// Explicit function syntax
:verify complex_div(complex(1, 0), complex(0, 1)) = complex(0, -1)
// ✅ Valid

Negation

define z = complex(3, 4)
define neg_z = neg_complex(z)    // -3 - 4i

:verify neg_complex(complex(3, 4)) = complex(-3, -4)
// ✅ Valid

:verify ∀(z : ℂ). complex_add(z, neg_complex(z)) = complex(0, 0)
// ✅ Valid

Inverse

define z = complex(0, 1)         // i
define inv = complex_inverse(z)   // 1/i = -i

:verify complex_inverse(complex(0, 1)) = complex(0, -1)
// ✅ Valid

// z * (1/z) = 1 (for non-zero z)
:verify ∀(z : ℂ). z ≠ complex(0, 0) ⟹ complex_mul(z, complex_inverse(z)) = complex(1, 0)
// ✅ Valid

Complex Conjugate

The conjugate of a + bi is a - bi:

define z = complex(3, 4)
define z_bar = conj(z)    // 3 - 4i

Verification:

:verify conj(complex(2, 3)) = complex(2, -3)
// ✅ Valid

// Double conjugate is identity
:verify ∀(z : ℂ). conj(conj(z)) = z
// ✅ Valid

// Conjugate of product
:verify ∀(z1 : ℂ)(z2 : ℂ). conj(complex_mul(z1, z2)) = complex_mul(conj(z1), conj(z2))
// ✅ Valid

// Conjugate of sum
:verify ∀(z1 : ℂ)(z2 : ℂ). conj(complex_add(z1, z2)) = complex_add(conj(z1), conj(z2))
// ✅ Valid

Magnitude Squared

The squared magnitude |z|² = re(z)² + im(z)²:

define z = complex(3, 4)
define mag_sq = abs_squared(z)    // 3² + 4² = 25

:verify abs_squared(complex(3, 4)) = 25
// ✅ Valid

:verify ∀(z : ℂ). abs_squared(z) = re(z) * re(z) + im(z) * im(z)
// ✅ Valid

Note: Full magnitude |z| = √(re² + im²) requires square root, which is not yet supported.

Field Properties

Complex numbers form a field. Kleis can verify all field axioms:

Commutativity

// Addition is commutative
:verify ∀(z1 : ℂ)(z2 : ℂ). complex_add(z1, z2) = complex_add(z2, z1)
// ✅ Valid

// Multiplication is commutative
:verify ∀(z1 : ℂ)(z2 : ℂ). complex_mul(z1, z2) = complex_mul(z2, z1)
// ✅ Valid

Associativity

// Addition is associative
:verify ∀(z1 : ℂ)(z2 : ℂ)(z3 : ℂ). 
    complex_add(complex_add(z1, z2), z3) = complex_add(z1, complex_add(z2, z3))
// ✅ Valid

// Multiplication is associative
:verify ∀(z1 : ℂ)(z2 : ℂ)(z3 : ℂ). 
    complex_mul(complex_mul(z1, z2), z3) = complex_mul(z1, complex_mul(z2, z3))
// ✅ Valid

Identity Elements

// Additive identity: z + 0 = z
:verify ∀(z : ℂ). complex_add(z, complex(0, 0)) = z
// ✅ Valid

// Multiplicative identity: z * 1 = z
:verify ∀(z : ℂ). complex_mul(z, complex(1, 0)) = z
// ✅ Valid

Distributive Law

:verify ∀(z1 : ℂ)(z2 : ℂ)(z3 : ℂ). 
    complex_mul(z1, complex_add(z2, z3)) = 
        complex_add(complex_mul(z1, z2), complex_mul(z1, z3))
// ✅ Valid

Embedding Real Numbers

Real numbers embed into complex numbers with imaginary part 0:

define r = 5
define z = complex(r, 0)    // 5 + 0i = 5

// Extracting real from embedded real
:verify ∀(a : ℝ). re(complex(a, 0)) = a
// ✅ Valid

:verify ∀(a : ℝ). im(complex(a, 0)) = 0
// ✅ Valid

Adding real and imaginary parts:

:verify ∀(x : ℝ)(y : ℝ). complex_add(complex(x, 0), complex(0, y)) = complex(x, y)
// ✅ Valid

The Multiplication Formula

The explicit formula for complex multiplication:

// (a + bi)(c + di) = (ac - bd) + (ad + bc)i
:verify ∀(a : ℝ)(b : ℝ)(c : ℝ)(d : ℝ). 
    complex_mul(complex(a, b), complex(c, d)) = complex(a*c - b*d, a*d + b*c)
// ✅ Valid

Mixing Symbolic and Concrete

Kleis can reason about mixed expressions:

// Symbolic z plus concrete value
:verify ∀(z : ℂ). complex_add(z, complex(0, 0)) = z
// ✅ Valid

// Symbolic z times concrete i
:verify ∀(z : ℂ). complex_mul(z, i) = complex_add(z, complex(0, 1))
// This checks if multiplying by i equals adding i (it doesn't!)
// ❌ Invalid — as expected!

// Correct: multiplying by i rotates
:verify ∀(a : ℝ)(b : ℝ). complex_mul(complex(a, b), i) = complex(-b, a)
// ✅ Valid (rotation by 90°)

The Fundamental Theorem

The defining property of complex numbers:

// i² = -1
:verify complex_mul(i, i) = complex(-1, 0)
// ✅ Valid

// More explicitly
:verify complex_mul(complex(0, 1), complex(0, 1)) = complex(-1, 0)
// ✅ Valid

Convention: Loop Indices

When using Sum or Product with complex numbers, avoid using i as a loop index:

// GOOD: use k, j, n, m as loop indices
Sum(k, complex_mul(complex(1, 0), pow(z, k)), 0, n)

// BAD: i as loop index clashes with imaginary i
Sum(i, complex_mul(i, pow(z, i)), 0, n)   // Which 'i' is which?

The convention is:

• k, j, n, m — loop indices
• i — imaginary unit

Complete Example: Verifying Complex Identities

Here’s a complete session verifying multiple complex number properties:

// Define some complex numbers
define z1 : ℂ = complex(1, 2)
define z2 : ℂ = complex(3, 4)

// Compute operations
define sum = complex_add(z1, z2)
define product = complex_mul(z1, z2)
define i_squared = complex_mul(i, i)

// Structure with axioms
structure ComplexTest {
    axiom i_squared_minus_one : complex_mul(i, i) = complex(-1, 0)
    axiom conj_involution : ∀(z : ℂ). conj(conj(z)) = z
    axiom add_commutes : ∀(a : ℂ)(b : ℂ). complex_add(a, b) = complex_add(b, a)
}

Operation Reference

Current Limitations

What’s Next?

Complex numbers enable reasoning about:

• Signal processing (Fourier transforms)
• Quantum mechanics (wave functions)
• Control theory (transfer functions)
• Complex analysis (contour integrals)

Continue exploring Kleis’s number systems:

→ Rational Numbers

Rational Numbers

Kleis provides complete support for rational numbers (ℚ), the field of fractions p/q where p and q are integers and q ≠ 0. Rational arithmetic in Kleis is exact—no floating-point approximation errors.

The Rational Type

Kleis recognizes three equivalent notations for the rational type:

define half : ℚ = rational(1, 2)
define third : Rational = rational(1, 3)
define quarter : Q = rational(1, 4)

Constructing Rationals

Use the rational(p, q) constructor to create rational numbers:

define one_half : ℚ = rational(1, 2)
define two_thirds : ℚ = rational(2, 3)
define negative : ℚ = rational(-3, 4)

Accessors

Extract the numerator and denominator:

structure RationalAccessors {
    axiom numer_ex : numer(rational(3, 4)) = 3
    axiom denom_ex : denom(rational(3, 4)) = 4
}

Arithmetic Operations

Basic Arithmetic

Kleis supports operator overloading for rationals:

define sum : ℚ = rational(1, 2) + rational(1, 3)
define diff : ℚ = rational(3, 4) - rational(1, 4)
define prod : ℚ = rational(2, 3) * rational(3, 2)
define quot : ℚ = rational(1, 2) / rational(1, 4)

These lower to explicit rational operations:

Reciprocal and Inverse

structure RationalInverse {
    axiom inv_half : rational_inv(rational(1, 2)) = rational(2, 1)
    axiom inv_def : ∀(p q : ℤ). p ≠ 0 ∧ q ≠ 0 → 
        rational_inv(rational(p, q)) = rational(q, p)
}

Derived Operations

Kleis defines several derived operations using conditionals:

Sign, Absolute Value, Min, Max

structure DerivedOps {
    define sign_rational(r : ℚ) : ℤ = 
        if rational_lt(r, rational(0, 1)) then 0 - 1
        else if r = rational(0, 1) then 0
        else 1
    
    define abs_rational(r : ℚ) : ℚ = 
        if rational_lt(r, rational(0, 1)) then neg_rational(r) 
        else r
    
    define min_rational(r1 : ℚ, r2 : ℚ) : ℚ = 
        if rational_le(r1, r2) then r1 else r2
    
    define max_rational(r1 : ℚ, r2 : ℚ) : ℚ = 
        if rational_le(r1, r2) then r2 else r1
    
    define midpoint(r1 : ℚ, r2 : ℚ) : ℚ = 
        rational_div(rational_add(r1, r2), rational(2, 1))
}

Comparison Operations

Rationals are totally ordered:

structure RationalOrder {
    axiom trichotomy : ∀(r1 r2 : ℚ). 
        rational_lt(r1, r2) ∨ r1 = r2 ∨ rational_gt(r1, r2)
    
    axiom transitive : ∀(r1 r2 r3 : ℚ). 
        rational_lt(r1, r2) ∧ rational_lt(r2, r3) → rational_lt(r1, r3)
}

Mixed-Type Comparisons

Kleis supports comparing rationals with other numeric types:

structure MixedComparisons {
    // Compare ℚ with ℕ
    axiom half_less_one : rational(1, 2) < 1
    
    // Compare ℚ with ℤ
    axiom neg_half_less_zero : rational(-1, 2) < 0
}

Type Promotion

When mixing rationals with other numeric types, Kleis promotes according to:

ℕ → ℤ → ℚ → ℝ → ℂ

Examples:

structure TypePromotion {
    // ℚ + ℤ → ℚ (integer lifted to rational)
    axiom int_plus_rat : rational(1, 2) + 1 = rational(3, 2)
    
    // ℚ + ℝ → ℝ (rational becomes real)
    axiom rat_plus_real : rational(1, 2) + 0.5 = 1.0
}

Field Axioms

Rationals form a field—all the familiar algebraic laws hold:

structure RationalField {
    // Addition is commutative and associative
    axiom add_comm : ∀(r1 r2 : ℚ). rational_add(r1, r2) = rational_add(r2, r1)
    axiom add_assoc : ∀(r1 r2 r3 : ℚ). 
        rational_add(rational_add(r1, r2), r3) = rational_add(r1, rational_add(r2, r3))
    
    // Additive identity and inverse
    axiom add_identity : ∀(r : ℚ). rational_add(r, rational(0, 1)) = r
    axiom add_inverse : ∀(r : ℚ). rational_add(r, neg_rational(r)) = rational(0, 1)
    
    // Multiplication is commutative and associative
    axiom mul_comm : ∀(r1 r2 : ℚ). rational_mul(r1, r2) = rational_mul(r2, r1)
    axiom mul_assoc : ∀(r1 r2 r3 : ℚ). 
        rational_mul(rational_mul(r1, r2), r3) = rational_mul(r1, rational_mul(r2, r3))
    
    // Multiplicative identity and inverse
    axiom mul_identity : ∀(r : ℚ). rational_mul(r, rational(1, 1)) = r
    axiom mul_inverse : ∀(r : ℚ). r ≠ rational(0, 1) → 
        rational_mul(r, rational_inv(r)) = rational(1, 1)
    
    // Distributive law
    axiom distributive : ∀(r1 r2 r3 : ℚ). 
        rational_mul(r1, rational_add(r2, r3)) = 
        rational_add(rational_mul(r1, r2), rational_mul(r1, r3))
}

Integer Operations

Floor and Ceiling

Convert rationals to integers:

structure FloorCeil {
    // floor: largest integer ≤ r
    axiom floor_def : ∀(r : ℚ). int_to_rational(floor(r)) ≤ r
    
    // ceil: smallest integer ≥ r
    axiom ceil_def : ∀(r : ℚ). r ≤ int_to_rational(ceil(r))
    
    // Examples
    axiom floor_ex : floor(rational(7, 3)) = 2
    axiom ceil_ex : ceil(rational(7, 3)) = 3
}

Integer Division and Modulo

structure IntDivMod {
    // Division identity: a = (a div b) * b + (a mod b)
    axiom div_mod_id : ∀(a b : ℤ). b ≠ 0 → 
        a = int_div(a, b) * b + int_mod(a, b)
    
    // Modulo is non-negative for positive divisor
    axiom mod_nonneg : ∀(a b : ℤ). b > 0 → 
        int_mod(a, b) ≥ 0 ∧ int_mod(a, b) < b
}

Greatest Common Divisor

GCD is defined axiomatically:

structure GCDAxioms {
    // GCD divides both arguments
    axiom gcd_divides_a : ∀(a b : ℤ). int_mod(a, gcd(a, b)) = 0
    axiom gcd_divides_b : ∀(a b : ℤ). int_mod(b, gcd(a, b)) = 0
    
    // GCD is the greatest such divisor
    axiom gcd_greatest : ∀(a b d : ℤ). 
        (int_mod(a, d) = 0 ∧ int_mod(b, d) = 0) → d ≤ gcd(a, b)
    
    // Euclidean algorithm
    axiom gcd_euclidean : ∀(a b : ℤ). b ≠ 0 → 
        gcd(a, b) = gcd(b, int_mod(a, b))
}

Density Property

Between any two distinct rationals, there’s another:

structure Density {
    axiom density : ∀(r1 r2 : ℚ). 
        rational_lt(r1, r2) → 
        (∃(r : ℚ). rational_lt(r1, r) ∧ rational_lt(r, r2))
    
    // The midpoint is always between
    axiom midpoint_between : ∀(r1 r2 : ℚ). 
        rational_lt(r1, r2) → 
        rational_lt(r1, midpoint(r1, r2)) ∧ rational_lt(midpoint(r1, r2), r2)
}

Z3 Verification

Z3 maps rationals to its Real sort, which provides exact rational arithmetic:

structure Z3Example {
    // This theorem is verified by Z3
    axiom half_plus_half : rational_add(rational(1, 2), rational(1, 2)) = rational(1, 1)
    
    // Field properties are automatically verified
    axiom comm_verified : ∀(a b : ℚ). rational_add(a, b) = rational_add(b, a)
}

Common Fractions

The standard library defines convenient names:

structure CommonFractions {
    axiom half_def : half = rational(1, 2)
    axiom third_def : third = rational(1, 3)
    axiom quarter_def : quarter = rational(1, 4)
    axiom fifth_def : fifth = rational(1, 5)
    axiom tenth_def : tenth = rational(1, 10)
}

Summary

See stdlib/rational.kleis for the complete axiom set.

What’s Next?

Explore fixed-width binary arithmetic for hardware and low-level verification:

→ Bit Vectors

Bit-Vectors

Kleis provides support for bit-vectors—fixed-width sequences of bits. Bit-vectors are essential for hardware verification, cryptography, and low-level systems programming.

Bourbaki Definition

Following Bourbaki’s rigorous style, a bit-vector of width n is defined as:

A bit-vector of width n is a mapping x : [0, n-1] → {0, 1}

Equivalently, it’s a family (xᵢ)_{i∈[0,n-1]} where each xᵢ ∈ {0, 1}.

The BitVec Type

define byte : BitVec(8) = bvzero(8)
define word : BitVec(32) = bvzero(32)
define qword : BitVec(64) = bvzero(64)

Mother Structures

Bit-vectors inherit three fundamental algebraic structures:

1. Vector Space over 𝔽₂

The set BitVec(n) forms a vector space over the two-element field 𝔽₂ = {0, 1}:

structure VectorSpaceF2 {
    // XOR is the addition operation
    axiom add_commutative : ∀(n : ℕ)(x y : BitVec(n)).
        bvxor(x, y) = bvxor(y, x)
    
    axiom add_associative : ∀(n : ℕ)(x y z : BitVec(n)).
        bvxor(bvxor(x, y), z) = bvxor(x, bvxor(y, z))
    
    axiom add_identity : ∀(n : ℕ)(x : BitVec(n)).
        bvxor(x, bvzero(n)) = x
    
    // Every element is its own additive inverse!
    axiom add_inverse : ∀(n : ℕ)(x : BitVec(n)).
        bvxor(x, x) = bvzero(n)
}

2. Boolean Algebra

With AND, OR, and NOT, bit-vectors form a Boolean algebra:

structure BooleanAlgebra {
    // De Morgan's laws
    axiom demorgan_and : ∀(n : ℕ)(x y : BitVec(n)).
        bvnot(bvand(x, y)) = bvor(bvnot(x), bvnot(y))
    
    axiom demorgan_or : ∀(n : ℕ)(x y : BitVec(n)).
        bvnot(bvor(x, y)) = bvand(bvnot(x), bvnot(y))
    
    // Complement laws
    axiom and_complement : ∀(n : ℕ)(x : BitVec(n)).
        bvand(x, bvnot(x)) = bvzero(n)
    
    axiom or_complement : ∀(n : ℕ)(x : BitVec(n)).
        bvor(x, bvnot(x)) = bvones(n)
    
    // Distributive law
    axiom distribute : ∀(n : ℕ)(x y z : BitVec(n)).
        bvand(x, bvor(y, z)) = bvor(bvand(x, y), bvand(x, z))
}

3. Ordered Set

Bit-vectors are totally ordered (both unsigned and signed):

structure TotalOrder {
    // Trichotomy: exactly one of <, =, > holds
    axiom trichotomy : ∀(n : ℕ)(x y : BitVec(n)).
        bvult(x, y) ∨ x = y ∨ bvult(y, x)
    
    // Transitivity
    axiom transitive : ∀(n : ℕ)(x y z : BitVec(n)).
        bvult(x, y) ∧ bvult(y, z) → bvult(x, z)
}

Bitwise Operations

Logical Operations

structure BitwiseLogic {
    // AND: set intersection on bit positions
    axiom and_idempotent : ∀(n : ℕ)(x : BitVec(n)). bvand(x, x) = x
    
    // OR: set union on bit positions  
    axiom or_idempotent : ∀(n : ℕ)(x : BitVec(n)). bvor(x, x) = x
    
    // XOR: symmetric difference
    axiom xor_self : ∀(n : ℕ)(x : BitVec(n)). bvxor(x, x) = bvzero(n)
    
    // NOT: complement
    axiom not_involution : ∀(n : ℕ)(x : BitVec(n)). bvnot(bvnot(x)) = x
}

Available Operations

Arithmetic Operations

Bit-vector arithmetic is modular (mod 2ⁿ):

structure ModularArithmetic {
    // Addition wraps around
    axiom add_commutative : ∀(n : ℕ)(x y : BitVec(n)).
        bvadd(x, y) = bvadd(y, x)
    
    axiom add_zero : ∀(n : ℕ)(x : BitVec(n)).
        bvadd(x, bvzero(n)) = x
    
    // Two's complement negation
    axiom neg_inverse : ∀(n : ℕ)(x : BitVec(n)).
        bvadd(x, bvneg(x)) = bvzero(n)
    
    // Multiplication distributes
    axiom mul_distribute : ∀(n : ℕ)(x y z : BitVec(n)).
        bvmul(x, bvadd(y, z)) = bvadd(bvmul(x, y), bvmul(x, z))
}

Available Operations

Shift Operations

structure ShiftOps {
    // Left shift: multiply by 2ᵏ
    axiom shl_zero : ∀(n : ℕ)(x : BitVec(n)).
        bvshl(x, bvzero(n)) = x
    
    // Logical right shift: divide by 2ᵏ (zero fill)
    axiom lshr_zero : ∀(n : ℕ)(x : BitVec(n)).
        bvlshr(x, bvzero(n)) = x
    
    // Arithmetic right shift: divide by 2ᵏ (sign extend)
    axiom ashr_zero : ∀(n : ℕ)(x : BitVec(n)).
        bvashr(x, bvzero(n)) = x
}

Comparison Operations

Unsigned Comparisons

structure UnsignedCompare {
    axiom zero_minimum : ∀(n : ℕ)(x : BitVec(n)).
        bvule(bvzero(n), x)
    
    axiom ones_maximum : ∀(n : ℕ)(x : BitVec(n)).
        bvule(x, bvones(n))
}

Signed Comparisons

structure SignedCompare {
    // In two's complement, high bit indicates negative
    axiom signed_negative : ∀(n : ℕ)(x : BitVec(n)).
        bit(x, n - 1) = 1 → bvslt(x, bvzero(n))
}

Construction and Extraction

Constants

structure Constants {
    // Zero vector (all bits 0)
    axiom zero_all : ∀(n : ℕ)(i : ℕ). i < n → bit(bvzero(n), i) = 0
    
    // Ones vector (all bits 1)
    axiom ones_all : ∀(n : ℕ)(i : ℕ). i < n → bit(bvones(n), i) = 1
    
    // Single 1 in lowest position
    axiom one_bit : bit(bvone(8), 0) = 1
}

Bit Extraction

structure BitExtraction {
    // Get individual bit
    axiom bit_range : ∀(n : ℕ)(x : BitVec(n))(i : ℕ). 
        i < n → (bit(x, i) = 0 ∨ bit(x, i) = 1)
    
    // Extract slice [high:low]
    axiom extract_width : ∀(n high low : ℕ)(x : BitVec(n)).
        high ≥ low ∧ high < n → width(extract(high, low, x)) = high - low + 1
}

Extension

structure Extension {
    // Zero extension (for unsigned)
    axiom zext_preserves : ∀(n m : ℕ)(x : BitVec(n)).
        m ≥ n → bvult(x, bvzero(n)) = bvult(zext(m, x), bvzero(m))
    
    // Sign extension (for signed)
    axiom sext_preserves : ∀(n m : ℕ)(x : BitVec(n)).
        m ≥ n → bvslt(x, bvzero(n)) = bvslt(sext(m, x), bvzero(m))
}

Z3 Verification

Kleis maps bit-vector operations directly to Z3’s native BitVec theory:

structure Z3BitVecExample {
    // XOR properties verified by Z3
    axiom xor_cancel : ∀(n : ℕ)(x : BitVec(n)). bvxor(x, x) = bvzero(n)
    
    // De Morgan verified
    axiom demorgan : ∀(n : ℕ)(x y : BitVec(n)).
        bvnot(bvand(x, y)) = bvor(bvnot(x), bvnot(y))
    
    // Arithmetic properties
    axiom add_neg : ∀(n : ℕ)(x : BitVec(n)). bvadd(x, bvneg(x)) = bvzero(n)
}

Example: Cryptographic Rotation

structure RotateExample {
    // Left rotation by k bits
    define rotl(n : ℕ, x : BitVec(n), k : BitVec(n)) : BitVec(n) =
        bvor(bvshl(x, k), bvlshr(x, bvsub(bvone(n) * n, k)))
    
    // Right rotation by k bits
    define rotr(n : ℕ, x : BitVec(n), k : BitVec(n)) : BitVec(n) =
        bvor(bvlshr(x, k), bvshl(x, bvsub(bvone(n) * n, k)))
    
    // Rotation is its own inverse
    axiom rotate_inverse : ∀(n k : ℕ)(x : BitVec(n)).
        rotr(n, rotl(n, x, k), k) = x
}

Example: Bit Manipulation

structure BitManipulation {
    // Set bit i to 1
    define set_bit(n : ℕ, x : BitVec(n), i : BitVec(n)) : BitVec(n) =
        bvor(x, bvshl(bvone(n), i))
    
    // Clear bit i to 0
    define clear_bit(n : ℕ, x : BitVec(n), i : BitVec(n)) : BitVec(n) =
        bvand(x, bvnot(bvshl(bvone(n), i)))
    
    // Toggle bit i
    define toggle_bit(n : ℕ, x : BitVec(n), i : BitVec(n)) : BitVec(n) =
        bvxor(x, bvshl(bvone(n), i))
    
    // Test if bit i is set
    define test_bit(n : ℕ, x : BitVec(n), i : BitVec(n)) : Bool =
        bvand(x, bvshl(bvone(n), i)) ≠ bvzero(n)
}

Summary

See stdlib/bitvector.kleis for the complete axiom set.

What’s Next?

Learn about string operations and Z3’s string theory:

→ Strings

Strings

Kleis provides comprehensive support for string operations via Z3’s QF_SLIA (Quantifier-Free Strings and Linear Integer Arithmetic) theory. This enables formal verification of string-manipulating programs.

The String Type

define greeting : String = "Hello, World!"
define empty : String = ""

Basic Operations

Concatenation

structure StringConcat {
    // Concatenation
    axiom concat_ex : concat("Hello", " World") = "Hello World"
    
    // Empty string is identity
    axiom concat_empty_left : ∀(s : String). concat("", s) = s
    axiom concat_empty_right : ∀(s : String). concat(s, "") = s
    
    // Associativity
    axiom concat_assoc : ∀(a b c : String). 
        concat(concat(a, b), c) = concat(a, concat(b, c))
}

Length

structure StringLength {
    axiom len_hello : strlen("Hello") = 5
    axiom len_empty : strlen("") = 0
    
    // Length of concatenation
    axiom len_concat : ∀(a b : String). 
        strlen(concat(a, b)) = strlen(a) + strlen(b)
    
    // Length is non-negative
    axiom len_nonneg : ∀(s : String). strlen(s) ≥ 0
}

Substring Operations

Contains

Check if one string contains another:

structure StringContains {
    axiom contains_ex : contains("Hello World", "World") = true
    axiom contains_empty : ∀(s : String). contains(s, "") = true
    axiom contains_self : ∀(s : String). contains(s, s) = true
}

Prefix and Suffix

structure PrefixSuffix {
    // Prefix check
    axiom prefix_ex : hasPrefix("Hello World", "Hello") = true
    axiom prefix_empty : ∀(s : String). hasPrefix(s, "") = true
    
    // Suffix check
    axiom suffix_ex : hasSuffix("Hello World", "World") = true
    axiom suffix_empty : ∀(s : String). hasSuffix(s, "") = true
}

Substring Extraction

structure Substring {
    // substr(s, start, length) extracts substring
    axiom substr_ex : substr("Hello World", 0, 5) = "Hello"
    axiom substr_middle : substr("Hello World", 6, 5) = "World"
    
    // Empty substring
    axiom substr_zero : ∀(s : String)(i : ℕ). substr(s, i, 0) = ""
}

Character Access

structure CharAt {
    // charAt(s, i) returns single character at index i
    axiom charAt_ex : charAt("Hello", 0) = "H"
    axiom charAt_last : charAt("Hello", 4) = "o"
}

Index Of

structure IndexOf {
    // indexOf(s, pattern, start) returns first index of pattern
    axiom indexOf_ex : indexOf("Hello World", "o", 0) = 4
    axiom indexOf_second : indexOf("Hello World", "o", 5) = 7
    
    // Not found returns -1
    axiom indexOf_notfound : indexOf("Hello", "z", 0) = 0 - 1
}

Replace

structure StringReplace {
    // replace(s, old, new) replaces first occurrence
    axiom replace_ex : replace("Hello World", "World", "Kleis") = "Hello Kleis"
    
    // No match means no change
    axiom replace_nomatch : ∀(s : String). 
        ¬contains(s, "xyz") → replace(s, "xyz", "abc") = s
}

String-Integer Conversion

String to Integer

structure StrToInt {
    axiom str_to_int_ex : strToInt("42") = 42
    axiom str_to_int_neg : strToInt("-17") = 0 - 17
    axiom str_to_int_zero : strToInt("0") = 0
}

Integer to String

structure IntToStr {
    axiom int_to_str_ex : intToStr(42) = "42"
    axiom int_to_str_neg : intToStr(0 - 17) = "-17"
    axiom int_to_str_zero : intToStr(0) = "0"
}

Round-trip Property

structure Roundtrip {
    // Converting back and forth preserves value
    axiom roundtrip_int : ∀(n : ℤ). strToInt(intToStr(n)) = n
    
    // For valid numeric strings
    axiom roundtrip_str : ∀(s : String). 
        isDigits(s) → intToStr(strToInt(s)) = s
}

Regular Expressions

Kleis supports regular expression matching via Z3’s regex theory:

structure RegexMatch {
    // Check if string matches pattern
    axiom digits_match : matchesRegex("12345", "[0-9]+") = true
    axiom alpha_match : matchesRegex("Hello", "[A-Za-z]+") = true
    
    // Built-in character class predicates
    axiom is_digits : isDigits("12345") = true
    axiom is_alpha : isAlpha("Hello") = true
    axiom is_alphanum : isAlphaNum("Test123") = true
}

Z3 Verification

String properties are verified using Z3’s native string theory:

structure Z3StringProofs {
    // Concatenation properties
    axiom concat_length : ∀(a b : String). 
        strlen(concat(a, b)) = strlen(a) + strlen(b)
    
    // Contains implies length relationship
    axiom contains_length : ∀(s t : String). 
        contains(s, t) → strlen(s) ≥ strlen(t)
    
    // Prefix implies contains
    axiom prefix_contains : ∀(s t : String). 
        hasPrefix(s, t) → contains(s, t)
}

Monoid Structure

Strings form a monoid under concatenation:

implements Monoid(String) {
    operation identity = ""
    operation mul = concat
}

// Monoid laws hold:
// 1. concat("", s) = s           (left identity)
// 2. concat(s, "") = s           (right identity)
// 3. concat(a, concat(b, c)) 
//    = concat(concat(a, b), c)   (associativity)

Practical Examples

Email Validation

structure EmailValidation {
    define isValidEmail(email : String) : Bool =
        contains(email, "@") ∧ 
        contains(email, ".") ∧
        indexOf(email, "@", 0) < indexOf(email, ".", 0)
    
    axiom valid_ex : isValidEmail("user@example.com") = true
    axiom invalid_ex : isValidEmail("invalid") = false
}

URL Parsing

structure URLParsing {
    define getProtocol(url : String) : String =
        substr(url, 0, indexOf(url, "://", 0))
    
    axiom http_ex : getProtocol("https://kleis.io") = "https"
}

String Builder Pattern

structure StringBuilder {
    define join(sep : String, a : String, b : String) : String =
        concat(concat(a, sep), b)
    
    axiom join_ex : join(", ", "Hello", "World") = "Hello, World"
}

Operation Reference

Summary

See src/solvers/z3/capabilities.toml for the complete list of supported string operations.

What’s Next?

Explore set theory operations and Z3’s set reasoning:

→ Sets

Set Theory

Kleis provides native set theory support backed by Z3’s set theory solver. This enables rigorous mathematical reasoning about collections, membership, and set operations.

Importing Set Theory

import "stdlib/sets.kleis"

This imports the SetTheory(T) structure with all operations and axioms.

Constructing Sets

Sets are built using empty_set() and insert():

// Empty set (note the parentheses!)
empty_set()

// Singleton set {5}
insert(5, empty_set())

// Set {1, 2, 3}
insert(3, insert(2, insert(1, empty_set())))

// Shorthand: singleton(x) creates {x}
singleton(5)

Important: Use empty_set() with parentheses (it’s a nullary function).

Verification Example

λ> :load stdlib/sets.kleis
λ> :sat in_set(2, insert(3, insert(2, insert(1, empty_set()))))
✅ Satisfiable (2 IS in {1,2,3})

λ> :sat in_set(5, insert(3, insert(2, insert(1, empty_set()))))
❌ Unsatisfiable (5 is NOT in {1,2,3})

λ> :sat subset(insert(1, empty_set()), insert(2, insert(1, empty_set())))
✅ Satisfiable ({1} ⊆ {1,2})

Basic Operations

Set Membership

// Check if element x is in set S
in_set(x, S)  // Returns Bool

// Example: Define a membership property
structure ClosedUnderAddition {
    axiom closed: ∀(S : Set(ℤ), x y : ℤ). 
        in_set(x, S) ∧ in_set(y, S) → in_set(x + y, S)
}

Set Construction

empty_set        // The empty set ∅
singleton(x)     // Set containing just x: {x}
insert(x, S)     // Add x to S: S ∪ {x}
remove(x, S)     // Remove x from S: S \ {x}

Set Operations

union(A, B)       // Union: A ∪ B
intersect(A, B)   // Intersection: A ∩ B
difference(A, B)  // Difference: A \ B
complement(A)     // Complement: ᶜA

Set Relations

subset(A, B)         // Subset: A ⊆ B
proper_subset(A, B)  // Proper subset: A ⊂ B (A ⊆ B and A ≠ B)

Verification Example

Here’s a complete example proving De Morgan’s laws:

import "stdlib/sets.kleis"

// Verify De Morgan's law: complement(A ∪ B) = complement(A) ∩ complement(B)
structure DeMorganProof(T) {
    axiom de_morgan_union: ∀(A B : Set(T)).
        complement(union(A, B)) = intersect(complement(A), complement(B))
}

In the REPL:

λ> :load stdlib/sets.kleis
✅ Loaded stdlib/sets.kleis

λ> :verify ∀(A B : Set(ℤ), x : ℤ). in_set(x, complement(union(A, B))) ↔ (¬in_set(x, A) ∧ ¬in_set(x, B))
✅ Valid (follows from axioms)

Mathematical Structures with Sets

Open Balls in Metric Spaces

import "stdlib/sets.kleis"

structure MetricSpace(X) {
    operation d : X → X → ℝ
    
    // Metric axioms
    axiom positive: ∀(x y : X). d(x, y) >= 0
    axiom zero_iff_equal: ∀(x y : X). d(x, y) = 0 ↔ x = y
    axiom symmetric: ∀(x y : X). d(x, y) = d(y, x)
    axiom triangle: ∀(x y z : X). d(x, z) <= d(x, y) + d(y, z)
}

structure OpenBalls(X) {
    operation d : X → X → ℝ
    operation ball : X → ℝ → Set(X)
    
    // x is in ball(center, r) iff d(x, center) < r
    axiom ball_def: ∀(center : X, r : ℝ, x : X).
        in_set(x, ball(center, r)) ↔ d(x, center) < r
    
    // Open balls are non-empty when radius is positive
    axiom ball_nonempty: ∀(center : X, r : ℝ).
        r > 0 → in_set(center, ball(center, r))
}

Measure Spaces

import "stdlib/sets.kleis"

structure MeasureSpace(X) {
    element sigma_algebra : Set(Set(X))
    operation measure : Set(X) → ℝ
    
    // σ-algebra contains empty set
    axiom contains_empty: in_set(empty_set, sigma_algebra)
    
    // Closed under complement
    axiom closed_complement: ∀(A : Set(X)).
        in_set(A, sigma_algebra) → in_set(complement(A), sigma_algebra)
    
    // Measure is non-negative
    axiom measure_positive: ∀(A : Set(X)). measure(A) >= 0
    
    // Measure of empty set is zero
    axiom measure_empty: measure(empty_set) = 0
}

Full Axiom Reference

The SetTheory(T) structure includes these axioms:

Unicode Operators (Future)

Currently, you must use function-style syntax. Future versions will support:

What’s Next?

Learn about matrix and vector operations for linear algebra:

→ Matrices

See Also

• Types and Values — Set(T) type documentation
• Z3 Verification — Using Z3 for proofs
• Structures — Defining mathematical structures

Matrices

Kleis provides comprehensive matrix support with both symbolic verification (via Z3) and concrete evaluation (via :eval).

Matrix Type

Matrices are parametric types with dimensions:

Matrix(m, n, T)   // m rows × n columns of type T

Examples:

• Matrix(2, 2, ℝ) - 2×2 matrix of reals
• Matrix(3, 4, ℂ) - 3×4 matrix of complex numbers

Creating Matrices

Use the Matrix constructor with dimensions and a list of elements (row-major order):

// 2×2 matrix: [[1, 2], [3, 4]]
Matrix(2, 2, [1, 2, 3, 4])

// 2×3 matrix: [[1, 2, 3], [4, 5, 6]]
Matrix(2, 3, [1, 2, 3, 4, 5, 6])

Arithmetic Operations

Addition and Subtraction

Element-wise operations for matrices of the same dimensions:

:eval matrix_add(Matrix(2, 2, [1, 2, 3, 4]), Matrix(2, 2, [5, 6, 7, 8]))
// → Matrix(2, 2, [6, 8, 10, 12])

:eval matrix_sub(Matrix(2, 2, [10, 20, 30, 40]), Matrix(2, 2, [1, 2, 3, 4]))
// → Matrix(2, 2, [9, 18, 27, 36])

Matrix Multiplication

True matrix multiplication (m×n) · (n×p) → (m×p):

:eval multiply(Matrix(2, 2, [1, 2, 3, 4]), Matrix(2, 2, [5, 6, 7, 8]))
// → Matrix(2, 2, [19, 22, 43, 50])

// Non-square: (2×3) · (3×2) → (2×2)
:eval multiply(Matrix(2, 3, [1, 2, 3, 4, 5, 6]), Matrix(3, 2, [1, 2, 3, 4, 5, 6]))
// → Matrix(2, 2, [22, 28, 49, 64])

Scalar Multiplication

Multiply all elements by a scalar:

:eval scalar_matrix_mul(3, Matrix(2, 2, [1, 2, 3, 4]))
// → Matrix(2, 2, [3, 6, 9, 12])

Matrix Properties

Transpose

Swap rows and columns (m×n) → (n×m):

:eval transpose(Matrix(2, 3, [1, 2, 3, 4, 5, 6]))
// → Matrix(3, 2, [1, 4, 2, 5, 3, 6])

Trace

Sum of diagonal elements (square matrices only):

:eval trace(Matrix(3, 3, [1, 0, 0, 0, 2, 0, 0, 0, 3]))
// → 6

Determinant

Determinant for 1×1, 2×2, and 3×3 matrices:

:eval det(Matrix(2, 2, [4, 3, 6, 8]))
// → 14  (4*8 - 3*6)

:eval det(Matrix(3, 3, [1, 2, 3, 0, 1, 4, 5, 6, 0]))
// → 1

Element Extraction

Get Single Element

Access element at row i, column j (0-indexed):

:eval matrix_get(Matrix(2, 3, [1, 2, 3, 4, 5, 6]), 0, 2)
// → 3  (row 0, column 2)

:eval matrix_get(Matrix(2, 3, [1, 2, 3, 4, 5, 6]), 1, 1)
// → 5  (row 1, column 1)

Get Row or Column

Extract entire row or column as a list:

:eval matrix_row(Matrix(2, 3, [1, 2, 3, 4, 5, 6]), 0)
// → [1, 2, 3]

:eval matrix_row(Matrix(2, 3, [1, 2, 3, 4, 5, 6]), 1)
// → [4, 5, 6]

:eval matrix_col(Matrix(2, 3, [1, 2, 3, 4, 5, 6]), 0)
// → [1, 4]

:eval matrix_col(Matrix(2, 3, [1, 2, 3, 4, 5, 6]), 2)
// → [3, 6]

Get Diagonal

Extract diagonal elements as a list:

:eval matrix_diag(Matrix(3, 3, [1, 2, 3, 4, 5, 6, 7, 8, 9]))
// → [1, 5, 9]

Row and Column Manipulation

Stacking Matrices

Combine matrices vertically or horizontally:

λ> :let A = matrix([[1, 2], [3, 4]])
λ> :let B = matrix([[5, 6], [7, 8]])

λ> :eval vstack(A, B)
✅ Matrix(4, 2, [1, 2, 3, 4, 5, 6, 7, 8])  // A on top, B below

λ> :eval hstack(A, B)
✅ Matrix(2, 4, [1, 2, 5, 6, 3, 4, 7, 8])  // A left, B right

Appending Rows and Columns

Add a single row or column:

λ> :let A = matrix([[1, 2], [3, 4]])

λ> :eval append_row(A, [5, 6])
✅ Matrix(3, 2, [1, 2, 3, 4, 5, 6])  // Row added at bottom

λ> :eval prepend_row([0, 0], A)
✅ Matrix(3, 2, [0, 0, 1, 2, 3, 4])  // Row added at top

λ> :eval append_col(A, [10, 20])
✅ Matrix(2, 3, [1, 2, 10, 3, 4, 20])  // Column added at right

λ> :eval prepend_col([10, 20], A)
✅ Matrix(2, 3, [10, 1, 2, 20, 3, 4])  // Column added at left

Building Augmented Matrices

Useful for linear algebra (solving Ax = b):

λ> :let A = matrix([[1, 2], [3, 4]])
λ> :let b = matrix([[5], [6]])
λ> :eval hstack(A, b)
✅ Matrix(2, 3, [1, 2, 5, 3, 4, 6])  // [A | b]

Setting Values

Kleis matrices are immutable, but you can create new matrices with modified values:

Set Individual Element

λ> :let A = zeros(3, 3)
λ> :eval A
✅ matrix([[0, 0, 0], [0, 0, 0], [0, 0, 0]])

λ> :eval set_element(A, 1, 1, 99)
✅ matrix([[0, 0, 0], [0, 99, 0], [0, 0, 0]])

Set Row or Column

λ> :eval set_row(zeros(3, 3), 0, [1, 2, 3])
✅ matrix([[1, 2, 3], [0, 0, 0], [0, 0, 0]])

λ> :eval set_col(zeros(3, 3), 2, [7, 8, 9])
✅ matrix([[0, 0, 7], [0, 0, 8], [0, 0, 9]])

Set Diagonal

λ> :eval set_diag(zeros(3, 3), [1, 2, 3])
✅ matrix([[1, 0, 0], [0, 2, 0], [0, 0, 3]])

Matrix Size

λ> :let A = matrix([[1, 2, 3], [4, 5, 6]])
λ> :eval size(A)
✅ [2, 3]

λ> :eval nrows(A)
✅ 2

λ> :eval ncols(A)
✅ 3

Symbolic Matrix Operations

Matrix operations support partial symbolic evaluation. When mixing concrete and symbolic values, Kleis evaluates what it can and leaves the rest symbolic:

:eval matrix_add(Matrix(2, 2, [1, 0, 0, 1]), Matrix(2, 2, [a, 0, 0, b]))
// → Matrix(2, 2, [1+a, 0, 0, 1+b])

:eval matrix_add(Matrix(2, 2, [0, 0, 0, 0]), Matrix(2, 2, [x, y, z, w]))
// → Matrix(2, 2, [x, y, z, w])  (0+x = x optimization)

Smart Optimizations

The evaluator applies algebraic simplifications:

• 0 + x = x
• x + 0 = x
• x - 0 = x
• 0 * x = 0
• 1 * x = x

Dimension Checking

Kleis enforces dimension constraints at the type level:

// This type-checks: same dimensions
matrix_add(Matrix(2, 2, [1, 2, 3, 4]), Matrix(2, 2, [5, 6, 7, 8]))

// This fails: dimension mismatch
matrix_add(Matrix(2, 2, [1, 2, 3, 4]), Matrix(3, 3, [1, 2, 3, 4, 5, 6, 7, 8, 9]))
// Error: dimension mismatch: 2x2 vs 3x3

For matrix multiplication, inner dimensions must match:

// OK: (2×3) · (3×2) → (2×2)
multiply(Matrix(2, 3, [...]), Matrix(3, 2, [...]))

// Error: (2×2) · (3×2) - inner dimensions 2 ≠ 3
multiply(Matrix(2, 2, [...]), Matrix(3, 2, [...]))
// Error: inner dimensions don't match

Complete Operations Reference

Matrix Constructors

Nested list syntax is recommended for readability:

λ> :eval matrix([[1, 2, 3], [4, 5, 6], [7, 8, 9]])
✅ Matrix(3, 3, [1, 2, 3, 4, 5, 6, 7, 8, 9])

λ> :eval matrix([[0, -1], [1, 0]])
✅ Matrix(2, 2, [0, -1, 1, 0])

λ> :eval eigenvalues(matrix([[0, -1], [1, 0]]))
✅ [complex(0, 1), complex(0, -1)]

Other constructors:

λ> :eval eye(3)
✅ Matrix(3, 3, [1, 0, 0, 0, 1, 0, 0, 0, 1])

λ> :eval diag_matrix([5, 10, 15])
✅ Matrix(3, 3, [5, 0, 0, 0, 10, 0, 0, 0, 15])

Core Matrix Operations

LAPACK Numerical Operations

When compiled with the numerical feature, Kleis provides high-performance numerical linear algebra via LAPACK:

Schur Decomposition for Control Theory

The Schur decomposition A = UTUᵀ is critical for control theory applications:

// Compute Schur decomposition
let A = Matrix(3, 3, [-2, 0, 1, 0, -1, 0, 1, 0, -3])
:eval schur(A)
// Returns [U, T, eigenvalues] where:
// - U is orthogonal (Schur vectors)
// - T is quasi-upper-triangular (Schur form)
// - eigenvalues are (real, imag) pairs

Use cases:

• Stability analysis (check if eigenvalues have Re(λ) < 0)
• Lyapunov equation solvers
• CARE/DARE (algebraic Riccati equations)
• Pole placement algorithms

Example: LQG Controller Design

This complete example demonstrates designing an LQG (Linear-Quadratic-Gaussian) controller for a mass-spring-damper system using Kleis’s numerical matrix operations.

System Definition

λ> :let A = matrix([[0, 1], [-2, -3]])
λ> :let B = matrix([[0], [1]])
λ> :let C = matrix([[1, 0]])

The system ẋ = Ax + Bu, y = Cx represents a 2nd-order mechanical system.

Open-Loop Stability Analysis

λ> :eval eigenvalues(A)
✅ [-1, -2]

Both eigenvalues have negative real parts → system is stable, but response is slow.

LQR Controller Design (Pole Placement)

Goal: Place closed-loop poles at -5, -5 for faster response.

Step 1: Check controllability (det ≠ 0 means we can place poles anywhere):

λ> :let Wc = hstack(B, multiply(A, B))
λ> :eval Wc
✅ matrix([[0, 1], [1, -3]])

λ> :eval det(Wc)
✅ -1

Step 2: Extract open-loop characteristic polynomial coefficients.

The open-loop characteristic polynomial is det(sI - A) = s² + a₁s + a₀. From A = [[0, 1], [-2, -3]], we get: s² + 3s + 2, so a₁ = 3, a₀ = 2.

λ> :let a1 = 3
λ> :let a0 = 2

Step 3: Set desired closed-loop characteristic polynomial.

For poles at -5, -5: (s+5)² = s² + 10s + 25, so α₁ = 10, α₀ = 25.

λ> :let alpha1 = 10
λ> :let alpha0 = 25

Step 4: Compute feedback gain K using coefficient matching.

For a controllable canonical form with B = [[0], [1]], the gain is K = [α₀-a₀, α₁-a₁]:

λ> :let k1 = alpha0 - a0
λ> :let k2 = alpha1 - a1
λ> :eval k1
✅ 23
λ> :eval k2
✅ 7

λ> :let K = matrix([[k1, k2]])
λ> :eval K
✅ matrix([[23, 7]])

Step 5: Verify closed-loop eigenvalues:

λ> :let A_cl = matrix_sub(A, multiply(B, K))
λ> :eval A_cl
✅ matrix([[0, 1], [-25, -10]])

λ> :eval eigenvalues(A_cl)
✅ [-5.000000042200552, -4.999999957799446]

Closed-loop poles are at -5 (2.5× faster than open-loop).

Kalman Observer Design

Goal: Design observer with poles at -10, -10 (faster than controller for separation principle).

Step 1: Check observability:

λ> :let Wo = vstack(C, multiply(C, A))
λ> :eval Wo
✅ matrix([[1, 0], [0, 1]])

λ> :eval det(Wo)
✅ 1

Step 2: Apply duality - observer design uses Aᵀ and Cᵀ.

For observer error dynamics (A - LC), the characteristic polynomial is: det(sI - A + LC) = s² + (3 + l₁)s + (2 + l₂)

Desired: (s+10)² = s² + 20s + 100

Step 3: Compute observer gain L:

λ> :let l1 = 20 - 3
λ> :let l2 = 100 - 2
λ> :eval l1
✅ 17
λ> :eval l2
✅ 98

λ> :let L = matrix([[l1], [l2]])
λ> :eval L
✅ matrix([[17], [98]])

Step 4: Verify observer eigenvalues:

λ> :let A_obs = matrix_sub(A, multiply(L, C))
λ> :eval A_obs
✅ matrix([[-17, 1], [-100, -3]])

λ> :eval eigenvalues(A_obs)
✅ [complex(-10, 7.14), complex(-10, -7.14)]

Observer eigenvalues have Re(λ) = -10 → faster error convergence than the controller.

Controllability and Observability

λ> :let Wc = hstack(B, multiply(A, B))
λ> :eval Wc
✅ matrix([[0, 1], [1, -3]])

λ> :eval det(Wc)
✅ -1

det(Wc) ≠ 0 → System is controllable.

λ> :let Wo = vstack(C, multiply(C, A))
λ> :eval Wo
✅ matrix([[1, 0], [0, 1]])

λ> :eval det(Wo)
✅ 1

det(Wo) ≠ 0 → System is observable.

Summary

The Separation Principle is satisfied: LQR and Kalman can be designed independently, and the combined LQG controller is guaranteed stable.

See Also

• Types and Values - Matrix as a parametric type
• Complex Numbers - Matrices over ℂ
• The REPL - Using :eval for concrete computation

Symbolic Computation

Kleis isn’t just about verification — it can compute with symbolic expressions. The crown jewel is symbolic_diff.kleis: a complete symbolic differentiation engine written in pure Kleis.

The Expression AST

Mathematical expressions are represented as an algebraic data type:

data Expression = 
    ENumber(value : ℝ)
  | EVariable(name : String)
  | EOperation(name : String, args : List(Expression))

This simple structure represents any mathematical expression:

Helper Constructors

For readability, helper functions build expressions:

// Value constructors
define num(n) = ENumber(n)
define var(x) = EVariable(x)

// Operation constructors (e_ prefix avoids builtin conflicts)
define e_add(a, b) = EOperation("plus", Cons(a, Cons(b, Nil)))
define e_mul(a, b) = EOperation("times", Cons(a, Cons(b, Nil)))
define e_sub(a, b) = EOperation("minus", Cons(a, Cons(b, Nil)))
define e_div(a, b) = EOperation("divide", Cons(a, Cons(b, Nil)))
define e_pow(a, b) = EOperation("power", Cons(a, Cons(b, Nil)))
define e_neg(a) = EOperation("negate", Cons(a, Nil))
define e_sin(a) = EOperation("sin", Cons(a, Nil))
define e_cos(a) = EOperation("cos", Cons(a, Nil))
define e_sqrt(a) = EOperation("sqrt", Cons(a, Nil))
define e_exp(a) = EOperation("exp", Cons(a, Nil))
define e_ln(a) = EOperation("ln", Cons(a, Nil))

Symbolic Differentiation

The diff function computes derivatives by pattern matching on the AST:

define diff(e, var_name) = match e {
    // Constant rule: d/dx(c) = 0
    ENumber(_) => num(0)
    
    // Variable rule: d/dx(x) = 1, d/dx(y) = 0 if y ≠ x
    EVariable(name) => if str_eq(name, var_name) then num(1) else num(0)
    
    // Operation rules
    EOperation(op_name, args) => diff_op(op_name, args, var_name)
}

Differentiation Rules

Each operation has its own differentiation rule:

define diff_op(op_name, args, var_name) = match op_name {
    // Sum rule: d/dx(f + g) = df/dx + dg/dx
    "plus" => match args {
        Cons(f, Cons(g, Nil)) => e_add(diff(f, var_name), diff(g, var_name))
        | _ => num(0)
    }
    
    // Product rule: d/dx(f × g) = f'g + fg'
    "times" => match args {
        Cons(f, Cons(g, Nil)) => 
            e_add(e_mul(diff(f, var_name), g), e_mul(f, diff(g, var_name)))
        | _ => num(0)
    }
    
    // Chain rule for sin: d/dx(sin(f)) = cos(f) × f'
    "sin" => match args {
        Cons(f, Nil) => e_mul(e_cos(f), diff(f, var_name))
        | _ => num(0)
    }
    
    // Chain rule for cos: d/dx(cos(f)) = -sin(f) × f'
    "cos" => match args {
        Cons(f, Nil) => e_neg(e_mul(e_sin(f), diff(f, var_name)))
        | _ => num(0)
    }
    
    // Power rule: d/dx(f^n) = n × f^(n-1) × f'
    "power" => match args {
        Cons(f, Cons(ENumber(n), Nil)) => 
            e_mul(e_mul(num(n), e_pow(f, num(n - 1))), diff(f, var_name))
        | _ => num(0)
    }
    
    // Exponential rule: d/dx(e^f) = e^f × f'
    "exp" => match args {
        Cons(f, Nil) => e_mul(e_exp(f), diff(f, var_name))
        | _ => num(0)
    }
    
    // Logarithm rule: d/dx(ln(f)) = f'/f
    "ln" => match args {
        Cons(f, Nil) => e_div(diff(f, var_name), f)
        | _ => num(0)
    }
    
    // Square root: d/dx(√f) = f'/(2√f)
    "sqrt" => match args {
        Cons(f, Nil) => e_div(diff(f, var_name), e_mul(num(2), e_sqrt(f)))
        | _ => num(0)
    }
    
    | _ => num(0)  // Unknown operation
}

Algebraic Simplification

Raw differentiation produces verbose expressions. The simplify function cleans them up:

define simplify(e) = match e {
    // Base cases
    ENumber(n) => ENumber(n)
    EVariable(x) => EVariable(x)
    
    // Simplify operations recursively
    EOperation(op, args) => simplify_op(op, list_map(simplify, args))
}

define simplify_op(op, args) = match op {
    "plus" => match args {
        // 0 + x = x
        Cons(ENumber(0), Cons(x, Nil)) => x
        // x + 0 = x
        Cons(x, Cons(ENumber(0), Nil)) => x
        // n + m = (n+m)
        Cons(ENumber(n), Cons(ENumber(m), Nil)) => ENumber(n + m)
        | _ => EOperation("plus", args)
    }
    
    "times" => match args {
        // 0 × x = 0
        Cons(ENumber(0), _) => num(0)
        Cons(_, Cons(ENumber(0), Nil)) => num(0)
        // 1 × x = x
        Cons(ENumber(1), Cons(x, Nil)) => x
        // x × 1 = x
        Cons(x, Cons(ENumber(1), Nil)) => x
        // n × m = (n×m)
        Cons(ENumber(n), Cons(ENumber(m), Nil)) => ENumber(n * m)
        | _ => EOperation("times", args)
    }
    
    "power" => match args {
        // x^0 = 1
        Cons(_, Cons(ENumber(0), Nil)) => num(1)
        // x^1 = x
        Cons(x, Cons(ENumber(1), Nil)) => x
        | _ => EOperation("power", args)
    }
    
    | _ => EOperation(op, args)
}

Example: Differentiating x²

example "derivative of x squared" {
    let expr = e_pow(var("x"), num(2)) in      // x²
    let deriv = diff(expr, "x") in              // d/dx(x²)
    let simplified = simplify(deriv) in
    // Result: 2x (after simplification)
    simplified
}

Step-by-step:

1. e_pow(var("x"), num(2)) = EOperation("power", [EVariable("x"), ENumber(2)])
2. Power rule: e_mul(e_mul(num(2), e_pow(var("x"), num(1))), diff(var("x"), "x"))
3. Variable rule: diff(var("x"), "x") = num(1)
4. Simplify: 2 × x^1 × 1 → 2 × x

Example: Chain Rule

example "derivative of sin(x²)" {
    let expr = e_sin(e_pow(var("x"), num(2))) in   // sin(x²)
    let deriv = diff(expr, "x") in
    simplify(deriv)
    // Result: cos(x²) × 2x
}

Substitution

The subst function replaces variables with values:

define subst(e, var_name, value) = match e {
    ENumber(n) => ENumber(n)
    EVariable(name) => if str_eq(name, var_name) then value else e
    EOperation(op, args) => EOperation(op, list_map(λ a . subst(a, var_name, value), args))
}

Usage:

example "evaluate at x=2" {
    let expr = e_pow(var("x"), num(2)) in   // x²
    let at_2 = subst(expr, "x", num(2)) in  // 2²
    simplify(at_2)                           // 4
}

Application: Cartan Geometry

The symbolic differentiation engine powers the Cartan geometry computation. See the Cartan Geometry appendix for details.

// Compute exterior derivative of a 1-form
define d0(f) = [
    simplify(diff(f, "t")),
    simplify(diff(f, "r")),
    simplify(diff(f, "theta")),
    simplify(diff(f, "phi"))
]

// Schwarzschild metric factor
let f = e_sub(num(1), e_div(e_mul(num(2), M), var("r"))) in
// d(f) = [0, 2M/r², 0, 0]
d0(f)

Coordinate-Specific Derivatives

For physics applications, we define coordinate-specific differentiation:

define diff_t(e) = diff(e, "t")
define diff_r(e) = diff(e, "r")
define diff_theta(e) = diff(e, "theta")
define diff_phi(e) = diff(e, "phi")

These are used in the exterior derivative for differential forms:

// (dω)_μν = ∂ω_ν/∂x^μ - ∂ω_μ/∂x^ν
define d1(omega) = 
    let w0 = nth(omega, 0) in
    let w1 = nth(omega, 1) in
    let w2 = nth(omega, 2) in
    let w3 = nth(omega, 3) in
    [
        [num(0),
         simplify(e_sub(diff_t(w1), diff_r(w0))),
         simplify(e_sub(diff_t(w2), diff_theta(w0))),
         simplify(e_sub(diff_t(w3), diff_phi(w0)))],
        // ... (antisymmetric matrix)
    ]

Why This Matters

Traditional computer algebra systems (Mathematica, Maple) implement differentiation in their host language. In Kleis:

1. Differentiation is pure Kleis — no Rust builtins needed
2. Rules are explicit — you can read and verify them
3. Extensible — add new rules for new operations
4. Verified — axioms can be checked by Z3

This is code as mathematics — the implementation is the specification.

Current Limitations

Symbolic integration is not implemented. The stdlib provides axioms for integration (calculus.kleis defines the Integrable structure with the Fundamental Theorem of Calculus), but no pattern-matching integrator like symbolic_diff.kleis.

Symbolic integration is fundamentally harder than differentiation — it requires heuristics, table lookups, and algorithms like Risch’s that don’t reduce to simple recursive rules. For now, use numerical integration via ode45 or external tools.

What’s Next

See how symbolic computation enables physics simulations:

→ Next: Physics Applications

Physics Applications

Kleis includes extensive physics libraries. This chapter showcases what’s possible.

Electromagnetism: Maxwell’s Equations

The maxwell.kleis module expresses electromagnetism in covariant (tensor) form.

The Field Tensor

The electromagnetic field tensor F_μν is antisymmetric and encodes both E and B fields:

structure FieldTensorProperties {
    operation F : Nat → Nat → ℝ
    
    // Antisymmetry: F_μν = -F_νμ
    axiom F_antisymmetric : ∀ mu : Nat . ∀ nu : Nat .
        F(mu, nu) = negate(F(nu, mu))
    
    // Diagonal vanishes
    axiom F_diagonal_zero : ∀ mu : Nat . F(mu, mu) = 0
}

Maxwell’s Equations

The four Maxwell equations reduce to two tensor equations:

structure MaxwellInhomogeneous {
    operation F : Nat → Nat → ℝ  // Field tensor
    operation J : Nat → ℝ         // 4-current
    operation divF : Nat → ℝ      // Divergence of F
    element mu0 : ℝ               // Permeability
    
    // ∂_μ F^μν = μ₀ J^ν
    // This encodes Gauss's law (ν=0) and Ampère's law (ν=i)
    axiom maxwell_inhomogeneous : ∀ nu : Nat .
        divF(nu) = times(mu0, J(nu))
}

structure MaxwellHomogeneous {
    operation F : Nat → Nat → ℝ
    operation cyclicF : Nat → Nat → Nat → ℝ  // ∂_[λ F_μν]
    
    // ∂_λ F_μν + ∂_μ F_νλ + ∂_ν F_λμ = 0
    // This encodes no magnetic monopoles and Faraday's law
    axiom maxwell_homogeneous : ∀ lam : Nat . ∀ mu : Nat . ∀ nu : Nat .
        cyclicF(lam, mu, nu) = 0
}

Einstein-Maxwell

Electromagnetism in curved spacetime (charged black holes):

structure EinsteinMaxwell {
    operation g : Nat → Nat → ℝ      // Metric
    operation G : Nat → Nat → ℝ      // Einstein tensor
    operation F : Nat → Nat → ℝ      // EM field tensor
    operation T_EM : Nat → Nat → ℝ   // EM stress-energy
    
    element Lambda : ℝ   // Cosmological constant
    element kappa : ℝ    // 8πG/c⁴
    
    // Einstein-Maxwell field equations:
    // G_μν + Λg_μν = κ T^EM_μν
    axiom einstein_maxwell_field_eqn : ∀ mu : Nat . ∀ nu : Nat .
        plus(G(mu, nu), times(Lambda, g(mu, nu))) = times(kappa, T_EM(mu, nu))
}

Fluid Dynamics: Navier-Stokes

The fluid_dynamics.kleis module covers incompressible and compressible flow.

Continuity Equation

Mass conservation:

structure ContinuityEquation {
    element drho_dt : ℝ      // ∂ρ/∂t
    element div_rho_u : ℝ    // ∇·(ρv)
    
    // ∂ρ/∂t + ∇·(ρv) = 0
    axiom continuity : plus(drho_dt, div_rho_u) = 0
}

Momentum Equation

The full Navier-Stokes momentum equation:

structure MomentumEquation {
    element rho : ℝ
    operation du_dt : Nat → ℝ
    operation div_momentum : Nat → ℝ
    operation grad_p : Nat → ℝ
    operation div_tau : Nat → ℝ
    operation f : Nat → ℝ
    
    // Navier-Stokes momentum equation
    axiom momentum : ∀ i : Nat .
        plus(times(rho, du_dt(i)), div_momentum(i)) = 
        plus(plus(negate(grad_p(i)), div_tau(i)), times(rho, f(i)))
}

Special Cases

Incompressible flow (∇·v = 0):

structure IncompressibleFlow {
    element div_u : ℝ
    axiom incompressible : div_u = 0
}

Stokes flow (creeping flow, Re << 1):

structure StokesFlow {
    operation grad_p : Nat → ℝ
    operation laplacian_u : Nat → ℝ
    element mu : ℝ
    
    // ∇p = μ∇²v (inertia negligible)
    axiom stokes : ∀ i : Nat .
        grad_p(i) = times(mu, laplacian_u(i))
}

Euler equations (inviscid, μ = 0):

structure EulerEquations {
    element rho : ℝ
    operation du_dt : Nat → ℝ
    operation convective : Nat → ℝ
    operation grad_p : Nat → ℝ
    
    // ρ∂v/∂t + ρ(v·∇)v = -∇p
    axiom euler : ∀ i : Nat .
        plus(times(rho, du_dt(i)), times(rho, convective(i))) = negate(grad_p(i))
}

Bernoulli’s Equation

For steady, inviscid, incompressible flow along a streamline:

structure BernoulliEquation {
    element rho : ℝ
    element g : ℝ
    element p1 : ℝ
    element p2 : ℝ
    element v1 : ℝ
    element v2 : ℝ
    element h1 : ℝ
    element h2 : ℝ
    
    // p + ½ρv² + ρgh = constant
    // Scaled: 2p + ρv² + 2ρgh = constant
    axiom bernoulli_conservation : 
        plus(plus(times(2, p1), times(rho, times(v1, v1))),
             times(times(2, rho), times(g, h1))) =
        plus(plus(times(2, p2), times(rho, times(v2, v2))),
             times(times(2, rho), times(g, h2)))
}

Solid Mechanics

The solid_mechanics.kleis module covers stress, strain, and failure criteria.

Stress and Strain Tensors

structure StressTensorSymmetry {
    operation sigma : Nat → Nat → ℝ
    
    // σ_ij = σ_ji (angular momentum balance)
    axiom stress_symmetric : ∀ i : Nat . ∀ j : Nat .
        sigma(i, j) = sigma(j, i)
}

structure ElasticityTensorSymmetries {
    // Fourth-order elasticity tensor: σ_ij = C_ijkl ε_kl
    operation C : Nat → Nat → Nat → Nat → ℝ
    
    // Major symmetry (strain energy)
    axiom C_major_symmetry : ∀ i j k l : Nat .
        C(i, j, k, l) = C(k, l, i, j)
    
    // Minor symmetries (stress/strain symmetry)
    axiom C_minor_symmetry_1 : ∀ i j k l : Nat .
        C(i, j, k, l) = C(j, i, k, l)
}

Yield Criteria

Von Mises (ductile metals):

structure VonMisesYieldCriterion {
    element sigma1 : ℝ
    element sigma2 : ℝ
    element sigma3 : ℝ
    element vm_sq_2 : ℝ
    
    // 2σ_vm² = (σ₁-σ₂)² + (σ₂-σ₃)² + (σ₃-σ₁)²
    axiom von_mises_def : vm_sq_2 = plus(plus(
        times(minus(sigma1, sigma2), minus(sigma1, sigma2)),
        times(minus(sigma2, sigma3), minus(sigma2, sigma3))),
        times(minus(sigma3, sigma1), minus(sigma3, sigma1)))
}

Mohr-Coulomb (soils and rocks):

structure MohrCoulombCriterion {
    element sigma_n : ℝ  // Normal stress
    element c : ℝ        // Cohesion
    element phi : ℝ      // tan(friction angle)
    element tau_critical : ℝ
    
    // |τ| = c + σ_n tan(φ)
    axiom mohr_coulomb : tau_critical = plus(c, times(sigma_n, phi))
}

Quantum Mechanics

The quantum.kleis module provides Hilbert space formalism.

State Vectors

structure Ket(dim: Nat, T) {
    operation normalize : Ket(dim, T) → Ket(dim, T)
    operation scale : T → Ket(dim, T) → Ket(dim, T)
}

structure Bra(dim: Nat, T) {
    operation conjugate : Ket(dim, T) → Bra(dim, T)
}

Inner Product

structure InnerProduct(dim: Nat) {
    operation inner : Bra(dim, ℂ) → Ket(dim, ℂ) → ℂ
    
    // ⟨φ|ψ⟩ is the probability amplitude
    // |⟨φ|ψ⟩|² is the probability
}

Operators

structure Operator(dim: Nat, T) {
    operation apply : Operator(dim, T) → Ket(dim, T) → Ket(dim, T)
    operation adjoint : Operator(dim, T) → Operator(dim, T)
    operation compose : Operator(dim, T) → Operator(dim, T) → Operator(dim, T)
}

structure Commutator(dim: Nat, T) {
    operation commutator : Operator(dim, T) → Operator(dim, T) → Operator(dim, T)
    
    // [Â, B̂] = ÂB̂ - B̂Â
    // [x̂, p̂] = iℏ (Heisenberg uncertainty!)
}

Pauli Matrices

structure PauliMatrices(T) {
    operation sigma_x : Operator(2, ℂ)  // |0⟩⟨1| + |1⟩⟨0|
    operation sigma_y : Operator(2, ℂ)  // -i|0⟩⟨1| + i|1⟩⟨0|
    operation sigma_z : Operator(2, ℂ)  // |0⟩⟨0| - |1⟩⟨1|
    
    // σ_x² = σ_y² = σ_z² = I
    // [σ_x, σ_y] = 2iσ_z
}

Time Evolution

structure TimeEvolution(dim: Nat) {
    // |ψ(t)⟩ = e^(-iĤt/ℏ) |ψ(0)⟩
    operation evolve : Operator(dim, ℂ) → ℝ → Ket(dim, ℂ) → Ket(dim, ℂ)
    operation propagator : Operator(dim, ℂ) → ℝ → Operator(dim, ℂ)
}

Cosmology

The cosmology.kleis module defines standard spacetimes.

Minkowski (Flat Space)

structure MinkowskiSpacetime {
    operation g : Nat → Nat → ℝ
    
    // All curvature vanishes
    axiom minkowski_ricci_vanish : ∀ mu nu : Nat . Ric(mu, nu) = 0
    axiom minkowski_einstein_vanish : ∀ mu nu : Nat . G(mu, nu) = 0
}

de Sitter (Accelerating Universe)

structure DeSitterSpacetime {
    operation g : Nat → Nat → ℝ
    operation G : Nat → Nat → ℝ
    element Lambda : ℝ
    
    axiom positive_lambda : Lambda = 1  // Λ > 0
    
    // Vacuum: G_μν = -Λg_μν
    axiom desitter_einstein : ∀ mu nu : Nat .
        G(mu, nu) = negate(times(Lambda, g(mu, nu)))
}

Schwarzschild (Black Hole)

structure SchwarzschildSpacetime {
    operation g : Nat → Nat → ℝ
    operation G : Nat → Nat → ℝ
    element M : ℝ  // Black hole mass
    
    // Vacuum with Λ=0
    axiom schwarzschild_vacuum : ∀ mu nu : Nat . G(mu, nu) = 0
}

See the Cartan Geometry appendix for computing the actual Schwarzschild curvature tensor.

FLRW (Cosmology)

structure FLRWCosmology {
    operation g : Nat → Nat → ℝ
    operation T : Nat → Nat → ℝ  // Stress-energy (perfect fluid)
    
    element Lambda : ℝ   // Cosmological constant
    element rho : ℝ      // Energy density
    element p : ℝ        // Pressure
    
    // Perfect fluid: T_00 = ρ
    axiom perfect_fluid_energy : T(0, 0) = rho
    
    // Einstein field equations
    axiom field_equations : ∀ mu nu : Nat .
        plus(G(mu, nu), times(Lambda, g(mu, nu))) = times(kappa, T(mu, nu))
}

Differential Forms

The differential_forms.kleis module provides Cartan calculus:

// Wedge product: α ∧ β
structure WedgeProduct(p: Nat, q: Nat, dim: Nat) {
    operation wedge : DifferentialForm(p, dim) → DifferentialForm(q, dim) 
                    → DifferentialForm(p + q, dim)
    
    axiom graded_antisymmetric : ∀ α β .
        wedge(α, β) = scale(power(-1, p*q), wedge(β, α))
}

// Exterior derivative: dα
structure ExteriorDerivative(p: Nat, dim: Nat) {
    operation d : DifferentialForm(p, dim) → DifferentialForm(p + 1, dim)
    
    axiom d_squared_zero : ∀ α . d(d(α)) = 0  // d² = 0
}

// Hodge star: ⋆α
structure HodgeStar(p: Nat, dim: Nat) {
    operation star : DifferentialForm(p, dim) → DifferentialForm(dim - p, dim)
    
    axiom hodge_involutive : ∀ α .
        star(star(α)) = scale(power(-1, p*(dim-p)), α)
}

Cartan’s Magic Formula

The Lie derivative ℒ_X connects all operations:

// ℒ_X = d ∘ ι_X + ι_X ∘ d
define cartan_magic_impl(X, alpha) = 
    plus(d(interior(X, alpha)), interior(X, d(alpha)))

What’s Next

Apply these physics structures with numerical methods:

→ Next: Control Systems

Control Systems

Kleis provides a complete control systems toolkit: state-space modeling, LQR/LQG design, ODE integration, and stability analysis.

State-Space Representation

A linear time-invariant (LTI) system is represented as:

ẋ = Ax + Bu    (state equation)
y = Cx + Du    (output equation)

In Kleis:

// State vector x = [x₁, x₂, ..., xₙ]
// Input vector u = [u₁, u₂, ..., uₘ]
// Output vector y = [y₁, y₂, ..., yₚ]

let A = [[a11, a12], [a21, a22]] in  // n×n state matrix
let B = [[b11], [b21]] in             // n×m input matrix
let C = [[c11, c12]] in               // p×n output matrix
let D = [[0]] in                      // p×m feedthrough matrix

Eigenvalue Analysis

System stability depends on eigenvalues of the A matrix:

example "stability check" {
    let A = [[-1, 2], [0, -3]] in
    let eigs = eigenvalues(A) in
    out("Eigenvalues:", eigs)
    // If all real parts < 0, system is stable
}

Linear Quadratic Regulator (LQR)

LQR finds the optimal feedback gain K that minimizes:

J = ∫₀^∞ (x'Qx + u'Ru) dt

Continuous-Time LQR

example "continuous LQR" {
    // Double integrator: ẍ = u
    let A = [[0, 1], [0, 0]] in
    let B = [[0], [1]] in
    
    // Cost matrices
    let Q = [[10, 0], [0, 1]] in  // State cost
    let R = [[1]] in               // Control cost
    
    // Compute optimal gain K and Riccati solution P
    let result = lqr(A, B, Q, R) in
    let K = nth(result, 0) in
    let P = nth(result, 1) in
    
    out("Feedback gain K:", K)
    out("Riccati solution P:", P)
    
    // Closed-loop: ẋ = (A - BK)x
    let A_cl = matrix_sub(A, matmul(B, K)) in
    out("Closed-loop eigenvalues:", eigenvalues(A_cl))
}

The CARE Solver

LQR requires solving the Continuous Algebraic Riccati Equation (CARE):

A'P + PA - PBR⁻¹B'P + Q = 0

Kleis uses the Schur method via LAPACK:

let P = care(A, B, Q, R) in   // Solve CARE for P
let K = lqr(A, B, Q, R) in    // Returns [K, P]

Discrete-Time Control

Discretization

Convert continuous-time to discrete-time with sampling period Ts:

let ts = 0.05 in  // 20 Hz sample rate

// Exact discretization: A_d = e^(A·Ts)
let A_disc = expm(scalar_matrix_mul(ts, A_cont)) in

// First-order approximation: B_d ≈ Ts·B
let B_disc = scalar_matrix_mul(ts, B_cont) in

Discrete LQR (DLQR)

For discrete-time systems xₖ₊₁ = Aₓₖ + Buₖ:

example "discrete LQR" {
    let ts = 0.05 in
    
    // Continuous system
    let A_cont = [[0, 1], [10, 0]] in  // Inverted pendulum
    let B_cont = [[0], [1]] in
    
    // Discretize
    let A_disc = expm(scalar_matrix_mul(ts, A_cont)) in
    let B_disc = scalar_matrix_mul(ts, B_cont) in
    
    // Cost matrices
    let Q = [[10, 0], [0, 1]] in
    let R = [[1]] in
    
    // Compute discrete optimal gain
    let result = dlqr(A_disc, B_disc, Q, R) in
    let K = nth(result, 0) in
    
    out("Discrete feedback gain:", K)
}

The DARE Solver

DLQR requires solving the Discrete Algebraic Riccati Equation (DARE):

A'PA - P - (A'PB)(B'PB + R)⁻¹(B'PA) + Q = 0

let P = dare(A, B, Q, R) in    // Solve DARE for P
let K = dlqr(A, B, Q, R) in    // Returns [K, P]

ODE Integration

The ode45 function integrates ODEs using the Dormand-Prince 5(4) method:

let result = ode45(dynamics, t_span, y0, dt)

Example: Inverted Pendulum

example "inverted pendulum with LQR" {
    // System parameters
    let g = 9.81 in
    let ell = 1.0 in
    
    // Linearized system (about upright equilibrium)
    let A = [[0, 1], [g/ell, 0]] in
    let B = [[0], [1/ell]] in
    
    // LQR design
    let Q = [[10, 0], [0, 1]] in
    let R = [[0.1]] in
    let result = lqr(A, B, Q, R) in
    let K = nth(result, 0) in
    let k1 = nth(nth(K, 0), 0) in
    let k2 = nth(nth(K, 0), 1) in
    
    // Nonlinear dynamics with control
    let dynamics = lambda t y .
        let theta = nth(y, 0) in
        let omega = nth(y, 1) in
        let u = neg(k1*theta + k2*omega) in
        [omega, (g/ell)*sin(theta) + u/ell]
    in
    
    // Simulate from initial angle
    let t_span = [0, 5] in
    let y0 = [0.2, 0] in  // 0.2 rad initial tilt
    let dt = 0.05 in
    
    let result = ode45(dynamics, t_span, y0, dt) in
    let times = nth(result, 0) in
    let states = nth(result, 1) in
    
    // Extract theta trajectory
    let thetas = list_map(lambda s . nth(s, 0), states) in
    
    diagram(
        plot(
            line(times, thetas, color = "blue", label = "θ (rad)"),
            xlabel = "Time (s)",
            ylabel = "Angle",
            title = "Inverted Pendulum Stabilization"
        )
    )
}

Complete Example: Pendulum Stabilization

Here’s a full control system design workflow:

import "stdlib/matrices.kleis"

example "pendulum control design" {
    // Physical parameters
    let g = 9.81 in
    let ell = 1.0 in
    
    // Step 1: State-space model
    // State: [θ, ω] where θ is angle from vertical, ω is angular velocity
    // Input: u = cart acceleration
    // ẋ = Ax + Bu
    let A = [[0, 1], [g/ell, 0]] in
    let B = [[0], [neg(1/ell)]] in
    
    // Step 2: Check controllability
    // The system is controllable if rank([B, AB]) = n
    out("A matrix:", A)
    out("B matrix:", B)
    
    // Step 3: Check open-loop stability
    let open_loop_eigs = eigenvalues(A) in
    out("Open-loop eigenvalues:", open_loop_eigs)
    // One eigenvalue is positive → unstable!
    
    // Step 4: LQR design
    let Q = [[10, 0], [0, 1]] in   // Penalize angle more than velocity
    let R = [[0.1]] in              // Cheap control
    
    let lqr_result = lqr(A, B, Q, R) in
    let K = nth(lqr_result, 0) in
    let k1 = nth(nth(K, 0), 0) in
    let k2 = nth(nth(K, 0), 1) in
    
    out("LQR gain K:", K)
    
    // Step 5: Check closed-loop stability
    let A_cl = matrix_sub(A, matmul(B, K)) in
    let closed_loop_eigs = eigenvalues(A_cl) in
    out("Closed-loop eigenvalues:", closed_loop_eigs)
    // All eigenvalues have negative real parts → stable!
    
    // Step 6: Simulate
    let dynamics = lambda t y .
        let theta = nth(y, 0) in
        let omega = nth(y, 1) in
        let u = neg(k1*theta + k2*omega) in
        [omega, (g/ell)*sin(theta) + u/ell]
    in
    
    let result = ode45(dynamics, [0, 5], [0.2, 0], 0.05) in
    let times = nth(result, 0) in
    let states = nth(result, 1) in
    
    let thetas = list_map(lambda s . nth(s, 0), states) in
    let omegas = list_map(lambda s . nth(s, 1), states) in
    let controls = list_map(lambda s . neg(k1*nth(s, 0) + k2*nth(s, 1)), states) in
    
    // Step 7: Plot results
    diagram(
        plot(
            line(times, thetas, color = "blue", label = "θ (rad)"),
            line(times, omegas, color = "red", label = "ω (rad/s)"),
            line(times, controls, color = "green", label = "u (m/s²)"),
            xlabel = "Time (s)",
            ylabel = "State / Control",
            title = "Inverted Pendulum LQR Control",
            legend = "right + bottom",
            width = 14,
            height = 8
        )
    )
}

Digital Control

For digital (discrete-time) control with zero-order hold:

example "digital pendulum control" {
    let ts = 0.05 in  // 20 Hz sampling
    
    // Continuous system
    let A_cont = [[0, 1], [9.81, 0]] in
    let B_cont = [[0], [neg(1)]] in
    
    // Discretize
    let A_disc = expm(scalar_matrix_mul(ts, A_cont)) in
    let B_disc = scalar_matrix_mul(ts, B_cont) in
    
    // Discrete LQR
    let Q = [[10, 0], [0, 1]] in
    let R = [[1]] in
    let result = dlqr(A_disc, B_disc, Q, R) in
    let K = nth(result, 0) in
    
    out("Discrete gain K:", K)
    
    // Verify discrete stability
    let A_cl = matrix_sub(A_disc, matmul(B_disc, K)) in
    let eigs = eigenvalues(A_cl) in
    out("Closed-loop eigenvalues:", eigs)
    // All eigenvalues should be inside unit circle
}

Stability Verification with Z3

Verify control system properties formally:

structure StabilityProperties {
    // Continuous-time: eigenvalues have negative real parts
    axiom hurwitz_stability : ∀ λ : ℂ . 
        is_eigenvalue(A, λ) → re(λ) < 0
    
    // Discrete-time: eigenvalues inside unit circle
    axiom schur_stability : ∀ λ : ℂ .
        is_eigenvalue(A_d, λ) → abs_squared(λ) < 1
    
    // Lyapunov stability: ∃ P > 0 such that A'P + PA < 0
    axiom lyapunov_continuous : ∃ P : Matrix(n, n, ℝ) .
        positive_definite(P) ∧ 
        negative_definite(plus(matmul(transpose(A), P), matmul(P, A)))
}

LAPACK Functions Reference

See LAPACK Functions appendix for complete documentation.

What’s Next

Explore more examples:

→ ODE Solver appendix — detailed ode45 documentation
→ LAPACK Functions — numerical linear algebra
→ Cartan Geometry — differential geometry

Appendix A: Grammar Reference

This appendix provides a reference to Kleis syntax based on the formal grammar specification (v0.97).

Complete Grammar: See vscode-kleis/docs/grammar/kleis_grammar_v097.md for the full specification.

v0.97 (Jan 2026): Added and, or, not as ASCII equivalents for ∧, ∨, ¬.

Program Structure

program ::= { declaration }

declaration ::= importDecl              // v0.8: Module imports
              | libraryAnnotation
              | versionAnnotation
              | structureDef
              | implementsDef
              | dataDef
              | functionDef
              | operationDecl
              | typeAlias
              | exampleBlock            // v0.93: Executable documentation

Import Statements (v0.8)

importDecl ::= "import" string

Example:

import "stdlib/prelude.kleis"
import "stdlib/complex.kleis"

Annotations

libraryAnnotation ::= "@library" "(" string ")"
versionAnnotation ::= "@version" "(" string ")"

Example:

@library("stdlib/algebra")
@version("0.7")

Data Type Definitions

dataDef ::= "data" identifier [ "(" typeParams ")" ] "="
            dataVariant { "|" dataVariant }

dataVariant ::= identifier [ "(" dataFields ")" ]

dataField ::= identifier ":" type    // Named field
            | type                   // Positional field

Examples:

data Bool = True | False

data Option(T) = None | Some(value : T)

Pattern Matching

matchExpr ::= "match" expression "{" matchCases "}"

matchCase ::= pattern [ "if" guardExpression ] "=>" expression   // v0.8: guards

pattern ::= basePattern [ "as" identifier ]  // v0.8: as-patterns

basePattern ::= "_"                              // Wildcard
              | identifier                       // Variable
              | identifier [ "(" patternArgs ")" ]  // Constructor
              | number | string | boolean        // Constant
              | tuplePattern                     // v0.8: Tuple sugar

tuplePattern ::= "()"                            // Unit
               | "(" pattern "," pattern { "," pattern } ")"  // Pair, Tuple3, etc.

Examples:

match x { True => 1 | False => 0 }
match opt { None => 0 | Some(x) => x }
match result { Ok(Some(x)) => x | Ok(None) => 0 | Err(_) => -1 }

// v0.8: Pattern guards
match n { x if x < 0 => "negative" | x if x > 0 => "positive" | _ => "zero" }

// v0.8: As-patterns
match list { Cons(h, t) as whole => process(whole) | Nil => empty }

Structure Definitions

structureDef ::= "structure" identifier "(" typeParams ")"
                 [ extendsClause ] [ overClause ]
                 "{" { structureMember } "}"

extendsClause ::= "extends" identifier [ "(" typeArgs ")" ]
overClause ::= "over" "Field" "(" type ")"

structureMember ::= operationDecl
                  | elementDecl
                  | axiomDecl
                  | nestedStructure
                  | functionDef

Example (aspirational - over and extends not yet implemented):

structure VectorSpace(V) over Field(F) extends AbelianGroup(V) {
    operation (·) : F × V → V
    
    axiom scalar_distributive : ∀(a : F)(b : F)(v : V).
        (a + b) · v = a · v + b · v
}

Implements

implementsDef ::= "implements" identifier "(" typeArgs ")"
                  [ overClause ]
                  [ "{" { implMember } "}" ]

implMember ::= elementImpl | operationImpl | verifyStmt

operationImpl ::= "operation" operatorSymbol "=" implementation
                | "operation" operatorSymbol "(" params ")" "=" expression

Example:

implements Ring(ℝ) {
    operation add = builtin_add
    operation mul = builtin_mul
    element zero = 0
    element one = 1
}

Function Definitions

functionDef ::= "define" identifier [ typeAnnotation ] "=" expression
              | "define" identifier "(" params ")" [ ":" type ] "=" expression

param ::= identifier [ ":" type ]

Examples:

define pi = 3.14159
define square(x) = x * x
define add(x: ℝ, y: ℝ) : ℝ = x + y

Type System

type ::= primitiveType
       | parametricType
       | functionType
       | typeVariable
       | "(" type ")"

primitiveType ::= "ℝ" | "ℂ" | "ℤ" | "ℕ" | "ℚ"
                | "Real" | "Complex" | "Integer" | "Nat" | "Rational"
                | "Bool" | "String" | "Unit"

parametricType ::= identifier "(" typeArgs ")"
                 | "BitVec" "(" number ")"      // Fixed-size bit vectors

functionType ::= type "→" type | type "->" type

typeAlias ::= "type" identifier "=" type

Examples:

ℝ                    // Real numbers
Vector(3)            // Parameterized type
ℝ → ℝ               // Function type
(ℝ → ℝ) → ℝ         // Higher-order function
type RealFunc = ℝ → ℝ  // Type alias

Expressions

expression ::= primary
             | matchExpr
             | prefixOp expression
             | expression postfixOp
             | expression infixOp expression
             | expression "(" [ arguments ] ")"
             | "[" [ expressions ] "]"           // List literal
             | lambda
             | letBinding
             | conditional

primary ::= identifier | number | string
          | "(" expression ")"

// Note: Greek letters (π, φ, etc.) are valid identifiers, not special constants.
// Use import "stdlib/prelude.kleis" for predefined constants like pi, e, i.

Lambda Expressions

lambda ::= "λ" params "." expression
         | "lambda" params "." expression

Examples:

λ x . x + 1              // Simple lambda
λ x y . x * y            // Multiple parameters
λ (x : ℝ) . x^2          // With type annotation
lambda x . x             // Using keyword

Let Bindings

letBinding ::= "let" pattern [ typeAnnotation ] "=" expression "in" expression
// Note: typeAnnotation only valid when pattern is a simple Variable

Examples:

let x = 5 in x + x
let x : ℝ = 3.14 in x * 2
let s = (a + b + c) / 2 in sqrt(s * (s-a) * (s-b) * (s-c))

// v0.8: Let destructuring
let Point(x, y) = origin in x^2 + y^2
let Some(Pair(a, b)) = opt in a + b
let Cons(h, _) = list in h

Conditionals

conditional ::= "if" expression "then" expression "else" expression

Example:

if x > 0 then x else -x

Quantifiers

forAllProp ::= ("∀" | "forall") variables [ whereClause ] "." proposition
existsProp ::= ("∃" | "exists") variables [ whereClause ] "." proposition

varDecl ::= identifier [ ":" type ]
          | "(" identifier { identifier } ":" type ")"

// Note: "x ∈ type" syntax is NOT implemented. Use "x : type" instead.

whereClause ::= "where" expression

Examples:

∀(x : ℝ). x + 0 = x
∃(x : ℤ). x * x = 4
∀(a : ℝ)(b : ℝ) where a ≠ 0 . a * (1/a) = 1

v0.9 Enhancements

Nested Quantifiers in Expressions

Quantifiers can now appear as operands in logical expressions:

// v0.9: Quantifier inside conjunction
axiom nested: (x > 0) ∧ (∀(y : ℝ). y > 0)

// Epsilon-delta limit definition
axiom epsilon_delta: ∀(ε : ℝ). ε > 0 → 
    (∃(δ : ℝ). δ > 0 ∧ (∀(x : ℝ). abs(x - a) < δ → abs(f(x) - L) < ε))

Function Types in Type Annotations

Function types are now allowed in quantifier variable declarations:

// Function from reals to reals
axiom func: ∀(f : ℝ → ℝ). f(0) = f(0)

// Higher-order function
axiom compose: ∀(f : ℝ → ℝ, g : ℝ → ℝ). compose(f, g) = λ x . f(g(x))

// Topology: continuity via preimages
axiom continuity: ∀(f : X → Y, V : Set(Y)). 
    is_open(V) → is_open(preimage(f, V))

v0.95 Big Operators

Big operators (Σ, Π, ∫, lim) can be used with function call syntax:

bigOpExpr ::= "Σ" "(" expr "," expr "," expr ")"
            | "Π" "(" expr "," expr "," expr ")"
            | "∫" "(" expr "," expr "," expr "," expr ")"
            | "lim" "(" expr "," expr "," expr ")"
            | ("Σ" | "Π" | "∫") primaryExpr      // prefix form

Summation: Σ

// Sum of f(i) from 1 to n
Σ(1, n, λ i . f(i))

// Parsed as: sum_bounds(λ i . f(i), 1, n)

Product: Π

// Product of g(i) from 1 to n
Π(1, n, λ i . g(i))

// Parsed as: prod_bounds(λ i . g(i), 1, n)

Integral: ∫

// Integral of x² from 0 to 1
∫(0, 1, λ x . x * x, x)

// Parsed as: int_bounds(λ x . x * x, 0, 1, x)

Limit: lim

// Limit of sin(x)/x as x approaches 0
lim(x, 0, sin(x) / x)

// Parsed as: lim(sin(x) / x, x, 0)

Prefix Forms

Simple prefix forms are also supported:

Σf        // Parsed as: Sum(f)
∫g        // Parsed as: Integrate(g)

Calculus Notation (v0.7)

Kleis uses Mathematica-style notation for calculus operations:

// Derivatives (function calls)
D(f, x)              // Partial derivative ∂f/∂x
D(f, x, y)           // Mixed partial ∂²f/∂x∂y
D(f, {x, n})         // nth derivative ∂ⁿf/∂xⁿ
Dt(f, x)             // Total derivative df/dx

// Integrals
Integrate(f, x)           // Indefinite ∫f dx
Integrate(f, x, a, b)     // Definite ∫[a,b] f dx

// Sums and Products
Sum(expr, i, 1, n)        // Σᵢ₌₁ⁿ expr
Product(expr, i, 1, n)    // Πᵢ₌₁ⁿ expr

// Limits
Limit(f, x, a)            // lim_{x→a} f

Derivatives use function call syntax: D(f, x) for partial derivatives and Dt(f, x) for total derivatives.

Operators

Prefix Operators

prefixOp ::= "-" | "¬" | "∇" | "∫" | "∬" | "∭" | "∮" | "∯"

Note: √ is NOT a prefix operator. Use sqrt(x) function instead.

Postfix Operators

postfixOp ::= "!" | "ᵀ" | "^T" | "†"

Note: * (conjugate) and ^† are NOT implemented as postfix operators.

Infix Operators (by precedence, low to high)

Note (v0.97): and, or, not now work as ASCII equivalents for ∧, ∨, ¬ in all expression contexts.

Note: Set operators use function-call syntax:

• x ∈ S → in_set(x, S)
• x ∉ S → ¬in_set(x, S)
• A ⊆ B → subset(A, B)
• A ⊂ B → proper_subset(A, B)
• ≈ and ≡ are not implemented

Comments

lineComment ::= "//" { any character except newline } newline
blockComment ::= "/*" { any character } "*/"

Note: Kleis uses C-style comments (// and /* */), not Haskell-style (-- and {- -}).

Unicode and ASCII Equivalents

Note: * is the multiplication operator in expressions, not an ASCII equivalent for × in product types. Use Unicode × for product types like Int × Int → Int.

Note: Greek letters like π, α, β are valid identifiers. Use import "stdlib/prelude.kleis" for common constants like pi.

Note (v0.97): and, or, not are now reserved keywords and work in all expression contexts, including axioms, assertions, and function bodies.

Lexical Elements

identifier ::= letter { letter | digit | "_" }

number ::= integer | decimal | scientific
integer ::= digit { digit }
decimal ::= digit { digit } "." { digit }
scientific ::= decimal ("e" | "E") ["+"|"-"] digit { digit }

string ::= '"' { character } '"'

letter ::= "a".."z" | "A".."Z" | greekLetter
digit ::= "0".."9"

greekLower ::= "α" | "β" | "γ" | "δ" | "ε" | "ζ" | "η" | "θ"
             | "ι" | "κ" | "λ" | "μ" | "ν" | "ξ" | "ο" | "π"
             | "ρ" | "σ" | "τ" | "υ" | "φ" | "χ" | "ψ" | "ω"

Appendix: Operators

This appendix covers all operators in the Kleis language. For built-in functions, see Built-in Functions. For numerical linear algebra, see LAPACK Functions.

Arithmetic Operators

Comparison Operators

Logical Operators

Note: All Unicode variants for implication (→, ⇒, ⟹) and biconditional (↔, ⇔, ⟺) are equivalent.

Postfix Operators

Prefix Operators

Big Operators (v0.95)

Kleis supports big operator syntax for summations, products, integrals, and limits:

Examples

// Sum from i=1 to n
Σ(1, n, i^2)

// Product from k=1 to 5
Π(1, 5, k)

// Integral from 0 to 1
∫(0, 1, x^2, x)

// Limit as x approaches 0
lim(x, 0, sin(x)/x)

Custom Mathematical Operators

Kleis recognizes many Unicode mathematical symbols as infix binary operators. These can be used directly in expressions like a • b.

Complete Operator Table

These operators are syntactic only — they are parsed as infix operators but have no built-in semantics. They remain symbolic: 2 • 3 evaluates to •(2, 3), not a number.

These operators cannot be used for computation. Kleis does not connect • to any function — u • v will always stay symbolic as •(u, v).

To compute, use a named function instead: define dot(u, v) and call it directly. The • operator is only useful for notation in axioms.

Important: These operators do NOT compute values. 2 • 3 returns •(2, 3) symbolically. To give them meaning, define functions and use those instead.

What They Actually Do

These operators are parsed but stay symbolic:

λ> :eval 2 • 3
✅ •(2, 3)      ← NOT computed to 6!

λ> :eval A ⊗ B
✅ ⊗(A, B)      ← stays symbolic

When to Use Them

Use these operators in axioms and symbolic expressions where you want readable mathematical notation:

structure VectorSpace(V) {
    // Use • for notation in axioms
    axiom symmetric : ∀(u : V)(v : V). u • v = v • u
    axiom bilinear : ∀(a : ℝ)(u : V)(v : V). (a * u) • v = a * (u • v)
}

For Actual Computation

If you need operators that compute values, use:

1. Built-in operators: +, -, *, /, ^
2. Function calls: dot(u, v), tensor(A, B), union(s1, s2)

// These compute actual values:
define sum = 2 + 3           // → 5
define product = times(4, 5)  // → 20

// These stay symbolic (for axioms):
define symbolic = a • b      // → •(a, b)

Type Operators