Signatures

Multi-sorted algebra signatures with constructors, typed binders, and optional vertex and edge kinds for graph-shaped signatures. These objects are the runtime carriers of signature { … } DSL declarations.

The de Bruijn discipline is enforced structurally: a BoundVar(i) term carries an integer index; binders push a fresh ContextEntry(var_sort, embedding, type_term) onto an implicit context Γ tracked by the encoder / decoder runtime. Binder variables may carry an annotation sort: the variable's type is stored alongside its embedding in Γ.

signature

Signatures: typed multi-sorted algebras with binders.

A Signature is the runtime form of a signature { … } DSL declaration. It carries the sort table, constructor table, binder table, and (for graph-shaped signatures) vertex / edge kind tables.

Terms over a signature are first-class Python values (Term instances): each carries the constructor / binder name and its positional arguments. The framework's encoder and decoder runtimes walk these records uniformly.

The de-Bruijn discipline is enforced structurally: a BoundVar term carries an integer index; binders push a fresh entry onto an implicit context Γ tracked by the encoder / decoder runtime.

All structured value types in this module are didactic didactic.api.Model records, matching the quivers convention for schema-bearing data; the only fields held opaque are runtime-only artefacts that don't round-trip (torch tensors, arbitrary Python data leaves).

SortVocabEntry didactic-model

SortVocabEntry(*, kind: Literal['string', 'integer', 'float'], value: DataLeaf)

Bases: Model

One closed-vocabulary entry on a data sort.

Each entry is a tagged Python value: kind is the leaf type ("string" | "integer" | "float"), value is the decoded Python value (str, int, or float).

Sort didactic-model

Sort(*, name: str, kind: SortKind, dim: int | None = None, vocab: tuple[SortVocabEntry, ...] = ())

Bases: Model

A sort declaration: name, kind, optional dim, optional closed vocabulary.

A data sort may carry a vocab tuple of SortVocabEntry records. Object / index sorts must have an empty vocab (the framework checks at runtime).

vocab_values property

vocab_values: tuple[DataLeaf, ...]

The decoded Python values in declaration order.

Constructor didactic-model

Constructor(*, name: str, domain: tuple[str, ...] = (), codomain: str = '')

Bases: Model

A typed constructor symbol.

arity property

arity: int

The number of arguments the constructor takes.

BinderVarSpec didactic-model

BinderVarSpec(*, var: str, sort: str, annot_sort: str | None = None)

Bases: Model

A scoped variable introduced by a binder.

sort is the variable's own sort. annot_sort is the sort of an optional type annotation, a sibling argument in the enclosing Term that travels alongside the variable's embedding in Γ. Used to track per-variable type information.

BinderArgSpec didactic-model

BinderArgSpec(*, arg: str, sort: str)

Bases: Model

A scoped argument of a binder.

Binder didactic-model

Binder(*, name: str, binds: tuple[BinderVarSpec, ...] = (), scoped: tuple[BinderArgSpec, ...] = (), codomain: str = '')

Bases: Model

A binder constructor: introduces variables of given sorts into the scope of given arguments.

arity property

arity: int

The number of positional arguments of the binder in a Term.

Each annotated bound variable contributes one annotation argument, and each scoped argument contributes one more.

domain

domain() -> tuple[str, ...]

Positional sort sequence of the binder's arguments in the enclosing Term: type-annotations for each annotated bound variable (in declaration order, outer-context-evaluated), followed by the scoped arguments (extended-context-evaluated).

RETURNS	DESCRIPTION
tuple[str, ...]	The sort name of each positional argument.

Source code in src/quivers/structural/signature.py

def domain(self) -> tuple[str, ...]:
    """Positional sort sequence of the binder's arguments in the
    enclosing `Term`: type-annotations for each annotated
    bound variable (in declaration order, outer-context-evaluated),
    followed by the scoped arguments (extended-context-evaluated).

    Returns
    -------
    tuple[str, ...]
        The sort name of each positional argument.
    """
    return tuple(
        b.annot_sort for b in self.binds if b.annot_sort is not None
    ) + tuple(a.sort for a in self.scoped)

VertexKind didactic-model

VertexKind(*, name: str, kind: SortKind, dim: int | None = None)

Bases: Model

A vertex kind in a graph-shaped signature.

EdgeKind didactic-model

EdgeKind(*, name: str, src: str, tgt: str, directed: bool = True)

Bases: Model

An edge kind in a graph-shaped signature.

Signature didactic-model

Signature(*, name: str, params: tuple[str, ...] = (), sorts_t: tuple[Sort, ...] = (), constructors_t: tuple[Constructor, ...] = (), binders_t: tuple[Binder, ...] = (), vertex_kinds_t: tuple[VertexKind, ...] = (), edge_kinds_t: tuple[EdgeKind, ...] = ())

Bases: Model

A multi-sorted algebra signature with optional binders / graph structure.

Sort, constructor, binder, vertex_kind and edge_kind tables are represented as tuples of records (rather than dicts) so the enclosing dx.Model keeps a schema-bearing layout. The runtime exposes O(1) name-keyed lookup methods (sort(name), constructor(name), etc.) on top of those tuples.

sorts property

sorts: dict[str, Sort]

The sort declarations keyed by sort name.

constructors property

constructors: dict[str, Constructor]

The constructor declarations keyed by constructor name.

binders property

binders: dict[str, Binder]

The binder declarations keyed by binder name.

vertex_kinds property

vertex_kinds: dict[str, VertexKind]

The graph vertex kinds keyed by kind name.

edge_kinds property

edge_kinds: dict[str, EdgeKind]

The graph edge kinds keyed by kind name.

is_inductive

is_inductive() -> bool

Whether the signature declares any constructor or binder.

RETURNS	DESCRIPTION
bool	True when terms over the signature are inductive.

Source code in src/quivers/structural/signature.py

def is_inductive(self) -> bool:
    """Whether the signature declares any constructor or binder.

    Returns
    -------
    bool
        ``True`` when terms over the signature are inductive.
    """
    return bool(self.constructors_t) or bool(self.binders_t)

is_graph

is_graph() -> bool

Whether the signature declares both vertex and edge kinds.

RETURNS	DESCRIPTION
bool	True when the signature is graph-shaped.

Source code in src/quivers/structural/signature.py

def is_graph(self) -> bool:
    """Whether the signature declares both vertex and edge kinds.

    Returns
    -------
    bool
        ``True`` when the signature is graph-shaped.
    """
    return bool(self.vertex_kinds_t) and bool(self.edge_kinds_t)

all_ops

all_ops() -> Iterable[str]

Iterate over every operation name of the signature.

YIELDS	DESCRIPTION
str	Each constructor name in declaration order, then each binder name in declaration order.

Source code in src/quivers/structural/signature.py

def all_ops(self) -> Iterable[str]:
    """Iterate over every operation name of the signature.

    Yields
    ------
    str
        Each constructor name in declaration order, then each
        binder name in declaration order.
    """
    for c in self.constructors_t:
        yield c.name
    for b in self.binders_t:
        yield b.name

codomain_of

codomain_of(op: str) -> str

Return the codomain sort of a constructor or binder.

PARAMETER	DESCRIPTION
op	The constructor or binder name. TYPE: str

RETURNS	DESCRIPTION
str	The name of the sort the operation produces.

RAISES	DESCRIPTION
KeyError	If op is neither a constructor nor a binder.

Source code in src/quivers/structural/signature.py

def codomain_of(self, op: str) -> str:
    """Return the codomain sort of a constructor or binder.

    Parameters
    ----------
    op : str
        The constructor or binder name.

    Returns
    -------
    str
        The name of the sort the operation produces.

    Raises
    ------
    KeyError
        If ``op`` is neither a constructor nor a binder.
    """
    for c in self.constructors_t:
        if c.name == op:
            return c.codomain
    for b in self.binders_t:
        if b.name == op:
            return b.codomain
    raise KeyError(
        f"signature {self.name!r}: op {op!r} not a constructor or binder"
    )

domain_of

domain_of(op: str) -> tuple[str, ...]

Return the positional argument sorts of a constructor or binder.

PARAMETER	DESCRIPTION
op	The constructor or binder name. TYPE: str

RETURNS	DESCRIPTION
tuple[str, ...]	The sort of each positional argument; for a binder, as given by Binder.domain.

RAISES	DESCRIPTION
KeyError	If op is neither a constructor nor a binder.

Source code in src/quivers/structural/signature.py

def domain_of(self, op: str) -> tuple[str, ...]:
    """Return the positional argument sorts of a constructor or binder.

    Parameters
    ----------
    op : str
        The constructor or binder name.

    Returns
    -------
    tuple[str, ...]
        The sort of each positional argument; for a binder, as
        given by `Binder.domain`.

    Raises
    ------
    KeyError
        If ``op`` is neither a constructor nor a binder.
    """
    for c in self.constructors_t:
        if c.name == op:
            return c.domain
    for b in self.binders_t:
        if b.name == op:
            return b.domain()
    raise KeyError(
        f"signature {self.name!r}: op {op!r} not a constructor or binder"
    )

is_binder

is_binder(op: str) -> bool

Whether an operation name is a binder of the signature.

PARAMETER	DESCRIPTION
op	The operation name. TYPE: str

RETURNS	DESCRIPTION
bool	True when a binder of that name is declared.

Source code in src/quivers/structural/signature.py

def is_binder(self, op: str) -> bool:
    """Whether an operation name is a binder of the signature.

    Parameters
    ----------
    op : str
        The operation name.

    Returns
    -------
    bool
        ``True`` when a binder of that name is declared.
    """
    return any(b.name == op for b in self.binders_t)

sort_dim

sort_dim(sort: str) -> int | None

Return the declared embedding dimension of a sort or vertex kind.

PARAMETER	DESCRIPTION
sort	The sort or vertex-kind name. TYPE: str

RETURNS	DESCRIPTION
int or None	The declared dimension, or None when the name is not declared or declares no dimension.

Source code in src/quivers/structural/signature.py

def sort_dim(self, sort: str) -> int | None:
    """Return the declared embedding dimension of a sort or vertex kind.

    Parameters
    ----------
    sort : str
        The sort or vertex-kind name.

    Returns
    -------
    int or None
        The declared dimension, or ``None`` when the name is not
        declared or declares no dimension.
    """
    for s in self.sorts_t:
        if s.name == sort:
            return s.dim
    for v in self.vertex_kinds_t:
        if v.name == sort:
            return v.dim
    return None

Term didactic-model

Term(*, op: str, args: tuple = field(default=(), opaque=True))

Bases: Model

A closed term over a signature.

op is the constructor name, the binder name, or the framework-reserved "BoundVar" for a de-Bruijn variable reference.

args are positional children. Object positions carry a Term; data positions carry a DataLeaf raw value; index positions carry a non-negative int. args is held opaque (its element type is the open union TermArg); the encoder / decoder enforce sort agreement structurally at use time.

No wrapping such as Term("Data", …) is used at any position; raw values appear directly at data positions.

to_tuple

to_tuple() -> tuple

A serialisable form matching the agenda's item-tuple convention: (op, *args_serialised). Children that are Terms are recursively serialised; data leaves and indices pass through.

RETURNS	DESCRIPTION
tuple	The nested tuple (op, *args_serialised).

Source code in src/quivers/structural/signature.py

def to_tuple(self) -> tuple:
    """A serialisable form matching the agenda's item-tuple
    convention: ``(op, *args_serialised)``. Children that are
    `Term`s are recursively serialised; data leaves and
    indices pass through.

    Returns
    -------
    tuple
        The nested tuple ``(op, *args_serialised)``.
    """
    out: list = [self.op]
    for a in self.args:
        if isinstance(a, Term):
            out.append(a.to_tuple())
        else:
            out.append(a)
    return tuple(out)

ContextEntry dataclass

ContextEntry(var_sort: str, embedding: Tensor, type_term: Term | None = None)

One scope entry on the binder stack.

embedding is a runtime tensor; type_term is the binder's annotation term captured at scope-extension time.

Context dataclass

Context(entries: tuple[ContextEntry, ...] = ())

The de-Bruijn scope context threaded through encoder and decoder runtimes.

Position 0 is the most recently bound variable; lookup var(i) returns the i-th entry from the top.

push

push(var_sort: str, embedding: Tensor, type_term: Term | None = None) -> 'Context'

Return the context extended by one innermost bound variable.

PARAMETER	DESCRIPTION
var_sort	The sort of the new variable. TYPE: str
embedding	The variable's embedding. TYPE: Tensor
type_term	The binder's annotation term for the variable, if any. TYPE: Term or None DEFAULT: None

RETURNS	DESCRIPTION
Context	A new context whose index 0 is the new variable; self is unchanged.

Source code in src/quivers/structural/signature.py

def push(
    self,
    var_sort: str,
    embedding: torch.Tensor,
    type_term: Term | None = None,
) -> "Context":
    """Return the context extended by one innermost bound variable.

    Parameters
    ----------
    var_sort : str
        The sort of the new variable.
    embedding : torch.Tensor
        The variable's embedding.
    type_term : Term or None
        The binder's annotation term for the variable, if any.

    Returns
    -------
    Context
        A new context whose index 0 is the new variable; ``self``
        is unchanged.
    """
    return Context(
        entries=(
            ContextEntry(
                var_sort=var_sort,
                embedding=embedding,
                type_term=type_term,
            ),
        )
        + self.entries,
    )

var

var(index: int) -> Tensor

Return the embedding of a bound variable.

PARAMETER	DESCRIPTION
index	The de-Bruijn index, counted from the innermost variable. TYPE: int

RETURNS	DESCRIPTION
Tensor	The variable's embedding.

RAISES	DESCRIPTION
IndexError	If index is negative or not below the context depth.

Source code in src/quivers/structural/signature.py

def var(self, index: int) -> torch.Tensor:
    """Return the embedding of a bound variable.

    Parameters
    ----------
    index : int
        The de-Bruijn index, counted from the innermost variable.

    Returns
    -------
    torch.Tensor
        The variable's embedding.

    Raises
    ------
    IndexError
        If ``index`` is negative or not below the context depth.
    """
    if index < 0 or index >= len(self.entries):
        raise IndexError(
            f"Context.var({index}): out of range "
            f"(context depth {len(self.entries)})"
        )
    return self.entries[index].embedding

type_of

type_of(index: int) -> Term | None

Return the annotation term of a bound variable.

PARAMETER	DESCRIPTION
index	The de-Bruijn index, counted from the innermost variable. TYPE: int

RETURNS	DESCRIPTION
Term or None	The annotation captured when the variable was bound, or None when it carries none.

Source code in src/quivers/structural/signature.py

def type_of(self, index: int) -> Term | None:
    """Return the annotation term of a bound variable.

    Parameters
    ----------
    index : int
        The de-Bruijn index, counted from the innermost variable.

    Returns
    -------
    Term or None
        The annotation captured when the variable was bound, or
        ``None`` when it carries none.
    """
    return self.entries[index].type_term

depth

depth() -> int

Return the number of variables in scope.

RETURNS	DESCRIPTION
int	The context depth.

Source code in src/quivers/structural/signature.py

def depth(self) -> int:
    """Return the number of variables in scope.

    Returns
    -------
    int
        The context depth.
    """
    return len(self.entries)

by_sort

by_sort(sort: str) -> list[tuple[int, ContextEntry]]

All entries whose var_sort matches; returned as (depth-index, entry) pairs for the decoder's categorical-over-in-scope-variables.

PARAMETER	DESCRIPTION
sort	The variable sort to select. TYPE: str

RETURNS	DESCRIPTION
list[tuple[int, ContextEntry]]	The matching entries with their de-Bruijn indices, innermost first.

Source code in src/quivers/structural/signature.py

def by_sort(self, sort: str) -> list[tuple[int, ContextEntry]]:
    """All entries whose ``var_sort`` matches; returned as
    ``(depth-index, entry)`` pairs for the decoder's
    categorical-over-in-scope-variables.

    Parameters
    ----------
    sort : str
        The variable sort to select.

    Returns
    -------
    list[tuple[int, ContextEntry]]
        The matching entries with their de-Bruijn indices, innermost
        first.
    """
    return [(i, e) for i, e in enumerate(self.entries) if e.var_sort == sort]

bound_var

bound_var(index: int) -> Term

A de-Bruijn variable reference.

PARAMETER	DESCRIPTION
index	The de-Bruijn index: 0 refers to the innermost bound variable. TYPE: int

RETURNS	DESCRIPTION
Term	The term BoundVar(index).

RAISES	DESCRIPTION
TypeError	If index is not a non-negative int.

Source code in src/quivers/structural/signature.py

def bound_var(index: int) -> Term:
    """A de-Bruijn variable reference.

    Parameters
    ----------
    index : int
        The de-Bruijn index: 0 refers to the innermost bound variable.

    Returns
    -------
    Term
        The term ``BoundVar(index)``.

    Raises
    ------
    TypeError
        If ``index`` is not a non-negative ``int``.
    """
    if not isinstance(index, int) or index < 0:
        raise TypeError(f"bound_var requires a non-negative int, got {index!r}")
    return Term(op="BoundVar", args=(index,))

make_term

make_term(op: str, *args) -> Term

Construct a term over a signature.

Each arg must be a Term, a DataLeaf raw value, or a non-negative int (for index-sorted positions). The encoder / decoder runtime validate sort agreement at use time.

PARAMETER	DESCRIPTION
op	The constructor or binder name. TYPE: str
*args	The positional children. TYPE: TermArg DEFAULT: ()

RETURNS	DESCRIPTION
Term	The term op(*args).

RAISES	DESCRIPTION
TypeError	If op is not a string.

Source code in src/quivers/structural/signature.py

def make_term(op: str, *args) -> Term:
    """Construct a term over a signature.

    Each ``arg`` must be a `Term`, a `DataLeaf` raw
    value, or a non-negative int (for index-sorted positions). The
    encoder / decoder runtime validate sort agreement at use
    time.

    Parameters
    ----------
    op : str
        The constructor or binder name.
    *args : TermArg
        The positional children.

    Returns
    -------
    Term
        The term ``op(*args)``.

    Raises
    ------
    TypeError
        If ``op`` is not a string.
    """
    if not isinstance(op, str):
        raise TypeError(f"make_term requires a string op, got {type(op).__name__}")
    return Term(op=op, args=tuple(args))

Type aliases and constants

Structural compression: signatures, encoders, decoders, losses.

Runtime substrate for QVR signatures, encoders, decoders, and attached losses: a uniform algebraic interface for compressing structured objects to fixed-length vectors and decoding them under a learned distribution.

EMPTY_CONTEXT module-attribute

EMPTY_CONTEXT = Context()

The context with no bound variables.

DataLeaf

DataLeaf = str | int | float | bytes | bool

A raw value at a data-sorted argument position of a Term.

Values outside this union are rejected at runtime with a typed error rather than coerced.

TermArg

TermArg = Term | DataLeaf | int

A positional argument of a Term: a subterm at an object position, a DataLeaf at a data position, or an int at an index position.

SortKind

SortKind = Literal['object', 'index', 'data']

The kinds of sort a Signature can declare.