Record grammar-only surface gaps

This commit is contained in:
developtheweb 2026-07-10 00:09:03 -04:00
parent b40ba77e26
commit 7e679fa86c
2 changed files with 22 additions and 0 deletions

View file

@ -36,3 +36,5 @@ against the existing examples.
- **Stage-1 exception: the imported interpreter's header comment was corrected in place** (`tested: 18/18` → the provable `10 tests in js/test/`) — a falsified claim inside the canonical artifact outranks byte identity with the pre-Stage-1 deploy; end-state identity is restored when the site deploys the pinned file. - **Stage-1 exception: the imported interpreter's header comment was corrected in place** (`tested: 18/18` → the provable `10 tests in js/test/`) — a falsified claim inside the canonical artifact outranks byte identity with the pre-Stage-1 deploy; end-state identity is restored when the site deploys the pinned file.
- **Stage-3 ratification (2026-07-09): the 26 judgment calls are ruled; JUDGMENT_CALLS.md is the semantic record of MPL M0.** Per-ruling record: (1) ÷0 is `err_div0`; (2) a `∀` expression is always `⊥`; (3) an unmatched guard yields `⊥` unless caught by `|`; (4) numbers are exact rationals — BigInt num/den, lowest terms, den > 0, decimal literals exact, display `n` or `n/d` (re-evaluates to itself); IEEE doubles rejected; (5) `✎` rendering spec'd per type; (6) `⊥` is first-class, arithmetic on it `err_num`; (7) equality is structural on data, cross-type `=` false, `0.5 = 1/2` true, any function in `=`/`≠` raises `err_fn_eq`; (8) ordering is number×number and string×string (code-point) only, else `err_compare`; (9) closures capture the environment; (10) λ-application depth counter, limit 10000, `err_depth` — no keyless host error may remain reachable; (11) the 500000-step budget is an environment resource limit, not semantics — corpus entry 053 moved to js/test; (12) string escapes are exactly `\n \t \" \\`, anything else `err_escape` (grammar ESC amended to match); (13) guard conditions must be boolean, else `err_bool`; (14) `∧ ` short-circuit and demand booleans on evaluated operands (`err_bool`); (15) braces group, binders scope; (16) `≜` binds once per scope (`err_redef`; inner shadowing legal), `←` mutates an existing binding only (`err_unbound`); (17) type constraints parse, unenforced; (18) nullary `λ: e` admitted (grammar amended); (19) ```×`; (20) the empty program is valid; (21) `( seqExpr )` — the interpreter now implements it; (22) `∘` is composition, `(f ∘ g)(x…) = f(g(x…))`, non-function operand `err_notfn`; (23) set literals parse, evaluate to `err_notyet`; (24) record literals likewise; (25) `λ(a, b):` rejected everywhere; (26) `λ` is reserved — never an identifier — while other Greek letters remain identifiers. - **Stage-3 ratification (2026-07-09): the 26 judgment calls are ruled; JUDGMENT_CALLS.md is the semantic record of MPL M0.** Per-ruling record: (1) ÷0 is `err_div0`; (2) a `∀` expression is always `⊥`; (3) an unmatched guard yields `⊥` unless caught by `|`; (4) numbers are exact rationals — BigInt num/den, lowest terms, den > 0, decimal literals exact, display `n` or `n/d` (re-evaluates to itself); IEEE doubles rejected; (5) `✎` rendering spec'd per type; (6) `⊥` is first-class, arithmetic on it `err_num`; (7) equality is structural on data, cross-type `=` false, `0.5 = 1/2` true, any function in `=`/`≠` raises `err_fn_eq`; (8) ordering is number×number and string×string (code-point) only, else `err_compare`; (9) closures capture the environment; (10) λ-application depth counter, limit 10000, `err_depth` — no keyless host error may remain reachable; (11) the 500000-step budget is an environment resource limit, not semantics — corpus entry 053 moved to js/test; (12) string escapes are exactly `\n \t \" \\`, anything else `err_escape` (grammar ESC amended to match); (13) guard conditions must be boolean, else `err_bool`; (14) `∧ ` short-circuit and demand booleans on evaluated operands (`err_bool`); (15) braces group, binders scope; (16) `≜` binds once per scope (`err_redef`; inner shadowing legal), `←` mutates an existing binding only (`err_unbound`); (17) type constraints parse, unenforced; (18) nullary `λ: e` admitted (grammar amended); (19) ```×`; (20) the empty program is valid; (21) `( seqExpr )` — the interpreter now implements it; (22) `∘` is composition, `(f ∘ g)(x…) = f(g(x…))`, non-function operand `err_notfn`; (23) set literals parse, evaluate to `err_notyet`; (24) record literals likewise; (25) `λ(a, b):` rejected everywhere; (26) `λ` is reserved — never an identifier — while other Greek letters remain identifiers.
- **Standing M1 decisions logged at ratification**: `√` vs (irrationals); an explicit local-binding construct (let/where); set semantics; record semantics; comprehension notation; `‖` parallel semantics. - **Standing M1 decisions logged at ratification**: `√` vs (irrationals); an explicit local-binding construct (let/where); set semantics; record semantics; comprehension notation; `‖` parallel semantics.
- **Grammar-only surface gaps are on the record** (SURFACE.md "Grammar-only surface" section): `≈`/`` comparisons, `"""raw strings"""`, hex/binary/exponent literals, and `_` as a λ pattern all parse in the grammar and fail in the Stage-3 interpreter — Stage 4+ material, no ruling; `err_comment` is dead pending removal at the next legitimate interpreter change.
- **Ruling 12's enumeration governs string escapes**: the grammar's ESC fragment was narrowed to exactly `\n \t \" \\``\r`, `\0` and `\u{hex}` were removed from the grammar; they were never in the ratified set.

View file

@ -84,6 +84,26 @@ parser rule** — any use is `err_expect`.
- Deep recursion overflows the host stack **before** the step budget — - Deep recursion overflows the host stack **before** the step budget —
a keyless RangeError, unpinnable by the corpus (see JUDGMENT_CALLS). a keyless RangeError, unpinnable by the corpus (see JUDGMENT_CALLS).
## Grammar-only surface (no ruling, Stage 4+ material)
The grammar accepts these; the Stage-3 interpreter does not. No ruling
covers them and the fuzzer's generator does not emit them — they are on
the record here so the gap is a listed fact, not a surprise:
- `≈` (APPROX) and `` (SIM) comparison operators — interpreter: `err_char`.
- `"""raw strings"""` (RAWSTRING) — interpreter: `err_char` at the second
quote pair's content or `err_string`/`err_expect` depending on context.
- Hex (`0x1F`), binary (`0b101`) and exponent (`1.5e3`) number literals —
interpreter lexes the leading digits as a plain number and fails to
parse the rest (`err_expect`).
- `_` as a λ pattern (patternAtom UNDERSCORE) — interpreter: `err_char`.
Dead key: `err_comment` can no longer be raised — since the comment lexer
matched the grammar (a `{-` without its `-}` is a brace, not an
unterminated comment), no code path produces it. It stays in the error-key
list pending removal at the next legitimate interpreter change (no hash
churn for hygiene alone).
## Explicitly out of corpus scope ## Explicitly out of corpus scope
- `‖` — parses, and the evaluator runs it as plain sequencing, but its - `‖` — parses, and the evaluator runs it as plain sequencing, but its