DSL Declarations¶

This page covers every declaration form a .qvr module can carry apart from program blocks and operadic contractions, which have their own pages (Programs and Let-Expressions, Contractions). The grammar summary lives in the Overview.

Algebra¶

Choose the enriching algebra (optional, defaults to product_fuzzy):

composition product_fuzzy as algebra
composition boolean as algebra
composition lukasiewicz as algebra
composition godel as algebra
composition tropical as algebra
composition max_plus as algebra
composition log_prob as algebra
composition markov as algebra
composition real as algebra
composition probability as algebra
composition counting as algebra

The keyword algebra resolves a name against the built-in composition-rule registry and verifies the registered rule is at the Algebra level. Three weaker levels are also surface-declarable:

composition material_impl as semigroupoid
composition some_bf as bilinear_form
composition any_rule as rule

A semigroupoid level promises associativity but not an identity; bilinear_form promises neither; rule is permissive and accepts any rule in the registry. Operations that need the identity element (identity(A), f.dagger, f.trace(A), cup(A), cap(A)) compile only under algebra. See Composition Rules for the algebraic hierarchy and the operadic contraction surface.

A composition rule can also be defined inline via an indented body, with each entry a let-expression:

composition my_godel as algebra
    tensor_op(a, b) = a * b
    join(t)         = sum(t)
    unit            = 1.0
    zero            = 0.0

composition my_semi as semigroupoid
    tensor_op(a, b) = a * b
    join(t)         = sum(t)

composition my_bf as bilinear_form
    tensor_op(a, b) = (a + b) * 0.5
    join(t)         = sum(t)

algebra bodies require tensor_op, join, unit, zero (with optional negation and meet); semigroupoid and bilinear_form bodies require only tensor_op and join. The compiler verifies the entry set against the declared level.

Object¶

Three surface forms:

# 1. anonymous-element FinSet of given cardinality, or a TypeExpr
object X : FinSet 3          # FinSet [name="X", cardinality=3]
object Y : FinSet 4
object XY : X * Y     # ProductSet(components=(X, Y))
object Sum : X + Y    # CoproductSet(components=(X, Y))

# 2. FreeMonoid, bounded Kleene closure over a FinSet of generators.
object Strings = FreeMonoid(X, max_length=4)

# 3. Residuated universe.
object Cat = FreeResiduated(Atoms, depth=4, ops=[slash])

Object-shaped aliases (resolvable to a SetObject) are interchangeable with the underlying object, so morphism f : Pair -> X [role=latent] is well-formed when Pair = X * Y.

Morphism¶

Declare a learnable or fixed morphism:

# Latent (learnable)
morphism f : X -> Y [role=latent]

# With init scale
morphism g : Y -> Z [role=latent, scale=0.3]

# Observed (fixed)
morphism h : X -> X = identity(X) [role=observed]

Latent morphism prior¶

A latent morphism declaration accepts a trailing ~ Family(args) clause that puts a prior on its representing tensor. The literal (args) carry the prior's hyperparameters at declaration time (in contrast to kernel's ~ Family clause, whose parameters come from a neural network at sample time). The axis-role configuration (over=, iid_over=) and any other modifiers live in the morphism's option block, before the ~. The compiler desugars the prior into a fresh sample site whose value is the tensor representing the morphism, making the morphism a deterministic wrap of that random tensor.

# Free-parameter morphism (point estimate; MLE / MAP target).
morphism W : Real D -> Real K [role=latent]

# The same morphism with a Matrix-Normal prior on its tensor.
morphism W : Real D -> Real K [role=latent, over=[dom, cod]]
    ~ MatrixNormal(0.0, 1.0, 1.0)

The axis-role clause is fully detailed alongside the program-step bind and observe forms.

Init recipes (`[init=auto]`)¶

The [init=auto] option overrides the default randn * scale init with the active algebra's saturation-free recipe, derived from Algebra.init_spec(depth, intermediate_size). For ProductFuzzy, Boolean, Gödel, Łukasiewicz, and Probability the recipe is applied through LatentMorphism's sigmoid bijector (the raw parameter is set via logit(value)); for the other algebras the recipe is applied to the raw parameter directly.

morphism W : Real D -> Real K [role=latent, init=auto]

The per-algebra recipes ensure that a fresh model with [init=auto] on every latent starts with intermediate activations close to the algebra's neutral element, avoiding saturated sigmoids on truth-valued algebras and exploding products on multiplicative algebras. See recommend_init and saturation_warnings in the fitting and diagnostics guide for the dynamic counterpart that audits a trained module.

Space¶

Declare a continuous space:

object R3 : Real 3
object R2_bounded : Real 2 [low=0.0, high=1.0]
object U : UnitInterval
object P2 : PositiveReals(2)
object S3 : Simplex 3

# Product space
object RU : R3 * U

Spaces resolve to subclasses of ContinuousSpace; see the continuous spaces guide for the full hierarchy and constraints.

Named composites¶

object is the only top-level type-introduction keyword: discrete sets, continuous spaces, and any composite (products, coproducts, residuated patterns) all enter the environment as object declarations whose RHS is an object expression.

object Hidden : Real 64
object Output : Real 32
object Combined : Hidden * Output

# Residuated / Lambek-style patterns are object expressions too.
object Sentence : S \ NP

A declared object can be referenced by name in any subsequent declaration; the compiler substitutes it wherever the name appears in a domain or codomain position.

Kernel¶

The kernel keyword declares a Markov kernel A -> B. Two shapes:

Without a ~ clause: a finite-set lookup-table kernel A -> D(B), realized as a learnable matrix of conditional probabilities.
With a ~ Family [options] [axis_role_clause] clause: a parametric kernel A -> G(B) whose family parameters come from the input by a parameter network at sample time. The optional axis-role clause configures the family's event / batch decomposition over codomain factors.

# Lookup-table kernel on finite sets.
morphism s : X -> Y [role=kernel]
morphism cat : X -> Y * Z [role=kernel]

# Parametric kernel: input-conditional Normal on R^3.
morphism f : X -> R3 [role=kernel] ~ Normal
# Family options control the parameter network.
morphism g : R3 -> R3 [role=kernel] ~ Normal [scale=0.5]
morphism k : X -> S3 [role=kernel] ~ Dirichlet
# 30+ families are registered; see the families guide.
morphism flow : R3 -> R3 [role=kernel] ~ Flow [n_layers=6, hidden_dim=32]

The kernel keyword unifies the discrete (finite-set lookup) and continuous / stochastic (parametric Family) cases under one surface; the runtime branches on whether the codomain is a FinSet or a ContinuousSpace.

Discretize¶

Convert a continuous space to a finite set via binning:

# Discretize a UnitInterval `U` into 20 bins.
morphism d : U -> FinSet 20 [role=discretize, bins=20]

# Discretize an R^3 box into 100 bins.
morphism d2 : R3 -> FinSet 100 [role=discretize, bins=100]

The runtime realization is Discretize, which produces uniform-width bins on bounded supports.

Embed¶

Embed a discrete object into a continuous space:

# Embed a finite-set value into R^3 (treated as uniform).
morphism e : X -> R3 [role=embed]

The runtime realization is Embed.

Deduction¶

A deduction NAME : Domain -> Codomain [options] declaration with an indented body declares an agenda-based weighted deduction. See the weighted deduction systems guide for the framework and the semiring layer for the scoring algebra. The seven irreducible parameters of an agenda-driven deduction (item algebra, rule set, semiring, axiom source, goal predicate, start symbol, depth bound) become named fields in the block:

deduction CCG : Term -> Term [semiring=LogProb, start=S, depth=6]
    atoms NP, S, N, VP, PP, Fwd, Bwd, span

    rule fwd_app
        : span(I, K, Fwd(X, Y)), span(K, J, Y)
        |- span(I, J, X)

    rule bwd_app
        : span(I, K, Y), span(K, J, Bwd(X, Y))
        |- span(I, J, X)

atoms NAME, NAME, ... declares the closed constructor universe. Every identifier appearing in a rule pattern must be either an atom or a single-uppercase wildcard variable (X, Y, Z, I, J, K, ...).
rule NAME : premises |- conclusion is a sequent. Premises are comma-separated; arity is arbitrary (unary rules fire on a single chart cell, binary on a pair of adjacent cells, etc.). A trailing #[learnable] pragma marks the rule's weight as bindings-keyed and learnable.
semiring=... in the option block selects the scoring algebra: LogProb, Viterbi, Boolean, Counting.
start=... declares the goal-item predicate (the start atom).
depth=... bounds the conclusion-category constructor depth so the agenda terminates on cyclic rule graphs.
tolerance=... (optional) enables Kleene-star convergence detection in the chart's aggregation, paired with rule-level #[learnable, bounded] for contractive-cycle log-weights.

Pattern variables are single uppercase identifiers; every other identifier in a rule pattern must be listed in atoms. A variable appearing more than once in the same rule must unify across occurrences.

Slash, tensor, and modal type constructors are user-declared atoms, not built-in syntax: Fwd(X, Y) ≡ X/Y, Bwd(X, Y) ≡ X\Y, Tns(X, Y) ≡ X⊗Y, Dia(X) ≡ ◇X, Box(X) ≡ □X, Cont(X) ≡ continuation-typed X. The user is free to introduce additional constructors for any algebra the deduction reasons over.

Axiom sources¶

A deduction needs an axiom-injection kernel that maps an input into initial weighted chart items. The block admits three forms:

deduction PCFG : Term -> Term [semiring=LogProb, start=S]
    atoms S, NP, VP, Det, N, V, the, cat, sleeps, span, leaf
    rule branch : span(I, K, B), span(K, J, C) |- span(I, J, A) #[learnable]
    rule anchor : leaf(I, T)                    |- span(I, J, A) #[learnable]

    # Inline lexicon: label-indexed lookup.
    lexicon
        "the"    : Det = the    #[learnable]
        "cat"    : N   = cat    #[learnable]
        "sleeps" : V   = sleeps #[learnable]

The three alternatives:

Form	Use when
`lexicon` block with `"word" : Cat = lf #[learnable]` entries	label-indexed lookup table inline in the body
`lexicon from "path.tsv" [learnable]`	label-indexed lookup loaded from a TSV at compile time
`[axioms=some_morphism]` in the deduction's option block	general kernel `Input -> List(Item × K)` defined as a declared morphism

Marking a lexicon entry #[learnable] allocates an nn.Parameter log-weight initialised to 0.0.

Chart-query expressions¶

The runtime view of a compiled deduction exposes the chart as a first-class differentiable value with four query methods. Inside a program block (Kleisli-bind sigil <-), a deduction call yields a chart value:

program parse_score : Sentence -> Real [effects=[Sample, Score]]
    sample chart <- CCG(input)
    let w = chart.goal_weight()
    observe valid <- Bernoulli(sigmoid(w))
    return w

chart.weight(item): log-weight of a fully-determined item.
chart.enumerate(pattern): list of (item, weight) pairs matching a pattern with wildcards.
chart.derivations(item): derivation forest under the derivation semiring.
chart.goal_weight(): log-weight of the goal predicate.

Each returns a torch.Tensor whose gradients flow back through the agenda's semiring operations to any learnable axiom or rule weight.

Replicated declarations¶

Declare N independent copies of a morphism. Each copy has independent parameters; the base name becomes a group that can be referenced by fan:

# creates head_0, head_1, head_2, head_3 with independent parameters
morphism head : Latent -> HeadOut [role=kernel, replicate=4, scale=0.1] ~ Normal

# works on every morphism whose role permits replication:
morphism T    : State -> Obs [role=kernel, replicate=3]               # lookup-table kernel
morphism emit : State -> Obs [role=kernel, replicate=3] ~ Normal      # parametric kernel
morphism tok  : Token -> Hidden [role=embed, replicate=2]              # finite-to-Real

Combinators on morphisms¶

These combinators appear inside let declarations to assemble morphisms from simpler pieces. They live at the expression level, outside program blocks.

Fan-out (diagonal morphism)¶

Copy a single input to N morphisms and concatenate their outputs. Accepts explicit morphism names or a group name from a replicated declaration:

# explicit: fan-out to three named morphisms
let parallel = fan(f, g, h)

# group expansion: fan(head) expands to fan(head_0, head_1, head_2, head_3)
morphism head : Latent -> HeadOut [role=kernel, replicate=4, scale=0.1] ~ Normal

let multi_head = fan(head)

# commonly followed by a projection to recombine
morphism proj : Combined -> Latent [role=kernel] ~ Normal [scale=0.1]
let attention = fan(head) >> proj

All component morphisms must have the same domain. The output dimension is the sum of all component codomain dimensions.

Repeat (iterated composition)¶

Compose a morphism (or composed expression) with itself N times. Two forms are available.

Static repeat. Count known at compile time, unrolled into a fixed composition chain:

# transition >> transition >> transition
let deep = repeat(transition, 3)

# works with composed expressions too
let layer = attn >> residual >> ffn >> residual
let deep_model = repeat(layer, 6)

# repeat(f, 1) = f
let same = repeat(f, 1)

Runtime-variable repeat. Count omitted, creates a RepeatMorphism whose step count is set via Program.forward(n_steps=N). Uses repeated squaring for \(O(\log n)\) compositions:

morphism transition : State -> State [role=kernel]
morphism emission : State -> Obs [role=kernel]

# runtime-variable: no count specified
let n_step = repeat(transition) >> emission

export n_step

prog = load("hmm.qvr")
obs_3 = prog(n_steps=3)    # T^3 >> E
obs_50 = prog(n_steps=50)  # T^50 >> E, same model, different length

The morphism's codomain must match its domain (endomorphism) for repeat to work.

Stack (independent multi-layer)¶

Create N independent deep copies of a morphism, each with its own parameters (no weight-tying):

# stack creates independent parameters per layer
let deep = stack(transition, 3)  # 3 layers, each with own params

# repeat reuses the same parameters (weight-tying)
let tied = repeat(transition, 3)  # 3 iterations, shared params

Unlike repeat, which composes a morphism with itself using the same parameters, stack(f, N) creates N fresh deep copies of f, each with independent learnable parameters. This is essential for deep neural networks where each layer has distinct parameters.

Scan (temporal recurrence)¶

Thread hidden state across a sequence using a recurrent cell:

# Basic syntax: cell has product domain A * H -> H
morphism cell : Embedded * Hidden -> Hidden [role=kernel] ~ Normal [scale=0.1]
let rnn = tok_embed >> scan(cell) >> output_proj

# With learned initial state (default is zeros)
let rnn_learned = tok_embed >> scan(cell, init=learned) >> output_proj

The scan combinator implements temporal recurrence by threading hidden state H across a sequence:

Cell signature. The morphism passed to scan must have a product domain A * H -> H, where A is the input type at each step and H is the hidden state type. The codomain must equal H (an endomorphism on the hidden state).
Execution. Given a sequence of inputs [x_0, x_1, ..., x_T] (implicit in batch-first tensor shape [batch, seq_len, input_dim]), scan computes:
h_0 = zeros(H) or a learned initial state (if init=learned)
h_t = cell(x_t, h_{t-1}) for t = 1..T
Returns the final hidden state h_T
Type. If cell : A * H -> H, then scan(cell) : A -> H. The sequence dimension is implicit in the tensor's second dimension.
Works with both forms. Parametric kernels (morphism cell : A * H -> H [role=kernel] ~ Normal) and MonadicPrograms (program cell(x, h) : A * H -> H with bind / let / return).

Example: vanilla RNN.

object Token : FinSet 256
object Embedded : Real 64
object Hidden : Real 128
object Output : Real 64

morphism tok_embed : Token -> Embedded [role=embed]

morphism cell : Embedded * Hidden -> Hidden [role=kernel] ~ Normal [scale=0.1]
morphism output_proj : Hidden -> Output [role=kernel] ~ Normal [scale=0.1]
let rnn = tok_embed >> scan(cell) >> output_proj

export rnn

For deeper temporal models, stack multiple scans:

let deep_rnn = tok_embed >> scan(cell_1) >> scan(cell_2) >> output_proj

Each scan threads its own hidden state independently.

Backward composition¶

Compose morphisms in reverse order using <<, or use Kleisli composition <=>:

# forward composition (both equivalent):
let fg = f >> g
let fg = f >=> g

# backward composition:
let gf = g << f    # equivalent to f >> g

<< reverses the direction of composition; >=> is the Kleisli composition operator (composes Markov kernels in Stoch or Kern).

Curry combinators (residuation witnesses)¶

The .curry_right and .curry_left postfix combinators witness the right- and left-residuation isomorphisms. For an inner morphism f : X * Y -> Z:

Postfix	Result
`f.curry_right`	morphism `X -> Z/Y`
`f.curry_left`	morphism `Y -> X\Z`

Underlying tensor data is unchanged; only the domain / codomain factoring is reinterpreted. Validity requires the inner morphism's domain to factor as a non-trivial product.

object X : FinSet 3
object Y : FinSet 4
object Z : FinSet 5
morphism f : X * Y -> Z [role=latent]
let g = f.curry_right    # g : X -> Z/Y
export g

The Lambek calculus inference rules (forward / backward application) become theorems derivable from identity + curry.

Top-level `let` declarations¶

Compose morphisms and bind:

let fg = f >> g
let par = f @ g
let marg = fg.marginalize(Y)
let composed = f >> g >> h

For arithmetic and family-argument let expressions inside a program block, see Programs and Let-Expressions.

`where` clauses¶

Attach local let-bindings to a top-level let declaration using where:

let model = embed >> layers >> output_proj

where

    let layers = stack(transition, 3)
    let embed = tok_embed

The where keyword introduces a block of local definitions scoped to the parent let binding. This improves readability for complex nested compositions.

Structural compression: `signature`, `encoder`, `decoder`, `loss`¶

The structural-compression surface gives transformers, tree LSTMs, GNNs, RNNs, autoregressive language models, and the vector inside-outside parser as instances of one interface. A signature { ... } block declares sorts and constructors over a free term algebra. An encoder { ... } block declares a per-constructor parametric function realizing the F-algebra homomorphism from terms to vectors. A decoder { ... } block declares the dual Kleisli arrow from vectors back to terms. A loss { ... } block attaches a training objective at any site in the graph.

The four blocks are detailed in Structural Compression: Signatures and Encoders and Structural Compression: Decoders and Losses.

Export¶

Export a morphism as a compiled program output. Any number of export declarations may appear per module; each is compiled into a separate output:

export f
export fg
export my_prog