Expressions¶
This page gives a compositional, big-step denotational semantics for the QVR expression sublanguage. The sublanguage is the body of let bindings and export declarations: it consists of morphism-valued combinators that take morphisms (and, for the parser combinator, grammar data) and produce new morphisms.
1. Syntactic class¶
Expressions \(e\) are generated by the grammar
The first grammar covers morphism-valued expressions. The auxiliary grammar for \(t\) covers transformation-valued expressions used inside \(\mathsf{change\_base}\): bare-name singletons from the built-in catalog (\(\mathit{trans\_singleton}\)), parametric constructors (\(\mathit{trans\_ctor}\)), sequential composition \(>>>\), and let-bound transformation references \(y\) in the dedicated transformation namespace.
The clause \(\mathit{op}(e_1, \dots, e_n)\) stands for a registered operadic contraction: \(\mathit{op}\) is the name of a \(\mathsf{contraction}\) declared elsewhere in the module, with its declared input arity and signature checked at the call site. See § Composition Rules § 4 for the operadic action.
Each expression denotes a morphism in one of the three strata of Morphisms. We write \(\llbracket e \rrbracket_{\rho}\) for the denotation under semantic environment \(\rho\), and we suppress \(\rho\) when only morphism-valued names are at play.
2. Identifiers, identity, and core combinators¶
2.1 Identifiers¶
Lookup fails (raising CompileError) if \(x \notin \mathrm{dom}(\rho_{\mathrm{mor}})\).
2.2 Identity¶
the categorical identity at the type denotation \(\llbracket \tau \rrbracket_{\rho}\). The stratum is determined by \(\tau\): a ObjectExpr produces the identity in \(\mathcal{V}\text{-}\mathbf{Rel}\), while a SpaceExpr produces the identity in \(\mathbf{Kern}\).
2.3 Composition¶
Well-typedness requires \(\mathrm{cod}(\llbracket e_1 \rrbracket) = \mathrm{dom}(\llbracket e_2 \rrbracket)\) in the appropriate category. The category is the smallest one containing both denotations under the embeddings of Morphisms §5.
2.4 Tensor¶
the parallel product. This is the symmetric monoidal structure of \(\mathcal{V}\text{-}\mathbf{Rel}\) / \(\mathbf{Stoch}\) / \(\mathbf{Kern}\); see Morphisms §4.
2.5 Marginalization¶
For \(\llbracket e \rrbracket : X_1 \otimes \cdots \otimes X_k \otimes Y \to Z\),
a morphism \(Y \to Z\) obtained by joining the marginalized coordinates out of the input. In \(\mathbf{Stoch}\) and \(\mathbf{Kern}\) the join \(\bigoplus\) is integration against the corresponding marginal; in \(\mathcal{V}\text{-}\mathbf{Rel}\) it is the algebra join. When \(k\) equals the full input arity (no remaining \(Y\)), the result is a morphism \(\mathbf{1} \to Z\).
2.6 Change of base¶
For a morphism \(\llbracket e \rrbracket : A \to B\) in \(\mathcal{V}\text{-}\mathbf{Rel}\) and a transformation \(\llbracket t \rrbracket : \mathrm{Trans}[\mathcal{V}, \mathcal{W}]\),
The action of \(\llbracket t \rrbracket\) is pointwise when \(t\) resolves to an algebra homomorphism, and shape-aware (possibly swapping the domain and codomain, as for bayes_invert) when \(t\) resolves to a MorphismTransformation. When \(t\) is a sequence \(t_1 \mathbin{>\!\!>\!\!>} \cdots \mathbin{>\!\!>\!\!>} t_k\), the action is the composition \(\llbracket t_k \rrbracket \circ \cdots \circ \llbracket t_1 \rrbracket\).
2.7 Sequential composition of transformations¶
For \(t_1\) with target \(\mathcal{V}'\) and \(t_2\) with source \(\mathcal{V}'\),
The well-typedness side-condition \(\mathrm{target}(t_1) = \mathrm{source}(t_2)\) is checked statically; a mismatch raises a typed compile-time error with line and column of the offending expression. Chains of length \(\ge 3\) flatten unambiguously: \(t_1 \mathbin{>\!\!>\!\!>} (t_2 \mathbin{>\!\!>\!\!>} t_3)\) and \((t_1 \mathbin{>\!\!>\!\!>} t_2) \mathbin{>\!\!>\!\!>} t_3\) denote the same transformation. See § Composition Rules § 5 for the full development.
2.8 The eleven composition operators¶
The composition combinator \(>\!\!>\) of §2.3 is one of an eleven-operator family. The operators fall into two groups by dispatch rule:
- Algebra-polymorphic. \(>\!\!>\), \(<\!\!<\), and \(>\!\!=\!\!>\) use the operands' shared algebra: whichever algebra the surrounding module declared (via the
algebra Xdirective, Composition Rules §3) supplies \(\otimes\) and \(\bigoplus\). A composition under one of these operators raises a typed error if the two operands disagree on their algebra. The three operators differ only in surface ergonomics: \(<\!\!<\) swaps operand order (\(g \mathbin{<\!\!<} f = f \mathbin{>\!\!>} g\)), and \(>\!\!=\!\!>\) is the Haskell-style "Kleisli arrow" surface alias for \(>\!\!>\) (it does not dispatch to a different algebra). - Algebra-tagged. The remaining eight operators each fix a target algebra and require both operands to already inhabit it; the compiler raises if either operand's declared algebra differs. These are the surface for spelling cross-algebra composition without an explicit
change_basechain.
| Operator | Dispatch | Algebra \(\mathcal{V}\) | Composition |
|---|---|---|---|
>> |
polymorphic | module's declared algebra | \(\bigoplus_y f \otimes g\) in that algebra |
<< |
polymorphic | module's declared algebra | \(g \mathbin{<\!\!<} f \;=\; f \mathbin{>\!\!>} g\) |
>=> |
polymorphic | module's declared algebra | same denotation as \(>\!\!>\) |
*> |
tagged | \(\mathcal{V}_{\mathrm{M}}\) | Markov sum-product on \(\mathbb{R}_{\ge 0}\) |
~> |
tagged | \(\mathcal{V}_{\mathrm{LP}}\) | log-domain sum-product (logsumexp / \(+\)) |
\|\|> |
tagged | \(\mathcal{V}_{\mathrm{G}}\) | Gödel (max / min) |
?> |
tagged | \(\mathcal{V}_{\mathrm{MP}}\) | Viterbi max-plus (max / \(+\)) |
&&> |
tagged | \(\mathcal{V}_{\mathbb{B}}\) | Boolean (\(\vee\) / \(\wedge\)) |
+> |
tagged | \(\mathcal{V}_{\mathrm{L}}\) | Łukasiewicz (bounded sum / \(\otimes_{\mathrm{L}}\)) |
$> |
tagged | \(\mathcal{V}_{\mathbb{R}}\) | real sum-product |
%> |
tagged | \(\mathcal{V}_{[0,1]}\) | saturated probability sum-product |
For every operator \(\circ\) with effective algebra \(\mathcal{V} = (V, \otimes, \bigoplus)\),
with the algebra-polymorphic operators sourcing \((\otimes, \bigoplus)\) from the module's declared algebra and the algebra-tagged operators sourcing them from the operator's fixed target. The reverse operator \(\mathbin{<\!\!<}\) satisfies \(\llbracket g \mathbin{<\!\!<} f \rrbracket = \llbracket f \mathbin{>\!\!>} g \rrbracket\) by definition; the parser swaps the operands and stores the forward form. Mixing tagged operators in a chain (e.g. f *> g ~> h) requires an explicit change_base between segments because the tagged operators do not auto-convert their operands.
2.9 Compact-closed structure¶
When the surrounding composition rule is at the algebra level (Composition Rules §1), supplying an identity element \(\mathbf{1}\), an absorbing zero \(\bot\) (so that \(a \otimes \bot = \bot\)), and strict distributivity of \(\otimes\) over \(\bigoplus\), the category \(\mathcal{V}\text{-}\mathbf{Rel}\) is compact closed with every object self-dual. Four expressions expose this structure; the compiler rejects them outside an algebra-level module (Composition Rules §2).
Cup (unit)¶
Cap (counit)¶
The pair \((\mathsf{cup}(A),\,\mathsf{cap}(A))\) are the unit / counit of the self-duality \(A \dashv A\) in \(\mathcal{V}\text{-}\mathbf{Rel}\). The snake equations
hold by direct verification on entries: \(\bigoplus_a \delta(x, a) \otimes \delta(a, y) = \delta(x, y)\), using absorption of \(\bot\) to collapse the off-diagonal terms.
Dagger¶
For \(f : A \to B\) in \(\mathcal{V}\text{-}\mathbf{Rel}\), the postfix \(f.\mathsf{dagger}\) is the transposed relation
The map \((\cdot)^\dagger\) is an involutive identity-on-objects functor \(\mathcal{V}\text{-}\mathbf{Rel}^{\mathrm{op}} \to \mathcal{V}\text{-}\mathbf{Rel}\) and equips the category with dagger-compact structure when paired with cup/cap.
Trace¶
For \(f : A \otimes X \to A \otimes Y\), the postfix \(f.\mathsf{trace}(A)\) is the partial trace along \(A\):
Equivalently, in the compact-closed structure,
up to the canonical reassociation of \(A \otimes (A \otimes X) \cong (A \otimes A) \otimes X\). This is the trace operation of Joyal, Street & Verity (1996) instantiated at the compact-closed structure; the trace axioms (yanking, sliding, vanishing) follow from the snake equations.
2.10 Residuation witnesses¶
For \(f : X \otimes Y \to Z\) in \(\mathcal{V}\text{-}\mathbf{Rel}\) where \(Z\) is an object of a residuated universe (Schemas §3.1) and under QVR's biclosed slash convention (the lexical-left operand of each slash is the result),
are the two adjunction witnesses of the right / left residuation. Concretely, \(\mathsf{curry\_right}(f)\) is the unique \(\mathcal{V}\)-relation \(X \to (Z / Y)\) whose right-residual evaluation against an element of \(Y\) recovers \(f\), and dually \(\mathsf{curry\_left}(f) : Y \to Z \backslash X\) witnesses the left-residual adjunction \(\mathcal{C}(X \otimes Y, Z) \cong \mathcal{C}(Y, Z \backslash X)\). The well-typedness of the postfix requires the codomain to inhabit a residuated category; the compiler rejects either form when the surrounding type universe does not declare the residuation slashes.
2.11 Freeze¶
The postfix \(f.\mathsf{freeze}\) has the same denotation as \(f\):
It is an operational marker, not a categorical operation: the resulting morphism is materialised as an ObservedMorphism and gradient flow through its parameters is severed (equivalent to Tensor.detach() on the entries). The categorical denotation is unchanged.
2.12 From-data¶
The expression \(\mathsf{from\_data}(\text{"K"})\) denotes the \(\mathcal{V}\)-relation whose tensor is the runtime data dictionary's value at key "K", resolved at fit time:
with the well-typedness requiring the surrounding type-annotation to match the tensor's shape. The resulting morphism is an ObservedMorphism: structural / frozen, not learnable.
2.13 Operadic contraction call¶
For a \(\mathsf{contraction}\) declaration \(\mathit{op}\) with input arity \(n\), declared signature \((A_i \to B_i)_{i = 1}^n\) and output signature \((A \to B)\), the call \(\mathit{op}(e_1, \dots, e_n)\) has denotation
where \(\Phi_w\) is the operadic action of the contraction's wiring spec \(w\) (see § Composition Rules § 4). The call site checks that each \(e_i\) has numel matching the declared \(A_i \to B_i\) signature; a mismatch raises CompileError.
3. Tupling and replication¶
3.1 Fan¶
The \(n\)-ary tupling combinator
is the Cartesian product (under the diagonal \(\Delta : X \to X^n\)) in the appropriate symmetric monoidal category. It is the morphism
3.2 Stack¶
For \(e : X \to Y\) and \(n \in \mathbb{N}_{>0}\),
a morphism \(X^{\otimes n} \to Y^{\otimes n}\).
3.3 Repeat¶
defined when \(\mathrm{dom}(\llbracket e \rrbracket) = \mathrm{cod}(\llbracket e \rrbracket)\), i.e.\ when \(\llbracket e \rrbracket\) is an endomorphism. With no explicit count, \(\mathsf{repeat}(e)\) denotes a single application of \(\llbracket e \rrbracket\) wrapped as a RepeatMorphism whose count is a learnable parameter; the \(n = 1\) default is a structural placeholder for downstream training.
3.4 Scan¶
For \(\llbracket e \rrbracket : X \otimes S \to Y \otimes S\),
where \(\mathrm{Tr}^{S} : \mathcal{C}(X \otimes S, Y \otimes S) \to \mathcal{C}(X, Y)\) is the trace operator of the appropriate traced symmetric monoidal category \(\mathcal{C}\) (Joyal, Street & Verity, 1996) eliminating the recurrent state \(S\). The trace itself is canonical; the annotation \(\mathit{init} \in \{\mathrm{zeros}, \mathrm{learned}\}\) selects the seed used by the iterative computation that realizes the trace in code, i.e. the distinguished element \(s_0 \in S\) at which the fixed-point iteration begins. Concretely:
- In \(\mathcal{V}\text{-}\mathbf{Rel}\), \(\mathrm{Tr}^{S}\) is the iterative trace, defined by algebra-join over the orbit of \(S\);
- In \(\mathbf{Stoch}\) and \(\mathbf{Kern}\), \(\mathrm{Tr}^{S}\) is implemented as a sequence of Markov-kernel compositions seeded by \(s_0\).
The runtime artefact ScanMorphism exposes a log_joint(x, hidden_states) method whose second argument is the full state trajectory of shape \((\mathrm{batch}, \mathrm{seq\_len}, \dim S)\). The argument accepts either a positional tensor of that shape or a dict \(\{k \mapsto \mathrm{tensor}\}\) keyed by state_key (default "h"); both forms denote the same Kleisli arrow with log-density \(\sum_{t} \log p(h_{t} \mid x_{t}, h_{t-1})\). The dict form is a transparent re-keying so that the inference layer's standard log_joint(x, observations: dict) contract dispatches without an adapter.
4. Parser combinators¶
The combinators \(\mathsf{parser}\), \(\mathsf{ccg}\), \(\mathsf{lambek}\), \(\mathsf{chart\_fold}\) all denote chart-parser kernels. We give the semantics in full generality for \(\mathsf{parser}\); the others are surface variations sharing the same denotational core.
Let
with \(R\) a tuple of rule names, \(C\) a tuple of atomic category names, \(s\) the start symbol, \(d\) the parse depth, and \(K\) the category constructors permitted (slash, product, …).
Let \(\mathcal{C}_{C, K}\) be the free residuated–monoidal category on the atoms \(C\) closed under the constructors \(K\). Concretely, \(\mathcal{C}_{C, K}\) is the item algebra (in the sense of Weighted Deduction Fragment §1) whose atoms are the category names \(C\) and whose constructor symbols are the residuation slashes, the monoidal product, and the diamond modality drawn from \(K\). Let \(\Sigma_R\) be the rule system: a finite signature of unary and binary inference rules over \(\mathcal{C}_{C, K}\), realized as hyperedges in the multicategory of items.
Then
is the chart-parser kernel: for an input string \(w \in \mathrm{Token}^{*}\) of length \(\le d\), it is the (semiring-weighted) sum over all \(\Sigma_R\)-derivations of the sequent \(w \vdash s\).
In the \(\mathcal{V}_{\mathrm{pf}}\)-semiring this is the inside-algorithm probability \(P(w \mid \mathit{rules})\); in the Boolean semiring it is the membership predicate \(w \in L(\Sigma_R, s)\). The denotation is independent of the parsing algorithm and depends only on the rule system.
4.1 Chart-fold¶
The desugared primitive \(\mathsf{chart\_fold}\) exposes the chart-parser kernel through morphism-valued arguments, in contrast to \(\mathsf{parser}\)'s by-name rule-list interface:
Here \(\ell\) is a morphism \(\mathrm{Token} \to \mathrm{Cat}\) (the axiom injector); \(B\) is a morphism \(\mathrm{Cat} \otimes \mathrm{Cat} \to \mathrm{Cat}\) representing the union of all binary rule schemas; \(U\) is an optional morphism \(\mathrm{Cat} \to \mathrm{Cat}\) representing the union of all unary rule schemas; \(s\) is the start category; \(d\) is the maximum category-nesting depth; \(e\) is the effect-stack depth (default 0). The denotation is the inside-algorithm chart kernel
with the same inside-score recurrence as \(\mathsf{parser}\) (Weighted Deduction Fragment §6). When \(e = 0\) the denotation reduces to the bare-residuated case of Effects §7; for \(e > 0\) each chart cell carries a stack of effects of length \(\le e\) (Effects §1) and the joint type-and-effect dispatch of Effects §4 governs firings.
\(\mathsf{parser}\), \(\mathsf{ccg}\), and \(\mathsf{lambek}\) are interchangeable surface keywords for the same expression form: each takes a list of rule names (resolved through the morphism / schema / bundle environments, with bundles spliced via Schemas §7) and assembles the corresponding \(B\) and \(U\) morphisms before constructing the inside-algorithm chart. The keyword choice is cosmetic; the standard CCG and Lambek combinator sets are addressed by naming the appropriate bundles in the rule list.
4.2 Deduction-system call sites¶
Three let-expression builtins target the agenda-driven deduction
fragment introduced by deduction NAME : … {} blocks
(Weighted Deduction Fragment §9.3):
The chart view \(\mathsf{ChartView}_{D}(x)\) exposes the deduction \(D\)'s K-presheaf on the input \(x\); its method-call surface \(\mathit{chart}.m(\mathit{args})\) denotes the corresponding presheaf evaluation:
| Postfix expression | Denotation |
|---|---|
| \(\mathit{chart}.\mathsf{weight}(i)\) | \(\alpha[i] \in K\) at the ground item \(i\). |
| \(\mathit{chart}.\mathsf{try\_weight}(i, d)\) | \(\alpha[i]\) or \(d\) or \(0_K\) if \(i \notin \mathrm{dom}\,\alpha\). |
| \(\mathit{chart}.\mathsf{enumerate}(\pi)\) | \(\{(i, \alpha[i]) \mid \pi \sim i\}\). |
| \(\mathit{chart}.\mathsf{goal\_weight}()\) | \(\bigoplus_{i \in \mathrm{goal}} \alpha[i]\). |
| \(\mathit{chart}.\mathsf{attached\_loss}\) | the cumulative attached-loss scalar. |
| \(\mathit{chart}.\mathsf{semiring}\) | the chart's semiring \(K\). |
Composition \(D_1 \mathbin{\mathrm{c}} D_2\) (Weighted Deduction
Fragment §9.1) realizes an
axiom-injector chaining: \(D_1\)'s goal items appear as \(D_2\)'s
axioms, with the resulting system inheriting \(D_2\)'s semiring,
agenda, and goal predicate. The composition's .parameters()
walks both factors' submodule side-tables, so a single fit
optimizes the joint parameter set.
Substitution \(t[v := w]\) (Weighted Deduction Fragment §9.3)
is structural: it walks \(t\) replacing every subterm equal to \(v\)
under tuple-structural equality with \(w\). Capture-avoidance is
automatic under the compile-time alpha-renaming invariant of the
binders block, since
every bound variable is canonicalised to a fresh unique symbol.
5. Coherence and equational laws¶
Every well-typed expression denotes a morphism in a symmetric monoidal category (closed in the discrete \(\mathcal{V}\)-enriched stratum; not generally closed for \(\mathbf{Stoch}\) or \(\mathbf{Kern}\)). Consequently the following equations between denotations hold by construction:
| Law | Statement |
|---|---|
| Composition associativity | \(\llbracket (e_1 \mathbin{>\!\!>} e_2) \mathbin{>\!\!>} e_3 \rrbracket = \llbracket e_1 \mathbin{>\!\!>} (e_2 \mathbin{>\!\!>} e_3) \rrbracket\) |
| Composition unit | \(\llbracket \mathsf{identity}(\tau) \mathbin{>\!\!>} e \rrbracket = \llbracket e \rrbracket = \llbracket e \mathbin{>\!\!>} \mathsf{identity}(\tau') \rrbracket\) |
| Tensor associativity | \(\llbracket (e_1 \mathbin{@} e_2) \mathbin{@} e_3 \rrbracket = \llbracket e_1 \mathbin{@} (e_2 \mathbin{@} e_3) \rrbracket\) |
| Tensor unit | \(\llbracket e \mathbin{@} \mathsf{identity}(\mathbf{1}) \rrbracket = \llbracket e \rrbracket\) |
| Bifunctoriality | \(\llbracket (e_1 \mathbin{>\!\!>} e_2) \mathbin{@} (e_3 \mathbin{>\!\!>} e_4) \rrbracket = \llbracket (e_1 \mathbin{@} e_3) \mathbin{>\!\!>} (e_2 \mathbin{@} e_4) \rrbracket\) |
| Symmetry | \(\llbracket e_1 \mathbin{@} e_2 \rrbracket = \sigma_{Y_1, Y_2} \circ \llbracket e_2 \mathbin{@} e_1 \rrbracket \circ \sigma^{-1}_{X_1, X_2}\) |
These are the equational theory of symmetric monoidal categories; together with the trace axioms (Joyal, Street & Verity 1996, §3), they constitute the equational semantics of QVR expressions.
The compiler does not normalize expressions modulo these laws; it computes a literal AST-driven tensor expression. The laws are nevertheless valid statements about denotations, and the Adequacy theorem confirms they are respected by the implementation up to the floating-point precision of the underlying tensor library.
References¶
André Joyal, Ross Street, and Dominic Verity. 1996. Traced monoidal categories. Mathematical Proceedings of the Cambridge Philosophical Society, 119(3):447–468.