mpl/conformance/JUDGMENT_CALLS.md

# JUDGMENT_CALLS — semantic decisions awaiting ratification

RATIFIED 2026-07-09 — this file is the semantic record of MPL M0.

Every section below is a semantic question Stage 2 surfaced, stated with
the behavior `js/mpl.js` exhibited at observation time (Stage 2 head,
`ea66a2a`) and the corpus entries that pinned it. Each `RULING:` line
records Reverend's ratified decision of 2026-07-09. BLESS rulings kept the
observed behavior; OVERRIDE/SPLIT/IMPLEMENT/AMEND rulings changed the
grammar or the interpreter in Stage 3, and the corpus was re-recorded to
match. The "Observed:" text is the historical record, not the current
behavior — the rulings govern.

## 1. Division by zero

Question: what does `x ÷ 0` do — error, infinity, or ⊥?
Observed: raises `err_div0` (both `÷` and `/`, integer or float operands).
Pins: `043_div_zero`.

RULING: BLESS. `x ÷ 0` (and `/`) raises `err_div0`. Division by zero is undefined.

## 2. The value of a ∀ expression

Question: what does `∀ x ∈ list : body` evaluate to?
Observed: the value of the last body evaluation; `⊥` for an empty list.
Pins: `018_forall_value`, `019_forall_scope`.

RULING: OVERRIDE. `∀` is an iterator; the expression's value is `⊥` always (including empty collections). Using a statement as a value is undefined — same principle as ruling 3.

## 3. Result when no guard matches

Question: what is `(false ⟹ e)` with no `|` fallback?
Observed: an internal no-match that surfaces as `⊥` everywhere except
directly to the left of `|`.
Pins: `021_no_guard_match`, `023_alt_chain`.

RULING: BLESS (semantics, not mechanism). An unmatched guard yields `⊥` unless caught by `|`. Implementations choose their own internal sentinel.

## 4. Integer vs float display

Question: is `4 ÷ 2` shown as `2` or `2.0`? Are all numbers one type?
Observed: all numbers are IEEE doubles; integral values display with no
decimal point (`2`), non-integral as JS renders them (`0.5`, and
`0.1 + 0.2` shows `0.30000000000000004`). Literals normalize (`007` → `7`,
`0.50` → `0.5`).
Pins: `006_number_display`, `007_float_arithmetic`.

RULING: OVERRIDE. Numbers are exact rationals (arbitrary-precision integer numerator/denominator). Decimal literals convert exactly (`0.1` = 1/10). Display: integers bare; otherwise lowest-terms fraction `num/den`, sign on the numerator, denominator > 0; zero as `0`. Output is valid MPL that re-evaluates to the same value. IEEE doubles are rejected: the language must not lie about `0.1`. `√ vs ℚ` is logged as a standing M1 decision.

## 5. ✎ formatting per type

Question: exactly how does `✎` render each value type?
Observed: numbers via host `String()`; strings bare at top level but
quoted inside lists; booleans `true`/`false`; lists `[a, b]` with
one-space separation; closures as `λ`; `⊥` as `⊥`.
Pins: `009_string_concat`, `011_list_display`, `031_show_all_types`.

RULING: BLESS, spec'd. `✎` renders: numbers per ruling 4; strings bare at top level, double-quoted inside lists; booleans `true`/`false`; lists `[a, b]` (comma-space); closures as `λ`; `⊥` as `⊥`.

## 6. ⊥ display and propagation

Question: is `⊥` a first-class value or a poison that propagates?
Observed: a first-class value — it displays as `⊥`, concatenates into
strings (`"x" + ⊥` → `x⊥`), sits in lists, but arithmetic on it is
`err_num`.
Pins: `030_bot`, `052_bot_arith`.

RULING: BLESS. `⊥` is first-class: displays as `⊥`, sits in lists, string concatenation renders it (`"x" + ⊥` → `x⊥`); arithmetic on it is `err_num`.

## 7. Equality across types

Question: what does `=` mean across types and on structures?
Observed: structural (JSON-serialization) equality — lists compare
element-wise, cross-type comparisons are `false` (`1 = "1"` → `false`),
and `⊥ = ⊥` → `true`. Comparing a self-referential closure crashes with a
keyless host error (unpinnable by the corpus).
Pins: `034_cross_type_equality`, `033_string_compare`.

RULING: SPLIT. Data equality is structural: element-wise lists, cross-type `=` is `false`, `⊥ = ⊥` is `true`, `0.5 = 1/2` is `true` (same rational). Any equality comparison involving a function raises `err_fn_eq` — function equality is undecidable; a keyed error replaces the current keyless crash.

## 8. Ordering across types

Question: what do `< > ≤ ≥` do on mixed or non-numeric operands?
Observed: raw host comparison with JS coercion — `1 < "2"` → `true`,
`"10" < 9` → `false`, `true < 2` → `true`; strings order lexicographically.
Pins: `035_mixed_compare`, `033_string_compare`.

RULING: OVERRIDE. `< > ≤ ≥` are defined on number×number and string×string (Unicode code-point order) only; anything else raises `err_compare`. Host coercion (`1 < "2"`) is JavaScript soul leakage, not mathematics.

## 9. Closure capture

Question: do closures capture values at definition time or the
environment?
Observed: the environment — later mutation of a captured variable is
visible on the next call (`013` prints 11 then 21).
Pins: `013_closure_capture`, `026_def_vs_assign_scope`.

RULING: BLESS. Closures capture the environment. (The corpus itself forces this: `factorial` only works because the λ sees its own later binding.)

## 10. Recursion depth

Question: what bounds recursion, and how does exceeding it surface?
Observed: the host JS stack — deep recursion dies as a keyless RangeError
before the 500 000-step budget can trigger, so the corpus cannot pin it
(no error key). Iteration-heavy programs do hit the budget and raise
`err_steps`. Depth ~500 is comfortably safe.
Pins: `016_recursion_sum` (works at 500), `053_step_budget` (`err_steps`).

RULING: OVERRIDE. Recursion is bounded by an explicit λ-application depth counter, limit 10 000, raising `err_depth`. A keyless host RangeError is a hole in the error surface; the limit is conformance surface in every implementation.

## 11. The step budget itself

Question: is "500 000 evaluation steps, then `err_steps`" part of the
language, and is that the right number?
Observed: hard-coded 500 000; nested `∀` loops over a 10-element list six
deep exceed it.
Pins: `053_step_budget`.

RULING: RECLASSIFY. The step budget is an environment resource limit, not language semantics — like out-of-memory. `err_steps` (500 000) remains in the browser implementation; entry 053 leaves the portable corpus and becomes a js/test implementation test.

## 12. String escape round-tripping

Question: which string escapes exist, and what does an unknown one mean?
Observed: `\n` and `\t` expand; `\"` and `\\` escape themselves; any other
`\x` silently drops the backslash (`"drop\qme"` → `dropqme`). The ANTLR
grammar instead REJECTS unknown escapes — a recorded divergence.
Pins: `008_string_escapes`; divergence in DIVERGENCES.md ("drop\qme" and
the `"a\zb"` fuzz entry).

RULING: OVERRIDE. Escapes are exactly `\n \t \" \\`; any other `\x` raises `err_escape`, matching the grammar. Silent data-mangling is forbidden.

## 13. Guard condition truthiness

Question: what may a guard condition be?
Observed: `true` and non-zero numbers fire the guard; `false`, `0`,
strings, lists and `⊥` do not (they yield the no-match path) — so numbers
are truthy for `⟹` but nothing else is.
Pins: `022_guard_truthiness`.

RULING: OVERRIDE. A guard condition must be boolean; any non-boolean condition (numbers included) raises `err_bool`. A condition is a proposition.

## 14. ∧ ∨ operand truth

Question: do `∧`/`∨` accept the same truthiness as `⟹`?
Observed: no — operands are tested with strict boolean equality, so
`1 ∧ true` → `false` while `(1 ⟹ x)` fires. Both operators short-circuit
(observable by side effect). This asymmetry with #13 is the sharpest
accident in the surface.
Pins: `036_logic_ops`, `037_logic_short_circuit`.

RULING: SPLIT. `∧ ∨` short-circuit (blessed, observable by side effect) and demand boolean operands — a non-boolean evaluated operand raises `err_bool` instead of silently comparing false. One notion of truth, everywhere; an unevaluated right operand raises nothing.

## 15. Block scoping

Question: does `{ … }` create a scope?
Observed: no — bindings made inside a brace block leak out (`028` prints
9). Only λ bodies and each `∀` iteration scope.
Pins: `028_block_no_scope`, `027_block_sequencing`.

RULING: BLESS. Braces group; they do not scope. Scope is created by binders only (λ parameters, ∀ iteration variables) — the Curry-Howard reading: a discharged hypothesis IS a λ. An explicit local-binding construct (let/where) is logged as a standing M1 decision.

## 16. ≜ vs ← scoping and creation

Question: how do define and assign differ?
Observed: `≜` always binds in the current scope; `←` mutates the nearest
enclosing binding and silently creates one in the current scope when
nothing is bound (assignment-before-definition is legal). Both are
expressions returning the value; both rebind freely (`x ≜ 1; x ≜ 3` is
legal re-definition).
Pins: `024_def_assign_rebind`, `025_def_assign_value`,
`026_def_vs_assign_scope`.

RULING: OVERRIDE (both halves). `≜` introduces a name exactly once per scope — same-scope redefinition raises `err_redef`; shadowing in inner scopes is legal. `←` mutates the nearest enclosing binding and raises `err_unbound` when none exists — silent creation is the typo trap. Both remain expressions returning the value.

## 17. Type constraints

Question: does `λx∈ℕ:` constrain anything?
Observed: the constraint parses (including supplementary-plane `𝔹`) and
is discarded unevaluated — `g ≜ λs∈𝔹: s + "!"` happily takes a string.
Matches the site's "parsed today, not yet enforced" claim.
Pins: `039_type_constraint_unenforced`.

RULING: BLESS. Type constraints parse and are discarded, unenforced — this is the published claim and Stage 5's mandate.

## 18. Nullary calls and zero-parameter λ

Question: `f()` parses — but can any function be called that way?
Observed: no zero-parameter λ can be written (`λ: e` is a parse error),
so every `f()` is a runtime `err_arity`. The call syntax exists; nothing
can satisfy it.
Pins: `046_arity_nullary`, `047_arity_extra`.

RULING: AMEND GRAMMAR. Nullary functions exist: `λ: e` is admitted (bare colon; the parenthesized spelling stays rejected per ruling 25). Effects made M0 procedural the day `✎` entered it; arity 0 is not an exception to ℕ. `f()` calls it; arity mismatches remain `err_arity`.

## 19. ∗ as multiplication

Question: is `∗` (U+2217) an operator, and what does it mean?
Observed: exactly `×` — same token, same precedence.
Pins: `041_asterisk_multiplication`.

RULING: BLESS. `∗` (U+2217) is exactly `×`.

## 20. Divergence: empty program

Question: is the empty program valid?
Observed: the grammar accepts it; the JS interpreter rejects it
(`err_unexpected` at 1:1).
Pins: none possible until ruled (decision 3 — divergent programs cannot
enter the corpus). Repro in DIVERGENCES.md (fuzz index 49).

RULING: OVERRIDE. The empty program is valid and produces no output. The grammar is right; the interpreter accepts it.

## 21. Divergence: sequences inside parentheses

Question: is `( e1 ; e2 )` valid? DECISIONS.md says `(...)` contains one
seqExpr; the JS parser allows exactly one expression.
Observed: the grammar accepts `(42;)` and `(a; b)`; the JS interpreter
rejects both (`err_expect`).
Pins: none until ruled. Repros in DIVERGENCES.md (fuzz indexes 86, 119,
247, 233, 279, 406, 468, 101…).

RULING: OVERRIDE. Parentheses contain one seqExpr per the standing DECISIONS ruling: `(e1; e2)` is legal, value = last expression. The interpreter implements its own language.

## 22. Divergence: `∘` composition

Question: does function composition exist in M0?
Observed: the grammar parses `f ∘ g`; the JS interpreter lexes `∘` (it
even has the `\circ` escape) but has no parse rule for it — every use is
`err_expect`.
Pins: none until ruled. Repro in DIVERGENCES.md (fuzz index 9).

RULING: IMPLEMENT. `∘` is function composition: `(f ∘ g)(args…) = f(g(args…))`. Operands must be functions — a non-function operand raises the expected-a-function key (reuse the existing key if the audit finds one, else introduce `err_fn`). Precedence and associativity follow the grammar.

## 23. Divergence: set literals

Question: `{a, b}` is a set per the grammar's brace disambiguation — does
the M0 core have sets?
Observed: the grammar accepts `({5, "a b"})` and friends; the JS
interpreter has no set support and rejects them (`err_expect`).
Pins: none until ruled. Repros in DIVERGENCES.md (multiple fuzz indexes).

RULING: PARSE-ONLY. Set literals parse (the interpreter gains the grammar's brace disambiguation) and evaluation raises `err_notyet`. Set semantics are an M1 design, logged.

## 24. Divergence: record literals

Question: `{k: v}` is a record per the grammar — does the M0 core have
records?
Observed: the grammar accepts `({y: 0})`; the JS interpreter rejects
(`err_expect`).
Pins: none until ruled. Repros in DIVERGENCES.md (fuzz indexes 25, 212,
425, 427, 447).

RULING: PARSE-ONLY. Record literals: same as 23.

## 25. Divergence: parenthesized λ parameters

Question: DECISIONS.md rejected `λ(a, b):` as a second parameter spelling
— but who enforces that?
Observed: inverted from every other divergence — the GRAMMAR rejects
`λ(a, b): e` (honoring the decision) while the JS interpreter accepts it.
The interpreter carries a syntax form the language explicitly rejected.
Pins: none until ruled. Repros in DIVERGENCES.md (fuzz indexes 13, 29,
76, …).

RULING: OVERRIDE. `λ(a, b): e` is rejected by the interpreter too — the grammar already enforces the ratified DECISIONS ruling.

## 26. Divergence: bare λ and Greek letters as identifiers

Question: the grammar tokenizes Greek letters (LAMBDA_VAR et al.) as
identifiers, so `{λ}` parses; the JS interpreter only knows λ as the
abstraction head.
Observed: grammar accepts `({λ})`; JS rejects (`err_expect` — λ demands a
parameter list).
Pins: none until ruled. Repro in DIVERGENCES.md (fuzz index 52).

RULING: AMEND GRAMMAR. `λ` is a reserved token, never an identifier. Only λ; other Greek letters (π et al.) remain identifiers — Fatima wants π.