Operators & Semantic Algebra

Operators in Sema are ordinary functions with symbolic names — typed, effect-checked, policy-confined, and contract-gated. The most important cluster is the equality family, because it is where Sema’s neurosymbolic core meets the core language: == is exact, is is a type test, and ~= returns a graded Sim, not a bool.

The equality-operator family

Operator	Meaning	Result type	Guarantee
a == b	exact structural equality	bool	proved / checked
a is b	type / conformance test	bool	proved
a ~= b	semantic similarity via embeddings	Sim	statistical(α) if calibrated
a ~= b with judge=J	similarity under an explicit judge	Sim	per J’s calibration
s matches re"..."	regex match	bool (+ groups)	checked
x in xs	membership over Iterable/dict/set	bool	checked
match v: case P:	structural patterns	—	proved

Syntactic-first dispatch is preserved: == never touches a model. It is exact structural equality, always.

is is a type test, not identity

Under value semantics, identity comparison is meaningless, so is is repurposed: value is Type and value is not Type return bool — true iff the value’s runtime type is that concrete type, or conforms to that trait (transitively through supertraits). It works on concrete types, traits, and built-ins:

n = n + (1 if it is Rule else 0)      # narrow a trait object to a concrete type
if x is int: ...                       # built-in type test

See Traits, Enums & Generics.

~= returns a Sim, not a bool

a ~= b does not return bool. It returns a Sim — a graded-truth value that carries its score and its evidence:

struct Sim:
    score: f32                          # in [0, 1], metric-normalized
    judge: JudgeId                      # full judge identity (model + prompt + metric + tier)
    calibration: Option[CalibrationId]  # named calibration set, if any

~= requires both operands to be Semantic (see Semantic values), and it adds model.embed to the effect row — comparing by similarity is an effect, and the compiler tracks it. The judge (embedding model tier + metric + calibration) resolves at compile time from context or a with clause.

Sim is the single graded-truth substrate: ~= scores, contract check results, and semantics() scores all inhabit it, so thresholding and evidence reporting are uniform. Full detail — the judge identity, calibration, and the non-transitivity of ~= — is on the Similarity page.

Coercing a Sim to control flow

Because a Sim is not a bool, coercing it into an if/while condition is explicit or calibrated, never silent:

if article.title ~= other.title:          # legal ONLY under a calibrated judge; region types statistical(α)
    dedupe(article, other)

s = article.body ~= reference.body with judge=minilm_cal
if s.score > 0.92:                        # explicit threshold: legal always, but best_effort unless certified
    log.info("near-duplicate", evidence=s)

• if a ~= b: is legal only when the judge carries a calibration; the guarded region types as statistical(α).
• if (a ~= b).score > τ: is always legal, but types the region as best_effort unless the threshold τ is itself certified against a calibration set.
• An uncalibrated judge compiles with a warning and types best_effort — it cannot guard proved/checked regions.
• The rule generalizes to every boolean-coercion context (while, boolean operands, bool-returning positions). Conjunction/disjunction of two calibrated guards composes by union bound: statistical(α₁ + α₂).

~= is not transitive

~= is reflexive and symmetric by construction, but not transitive — it is similarity, not equivalence. Chained rewriting that assumes transitivity is a compile-time error.

Operator overloading — semantic algebra

You can define operators for your own types. Built-in scalar operations win for built-in scalar operands; a user-defined operator dispatches only on its declared operand types. Ambiguous overloads are compile errors. Effects, trust labels, policy reachability, contracts, and monitors apply exactly as they do to def:

operator +(left: Money, right: Money) -> Money !{}:
    require left.currency == right.currency
    return Money(currency=left.currency, minor_units=left.minor_units + right.minor_units)

An operator can even be model-backed — a simulate operator has a declarative body that a model fulfills, fenced by a sem descriptor, a budget, and contracts, just like simulate def:

simulate operator -(book: Book, paper: Paper) -> Book !{model.invoke, model.embed} by editor:
    sem "Remove or redact the paper's claims from the book while preserving unrelated material"
    budget tokens=4096, time="12s"
    ensure result.title == book.title
    check semantics("no substantive claim from paper remains in result", paper, result, alpha=0.01)
    check semantics("unrelated book content remains coherent", book, paper, result, alpha=0.01)

Deterministic operators execute as ordinary functions. Semantic operators emit journaled model calls, contract verdicts, and policy decisions; their results are born untrusted until blocking contracts pass. See /neurosymbolic/simulate/ and /neurosymbolic/contracts/.

Which tokens you can overload

Phase 1 overloads the existing precedence classes: +, -, *, /, %, &, |, ^, <<, >>. A future custom-token form is reserved but not yet available:

operator infix "⊖" precedence additive (...) -> T: ...    # reserved, not in v0.1

^ is xor outside equations

Outside equation blocks, ^ is bitwise xor and ** is exponentiation (right-associative, tighter than *). Inside an equation block, ^ means exponentiation. The meaning never changes silently — the boundary is the block.

Failure modes

• Ambiguous overload → compile error.
• Uncalibrated ~= guarding a checked/proved region → compile error (warning + best_effort for softer positions).
• Assuming ~= transitivity in chained rewriting → compile error.
• Cross-domain ~= (disjoint sem domains) → compile error unless explicitly widened.
• Embedding-model version change → semver-major (judge identity is ABI).

See also

• Similarity — the Sim type, judges, and calibration in depth.
• Types — the scalar types operators dispatch over.
• Simulate — model-backed simulate operator.
• Contracts — require/ensure/check on operators.