Similarity and the Sim Type

The single most consequential design decision in Sema’s neurosymbolic core is that semantic comparison does not return a bool. It returns a graded truth value — a Sim — and turning that grade into a branch is explicit and calibrated, never silent. This page covers the ~= operator, the Sim type, the equality-operator family, and semantics(...) — natural-language predicates used as typed guards.

a ~= b yields a Sim

a ~= b compares two semantic values by their embeddings. It does not produce true/false:

struct Sim:
    score: f32              # in [0, 1], metric-normalized
    judge: JudgeId          # full judge identity, see below
    calibration: Option[CalibrationId]   # named calibration set, if any

Sim is the single graded-truth substrate in the language. ~= scores, contract check results, and semantics() verdicts all inhabit it, so thresholding, evidence reporting, and the guarantee map treat them uniformly. Where a grade travels with its subject, the pair is written (T, Sim) — there is no separate Scored[T] type to learn.

~= requires both operands to be Semantic, and it adds model.embed to the function’s effect row. The syntactic-first rule is preserved: == never touches a model — it is exact structural equality. Only the ~-marked operator invokes an embedder.

The judge is the identity of a comparison

A Sim carries a JudgeId: the complete tuple (model hash, prompt/template hash, decode + seed policy, metric + embedding tier). A decision site’s static type additionally carries (calibration-set id, threshold τ, α). This matters because any component change is a semver-major change to program semantics — swap the embedding model or the tier and every comparison that used it means something different. The judge is ABI. Pin it explicitly with a model(..., role=embedder) binding:

model document_embedder = model(
    "static-embed-document-384",
    rev="sha256:8181c0ffee00...",
    role=embedder,
    calibration="calsets/document-overlap@v1",
)

def claim_overlap(a: Book, b: Paper) -> Sim !{model.embed}:
    return book_claim_text(a) ~= paper_claim_text(b) with judge=document_embedder

The with judge=<binding> clause names the judge for a comparison explicitly; a bare ~= uses the module’s calibrated default judge if one is bound. See /neurosymbolic/simulate/ for model bindings and roles.

Coercing a Sim into control flow

Because Sim is graded, using it in a boolean position is explicit or calibrated, never silent. There are exactly three cases:

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

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

• if a ~= b: — legal only when the judge carries a calibration. The threshold is chosen by conformal risk control (Learn-then-Test) with a declared α, and the guarded region types statistical(α). This is the honest branch: its false-guard rate is bounded.
• if (a ~= b).score > 0.9: — always legal, but the region types best_effort unless that literal threshold has itself been certified against a calibration set. You may compare .score freely, but you get no statistical guarantee for free.
• Uncalibrated judge → compile warning + best_effort. An uncalibrated comparison cannot guard a proved or checked region. The prelude’s default judge ships uncalibrated on purpose (the honesty clause), so ~= under it is best_effort until a named, domain-applicable calibration set is bound.

The rule generalizes to every boolean-coercion context — while conditions, boolean operands, and bool-returning positions like return semantics(...). An uncalibrated coercion in any of these is a compile error, not a silent downgrade. And conjunction/disjunction of calibrated guards composes by the union bound: two calibrated coercions on a path yield statistical(α₁ + α₂), and chains that would blow the site’s α budget are compile errors.

~= is similarity, not equivalence

~= is reflexive and symmetric by construction, but not transitive — it is similarity, not equality. Chained rewriting that assumes a ~= b and b ~= c imply a ~= c is a compile-time error. Similarity does not compose like ==.

The equality-operator family

~= lives in a family of comparison operators. The strict operator is always the default; its ~-prefixed twin is the explicitly-marked semantic version.

Operator	Meaning	Result type	Guarantee
a == b	exact structural equality	bool	proved/checked
a is b	identity	bool	proved
a ~= b	semantic similarity via embeddings	Sim	statistical(α) if calibrated
a ~= b with judge=J	similarity under 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

The full ~-family (semantic ordering ~</~>, membership ~in, combine ~+, logic ~and/~or/~not, and lookup xs ~[query]) is covered under /neurosymbolic/semantic-operations/ and the operators page. Every one of them carries model.invoke or model.embed in its effect row — remoteness to a model is always visible to policy and budgets.

How evaluation actually runs

~= does not blindly run a full embedding compare every time. The evaluation funnel escalates only as needed: content-hash intern lookup → binary-prefix Hamming distance → int8 rescore → full-precision score. Any tier may answer within the judge’s stated tolerance, and every score is recorded to the event log.

semantics(...) — predicates in natural language

Where ~= asks “how similar are these two values,” semantics(...) asks a typed natural-language question about one or more values and returns a graded verdict. It is Sema’s way of putting a human-legible property into the type system.

if semantics("this text contains no SQL DDL", doc):
    apply_migration(doc)

expect semantics("output describes a valid SQL migration", judge=sqlcheck, alpha=0.02):
    plan = planner(request)
except SemanticsViolation as v:
    escalate(v)          # v.predicate, v.judge, v.score, v.threshold, v.excerpts, v.blame

The predicate’s type carries (judge hash, calibration-set id, α). semantics adds model.invoke (and model.embed where the verification protocol embeds) to the effect row. It is a soft keyword — a plausible identifier in NLP code — so it only takes on special meaning in predicate position.

A calibrated semantics(...) used as a guard follows the same coercion rule as ~=: legal only under a calibrated judge, typing the region statistical(α). Here it is used exactly that way in verified corpus code:

def possible_duplicate(a: AdverseEvent, b: AdverseEvent) -> bool !{model.invoke, model.embed}:
    if not same_subject(a.subject, b.subject):
        return false
    event_match = a.narrative_summary ~= b.narrative_summary with judge=duplicate_embedder
    if event_match.score < 0.72:
        return false
    # calibrated coercion; region types statistical(α)
    return semantics(
        "adverse-event candidates are duplicate reports of the same clinical event",
        a,
        b,
        judge=medical_grounder,
        alpha=0.01,
    )

Note the pattern: a cheap ~= prefilter on .score first, then a calibrated semantics(...) verdict for the decision. The ~= compare is best_effort (it gates only an early return), but the returned bool is statistical(α=0.01).

Evaluation is a protocol, not one raw judge call

A single language-model call as a judge is reliable but not valid — verdicts can flip when you swap the order of the operands. So semantics(...) never fires one raw call. It runs an escalating protocol: a calibrated small on-device verifier → an uncertainty-probe gate → k-vote self-consistency → an ensemble, with escalation chosen by policy and measured uncertainty. The verdict is a Sim plus a threshold decision; a violation raises a typed, catchable SemanticsViolation carrying full evidence (score, model, version, excerpts, blame).

The expect ...: / except E as v: block is surface syntax over a sum-typed result — the guarded expression types T | SemanticsViolation, and the except arm is the handling branch. There is no stack unwinding; see /language/error-handling/ for the general typed-failure model.

Over deterministic code, semantics compiles to tests

When a semantics("concern", …) declaration guards purely deterministic code, the compiler turns it into targeted mutants plus killing tests — a permanent, deterministic artifact rather than a runtime judge call. The property becomes part of what sema assure verifies. See /neurosymbolic/verification/.

Failure modes

• Uncalibrated branch — compiles with a warning and types best_effort; it cannot guard a checked region. Bind a calibration set to fix it.
• Cross-domain comparison — comparing values whose sem domains are disjoint is a compile error unless explicitly widened.
• Embedding-model version change — semver-major, because the judge identity is ABI. sema doctor reports judge/calibration mismatches.
• Off-distribution inputs — a statistical(α) guard is honest only while the live distribution matches calibration. Sema requires an active monitor on the input stream of every calibrated site (the compiler auto-derives one if you don’t declare it); without coverage the site decays to best_effort at the type level. See /governance/monitor/.

How it is checked

• sema check flags uncalibrated coercions (error), cross-domain ~= (error), and transitivity-assuming rewrites (error). It reports the guarantee status (statistical(α) vs best_effort) at each decision site.
• sema assure verifies the deterministic obligations and, for semantics over deterministic code, runs the compiled mutant/test artifacts.
• sema doctor reports judge identity, calibration coverage, and monitor footprint per site, so the cost and guarantee of every calibrated comparison is visible.

Where to go next

• The operator syntax and precedence: /language/operators/.
• Contracts built on Sim — hard vs soft: /neurosymbolic/contracts/.
• The full ~-verb family and pipelines: /neurosymbolic/semantic-operations/.