Repository navigation
TG-7 decision: braid == semantics — list-equality vs braid-group equivalence #50
Description
Decision needed (owner)
TG-7 asks whether == on braids should decide braid-group equivalence rather than list equality.
Current state. == on braids is list equality in both compiler/lib/eval.ml and the Lean Step.eqBraids rule. A complete braid-group equivalence checker (Dehornoy handle reduction) now exists out-of-band as compiler/lib/braid_equiv.ml (tested in compiler/test/tg7, 2220 assertions). It does not change ==.
The fork:
- (a) Change semantics — route
==/Step.eqBraidsthrough braid-group equivalence. Changes the observable semantics of==on braids; toucheseval.mland the LeanSteprelation, rippling into the Progress / Preservation / Determinism proofs. - (b) Keep
==as list equality — usebraid_equivonly as a tool (tooling /compute-style checks), leaving language semantics unchanged.
A mechanised Lean Garside/Dehornoy correctness proof for braid_equiv is research-grade either way (tracked in the remaining-work issue).
Refs: PROOF-NEEDS.md (TG-7); landed at origin/main 5ed31f8.
Activity
hyperpolymath commentedon Jul 28, 2026
Owner ruling (2026-07-28): (a) true braid-group equivalence
==on braids decides braid-group equivalence, not list equality. Rationale: syntactic equality contradicts the language's own thesis — Tangle's premise is that programs are topological objects and equivalence is isotopy. Keeping==syntactic would quietly abandon that at the one operator where users most expect it to hold.Consequences to work through
compiler/lib/eval.ml— route==on braids through the existingbraid_equiv.ml(Dehornoy handle reduction, already tested with 2,220 assertions incompiler/test/tg7). This is the cheap half: the decision procedure exists and is exercised.Step.eqBraids— theSteprelation must reflect the new semantics, which ripples into Progress / Preservation / Determinism. Determinism is the one to watch:==must still reduce to a unique value, which holds because braid-group equivalence is a decidable equivalence relation — but the proof obligation is real, not free.braid_equivis trusted code, not proven code. That boundary must be stated honestly inPROOF-NARRATIVE.md/PROOF-NEEDS.md— theSteprule is proven relative to an unproven decision procedure. Do not let the sorry/axiom gate imply otherwise.TG3Differential.leanasserts OCamlinfer_expr≡ Leaninfer; check whether any corpus term's typing depends on==semantics, and regenerate viatg3_emitif so.Sequencing note: land the OCaml side and the Lean
Stepchange together, since the TG-3 differential and the proof oracle both straddle them.Closing this as decided; the implementation work belongs to #51 and the TG-7 line in
PROOF-NEEDS.md.hyperpolymath commentedon Jul 28, 2026
Decision recorded above: (a) true braid-group equivalence. Implementation tracked in #51 and the TG-7 line of
PROOF-NEEDS.md.feat(tg-7): `==` on braids decides braid-group equivalence (#50 rulin…
fix(rsr): finish template instantiation + enforce it (#56) (#90)
fix(typecheck): infer recursive functions' return type by fixpoint (#88…