Denotational Semantics of the QVR DSL¶

This section gives a mathematical interpretation of the QVR DSL and records how that interpretation relates to the current implementation. Some results are conditional on algebraic laws that the runtime interface does not verify; the chapters mark those assumptions and distinguish them from tested behavior.

The development is organized as follows.

Setting and notation. The semantic universe: \(\mathcal{V}\)-enriched symmetric monoidal closed categories, finite sets, standard Borel spaces, and the global parameters that distinguish discrete, stochastic, and continuous fragments.
Algebras and base change. The algebraic structure underlying \(\mathcal{V}\)-enriched composition, the eleven built-in algebras, and the base-change functors that mediate between them.
Composition rules. The class hierarchy \(\mathbf{CompositionRule} \supseteq \{\mathbf{BilinearForm},\ \mathbf{Semigroupoid} \supseteq \mathbf{Algebra}\}\); user-defined inline composition rules; operadic n-ary contractions via flat wirings; first-class transformations with sequential composition.
Types and spaces. The denotation of ObjectExpr and SpaceExpr syntactic categories as objects in \(\mathbf{FinSet}\) and \(\mathbf{SBor}\) respectively.
Morphisms. \(\mathcal{V}\)-relations, stochastic kernels, and continuous conditional families as the three morphism strata; their composition, tensor product, marginalization, and trace.
Expressions. Compositional semantics of expression-level combinators: >>, >>>, @, .marginalize, .change_base, fan, repeat, stack, scan, and the parser combinators.
Programs. Probability- and weighted-kernel semantics of program blocks; the denotation of bind (<-), observe, let, score, finite marginalize, and return; grouped marginalization with multi-observe fibrations; and the boundary between exact finite enumeration and ordinary sampling.
Typing and checking. The current two-layer checker: source-level objects, spaces, axes, and family shapes; QIEC kinds, indexed families, computations, lexical effect rows, handlers, and program elaboration; plus the guarantees and dynamic limits of that implementation.
Weighted deduction fragment. Item algebras, rule systems as hyperedges in a multicategory, semiring-weighted chart enumeration, axiom injectors, strategy independence, and differentiable charts. Includes learnable per-rule and bindings-keyed weights, hierarchical (parent=) and bounded (bounded) rule parameterizations, alpha-renamed binder blocks, convergent-cycle (tolerance=) chart evaluation, and the chart API (parse(D, x), compose(D_1, D_2), subst(t, v, w)) that lifts a chart's goal weight into a program's log-joint via a score step.
Schemas, rules, categories, bundles. Category atoms; rule declarations as universally-quantified hyperedges; pattern-polymorphic schema declarations; bundles as first-class rule sets; the residuated type formers \(/\), \(\backslash\), \(T(\cdot)\); free residuated category universes; object- and space-level aliases.
Structural compression. Signatures as generalized algebraic theories; encoders as initial-algebra catamorphisms into a vector carrier; decoders as Kleisli coalgebras of the Giry monad; losses as attached scalar functionals on training-site traces.
Compositional effects. Typeclass + algebraic-effects framework over a residuated category universe; class-driven schema lifting; joint type-and-effect dispatch in the chart parser; conservativity over the bare deduction fragment.
The program-shape protocol. Extraction of a compiled environment into a validating panproto Schema, plus the limits of schema equality.
Implementation correspondence and limits. Direct correspondences, test evidence, Monte Carlo qualifications, and open gaps.
Transpilation architecture. The Module -> IRProgram -> panproto.Schema -> bytes pipeline, its shared family metadata, and backend renderers.
Transpilation correctness. Structural, re-emission, external-syntax, and numeric-equivalence evidence, with per-target support notes: Stan, NumPyro, Pyro, PyMC, Edward2, Turing.jl, Gen.jl, Church, WebPPL, BUGS, and JAGS.

Declaration syntax¶

The categorical and probabilistic declarations use a shared option-block and initializer vocabulary. Their common schematic shape is:

KIND NAME : SIGNATURE [k = v, ...] [~ INIT] [BODY]

This is not a production for every declaration. QIEC declarations have their own checked forms: index, family and constructor, effect and operations, instance, handler, and computation-valued define. Their static telescopes, runtime telescopes, indexed results, and effect rows are described in Typing and checking and summarized in the grammar.

For the categorical/probabilistic shape above:

KIND is one of composition, category, object, morphism, bundle, program, contraction, export, deduction, signature, encoder, decoder, loss, schema, or rule. A define may instead introduce a QIEC computation or one of the established expression aliases such as a parser or composed morphism. let is reserved for deterministic bindings inside computations and program bodies.
SIGNATURE is a colon-prefixed phrase (an object value for object, a dom -> cod arrow for everything that denotes a morphism, an inputs / codomain shape for contraction, etc.).
[k = v, ...] is the shared option block. Each declaration or step accepts a closed set of keys and rejects ignored or misspelled entries. Options select a role, shape, family, reduction, or elaboration policy; they are not an untyped metadata bag.
~ INIT is the optional initializer: either a Family(args) clause (sampled stochastic kernel, evaluated through the family registry) or an arbitrary expr (deterministic morphism, evaluated through the expression denotation). On a morphism declaration the initializer interacts with role in the option block: role=latent admits only ~ Family(...); role=let / role=observed admits only ~ expr; role=kernel admits both.
[BODY] is an optional indented block: a rule list for composition, deduction, or signature; a step list for program; or the declaration-specific body defined by the grammar.

Pragmas are top-level attribute statements that decorate the next declaration (outer form #[k = v, ...]) or the enclosing module (inner form #![k = v, ...]). They carry the same pragma_entry shape as the unified option block; the compiler attaches the entries to the decorated declaration or module-level environment.

The deduction fragment adds a parallel form: lexicon entries and individual rule lines admit a trailing #[k = v, ...] pragma that controls per-entry / per-rule behavior (learnable, bounded, parent, weight = expr, etc.; see Weighted deduction fragment §2.1–§2.3).

Conventions¶

Throughout, we use the following conventions.

Symbol	Meaning
\(\mathcal{V}\)	A QVR algebra (see Algebras §1).
\(\otimes,\ \mathbf{1}\)	Monoidal product and unit of \(\mathcal{V}\).
\(\bigoplus\)	The join of \(\mathcal{V}\) (the costructure used to marginalize).
\(\mathbf{FinSet}\)	The category of finite sets.
\(\mathbf{SBor}\)	The category of standard Borel spaces with measurable maps.
\(\mathcal{V}\text{-}\mathbf{Rel}\)	The \(\mathcal{V}\)-enriched category of \(\mathcal{V}\)-relations on finite sets.
\(\mathbf{Stoch}\)	The Kleisli category of the (discrete) Giry monad.
\(\mathbf{Kern}\)	The category of standard Borel spaces and Markov kernels.
\(\mathcal{G}\)	The Giry monad (discrete or continuous, disambiguated by context).
\(\llbracket \phi \rrbracket\)	The denotation of phrase \(\phi\).
\(\Gamma \vdash \phi : \tau\)	\(\phi\) is well-typed of type \(\tau\) under environment \(\Gamma\).
\(\rho\)	A semantic environment (assignment of denotations to free names).

In the categorical fragment, a type is a finite-set object and a space is a standard Borel object. QIEC additionally has a Type kind for primitive, product, distribution, and indexed-family types; Typing and checking keeps those two uses separate. We write \(|X|\) for the cardinality of a finite set \(X\), and \(\dim(S)\) for the dimension of a continuous space \(S\).

Audience¶

This document is written for users who wish to reason formally about QVR programs: to verify that two .qvr files denote the same morphism, to prove that an optimization pass preserves meaning, or to understand the precise relationship between the syntactic AST, the dx.Model value-type layer, and the underlying tensor computations. Familiarity with enriched category theory at the level of Kelly's Basic Concepts of Enriched Category Theory and with the categorical foundations of probability (Giry, 1982; Fritz, 2020) is assumed.

References¶

Tobias Fritz. 2020. A synthetic approach to Markov kernels, conditional independence and theorems on sufficient statistics. Advances in Mathematics, 370:107239.
Michèle Giry. 1982. A categorical approach to probability theory. In Bernhard Banaschewski, editor, Categorical Aspects of Topology and Analysis, volume 915 of Lecture Notes in Mathematics, pages 68–85. Springer, Berlin, Heidelberg.
Gregory M. Kelly. 1982. Basic Concepts of Enriched Category Theory. Cambridge University Press; reprinted as Reprints in Theory and Applications of Categories 10 (2005):1–136.