Types and Spaces

This page gives the denotation of the syntactic categories ObjectExpr (finite-set types) and SpaceExpr (continuous spaces). Both are interpreted compositionally by structural recursion on the syntactic constructors of quivers.dsl.ast_nodes, and both are realized by the unified resolution walk in quivers.dsl.compiler.resolution.

1. Syntactic categories

We assume the following grammar fragment, whose constructors are realized one-to-one by the AST classes named in parentheses.

\[ \begin{array}{rcl} \tau & ::= & n \;\big|\; X \;\big|\; \tau_1 \times \tau_2 \;\big|\; \tau_1 + \tau_2 \;\big|\; \tau_1 / \tau_2 \;\big|\; \tau_1 \backslash \tau_2 \;\big|\; T(\bar \tau) \\[2pt] & & \quad (\textsf{TypeName} \mid \textsf{ObjectProduct} \mid \textsf{ObjectCoproduct} \mid \textsf{ObjectSlash} \mid \textsf{ObjectEffectApply}) \\[6pt] \sigma & ::= & C(\bar a; \bar k) \;\big|\; S \;\big|\; \sigma_1 \times \sigma_2 \\[2pt] & & \quad (\textsf{ContinuousConstructor} \mid \textsf{TypeName} \mid \textsf{ObjectProduct}) \end{array} \]

Here \(n \in \mathbb{N}\) is an integer literal, \(X\) ranges over object names, \(S\) over space names, \(T\) over declared effect identifiers, and \(C \in \{\mathrm{Real}, \mathrm{Simplex}, \mathrm{Sphere}, \mathrm{Ball}, \mathrm{CholeskyFactor}, \mathrm{Covariance}, \mathrm{Correlation}, \mathrm{Orthogonal}, \mathrm{Stiefel}, \mathrm{LowerTriangular}, \mathrm{Diagonal}\}\) over constructor names. The notation \(C(\bar a; \bar k)\) stands for a constructor invocation with positional arguments \(\bar a\) and keyword arguments \(\bar k\). The two slash directions (/ and \) and the effect-apply form are residuated / effect-extended formers whose denotations live in a residuated-monoidal universe (Schemas §3); they have no denotation in the bare \(\mathbf{FinSet}\) stratum, and well-typedness restricts them to expressions whose every named atom resolves in a residuated universe such as FreeResiduated.

2. Denotation of types

Type denotation is a function

\[ \llbracket \cdot \rrbracket_{\mathrm{Ty}} : \textsf{ObjectExpr} \times \mathrm{Env}_{\mathrm{obj}} \to \mathrm{Ob}(\mathbf{FinSet}). \]

We omit the environment argument when it is clear.

\[ \begin{array}{rcl} \llbracket n \rrbracket & = & \{0, 1, \dots, n - 1\} \\[2pt] \llbracket X \rrbracket_{\rho} & = & \rho_{\mathrm{obj}}(X) \quad \text{if } X \in \mathrm{dom}(\rho_{\mathrm{obj}}) \\[2pt] \llbracket \tau_1 \times \tau_2 \rrbracket_{\rho} & = & \llbracket \tau_1 \rrbracket_{\rho} \times \llbracket \tau_2 \rrbracket_{\rho} \\[2pt] \llbracket \tau_1 + \tau_2 \rrbracket_{\rho} & = & \llbracket \tau_1 \rrbracket_{\rho} \sqcup \llbracket \tau_2 \rrbracket_{\rho} \\[2pt] \llbracket \tau_1 / \tau_2 \rrbracket_{\rho} & = & \llbracket \tau_1 \rrbracket_{\rho} \,/\, \llbracket \tau_2 \rrbracket_{\rho} \quad \text{(right residual; see [Schemas §3.1](schemas.md#31-residuation-slashes))} \\[2pt] \llbracket \tau_1 \backslash \tau_2 \rrbracket_{\rho} & = & \llbracket \tau_1 \rrbracket_{\rho} \,\backslash\, \llbracket \tau_2 \rrbracket_{\rho} \quad \text{(left residual; see [Schemas §3.1](schemas.md#31-residuation-slashes))} \\[2pt] \llbracket T(\tau_1, \dots, \tau_k) \rrbracket_{\rho} & = & T\bigl(\llbracket \tau_1 \rrbracket_{\rho}, \dots, \llbracket \tau_k \rrbracket_{\rho}\bigr) \quad \text{(effect application; see [Schemas §3.2](schemas.md#32-effect-application))} \end{array} \]

The last three cases require the surrounding object universe to be residuated and/or effect-extended; otherwise the denotation is undefined and well-typedness rejects the expression.

If \(X\) is not bound in \(\rho_{\mathrm{obj}}\) but parses as a non-negative integer literal, the literal rule is used: this allows ad-hoc cardinalities such as f : 3 -> 4 without prior object declarations.

The cartesian product \(\times\) in \(\mathbf{FinSet}\) is associative and commutative up to canonical isomorphism. The implementation chooses the right-associated, flattened representative; this is enforced by the _flatten_products converter on ProductSet.components and the analogous flattener on CoproductSet.components. The chosen representatives are equal (not merely isomorphic) under the dx.Model structural equality used throughout the codebase.

2a. Object initializers

The surface form

object X : value

admits five initializer shapes for the right-hand side value, each binding \(X\) to a concrete object of \(\mathbf{FinSet}\) or \(\mathbf{SBor}\) built from explicit data rather than from a syntactic ObjectExpr. Each is interpreted at the value layer and contributes its denotation directly to \(\rho_{\mathrm{obj}}(X)\) (or \(\rho_{\mathrm{spc}}(X)\) for the continuous-space initializer):

Initialiser	Denotation
FinSet n	a finite set of cardinality \(n\)
Real d (or any other ContinuousSpace family invocation)	a standard Borel space of the named family at the supplied parameters
{e_1, …, e_n}	the enum set on the named labels (§2a.1)
FreeMonoid(X, max_length = n)	the bounded Kleene closure (§2a.2)
FreeResiduated(G, depth = d, ops = O)	the depth-bounded free residuated category over \(G\) (§2a.3)

The five initialisers share a single declaration form: there is no space X : … keyword variant. Whether \(X\) lands in \(\mathbf{FinSet}\) or \(\mathbf{SBor}\) is decided by the family invoked on the right-hand side; the surrounding object keyword is uniform.

2a.1 Enum sets

object Atoms = {NP, S, VP}

denotes the finite set whose elements are exactly the named labels, ordered by declaration position:

\[ \llbracket \{e_1, \dots, e_n\} \rrbracket \;=\; \{e_1, \dots, e_n\}, \qquad |{\cdot}| = n. \]

The label identity is part of the object: two enum sets with the same cardinality but different labels are different objects of \(\mathbf{FinSet}\) under the dx.Model structural equality used throughout the codebase.

A category C_1, …, C_n declaration is the singleton-cardinality special case (Schemas §1).

2a.2 Free monoids

The FreeMonoid(X, max_length = n) initializer binds \(X\) to the bounded Kleene closure of the generator set. See §3 below for the denotation.

2a.3 Free residuated categories

The FreeResiduated(G, depth = d, ops = O) initializer binds \(X\) to a finite enumeration of category expressions over the generators, closed under the chosen residuation operations up to a depth bound. The denotation is given in Schemas §4.

3. Free monoids

The runtime value layer exposes a FreeMonoid object class, which arises in the deduction fragment as the carrier of strings over an alphabet (see Weighted Deduction Fragment). At the surface, FreeMonoid(X, max_length = n) appears only as an object initializer (§2a.2 above), not as a ObjectExpr constructor: a free monoid must be bound to an object name via object Words = FreeMonoid(...) before it can be referenced as a type.

The denotation of FreeMonoid(generators = X, max_length = n) is the bounded Kleene star

\[ \llbracket \mathrm{FreeMonoid}(X, n) \rrbracket \;=\; \coprod_{k = 0}^{n} \rho_{\mathrm{obj}}(X)^{k}, \]

a finite set of size \(\sum_{k=0}^{n} |\rho_{\mathrm{obj}}(X)|^{k}\). The bound \(n\) is supplied by the grammar's depth parameter; the unbounded free monoid \(\rho_{\mathrm{obj}}(X)^{*}\) is countably infinite and is not realized as a SetObject.

4. Denotation of spaces

The continuous-space sublanguage is the family-registry surface Real d, Simplex d, plus the matrix-manifold and submanifold variants below, combined under product via *. Each of these is a family invocation against the ContinuousSpace family registry:

Surface	Family identifier	Carrier	Parameters
Real d	Euclidean	\(\mathbb{R}^d\)	dimension \(d\), optional low= / high= bounds (use low=0 for \((0, \infty)^d\) once a positive prior is attached; low=0, high=1 for \([0,1]^d\))
Simplex d	Simplex	\(\Delta^{d-1}\)	dimension \(d\)
Sphere d	Sphere	\(S^{d-1} \subset \mathbb{R}^d\)	ambient dimension \(d\)
Ball d [radius = r]	Ball	\(\{x \in \mathbb{R}^d : \lVert x \rVert_2 \le r\}\)	ambient dim \(d\), radius \(r\)
CholeskyFactor d	CholeskyFactor	unit-row-norm lower-triangular \(d \times d\)	\(d\)
Covariance d	Covariance	\(\mathrm{Sym}^+_d\) (SPD cone)	\(d\)
Correlation d	Correlation	SPD with unit diagonal	\(d\)
Orthogonal d	Orthogonal	\(O(d) \subset \mathbb{R}^{d \times d}\)	\(d\)
Stiefel(rows, cols)	Stiefel	\(V_K(\mathbb{R}^N)\) with \(K \le N\)	rows \(N\), cols \(K\)
LowerTriangular d	LowerTriangular	\(d \times d\) lower-triangular	\(d\)
Diagonal d	Diagonal	\(\mathbb{R}^d\) via diagonal embedding	\(d\)

The surface Real d resolves to the Euclidean class through the same family-registry lookup. New continuous-space families register through the same registry without surface keyword changes once the grammar adds the constructor name to the ContinuousConstructor AST node's accepted Literal[...], and the surface Family d [args] denotes Family(d, **args) against the registry.

For the matrix-manifold variants (CholeskyFactor, Covariance, Correlation, Orthogonal, Stiefel, LowerTriangular) the carrier is a flat \(d \times d\) (or \(N \times K\)) tensor laid out row-major; the on-manifold predicate is enforced by the sampling family that targets the space, not by the type. The membership check ContinuousSpace.contains returns a per-batch boolean mask testing the manifold equations up to a fixed numerical tolerance (symmetric and SPD for Covariance; orthogonal columns for Stiefel, etc.).

Space denotation is a function

\[ \llbracket \cdot \rrbracket_{\mathrm{Sp}} : \textsf{SpaceExpr} \times \mathrm{Env}_{\mathrm{spc}} \times \mathrm{Env}_{\mathrm{obj}} \to \mathrm{Ob}(\mathbf{SBor}). \]

For brevity write \(\rho = (\rho_{\mathrm{spc}}, \rho_{\mathrm{obj}})\). The constructor cases are:

\[ \begin{array}{rcl} \llbracket \mathrm{Euclidean}(d) \rrbracket & = & \mathbb{R}^{d} \\[2pt] \llbracket \mathrm{Euclidean}(d; \mathrm{low} = \ell, \mathrm{high} = h) \rrbracket & = & \prod_{i=1}^{d} [\ell, h] \\[2pt] \llbracket \mathrm{Simplex}(d) \rrbracket & = & \Delta^{d-1} \;=\; \Bigl\{ x \in \mathbb{R}^{d}_{\ge 0} \,\Big|\, \textstyle\sum_i x_i = 1 \Bigr\} \\[2pt] \llbracket \mathrm{Sphere}(d) \rrbracket & = & S^{d-1} \;=\; \bigl\{ x \in \mathbb{R}^{d} : \lVert x \rVert_2 = 1 \bigr\} \\[2pt] \llbracket \mathrm{Ball}(d; \mathrm{radius} = r) \rrbracket & = & \bigl\{ x \in \mathbb{R}^{d} : \lVert x \rVert_2 \le r \bigr\} \\[2pt] \llbracket \mathrm{Covariance}(d) \rrbracket & = & \mathrm{Sym}^{+}_{d} \;=\; \bigl\{ M \in \mathbb{R}^{d \times d} : M = M^{\top},\ M \succ 0 \bigr\} \\[2pt] \llbracket \mathrm{Correlation}(d) \rrbracket & = & \bigl\{ R \in \mathrm{Sym}^{+}_{d} : R_{ii} = 1 \text{ for all } i \bigr\} \\[2pt] \llbracket \mathrm{CholeskyFactor}(d) \rrbracket & = & \bigl\{ L \in \mathbb{R}^{d \times d} : L_{ij} = 0 \text{ if } j > i,\ \textstyle\sum_{j \le i} L_{ij}^{2} = 1 \bigr\} \\[2pt] \llbracket \mathrm{Orthogonal}(d) \rrbracket & = & O(d) \;=\; \bigl\{ Q \in \mathbb{R}^{d \times d} : Q^{\top} Q = I_{d} \bigr\} \\[2pt] \llbracket \mathrm{Stiefel}(N, K) \rrbracket & = & V_{K}(\mathbb{R}^{N}) \;=\; \bigl\{ X \in \mathbb{R}^{N \times K} : X^{\top} X = I_{K} \bigr\} \\[2pt] \llbracket \mathrm{LowerTriangular}(d) \rrbracket & = & \bigl\{ L \in \mathbb{R}^{d \times d} : L_{ij} = 0 \text{ if } j > i \bigr\} \\[2pt] \llbracket \mathrm{Diagonal}(d) \rrbracket & = & \mathbb{R}^{d} \quad \text{(diagonal embedding into } \mathbb{R}^{d \times d}\text{)} \end{array} \]

each carrying its standard Borel \(\sigma\)-algebra (inherited as a Borel submanifold of the ambient \(\mathbb{R}^{d}\) or \(\mathbb{R}^{d \times d}\)). The matrix carriers (CholeskyFactor, Covariance, Correlation, Orthogonal, Stiefel, LowerTriangular) are stored as flat row-major tensors; the manifold equations cut out a smooth submanifold of the ambient Euclidean space and the Borel structure descends. The remaining cases are:

\[ \begin{array}{rcl} \llbracket S \rrbracket_{\rho} & = & \rho_{\mathrm{spc}}(S) \quad \text{if } S \in \mathrm{dom}(\rho_{\mathrm{spc}}) \\[2pt] \llbracket S \rrbracket_{\rho} & = & \iota\bigl(\rho_{\mathrm{obj}}(S)\bigr) \quad \text{otherwise, if } S \in \mathrm{dom}(\rho_{\mathrm{obj}}) \\[2pt] \llbracket \sigma_1 \times \sigma_2 \rrbracket_{\rho} & = & \llbracket \sigma_1 \rrbracket_{\rho} \times \llbracket \sigma_2 \rrbracket_{\rho} \end{array} \]

where \(\iota : \mathbf{FinSet} \hookrightarrow \mathbf{SBor}\) is the canonical inclusion (every finite set as a discrete standard Borel space). The fallback rule for SpaceName allows mixed-domain ProductSpace instances such as Real(3) * Token where Token : 256 is a previously declared object. The denotation is the product in \(\mathbf{SBor}\), which is well-defined precisely because \(\iota\) is a faithful functor preserving finite products.

5. Coherence

The two type-formers \(\times\) and \(+\) on ObjectExpr are interpreted by the cartesian product and disjoint union in \(\mathbf{FinSet}\), both of which are associative, commutative, and unital up to canonical isomorphism (with units the singleton \(\mathbf{1}\) and the empty set \(\emptyset\) respectively). Concretely:

• The flattening converters on ProductSet and CoproductSet realize the coherence isomorphisms \(((\tau_1 \times \tau_2) \times \tau_3) \cong (\tau_1 \times (\tau_2 \times \tau_3))\) as identities on the chosen representative.
• Empty products denote \(\mathbf{1}\) (a singleton; EmptySet for coproducts denotes \(\emptyset\)).
• The EmptySet constructor in categorical.monoidal is the unit for \(+\).

Mac Lane's coherence theorem guarantees that any two parses of the same ObjectExpr denote equal finite sets in \(\mathbf{FinSet}\), not merely isomorphic ones, when the implementation uses the canonical flattened normal form.

6. Resolution in code

Both denotations are realized by a single unified walk on ObjectExpr in quivers.dsl.compiler.resolution. The mixin _ResolutionMixin exposes _resolve_any_space, which dispatches on the AST kind field and returns either a SetObject (for DiscreteConstructor / TypeName / ObjectProduct / ObjectCoproduct resolving to finite sets) or a ContinuousSpace (for ContinuousConstructor / TypeName / ObjectProduct resolving to continuous spaces, including mixed-domain ProductSpace instances such as Real(3) * Token where Token : 256 is a previously declared finite object). The narrowing wrapper _resolve_type constrains the result to the discrete stratum so callers that know they want a SetObject can demand one without re-encoding the constraint at every call site. The mixed-domain case is well-defined precisely because the inclusion \(\iota : \mathbf{FinSet} \hookrightarrow \mathbf{SBor}\) is a faithful functor preserving finite products.