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

CHANGELOG.md

@@ -4,6 +4,12 @@ All notable changes to the quivers library are documented in this file.
 
 The format is based on [Keep a Changelog](https://keepachangelog.com/), and this project adheres to [Semantic Versioning](https://semver.org/).
 
+## [0.17.0] - 2026-07-16
+
+### Fixed
+
+- **Nullary constants share one chart encoding in patterns and lexicon LFs.** Rule patterns already compiled atoms to `("atom", name)`, but the lexicon LF evaluator emitted a bare `(name,)`, so a premise like `Claim(App(forall_t, X))` compiled cleanly and never matched the chart. Lexicon LFs now emit the same tagged `("atom", name)` for nullary constants, and bound variables are tagged `("var", name)` so alpha-renaming still finds occurrences after constants adopt the atom tag. `atom` and `var` are reserved term-algebra tags: declaring either as an atom or binder name is now a compile error. This changes the observable chart encoding of logical forms (a bound variable that was `("#v1",)` is now `("var", "#v1")`, and a nullary LF constant that was `("dog_p",)` is now `("atom", "dog_p")`), so consumers that inspect chart LFs must read the tagged forms.
+
 ## [0.16.0] - 2026-07-15
 
 ### Changed

docs/developer/changelog.md

@@ -4,6 +4,12 @@ All notable changes to the quivers library are documented in this file.
 
 The format is based on [Keep a Changelog](https://keepachangelog.com/), and this project adheres to [Semantic Versioning](https://semver.org/).
 
+## [0.17.0] - 2026-07-16
+
+### Fixed
+
+- **Nullary constants share one chart encoding in patterns and lexicon LFs.** Rule patterns already compiled atoms to `("atom", name)`, but the lexicon LF evaluator emitted a bare `(name,)`, so a premise like `Claim(App(forall_t, X))` compiled cleanly and never matched the chart. Lexicon LFs now emit the same tagged `("atom", name)` for nullary constants, and bound variables are tagged `("var", name)` so alpha-renaming still finds occurrences after constants adopt the atom tag. `atom` and `var` are reserved term-algebra tags: declaring either as an atom or binder name is now a compile error. This changes the observable chart encoding of logical forms (a bound variable that was `("#v1",)` is now `("var", "#v1")`, and a nullary LF constant that was `("dog_p",)` is now `("atom", "dog_p")`), so consumers that inspect chart LFs must read the tagged forms.
+
 ## [0.16.0] - 2026-07-15
 
 ### Changed

docs/examples/montague-nli.md

@@ -266,11 +266,25 @@ The two deductions are chained by hand rather than by a `compose(...)` step, and
 
 ## Limitations
 
-The fragment is deliberately small, and two limits are structural rather than incidental.
-
-First, there is no beta-reduction on the deduction surface, so the grammar cannot use continuation-form determiner denotations and recover a readable logical form; it builds the normal form directly instead. A grammar that genuinely needed higher-order denotations (quantifier raising, for instance, or the scope ambiguities the [quantifier-scope example](quantifier-scope.md) encodes in its categories) would have to encode the reduction in its rules or its categories, not rely on the runtime to normalise.
-
-Second, a rule pattern cannot mention a nullary constant inside a logical form. Rule patterns compile atoms to a tagged `("atom", name)` pair while the lexicon's logical-form evaluator emits a bare `(name,)` tuple, so a pattern like `Claim(Quant(every_t, P, Q))` never matches a chart item. That is why quantificational force is carried by the determiner's category here rather than by a constant in the logical form. The workaround costs one category per determiner, which is why the fragment has `DetEvery` and `DetSome` instead of a single `Det`.
+The fragment is deliberately small, and one limit is structural
+rather than incidental.
+
+There is no beta-reduction on the deduction surface, so the
+grammar cannot use continuation-form determiner denotations and
+recover a readable logical form; it builds the normal form
+directly instead. A grammar that genuinely needed higher-order
+denotations (quantifier raising, for instance, or the scope
+ambiguities the [quantifier-scope example](quantifier-scope.md)
+encodes in its categories) would have to encode the reduction in
+its rules or its categories, not rely on the runtime to
+normalise.
+
+Quantificational force still rides on the determiner's category
+(`DetEvery` / `DetSome`) here for pedagogical clarity about
+generalised-quantifier constructors, but a rule pattern *can*
+mention a nullary constant inside a logical form: patterns and
+lexicon LFs share the tagged `("atom", name)` encoding, so a
+premise like `Claim(Quant(every_t, P, Q))` matches the chart.
 
 ## References
 

docs/examples/source/montague_nli.qvr

@@ -34,10 +34,13 @@
 # a determiner denotes a relation between two sets, written here
 # as the binary constructors ``Every(P, Q)`` and ``Some(P, Q)``.
 # The determiner's quantificational force rides on its category
-# (``DetEvery`` / ``DetSome``), and the sentence rule that consumes
-# that category builds the matching constructor. Restrictor and
-# scope stay genuine lambda terms, so the ``binders`` machinery is
-# doing real work at the predicate level.
+# (``DetEvery`` / ``DetSome``) so the sentence rule that consumes
+# that category can build the matching constructor without an
+# extra LF constant. Restrictor and scope stay genuine lambda
+# terms, so the ``binders`` machinery is doing real work at the
+# predicate level. (A single ``Det`` plus a nullary quantifier
+# constant in the LF is also expressible: patterns and lexicon
+# LFs share the tagged ``("atom", name)`` encoding.)
 #
 # Reference: [Montague (1973)](https://doi.org/10.1007/978-94-010-2506-5_10).
 

docs/semantics/grammar.md

@@ -176,6 +176,21 @@ source therefore produce chart items with *distinct* canonical
 bound names, so the chart's structural identity on item tuples
 coincides with alpha-equivalence on the source terms.
 
+Nullary constants and bound variables share a bare-identifier
+surface form, so the runtime discriminates them with reserved
+heads:
+
+| Role | Chart encoding |
+| --- | --- |
+| Nullary constant (category or LF) | `("atom", name)` |
+| Bound variable | `("var", name)` |
+| $n$-ary constructor application ($n \ge 1$) | `(ctor, *args)` |
+
+Rule patterns and lexicon LFs therefore agree on nullary
+constants: a premise `Claim(App(forall_t, X))` matches a chart
+item whose LF carries `forall_t`. The tags `atom` and `var` are
+reserved and cannot be declared as atom or binder names.
+
 The compiler additionally collects every bound variable name
 appearing in any lexicon LF and extends the constructor set
 $\mathsf{atoms}(D)$ with those names for the duration of LF

pyproject.toml

@@ -4,7 +4,7 @@ build-backend = "hatchling.build"
 
 [project]
 name = "quivers"
-version = "0.16.0"
+version = "0.17.0"
 description = "A functional probabilistic programming language that compiles to PyTorch."
 readme = "README.md"
 license = {text = "MIT"}

src/quivers/dsl/compiler/deductions.py

@@ -147,12 +147,21 @@ def _candidate_atoms(
     )
 
 
+# Internal term-algebra tags. Nullary constants and bound variables
+# share the same surface shape in source (a bare identifier), so the
+# runtime discriminates them with reserved heads that cannot appear
+# as user-declared atom or binder names.
+_TERM_TAG_ATOM = "atom"
+_TERM_TAG_VAR = "var"
+_RESERVED_TERM_TAGS = frozenset({_TERM_TAG_ATOM, _TERM_TAG_VAR})
+
+
 def _category_depth(value) -> int:
     """Constructor-tree depth of a chart category or item.
 
-    Atoms count as depth 0; the tagged pair ``("atom", "S")``
-    counts as depth 0 (a leaf category); a wrapping tuple
-    ``(<ctor>, <args>...)`` whose head is a non-``"atom"``,
+    Atoms and bound variables count as depth 0; the tagged pairs
+    ``("atom", "S")`` and ``("var", "#v1")`` are leaves. A wrapping
+    tuple ``(<ctor>, <args>...)`` whose head is a non-tag,
     non-``"span"`` constructor counts as
     :math:`1 + \\max_i \\text{depth}(\\text{args}_i)`. Used to gate
     rules that would otherwise rewrite ``A`` into ``Dia(A)`` or
@@ -163,7 +172,7 @@ def _category_depth(value) -> int:
     if not value:
         return 0
     head = value[0]
-    if head == "atom":
+    if head in _RESERVED_TERM_TAGS:
         return 0
     if head == "span":
         # span(I, J, C, ...): depth of the surrounding span is the
@@ -425,11 +434,27 @@ def _compile_deduction(self, decl: DeductionDecl) -> None:
         # ground; undeclared identifiers in patterns are variables).
         atoms_set = set(decl.atoms)
 
+        reserved_clash = sorted(
+            (atoms_set | set(decl.binders)) & _RESERVED_TERM_TAGS
+        )
+        if reserved_clash:
+            names = ", ".join(repr(n) for n in reserved_clash)
+            raise CompileError(
+                f"deduction {decl.name!r}: {names} "
+                f"{'is' if len(reserved_clash) == 1 else 'are'} "
+                f"reserved as term-algebra tag"
+                f"{'' if len(reserved_clash) == 1 else 's'} "
+                f"(nullary constants use {(_TERM_TAG_ATOM, '<name>')!r}; "
+                f"bound variables use {(_TERM_TAG_VAR, '<name>')!r})",
+                decl.line,
+                decl.col,
+            )
+
         def _convert_pattern(texpr):
             if isinstance(texpr, TypeName):
                 name = texpr.name
                 if name in atoms_set:
-                    return ("atom", name)
+                    return (_TERM_TAG_ATOM, name)
                 # Variable convention: any identifier not in the
                 # atoms list (and not a numeric literal) is a
                 # wildcard. This permits arbitrary metavariable
@@ -458,7 +483,7 @@ def _convert_pattern(texpr):
                 args = tuple(_convert_pattern(a) for a in texpr.args)
                 return (texpr.effect, *args)
             # Fallback: a structural-equality probe.
-            return ("atom", repr(texpr))
+            return (_TERM_TAG_ATOM, repr(texpr))
 
         # Detect whether this deduction's item algebra carries an
         # LF slot. The signal: any rule pattern of the form
@@ -702,12 +727,16 @@ def _collect_bound_vars(node, acc: set[str]) -> None:
             # variable names are constructor-like only inside their
             # scope, but at compile time we expand the set
             # uniformly and rely on the alpha-renaming pass to
-            # disambiguate scopes.
+            # disambiguate scopes. Bound names are also recorded in
+            # ``__bound_vars__`` so the let-expression compiler emits
+            # the tagged ``("var", name)`` form rather than a nullary
+            # ``("atom", name)`` constant.
             globals_["__constructors__"] = (
                 frozenset(decl.atoms)
                 | frozenset(decl.binders)
                 | frozenset(bound_var_names)
             )
+            globals_["__bound_vars__"] = frozenset(bound_var_names)
             # The LF compiler treats binder-applied terms specially:
             # the first argument of any constructor listed in
             # ``binders`` is the bound variable. We alpha-rename it
@@ -724,27 +753,39 @@ def _fresh() -> str:
 
             def _normalise_binders(term, env: dict):
                 # Apply alpha-renaming of bound variables to fresh
-                # canonical symbols. ``env`` maps original
-                # variable names to their canonical replacements;
-                # references to bound variables are substituted.
+                # canonical symbols. ``env`` maps original variable
+                # names to their canonical replacements; references
+                # to bound variables (tagged ``("var", name)``) are
+                # substituted. Nullary constants stay
+                # ``("atom", name)`` and are never rewritten.
                 if isinstance(term, tuple) and term:
                     head = term[0]
                     if head in binders_set and len(term) >= 3:
                         var_term = term[1]
-                        if not (isinstance(var_term, tuple) and var_term):
+                        if not (
+                            isinstance(var_term, tuple)
+                            and len(var_term) == 2
+                            and var_term[0] == _TERM_TAG_VAR
+                            and isinstance(var_term[1], str)
+                        ):
                             # Malformed binder; pass through.
                             return tuple(_normalise_binders(x, env) for x in term)
-                        var_name = var_term[0]
+                        var_name = var_term[1]
                         canonical = _fresh()
                         new_env = dict(env)
                         new_env[var_name] = canonical
                         body_norm = tuple(
                             _normalise_binders(x, new_env) for x in term[2:]
                         )
-                        return (head, (canonical,), *body_norm)
+                        return (head, (_TERM_TAG_VAR, canonical), *body_norm)
                     # Reference to a bound variable: substitute.
-                    if len(term) == 1 and isinstance(head, str) and head in env:
-                        return (env[head],)
+                    if (
+                        head == _TERM_TAG_VAR
+                        and len(term) == 2
+                        and isinstance(term[1], str)
+                        and term[1] in env
+                    ):
+                        return (_TERM_TAG_VAR, env[term[1]])
                     return tuple(_normalise_binders(x, env) for x in term)
                 return term
 
@@ -812,7 +853,7 @@ def _normalise_binders(term, env: dict):
                             entries.append(
                                 (
                                     word,
-                                    ("atom", atom),
+                                    (_TERM_TAG_ATOM, atom),
                                     lf_value,
                                     True,
                                 )
@@ -923,7 +964,7 @@ def _goal(item) -> bool:
             # underlying DeductionSystem).
             head = item[0]
             # 1. Bare atom: ("atom", "S").
-            if head == "atom" and len(item) == 2 and item[1] == start:
+            if head == _TERM_TAG_ATOM and len(item) == 2 and item[1] == start:
                 return True
             # 2. Head-keyed (Datalog-style): ("reach", ...).
             if isinstance(head, str) and head == start:
@@ -934,7 +975,7 @@ def _goal(item) -> bool:
                 if (
                     isinstance(cat, tuple)
                     and len(cat) == 2
-                    and cat[0] == "atom"
+                    and cat[0] == _TERM_TAG_ATOM
                     and cat[1] == start
                 ):
                     return True
@@ -1127,7 +1168,7 @@ def _load_lexicon_tsv(
                 # category-shape parsing happens on the live
                 # grammar; here we accept atom identifiers as a
                 # safe, broadly-useful starting point.)
-                cat_pattern = ("atom", cat_text)
+                cat_pattern = (_TERM_TAG_ATOM, cat_text)
                 # LF: treat as a constructor-application or atom.
                 # If the text contains '(' it's a let-call shape;
                 # otherwise it's a bare identifier. Building the

src/quivers/dsl/compiler/programs.py

@@ -3051,13 +3051,27 @@ def _string(env: dict) -> str:
             name = node.name
             globs = globals_ or {}
             constructors = globs.get("__constructors__", frozenset())
+            # Bound-variable names collected by the deduction compiler
+            # (see ``_normalise_binders``). Discriminated from nullary
+            # constants so alpha-renaming can find occurrences by the
+            # ``"var"`` head rather than by tuple shape alone.
+            bound_vars = globs.get("__bound_vars__", frozenset())
 
             def _var(env: dict):
                 if name in env:
                     return env[name]
+                if name in bound_vars:
+                    return ("var", name)
                 if name in constructors:
-                    return (name,)
-                if name in globs and name != "__constructors__":
+                    # Nullary constant: same tagged form patterns and
+                    # categories use (``("atom", name)``), so a rule
+                    # that mentions a constant inside an LF matches
+                    # the lexicon-emitted chart item.
+                    return ("atom", name)
+                if name in globs and name not in (
+                    "__constructors__",
+                    "__bound_vars__",
+                ):
                     return globs[name]
                 raise CompileError(f"undefined variable {name!r} in let expression")
 
@@ -3278,18 +3292,15 @@ def _call(env: dict):
                 if func_name == "subst":
                     # subst(term, var, value) — capture-avoiding
                     # substitution on a structural LF term. Walks the
-                    # term tree, replacing every occurrence of the
-                    # ``(var,)`` 1-tuple with ``value``. Bound
-                    # variables (subterms whose head was listed in a
-                    # ``binders`` block, recognisable by their fresh
-                    # ``#vN`` canonical names) are passed through;
-                    # under-binders that shadow ``var`` halt the
-                    # descent. Because the lexicon LF compiler has
-                    # already alpha-renamed every bound variable to
-                    # a unique canonical symbol, no further capture
-                    # is possible: alpha-equivalence is structural
-                    # at this point and ``subst`` is a single
-                    # recursive pass.
+                    # term tree, replacing every subterm equal to
+                    # ``var`` with ``value``. Bound variables are
+                    # tagged ``("var", name)`` with a fresh ``#vN``
+                    # canonical name after lexicon alpha-renaming;
+                    # nullary constants are tagged ``("atom", name)``.
+                    # Because every binder has already been
+                    # alpha-renamed to a unique canonical symbol,
+                    # naive structural substitution is
+                    # capture-avoiding.
                     if len(arg_fns) != 3:
                         raise CompileError(
                             "subst() takes exactly three arguments: term, var, value"
@@ -3302,14 +3313,14 @@ def _call(env: dict):
                     # ``var`` argument is matched against every
                     # subterm by ``==``; matching subterms are
                     # replaced wholesale by ``value``. This handles
-                    # both bare-variable patterns ``(x,)`` and
-                    # wrapped variable patterns ``Var(x)`` /
-                    # ``(\"Var\", (\"x\",))`` uniformly. Capture
-                    # avoidance is automatic because the lexicon-LF
-                    # compiler has already alpha-renamed every
-                    # binder's bound variable to a fresh canonical
-                    # symbol, so no two distinct variables share a
-                    # name.
+                    # tagged variables ``("var", name)``, tagged
+                    # constants ``("atom", name)``, and wrapped
+                    # forms ``("Var", ("var", name))`` uniformly.
+                    # Capture avoidance is automatic because the
+                    # lexicon-LF compiler has already alpha-renamed
+                    # every binder's bound variable to a fresh
+                    # canonical symbol, so no two distinct variables
+                    # share a name.
                     def _subst(t, _v=var, _r=value):
                         if t == _v:
                             return _r