feat(#92): widths need not agree for ==, and match arms join on width - #95
Merged
Conversation
Implements the #92 ruling across both engines, plus two bugs found while verifying it. ## The rule `T-Eq-Word` required both operands at the same width. That was inconsistent with the rest of the language in four ways, all recorded in #92: * `tComposeWord` already WIDENS to max n m — a program could compose two braids it was then forbidden to compare; * `~` accepted differing widths and, since TG-7, evaluates through the SAME `Braid_equiv.equiv` — identical operands, identical answer, one rejected; * `eqIdBraid`/`eqBraidId` decide "is this braid trivial?" against `identity : word 0`, so under the old rule they could only ever fire when the braid was empty — the step relation had rules for a question the typing rule forbade asking; * `braid_equiv.equiv` has no width parameter at all. Lean `tEqWord` now takes (n m); `infer`'s `.eq` case drops the `if n = m`. OCaml `Eq` mirrors it. Match arms join on width for words (max) and still require exact agreement for everything else. ## The metatheory did not need patching Progress, Preservation, Determinism, TypeSafety, infer_sound and infer_complete all still hold — `lean Tangle.lean` reports 0 errors, and the sorry/axiom gate passes. The `infer_sound` proof got SIMPLER: with no `if n = m` there is no inner `split` left to case on, which is a decent sign the restriction was load-bearing for nothing. TG-3 regenerated and kernel-checked: 496 obligations, 0 errors. 46 of them flipped from `= none` to `= some .bool` — precisely the `identity == braid` shape that was previously unreachable. ## Two bugs found while verifying 1. STATEMENT ORDER. `parse_file_recovering` in bin/main.ml did `stmts := prog @ !stmts` and then `List.rev` on the flattened result. That reversal is right for an accumulator built by prepending single items — as `diagnostics` is — but whole SEGMENTS were prepended, so every program came out backwards: `def x; def y; def z` parsed to [z; y; x]. Any program whose statements depend on order failed at evaluation with "Unbound variable". The test suites never caught it because they call `Tangle.Parser.program` directly; only the CLI goes through the recovering path. Now accumulates segments and flattens in order. 2. A FALSE ASSERTION in examples/trefoil.tangle: assert reversed == braid[s1, s1, s1] `reverse` reverses the word AND negates exponents, so it yields the INVERSE braid. writhe(trefoil) = 3 but writhe(reversed) = -3, and writhe is invariant under the braid relations, so they cannot be equal. The assertion had been wrong since it was written; nothing ran the examples until #89. Corrected to braid[s1^-1, s1^-1, s1^-1], which passes. ## Result examples evaluating : 2/7 -> 7/7 (all now in the must-run set) lib/stdlib.tangle : did not typecheck -> typechecks conformance : 18/19 (v11 add{} is the Harvard sub-language, #94) ## Trusted base Registered as A-TG-92.1: the embedding Bn -> Bn+1 that justifies cross-width comparison is standard mathematics but is asserted IN PROSE, not mechanised. What is machine-checked is that the metatheory holds under the widened rule and that OCaml still agrees with Lean on the corpus. Tests: 6 new typecheck cases including two negatives (mismatched KINDS still rejected; match arms of different kinds still rejected) so widening cannot degrade into "anything compares to anything". Three test_check cases repointed at an error that is still an error. Co-Authored-By: Claude Opus 5 <noreply@anthropic.com>
Uh oh!
There was an error while loading. Please reload this page.
Note Automatic reviews are paused because your trial's included automatic processing has been used for this period. Upgrade now, or comment "Gitar review" to run a review anytime. Code Review✅ ApprovedRemoves strict width agreement requirements for equality comparisons and adds match arm width joining across both engines, enabling all 7 example programs to evaluate successfully. No issues found.
OptionsDisplay: compact → Showing less information. Comment with these commands to change the behavior for this request:
Was this helpful? React with 👍 / 👎 | Gitar |
hyperpolymath added a commit
that referenced
this pull request
Jul 29, 2026
…ertion (#97) The false assertion corrected in #95 was **not an isolated slip**. Auditing whether the conformance corpus actually *runs* — the gate only ever checked that it *parsed* — turned up a second mathematically false claim of exactly the same kind, plus one genuine unimplemented feature. ## The second false assertion `conformance/valid/v16_close_mirror_reverse.tangle`: ```tangle assert reverse(braid[s1, s2]) == braid[s2, s1] ``` `reverse` reverses the word **and** negates every exponent — it yields the *inverse* braid, so `reverse(s1 s2) = s2⁻¹ s1⁻¹`. Disproved by invariant: `writhe(reverse(braid[s1,s2])) = -2` while `writhe(braid[s2,s1]) = +2`, and writhe is invariant under the braid relations, so they cannot be the same element. ## Two authors, same mistake → a documentation failure `examples/trefoil.tangle` and this file made the *identical* wrong assumption. That is not carelessness. `FORMAL-SEMANTICS.md` described the operation as: ``` | reverse(e) -- reverse word ``` which reads as order-only. Now stated as an identity: ``` reverse(g₁ g₂ … gₙ) = gₙ⁻¹ … g₂⁻¹ g₁⁻¹ i.e. reverse(w) = w⁻¹ ``` with the contrast against `mirror` (which negates **in place**) spelled out, and the writhe argument recorded so the next reader can check it rather than trust it. ## The systemic fix `scripts/check-corpus.sh` now **evaluates** `conformance/valid`, not just parses it. Parsing was never enough — a program can parse perfectly and assert something false. Both bad assertions survived precisely because nothing ran them. **Verified in both directions:** reintroducing the exact false assertion makes the gate fail (`exit 1`, *"parses but does not evaluate"*); restoring it returns `exit 0`. ## The genuine gap `v09_twist.tangle` uses `(~a)` to twist a named strand inside a weave. `spec/grammar.ebnf` says *"In weave context: (~a) twists named strand a"*, but `infer_expr` rejects any strand name used as an expression — specified and unimplemented. Recorded in the new `CONFORMANCE_KNOWN_UNRUNNABLE` list rather than papered over, and raised as **#96**. Worth noting *why* it was invisible: until #93 a weave block could not be bound to anything, so its body was never evaluated. The construct has literally never run. ## Regression tests Four pinning `reverse`, chosen so they cannot pass vacuously: | Test | Why it can't be faked | |---|---| | reverse is **not** order-reversal | asserts inequality with the wrong answer | | `reverse(reverse(w)) = w` | only holds if it genuinely inverts | | reverse negates writhe | the invariant that disproved both false claims | | `mirror` negates *in place* | pins the contrast that caused the confusion | Suites 112 → 116, all green; TG-3 still 1008/0. 🤖 Generated with [Claude Code](https://claude.com/claude-code) Co-authored-by: Claude Opus 5 <noreply@anthropic.com>
hyperpolymath added a commit
that referenced
this pull request
Jul 29, 2026
…ent-order bug (#99) TG-11 (#98) landed the type former, typing, evaluation and six proofs — but there was **no way to write one**. Zero occurrences of the constructors in `lexer.mll` or `parser.mly`, against 4 for echo. Fully implemented and unreachable. ## Surface syntax ```tangle def w = warrant[0](42, braid[s1, s2]) -- at standpoint 0 def token = evidence(w) -- the ONLY elimination ``` The standpoint is bracketed because it's an *index*, not an operand — the same reading as a braid generator's subscript. No grammar conflicts. **Non-factivity reaches the syntax.** There is deliberately no keyword extracting the claim: `claim(w)` parses as an ordinary call to an undefined function, never as a language form. A test pins that distinction — if a `Claim` form ever appears, it contradicts `epi_only_yields_evidence`. ## A *second* copy of the statement-order bug Writing the first epistemic program surfaced it immediately: ``` def w = warrant[0](42, braid[s1]) def tok = evidence(w) → In definition 'tok': evidence requires an Epi[k, rho, tau], got Word[0] ``` That `Word[0]` is the pass-1a **placeholder** — `tok` was being checked *before* `w` was refined. Same root cause as #95 (`stmts := prog @ !stmts` then `List.rev` on the flattened list), but in a **second copy**, in `lib/check.ml`. **That copy feeds `tanglec --check` and the LSP.** Both have been analysing programs with their statements reversed. And it was never epistemic-specific: ``` def e = echoClose(braid[s1]) def r = residue(e) → residue requires Echo[_, _], got Word[0] ``` **Any cross-definition reference to a non-`Word` type was mis-typed.** Echo has been broken this way for as long as the recovering path has existed. The test suites missed *both* copies for the same reason: they call `Parser.program` directly and never exercise the recovering path. ## Tests **Parser** — warrant with bracketed standpoint; evidence; TG-4 round-trip; the no-claim-form guard. **Check** — three cross-definition cases (plain, echo, epistemic), all of which would have failed before this. ## Example `examples/epistemic.tangle`, wired into the corpus gate's must-run set — warrants at three standpoints, evidence recovery, and the echo composition `residue(evidence(we))`. All assertions pass. It also documents *why* the claim is unreachable: if it were extractable, anything anyone attested would become true by fiat — precisely the bug you don't want in a provenance system. All gates green: Lean 0 errors, full suite, corpus, RSR. 🤖 Generated with [Claude Code](https://claude.com/claude-code) Co-authored-by: Claude Opus 5 <noreply@anthropic.com>
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Sign up for freeto join this conversation on GitHub.
Already have an account?
Sign in to comment
1 participant
Add this suggestion to a batch that can be applied as a single commit.This suggestion is invalid because no changes were made to the code.Suggestions cannot be applied while the pull request is closed.Suggestions cannot be applied while viewing a subset of changes.Only one suggestion per line can be applied in a batch.Add this suggestion to a batch that can be applied as a single commit.Applying suggestions on deleted lines is not supported.You must change the existing code in this line in order to create a valid suggestion.Outdated suggestions cannot be applied.This suggestion has been applied or marked resolved.Suggestions cannot be applied from pending reviews.Suggestions cannot be applied on multi-line comments.Suggestions cannot be applied while the pull request is queued to merge.Suggestion cannot be applied right now. Please check back later.
Implements the #92 ruling across both engines — plus two bugs found while verifying it.
The rule
T-Eq-Wordrequired both operands at the same width. Four ways that was inconsistent with the language itself (evidence in #92):tComposeWordalready widens tomax n m— you could compose two braids you were then forbidden to compare.~accepted differing widths and, since TG-7, evaluates through the sameBraid_equiv.equiv. Identical operands, identical answer, one rejected by the typechecker.eqIdBraid/eqBraidIddecide "is this braid trivial?" againstidentity : word 0, so under the old rule they could only fire when the braid was empty. The step relation had rules for a question the typing rule forbade asking.braid_equiv.equivhas no width parameter at all.Lean's
tEqWordnow takes(n m);infer's.eqcase drops theif n = m; OCamlEqmirrors it. Match arms join on width for words and still require exact agreement otherwise.The metatheory needed no patching
Progress, Preservation, Determinism, TypeSafety,
infer_sound,infer_completeall still hold —lean Tangle.leanreports 0 errors, sorry/axiom gate passes.infer_sound's proof got simpler: with noif n = mthere's no innersplitto case on. A restriction whose removal shortens the proof was carrying no weight.TG-3 regenerated and kernel-checked: 496 obligations, 0 errors. 46 flipped from
= noneto= some .bool— exactly theidentity == braidshape that was unreachable before.Two bugs found while verifying
1. Statement order.
parse_file_recoveringdidstmts := prog @ !stmtsthenList.revon the flattened result. That reversal is correct for an accumulator built by prepending single items (asdiagnosticsis) — but whole segments were prepended, so every program came out backwards:Any program whose statements depend on order died with "Unbound variable". The test suites never caught it because they call
Tangle.Parser.programdirectly — only the CLI goes through the recovering path.2. A false assertion in
examples/trefoil.tangle:reversereverses the word and negates exponents, yielding the inverse braid. Verified by invariant:writhe(trefoil) = 3,writhe(reversed) = -3, and writhe is invariant under the braid relations — so they cannot be equal. The assertion had been wrong since it was written; nothing ran the examples until #89. Corrected tobraid[s1^-1, s1^-1, s1^-1], which passes.Result
lib/stdlib.tanglev11is the Harvard sub-language, #94)All seven examples are now in the corpus gate's must-run set, so none can regress.
⚠ Trusted base — registered as A-TG-92.1
The embedding Bₙ ↪ Bₙ₊₁ that justifies cross-width comparison is standard mathematics, but it is asserted in prose, not mechanised — no Lean lemma states it.
What is machine-checked: that the metatheory holds under the widened rule, and that OCaml
infer_exprstill agrees with Leaninferon the corpus. That distinction is recorded inASSUMPTIONS.mdrather than left implicit.Tests
6 new typecheck cases, including two negatives — mismatched kinds still rejected, match arms of different kinds still rejected — so widening cannot quietly become "anything compares to anything". Three
test_checkcases repointed at an error that is still an error (and an assertion helper left unused by the change was put back to work rather than deleted).🤖 Generated with Claude Code