Defining Functions

@logos.define is how you introduce functions into the logos proof system. The function body runs in expression-tree mode — operators build trees instead of evaluating — and the result is a Function object you can use in proofs.

Basic Usage

import logos
import logos.tactics as t

@logos.define
def double(x: int):
    return x + x

# double is now a Function object
print(type(double))        # <class 'logos.define.Function'>
print(double.name)         # double
print(double.params)       # [Var('x', int)]

<class 'logos.define.Function'>
double
[Var(name='x', type=<class 'int'>)]

Dual Mode

The same function works as a normal Python function and as a symbolic expression builder:

x = logos.var("x", int)
from logos.expr import App

# Python mode — called with a concrete value
print(double(5))    # 10 (= 5 + 5)
print(double(7))    # 14

# Symbolic mode — called with a Var
result = double(x)
print(type(result).__name__)   # App
print(result.func_name)        # double
print(result.args)             # [Var("x", int)]

10
14
App
double
[Var(name='x', type=<class 'int'>)]

Proving About Defined Functions

Use t.unfold(double) (the Function object) to replace double(x) with its definition body:

@logos.theorem
def double_is_2x(x: int):
    return double(x) == logos.lit(2) * x

logos.check(double_is_2x.proof(t.intro("x"), t.unfold(double), t.ring()))
print("Proved: double(x) = 2x")

Proved: double(x) = 2x

The proof trace is: 1. intro("x") — introduce x from the Forall 2. unfold(double) — replaces double(x) with x + x in the goal 3. ring() — proves x + x == 2 * x by polynomial normalization

Composing Definitions

Defined functions can call each other:

@logos.define
def square(x: int):
    return x * x

@logos.define
def sum_of_squares(x: int, y: int):
    return square(x) + square(y)

@logos.theorem
def sos_symmetric(x: int, y: int):
    return sum_of_squares(x, y) == sum_of_squares(y, x)

logos.check(sos_symmetric.proof(
    t.intro("x", "y"),
    t.unfold(sum_of_squares),
    t.unfold(square),
    t.ring(),
))
print("Proved: sum_of_squares is symmetric")

Proved: sum_of_squares is symmetric

Case Expressions

Use logos.cases() for conditional definitions. Each branch is a (condition, value) pair:

@logos.define
def abs_val(x: int):
    return logos.cases(
        (x >= logos.lit(0),  x),
        (x < logos.lit(0),  -x),
    )

# Python mode still works
print(abs_val(-5))   # 5
print(abs_val(3))    # 3

CaseExpr(branches=[(Le(left=Lit(value=0), right=Lit(value=-5)), -5), (Gt(left=Lit(value=0), right=Lit(value=-5)), 5)])
CaseExpr(branches=[(Le(left=Lit(value=0), right=Lit(value=3)), 3), (Gt(left=Lit(value=0), right=Lit(value=3)), -3)])

External (Black-Box) Functions

For functions logos can’t inspect — C extensions, external APIs, database queries — declare them symbolically with logos.extern and axiomatize their properties:

# Declare an external sorting function
sorted_fn = logos.extern("my_sorted", [list], list)

xs = logos.var("xs", list)

# State what we know about it
@logos.axiom
def sorted_returns_same_type(xs: list):
    return sorted_fn(xs) == sorted_fn(xs)

# Now we can use sorted_fn in propositions and proofs
from logos.expr import App
result = sorted_fn(xs)
print(type(result).__name__)  # App
print(result.func_name)       # my_sorted

App
my_sorted

Note

The extern approach is how logos reasons about library functions you can’t redefine. You state the properties you need as axioms, then build proofs on top of them.

Multiple Parameters

Definitions can take any number of parameters:

@logos.define
def clamp(x: int, lo: int, hi: int):
    return logos.cases(
        (x < lo, lo),
        (x > hi, hi),
        (logos.lit(True), x),   # default/else case
    )

print(clamp(-5, 0, 10))   # 0
print(clamp(50, 0, 10))   # 10
print(clamp(5, 0, 10))    # 5

CaseExpr(branches=[(True, 0), (False, 10), (Lit(value=True), -5)])
CaseExpr(branches=[(False, 0), (True, 10), (Lit(value=True), 50)])
CaseExpr(branches=[(False, 0), (False, 10), (Lit(value=True), 5)])