The Program Theory

The denotational semantics of the previous pages assigns each well-typed QVR module a morphism in \(\mathbf{Kern}\) (or one of its sub-strata). This page introduces a second, schema-level denotation: every compiled module also lifts to a panproto Schema over a fixed protocol \(\mathsf{QVR}\). The two interpretations are connected by a structure-preserving map, and the schema-level interpretation is what powers diff/migrate/lens-generation tooling on .qvr programs.

1. The protocol \(\mathsf{QVR}\)

The constant QVR_PROGRAM_PROTOCOL defined in quivers.dsl.program_theory is a panproto protocol: a pair of generalised algebraic theories \((\mathcal{T}_{\mathrm{schema}}, \mathcal{T}_{\mathrm{instance}})\) together with vertex- and edge-kind declarations. Its content is summarised below.

1.1 Vertex kinds

Vertex kinds enumerate the runtime value layer:

Group Vertex kinds
Discrete objects finset, product_set, coproduct_set, free_monoid, empty_set
Continuous spaces euclidean, simplex, positive_reals, unit_interval, product_space
Declarations object_decl, space_decl, morphism_decl, stochastic_morphism_decl, continuous_morphism_decl, discretize_decl, embed_decl, program_decl, output_decl

Each vertex carries a string label (typically the declared identifier or a synthesised key) and the kind-specific payload (cardinality, dimension, family name, …).

1.2 Edge kinds

Edges encode structural relations:

Edge kind Source Target Meaning
component product_set, coproduct_set, product_space, free_monoid any vertex Position in a finite tuple
domain *_morphism_decl, program_decl object/space Domain of the declaration
codomain *_morphism_decl, program_decl object/space Codomain of the declaration
output output_decl program/morphism Output expression of the program

The instance theory \(\mathcal{T}_{\mathrm{instance}}\) is the W-type theory ThWType, so each instance is tree-shaped — appropriate for the strict tree of declarations in a .qvr module.

2. The extraction functor

The function extract_program_schema in quivers.dsl.program_theory realises a functor

\[ \mathcal{S} : \mathrm{Modules}_{\mathrm{compiled}} \to \mathrm{Schema}(\mathsf{QVR}), \]

from the category of well-typed, compiled QVR modules (with module morphisms given by environment-preserving renamings) to the category of schemas over \(\mathsf{QVR}\).

Concretely, \(\mathcal{S}\) walks the resolved environment \(\rho_{\mathrm{obj}} \cup \rho_{\mathrm{spc}} \cup \rho_{\mathrm{mor}}\) produced by the compiler and emits one vertex per binding. The walk is id-based: two structurally-equal dx.Model instances declared under different identifiers produce two distinct vertices (sharing structural payload but with distinct labels), reflecting the user's intent that distinct declarations are distinct schema elements.

3. Two denotations, one module

For a compiled module \(M\) we therefore have two denotations:

\[ \llbracket M \rrbracket_{\mathrm{kern}} \in \mathbf{Kern}\bigl(\llbracket \tau_{\mathrm{in}} \rrbracket, \llbracket \tau_{\mathrm{out}} \rrbracket\bigr), \qquad \mathcal{S}(M) \in \mathrm{Schema}(\mathsf{QVR}). \]

These are related by a forgetful projection: \(\mathcal{S}(M)\) enumerates the generators of \(\llbracket M \rrbracket_{\mathrm{kern}}\), but does not record the numerical content of any morphism (no tensor data, no learned parameters). Two modules \(M_1, M_2\) with \(\mathcal{S}(M_1) = \mathcal{S}(M_2)\) have isomorphic shape, but their kernel denotations may differ on the parameter values.

4. Diff, migrate, and lens generation

Because \(\mathcal{S}(M) \in \mathrm{Schema}(\mathsf{QVR})\), every panproto operation on schemas is automatically available on .qvr modules:

These operate on the shape of a module (its declarations and the relations between them) and not on its parameter values. Numerical-content migration — e.g.\ initialising the parameters of a renamed latent morphism from those of the original — is a separate concern, handled by panproto's field-transform layer (Field Transforms) using compute-field / coerce-type rules.

5. Naturality

The extraction \(\mathcal{S}\) is natural in the following sense. Let \(\phi : \rho \to \rho'\) be a renaming of the resolved environment that preserves structural payload (changes only identifiers). Then there is an induced renaming \(\phi^{*} : \mathcal{S}(M_{\rho}) \to \mathcal{S}(M_{\rho'})\) on the level of schemas, and \(\mathcal{S}\) commutes with this action:

\[ \mathcal{S}(M_{\phi(\rho)}) \;=\; \phi^{*}\bigl(\mathcal{S}(M_{\rho})\bigr). \]

This naturality is what licenses the use of panproto's auto-lens generation on QVR modules: the lens search may freely rename vertices, knowing that the underlying denotation is preserved up to the canonical relabelling.

6. Connection to the kernel denotation

There is an evaluation functor

\[ \mathrm{eval} : \mathrm{Schema}(\mathsf{QVR}) \times \Theta \to \mathbf{Kern} \]

that takes a schema and a parameter assignment \(\theta \in \Theta\) (where \(\Theta\) collects the parameters of all latent, stochastic, and continuous declarations in the schema) and produces the corresponding kernel. The denotation \(\llbracket M \rrbracket_{\mathrm{kern}}\) is recovered by

\[ \llbracket M \rrbracket_{\mathrm{kern}} \;=\; \mathrm{eval}\bigl(\mathcal{S}(M),\ \theta_M\bigr), \]

where \(\theta_M\) is the parameter assignment realised in the compiled module's PyTorch state. This factorisation is the formal statement that the schema layer captures the type structure and the kernel layer captures the parameter content.

The implementation does not currently expose eval as a stand-alone operation; it is implicit in the compiler's tensor-construction pass.