fix(dsl): unify nullary-constant chart encoding across patterns and LFs

[aaronstevenwhite]

Summary

A nullary constant had two incompatible chart encodings — ("atom", name) in rule patterns but a bare (name,) in lexicon logical forms — so a rule that mentioned a constant inside an LF (e.g. Claim(App(forall_t, X))) compiled clean and silently never fired. This unifies both positions on one discriminated representation.

Motivation

Closes #49. The divergence made a whole class of well-formed rules dead on arrival, and forced the Montague NLI example to carry quantificational force on the determiner's category (DetEvery / DetSome) instead of on a constant in the logical form. The naive one-line unifications both fail: tagging LFs ("atom", …) breaks the alpha-renamer (it matches occurrences by tuple head), and a bare-tuple encoding collides a nullary constant ("dog_p",) with a canonical bound variable ("#v1",).

Changes

Picks one discriminated encoding and carries it through categories, LFs, patterns, _normalise_binders, _category_depth, goal matching, and the public chart API together:

Role	Chart encoding
Nullary constant (category or LF)	("atom", name)
Bound variable	("var", name)
$n$-ary application ($n \ge 1$)	(ctor, *args)

• dsl/compiler/deductions.py: reserved _TERM_TAG_ATOM / _TERM_TAG_VAR tags; a compile-time check rejecting atom / var as atom or binder names; _category_depth treats both tags as depth-0 leaves; _normalise_binders matches and rewrites the ("var", name) head; goal matching keyed on the atom tag.
• dsl/compiler/programs.py: the let-expression _var compiler emits ("var", name) for collected bound names (via a new __bound_vars__ global) and ("atom", name) for constructors; subst docs updated.
• docs: semantics/grammar.md §3a gains the encoding table; examples/montague-nli.md and the .qvr example note the resolved limitation; CHANGELOG + mirrored docs changelog.

API impact

• Breaking change. Migration notes: the observable chart encoding of logical forms changed — a bound variable that was ("#v1",) is now ("var", "#v1"), and a nullary LF constant that was ("dog_p",) is now ("atom", "dog_p"). Consumers that inspect chart LFs must read the tagged forms. Additionally, atom and var are now reserved and cannot be declared as atom or binder names. Versioned as a minor bump (0.16.0 → 0.17.0) per pre-1.0 SemVer.

Tests

• pytest -x passes (2415 non-CLI tests green).
• New tests added for new behaviour: test_rule_pattern_matches_nullary_lf_constant (pins pattern↔LF matching), test_reserved_term_tags_rejected_as_atoms; binder / subst / occurrence tests updated to the tagged forms.

Documentation

• User-facing pages under docs/ updated.
• docs/developer/changelog.md regenerated from the root CHANGELOG.md.
• Denotational semantics under docs/semantics/ updated (encoding table in grammar.md §3a).

Checklist

• Commits are focused and have descriptive messages.
• No backward-compatibility shims added (pre-1.0; clean break).
• Comments describe the code as it stands.
• No secrets, credentials, or large binary artefacts in the diff.

Made with Cursor