Keyboard shortcuts

Press ← or → to navigate between chapters

Press S or / to search in the book

Press ? to show this help

Press Esc to hide this help

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

OperatorUnicodeNameExampleResult
+Addition3 + 47
-Subtraction10 - 37
*×Multiplication6 × 742
/÷Division15 / 35
^Exponentiation2 ^ 101024
- (unary)Negation-5-5
·Dot producta · bscalar

Comparison Operators

OperatorUnicodeNameExample
=Equalityx = y
==Equality (alt)x == y
!=≠Inequalityx ≠ y
<Less thanx < y
>Greater thanx > y
<=≤Less or equalx ≤ y
>=≥Greater or equalx ≥ y

Logical Operators

OperatorUnicodeNameExample
and∧ConjunctionP ∧ Q
or∨DisjunctionP ∨ Q
not¬Negation¬P
implies / ->→ ⇒ ⟹ImplicationP → Q or P -> Q
iff↔ ⇔ ⟺BiconditionalP ↔ Q
&&Conjunction (alt)P && Q
||Disjunction (alt)P || Q

Note: All Unicode variants for implication (→, ⇒, ⟹) and the ASCII -> are equivalent. All Unicode variants for biconditional (↔, ⇔, ⟺) are equivalent.

Postfix Operators

OperatorNameExampleResult
!Factorial5!120 (requires import "stdlib/combinatorics.kleis")
ᵀ or ^TTransposeAᵀ or A^Ttransposed matrix
† or ^†Dagger/AdjointA† or A^†conjugate transpose
′Primef′derivative notation
″Double primef″second derivative
‴Triple primef‴third derivative
⁺Superscript plusA⁺pseudo-inverse
⁻Superscript minusA⁻inverse notation

Prefix Operators

OperatorNameExampleResult
-Negation-xnegated value
∇Gradient/Del∇fgradient of f
∫Integral∫fintegral of f
¬Logical not¬Pnegation of P

Big Operators (v0.95)

Kleis supports big operator syntax for summations, products, integrals, and limits:

OperatorNameSyntaxTranslates to
ΣSummationΣ(from, to, body)sum_bounds(body, from, to)
ΠProductΠ(from, to, body)prod_bounds(body, from, to)
∫Integral∫(lower, upper, body, var)int_bounds(body, lower, upper, var)
limLimitlim(var, target, body)lim(body, var, target)

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.

OperatorUnicodeNameTypical Mathematical Use
•U+2022BulletInner/dot product notation
∘U+2218Ring operatorFunction composition notation
⊗U+2297Circled timesTensor product notation
⊕U+2295Circled plusDirect sum notation
⊙U+2299Circled dotHadamard product notation
⊛U+229BCircled asteriskConvolution notation
⊘U+2298Circled slash(user-defined)
⊚U+229ACircled ring(user-defined)
⊝U+229DCircled minus(user-defined)
⊞U+229ESquared plus(user-defined)
⊟U+229FSquared minus(user-defined)
⊠U+22A0Squared times(user-defined)
⊡U+22A1Squared dot(user-defined)
∪U+222AUnionSet union notation
∩U+2229IntersectionSet intersection notation
⊔U+2294Square cupJoin/supremum notation
⊓U+2293Square capMeet/infimum notation
△U+25B3Triangle upSymmetric difference notation
▽U+25BDTriangle down(user-defined)

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

OperatorNameExample
→Function typeℝ → ℝ
×Product typeℝ × ℝ
:Type annotationx : ℝ

Precedence Table

From lowest to highest precedence:

LevelOperatorsAssociativity
1↔ ⇔ ⟺ (biconditional)Left
2→ ⇒ ⟹ -> (implication)Right
3∨ or ||Left
4∧ and &&Left
5¬ notPrefix
6= ≠ < > ≤ ≥ ∈ ∉ ⊂ ⊆ ⊃ ⊇Non-associative
7+ -Left
8* / × ·Left
9^ (power)Right
10- (unary negation)Prefix
11! ᵀ ^T † ^† ′ (postfix)Postfix
12Function applicationLeft

Examples

Arithmetic Precedence

define ex1 = 2 + 3 * 4        // 14 (not 20)
define ex2 = (2 + 3) * 4      // 20
define ex3 = 2 ^ 3 ^ 2        // 512 (= 2^9, right associative)
define neg_sq(x) = -x^2       // -(x^2), not (-x)^2

Logical Precedence

define logic1(P, Q, R) = P ∧ Q ∨ R        // (P ∧ Q) ∨ R
define logic2(P, Q, R) = P → Q → R        // P → (Q → R)
define logic3(P, Q) = ¬P ∧ Q              // (¬P) ∧ Q

Postfix with Power

n!^2        // (n!)^2 - factorial first, then square
Aᵀᵀ         // (Aᵀ)ᵀ = A - transpose twice

Type Expressions

ℝ → ℝ → ℝ        // ℝ → (ℝ → ℝ) (curried binary function)
(ℝ → ℝ) → ℝ      // Higher-order: takes function, returns value
ℝ × ℝ → ℝ        // Takes pair, returns value

See Also