From 997554e7c6dad3401956457613259ba106c02f8e Mon Sep 17 00:00:00 2001 From: Aaron Steven White Date: Thu, 16 Jul 2026 15:07:43 -0400 Subject: [PATCH] fix(dsl): unify nullary-constant chart encoding across patterns and LFs (0.17.0) Rule patterns compiled a nullary constant to ("atom", name) while the lexicon LF evaluator emitted a bare (name,), so a premise mentioning a constant inside a logical form (e.g. Claim(App(forall_t, X))) compiled clean and could never match the chart. Lexicon LFs now emit the same tagged ("atom", name); bound variables are tagged ("var", name) so alpha-renaming still finds occurrences once constants take the atom tag. "atom" and "var" are reserved term-algebra tags. This changes the observable chart encoding of logical forms, so it is a minor (breaking) bump under pre-1.0 SemVer. Closes #49 Co-authored-by: Cursor --- CHANGELOG.md | 6 ++ docs/developer/changelog.md | 6 ++ docs/examples/montague-nli.md | 24 +++++-- docs/examples/source/montague_nli.qvr | 11 +-- docs/semantics/grammar.md | 15 ++++ pyproject.toml | 2 +- src/quivers/dsl/compiler/deductions.py | 79 ++++++++++++++++------ src/quivers/dsl/compiler/programs.py | 55 +++++++++------ tests/test_deduction.py | 94 ++++++++++++++++++++++++-- 9 files changed, 235 insertions(+), 57 deletions(-) diff --git a/CHANGELOG.md b/CHANGELOG.md index 8a6fc19..d538e91 100644 --- a/CHANGELOG.md +++ b/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 diff --git a/docs/developer/changelog.md b/docs/developer/changelog.md index 8a6fc19..d538e91 100644 --- a/docs/developer/changelog.md +++ b/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 diff --git a/docs/examples/montague-nli.md b/docs/examples/montague-nli.md index 56407a3..3389c30 100644 --- a/docs/examples/montague-nli.md +++ b/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 diff --git a/docs/examples/source/montague_nli.qvr b/docs/examples/source/montague_nli.qvr index 799e179..64feb51 100644 --- a/docs/examples/source/montague_nli.qvr +++ b/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). diff --git a/docs/semantics/grammar.md b/docs/semantics/grammar.md index fcee29b..143194a 100644 --- a/docs/semantics/grammar.md +++ b/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 diff --git a/pyproject.toml b/pyproject.toml index 89da736..d008ce7 100644 --- a/pyproject.toml +++ b/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"} diff --git a/src/quivers/dsl/compiler/deductions.py b/src/quivers/dsl/compiler/deductions.py index 1e5ed34..87105ea 100644 --- a/src/quivers/dsl/compiler/deductions.py +++ b/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 - ``(, ...)`` 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 ``(, ...)`` 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, '')!r}; " + f"bound variables use {(_TERM_TAG_VAR, '')!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 diff --git a/src/quivers/dsl/compiler/programs.py b/src/quivers/dsl/compiler/programs.py index ac0f005..cb568b6 100644 --- a/src/quivers/dsl/compiler/programs.py +++ b/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 diff --git a/tests/test_deduction.py b/tests/test_deduction.py index 4029955..2555618 100644 --- a/tests/test_deduction.py +++ b/tests/test_deduction.py @@ -20,7 +20,7 @@ import torch from quivers.dsl.parser import parse -from quivers.dsl.compiler import Compiler +from quivers.dsl.compiler import Compiler, CompileError from quivers.stochastic.deduction import ( DeductionSystem, adam_fit_deduction, @@ -187,9 +187,13 @@ def test_binders_alpha_rename_lexicon_lfs(): # canonical name despite both using ``x`` in source. canon_per_lex = [] for lf in lfs: - # lf is ("Lam", (canon,), ("App", ..., ("Var", (canon,)))) + # lf is ("Lam", ("var", canon), ("App", ..., ("Var", ("var", canon)))) assert lf[0] == "Lam" - canon_per_lex.append(lf[1][0]) + binder = lf[1] + assert isinstance(binder, tuple) and binder[0] == "var", ( + f"binder should be tagged ('var', name), got {binder!r}" + ) + canon_per_lex.append(binder[1]) assert canon_per_lex[0] != canon_per_lex[1], ( f"binders failed to alpha-rename: both entries got {canon_per_lex[0]!r}" ) @@ -261,7 +265,62 @@ def test_subst_capture_avoiding(): expr, globals_={"__constructors__": frozenset({"App", "Var", "f", "x", "arg"})} ) out = fn({}) - assert out == ("App", ("f",), ("Var", ("arg",))), f"subst gave {out!r}" + assert out == ( + "App", + ("atom", "f"), + ("Var", ("atom", "arg")), + ), f"subst gave {out!r}" + + +def test_rule_pattern_matches_nullary_lf_constant(): + """A rule that mentions a nullary constant inside an LF must + match the lexicon-emitted chart encoding of that constant. + + Patterns and lexicon LFs both use ``("atom", name)`` for nullary + constants, so ``Claim(App(forall_t, X))`` can fire against a + chart item whose LF carries ``forall_t``. Bound variables stay + tagged ``("var", name)`` so alpha-renaming is unaffected. + """ + src = """ + object Term : FinSet 4 + deduction Quant : Term -> Term [semiring=LogProb, start=S] + atoms S, N, span, App, Var, Claim, forall_t, dog_p + binders Lam + rule lift : span(I, J, S, F) |- Claim(F) + rule forall_intro : Claim(App(forall_t, X)) |- Claim(X) + lexicon + "every" : S = App(forall_t, Lam(x, App(dog_p, Var(x)))) + """ + mod = parse(textwrap.dedent(src)) + prog = Compiler(mod).compile() + ded = prog.deductions["Quant"] + chart = ded(["every"]) + + # Lexicon LF uses the tagged nullary encoding. + span_lfs = [ + item[4] + for item, _ in chart.chart.items() + if isinstance(item, tuple) and item[:3] == ("span", 0, 1) and len(item) > 4 + ] + assert span_lfs, "lexicon did not emit a span item" + lf = span_lfs[0] + assert lf[0] == "App" and lf[1] == ("atom", "forall_t"), ( + f"nullary constant should be ('atom', 'forall_t'), got {lf!r}" + ) + lam = lf[2] + assert lam[0] == "Lam" and lam[1][0] == "var", ( + f"binder should be tagged ('var', …), got {lam!r}" + ) + + # The rule over forall_t must fire and expose the lambda. + claims = [ + item + for item, _ in chart.chart.items() + if isinstance(item, tuple) and item and item[0] == "Claim" + ] + assert any(c[1] == lam for c in claims), ( + f"forall_intro did not fire: claims={claims!r}, expected Claim({lam!r})" + ) def test_montague_nli_lambda_lfs_load(): @@ -344,8 +403,13 @@ def test_lambda_body_occurrence_matches_its_binder(): assert lf[0] == "Lam", f"expected a Lam-headed LF, got {lf!r}" bound = lf[1] - assert isinstance(bound, tuple) and len(bound) == 1, ( - f"binder should carry one canonical symbol, got {bound!r}" + assert isinstance(bound, tuple) and len(bound) == 2 and bound[0] == "var", ( + f"binder should carry a tagged canonical symbol, got {bound!r}" + ) + # Predicate constant is tagged like every other nullary atom. + app = lf[2] + assert app[0] == "App" and app[1] == ("atom", "dog_p"), ( + f"nullary LF constant should be ('atom', 'dog_p'), got {app!r}" ) def _occurrences(term) -> list: @@ -362,3 +426,21 @@ def _occurrences(term) -> list: f"lambda binds {bound!r} but its body references {occurrence!r}; " f"the occurrence is unbound" ) + + +def test_reserved_term_tags_rejected_as_atoms(): + """``atom`` and ``var`` are reserved term-algebra tags.""" + src = """ + object Term : FinSet 2 + deduction Bad : Term -> Term [semiring=LogProb, start=S] + atoms S, atom + rule r : S |- S + """ + mod = parse(textwrap.dedent(src)) + try: + Compiler(mod).compile() + except CompileError as exc: + assert "reserved" in str(exc).lower() + assert "atom" in str(exc) + else: + raise AssertionError("expected CompileError for reserved atom name")