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 should have compatible types for meaningful results.
// if True then 42 else "hello"  // evaluates to 42 (unreachable branch ignored)

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 can express the same logic:

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

// With pattern matching and guards (parses; see note on guards in Ch. 5)
define classify_match(n) =
    match n {
        x if x < 0 => "negative"
        0 => "zero"
        _ => "positive"
    }

For concrete evaluation with :eval, prefer if-then-else since comparison guards are not yet fully evaluated at runtime (see Pattern Matching: Guards).

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"

Boolean Operators in Conditions

Note that ∧ and ∨ in the evaluator currently use eager evaluation — both operands are evaluated before the logical operation is applied. For guarding against division by zero, use nested conditionals:

// Safe: nested if avoids evaluating y/x when x = 0
define check_ratio(x, y) =
    if x ≠ 0 then
        if y/x > 1 then "big ratio" else "safe"
    else "safe"

In Z3 verification contexts, ∧ and ∨ are translated to Z3’s native logical operators which handle short-circuit semantics appropriately.

What’s Next?

Learn about structures for defining mathematical objects!

→ Next: Structures