Equivalence

PFCL language reference · composure.systems

1.Two invariants, held at every grade

1. Equivalence never mutates identity. No matter how confidently two entries are judged equivalent, their hashes remain distinct and unaffected. Equivalence is metadata about the relationship between two identities, never an operation on either one.
2. Grades stay distinct. A judgment produced by testing on a sample of inputs is recorded as evidence. A judgment produced by a completed proof is recorded as proof. The two are never merged or presented as equivalent kinds of confidence.

2.Grade 0 — alias detection (exact identity coincidence)

Status: shipped. Not equivalence in the graded sense below — the trivial case. Two entries sharing a hash are, by definition of identity, the same function under two names. The catalog's test suite walks the full name→hash table, groups names sharing a hash, and classifies each group: an ALIAS group is an intentional, declared rebinding; an INCOMPLETE group is undifferentiated debt — two names that happen to coincide with nothing declaring that it's intentional. This runs today as a gate: it fails on any undeclared collision and reports a headline metric (total redundant group size) as a standing measure of alias hygiene.

3.Grade 1 — normalization / alpha-equivalence

Status: designed, not built. Match via structural comparison up to bound-variable renaming — two bodies that differ only in what their local bindings are called. This is the narrowest non-trivial grade: sound, decidable, and cheap once implemented, because it requires no semantic reasoning about behavior, only a normalized structural comparison.

What ships here, when built: a normalizer that produces a canonical form for alpha-equivalence classes, and an index keyed on that normalized form, letting the loader flag near-duplicates at admission time without altering either candidate's identity.

4.Grade 2 — law-based matching (equality saturation)

Status: designed, not built. Match via a fixed set of algebraic rewrite rules applied exhaustively — two bodies related by a known law (associativity, a fusion rule, a known identity element) are recognized as equivalent even though neither normalizes to the other syntactically.

Open, pending design detail: the specific rule set, and how a rule earns admission to it.

5.Grade 3 — SMT on the decidable fragment

Status: designed, not built. Match via automated theorem proving, scoped strictly to the fragment of the language the solver can decide. Outside that fragment, this grade simply does not produce a judgment — it never guesses.

Open, pending design detail: which fragment is in scope, and which solver/encoding.

6.Grade 4 — bounded evidence

Status: designed, not built. Match via testing on a finite, generated sample of inputs. This is evidence, explicitly not proof, and is recorded as such per the distinctness invariant above.

The total-fragment caveat. Because PFCL is a total language (see /totality), every function's input domain is fully representable — but a bounded sample still only covers part of that domain. A bounded-evidence judgment is scoped to the inputs actually sampled, not to the function's behavior everywhere. This caveat doesn't shrink as the language gets more total; it's inherent to sampling.

7.Grade 5 — inductive proof

Status: designed, not built. A completed proof of equivalence, where one exists and is findable. The strongest possible grade, and the rarest — most equivalences a catalog will encounter won't have a hand-reachable inductive proof, which is why the weaker grades exist rather than waiting for this one.

8.What this specifies, and what it doesn't

This page specifies the ladder's shape, its invariants, and the status of each grade. It does not specify the admission-time policy question of what happens once a near-duplicate is detected — whether the loader blocks a new candidate, redirects it to a canonical representative, or simply flags it for review. That policy question, along with the broader admission mechanisms it fits inside, is covered in /catalog/governance and will be extended there once grades above 0 exist to feed it.