Appendix A: Grammar Reference

This appendix provides a reference to Kleis syntax based on the formal grammar specification (v1.00).

Complete Grammar: See docs/grammar/kleis_grammar_v100.ebnf for the full EBNF specification.

v1.00 (May 2026): Full convergence audit against kleis_parser.rs. Added type ascription, tuples, product/forall types, dimension expressions, custom operators (30 Unicode symbols), named arguments, list patterns, set literals, -> implication, ^T/^† postfix, generic annotations, kind annotations, verify statements, where clauses. See the EBNF file for complete version history.

Program Structure

program ::= { [ annotation ] declaration }

declaration ::= importDecl              // v0.8: Module imports
              | 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

annotation ::= "@" identifier [ "(" balancedContent ")" ]

The parser accepts any @name(...) annotation and skips it. Common annotations:

• @library("stdlib/algebra") — marks library membership
• @version("0.7") — marks version

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

matchCases ::= matchCase { [ "|" ] matchCase }   // "|" separator is optional

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
              | listPattern                      // v0.98: List sugar

tuplePattern ::= "()"                            // Unit
               | "(" pattern "," pattern { "," pattern } ")"  // Pair, Tuple3, etc.

listPattern ::= "[" [ pattern { "," pattern } ] "]"   // Desugars to Cons/Nil

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

typeParam ::= identifier [ ":" kindExpr ]   // e.g., T, N: Nat, F: Type → Type

extendsClause ::= "extends" identifier [ "(" typeArgs ")" ]
overClause ::= "over" identifier [ "(" typeArgs ")" ]

structureMember ::= operationDecl
                  | elementDecl
                  | axiomDecl
                  | nestedStructure
                  | functionDef
                  | fieldDecl

elementDecl ::= "element" identifier ":" type
axiomDecl ::= "axiom" identifier ":" proposition
nestedStructure ::= "structure" identifier ":" type [ "{" { structureMember } "}" ]
fieldDecl ::= identifier ":" type

Note: The extends and over clauses may appear in either order. Both structure Foo(X) extends Bar(X) over Baz(Y) and structure Foo(X) over Baz(Y) extends Bar(X) are valid.

Example:

structure VectorSpace(V) extends AbelianGroup(V) over Field(F) {
    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 ] [ whereClause ]
                  "{" { implMember } "}"

whereClause ::= "where" constraint { "," constraint }
constraint ::= identifier "(" typeArgs ")"   // e.g., Field(ℝ), Ord(T)

implMember ::= elementImpl | operationImpl | verifyStmt

elementImpl ::= "element" identifier "=" expression

operationImpl ::= "operation" operatorName "=" expression
                | "operation" operatorName "(" params ")" "=" expression

verifyStmt ::= "verify" identifier     // Verify a named axiom from the structure

Example:

implements Ring(ℝ) {
    operation add = builtin_add
    operation mul = builtin_mul
    element zero = 0
    element one = 1
}

Function Definitions

functionDef ::= "define" operatorName [ ":" type ] "=" expression
              | "define" operatorName "(" params ")" [ ":" type ] "=" expression

param ::= identifier [ ":" type ]

Examples:

define pi = 3.14159
define square(x) = x * x
define add(x: ℝ, y: ℝ) : ℝ = x + y

Operation Declarations

operationDecl ::= "operation" operatorName ":" type

operatorName ::= identifier
               | "(" operatorSymbol ")"   // e.g., (+), (×), (⊗)

operatorSymbol ::= "+" | "-" | "*" | "/" | "^" | "×" | "·" | "•"
                 | "=" | "<" | ">" | "≤" | "≥" | "≠"
                 | "∧" | "∨" | "¬" | "⟹"
                 | "∘" | "⊗" | "⊕" | "⊙"

Operation declarations appear at top level or inside structures to declare typed operations without implementation.

Example Blocks (v0.93)

exampleBlock ::= "example" string "{" { exampleStatement } "}"

exampleStatement ::= exampleLet
                   | exampleAssert
                   | expression [ ";" ]

exampleLet ::= "let" identifier ":" type "=" expression     // Typed with value
             | "let" identifier ":" type                     // Symbolic (no value)
             | "let" identifier "=" expression               // Untyped

exampleAssert ::= "assert" "(" expression ")"    // Expression must be equality/comparison

Example:

example "arithmetic" {
    let x = 2 + 3
    assert(x = 5)
}

Type System

type ::= forallType
       | functionType
       | productType
       | simpleType

simpleType ::= primitiveType
             | parametricType
             | typeVariable
             | "(" type ")"
             | "(" type "," type { "," type } ")"   // Tuple type

primitiveType ::= "ℝ" | "ℂ" | "ℤ" | "ℕ" | "ℚ"
                | "Real" | "Complex" | "Int" | "Integer"
                | "Nat" | "Natural" | "Rational"
                | "Bool" | "String" | "Unit"

parametricType ::= identifier "(" typeArgs ")"
                 | "BitVec" "(" number ")"      // Fixed-size bit vectors

functionType ::= productType "→" functionType   // Right-associative
               | productType "->" functionType

productType ::= simpleType "×" productType      // Right-associative
              | simpleType

forallType ::= ("∀" | "forall") "(" typeParams ")" "." type

typeAlias ::= "type" identifier [ "(" typeAliasParams ")" ] "=" type

typeAliasParam ::= identifier [ ":" kindExpr ]
kindExpr ::= kindAtom [ ("→" | "->") kindExpr ]   // Right-associative
kindAtom ::= "Type" | "Nat" | "String" | "(" kindExpr ")"

Type arguments can include dimension expressions: Matrix(m+1, n*2, T) where arithmetic in type positions is parsed as dimension expressions.

Examples:

ℝ                    // Real numbers
Vector(3)            // Parameterized type
ℝ → ℝ               // Function type
(ℝ → ℝ) → ℝ         // Higher-order function
ℝ × ℝ               // Product type
(ℝ, ℝ, ℝ)           // Tuple type (desugars to Product)
∀(n : ℕ). Vector(n) → ℝ  // Forall type (dependent)
Matrix(m+1, n*2, ℝ)  // Dimension expressions in type args
type RealFunc = ℝ → ℝ  // Type alias
type Functor(F: Type → Type) = F  // With kind annotation

Expressions

expression ::= primary
             | matchExpr
             | prefixOp expression
             | expression postfixOp
             | expression infixOp expression
             | expression "(" [ arguments ] ")"
             | "[" [ expressions ] "]"           // List literal
             | "{" [ expressions ] "}"           // Set literal
             | "()"                              // Unit
             | "(" expression "," expression { "," expression } ")"  // Tuple
             | expression ":" type               // Type ascription
             | lambda
             | letBinding
             | conditional

primary ::= identifier | number | string
          | "(" expression ")"

arguments ::= positionalArgs [ "," namedArgs ]
            | namedArgs
positionalArgs ::= expression { "," expression }
namedArgs ::= namedArg { "," namedArg }
namedArg ::= identifier "=" expression   // Named argument (key = value)

// Note: Greek letters (π, φ, etc.) are valid identifiers, not special constants.
// Use import "stdlib/prelude.kleis" for predefined constants like pi, e, i.

Tuple expressions desugar: (a, b) → Pair(a, b), (a, b, c) → Tuple3(a, b, c), (a, b, c, d) → Tuple4(a, b, c, d).

Named arguments desugar into a record(field("key", value), ...) appended to positional args.

Lambda Expressions

lambda ::= ("λ" | "lambda") lambdaParams "." expression

lambdaParam ::= identifier                      // Untyped: x
              | "(" identifier ":" type ")"     // Typed: (x : ℝ)
lambdaParams ::= lambdaParam { lambdaParam }    // One or more

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") varGroups [ whereClause ] "." proposition
existsProp ::= ("∃" | "exists") varGroups [ whereClause ] "." proposition

varGroups ::= varGroup { varGroup }             // Multiple groups can be chained
varGroup ::= "(" varDecls ")"                   // e.g., (x y z : ℝ)

varDecls ::= varDecl { "," varDecl }            // Comma-separated type groups
varDecl ::= identifier { identifier } ":" type  // e.g., x y z : ℝ or f : ℝ → ℝ

// 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
∀(x y z : ℝ). (x + y) + z = x + (y + z)
∀(f : ℝ → ℝ, g : ℝ → ℝ). compose(f, g) = λ x . f(g(x))

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
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 ::= "-" | "¬" | "not" | "∇" | "∫" | "∬" | "∭" | "∮" | "∯"

Note: √ is NOT a prefix operator. Use sqrt(x) function instead.

Postfix Operators

postfixOp ::= "!" | "ᵀ" | "†" | "^T" | "^†"

Note: ^T is an ASCII equivalent of Unicode ᵀ (transpose). It is recognized only when T is not part of a longer identifier (e.g., A^T is transpose, but A^Tensor is exponentiation). Similarly, ^† is the ASCII form of the dagger operator.

Note: * (conjugate) is NOT implemented as a postfix operator.

Custom Infix Operators

customOp ::= "•" | "∘" | "∗" | "⋆" | "⊗" | "⊕" | "⊙" | "⊛" | "⊘" | "⊚"
           | "⊝" | "⊞" | "⊟" | "⊠" | "⊡" | "⨀" | "⨁" | "⨂" | "⨃" | "⨄"
           | "⊓" | "⊔" | "⊎" | "⊍" | "∪" | "∩" | "⋃" | "⋂" | "△" | "▽"

These Unicode math symbols are parsed as binary infix operators at arithmetic precedence (level 7). Their semantics are defined by operation declarations in structures.

Infix Operators (by precedence, low to high)

Note (v0.97): and, or, not now work as ASCII equivalents for ∧, ∨, ¬ in all expression contexts.

Note: -> works as ASCII equivalent of → for implication in both expressions and type annotations.

Note: Set operators work as both infix and function calls:

• x ∈ S or in_set(x, S) for membership
• x ∉ S or not_in_set(x, S) for non-membership
• A ⊆ B or subset(A, B) for subset
• A ⊂ B or proper_subset(A, B) for proper subset
• A ⊇ B or superset(A, B) for superset
• A ⊃ B or proper_superset(A, B) for proper superset

Note: Custom Unicode math operators (•, ∘, ⊗, ⊕, ⊙, ⊛, ⊘, ⊚, ⊝, ⊞, ⊟, ⊠, ⊡, ⨀, ⨁, ⨂, ⨃, ⨄, ⊓, ⊔, ⊎, ⊍, ∪, ∩, ⋃, ⋂, △, ▽) are parsed as binary infix operators at arithmetic precedence. Their semantics come from operation declarations in structures.

Note: ≈ and ≡ are not yet implemented as operators.

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 ::= '"' { stringChar } '"'
stringChar ::= escapeSeq | anyCharExceptQuoteOrBackslash
escapeSeq ::= "\\" ("n" | "t" | '"' | "\\")

letter ::= "a".."z" | "A".."Z" | greekLetter | unicodeAlphabetic
digit ::= "0".."9"

greekLower ::= "α" | "β" | "γ" | "δ" | "ε" | "ζ" | "η" | "θ"
             | "ι" | "κ" | "λ" | "μ" | "ν" | "ξ" | "ο" | "π"
             | "ρ" | "σ" | "τ" | "υ" | "φ" | "χ" | "ψ" | "ω"

greekUpper ::= "Α" | "Β" | "Γ" | "Δ" | "Ε" | "Ζ" | "Η" | "Θ"
             | "Ι" | "Κ" | "Λ" | "Μ" | "Ν" | "Ξ" | "Ο"
             | "Ρ" | "Τ" | "Υ" | "Φ" | "Χ" | "Ψ" | "Ω"
// Note: Σ and Π are reserved for big operators (sum, product)

greekLetter ::= greekLower | greekUpper