The decidability boundary¶

valgebra compares schemas as sets: is_subtype_of is set inclusion, is_equivalent is mutual inclusion, and is_empty reports an unsatisfiable schema. The relation is s <= t exactly when s and not t share no value, so every comparison reduces to an emptiness test (see foundations).

Every answer is sound. A True from is_subtype_of/is_equivalent, or a True from is_empty, is always correct. Where valgebra cannot yet prove a relation it answers conservatively — False, or "not empty" — never a wrong True. So a positive answer is a guarantee, and a negative answer is "no, or not proven".

This page states which queries valgebra decides completely, which stay conservative, and which are undecidable at runtime and so are rejected or treated opaquely by necessity.

is_empty answers in two, and the question behind it answers in three. A False from is_empty covers both "a value is in this schema" and "no reading proves it holds none", which are different claims — one names a value, the other names a limit. Emptiness is s <= nothing, so relation_to(nothing) is where the third answer is:

from typing import Annotated

import annotated_types as at

from valgebra import Validator, nothing

opaque = Validator(Annotated[int, at.Predicate(lambda value: value > 0)])
assert opaque.is_empty() is False  # not proven empty
assert opaque.relation_to(nothing) == "undecided"  # and not proven inhabited
assert Validator(int).relation_to(nothing) == "not_subset"  # a value says so

Decided exactly¶

Over this fragment, valgebra returns the exact set-theoretic answer: on every case below it agrees with set inclusion in both directions, not only the sound one. This exactness is verified case by case against a completeness ledger — a curated set of relations the procedure is asserted to decide — and re-checked by a fuzzer that confirms the sound direction over a finite value universe; it is a gated, exercised guarantee, not a proved theorem over the whole fragment. Outside this fragment the procedure stays sound (see Sound but conservative).

relation_to reports which of the two a False is: "not_subset" where a value of the subject is outside the other schema, and "undecided" where no rule and no set reading answers. Everything in the conservative list below answers "undecided".

The scalar Boolean algebra. Every union, intersection, and complement of the scalar atoms (None, bool, int, float, str, bytes), with bool a subtype of int. The complement laws hold: int & ~int is empty, int | ~int is the universe.
Complement and disjointness across kinds. An intersection that carries a schema together with its complement (A & ~A), or two members of provably disjoint kinds (a list and a set, an int and a str), is empty — for the structural kinds, not only the scalars. Any is the top, spelled, so the rule reaches it like any other set: intersection(Any, complement(Any)) is decided empty.
A bare container class and its parameterised form. list and list[object] are one schema: an unparameterised generic names its kind's whole set, which is what the typing spec assigns it. tuple, set, frozenset and dict read the same way, as str and int do.
Class and literal inclusion. A class is a subtype of its base classes, by issubclass, and a literal is a subtype of any schema it is a member of. A dataclass or named tuple relates the same way: its schema is below one over a base class it carries every attribute of, each with a narrower schema, and below the bare class it is an instance of. A named tuple relates to the tuple its fields lay out as well, in both directions where both hold: its positions are its fields, the schema says so, and the ordinary sequence rules decide from there. A class built on a builtin relates to that builtin too: Validator(MyInt) is below Validator(int) and Validator(MyStr) below Validator(str), because every instance of such a class is a value of that kind and the class narrows the kind rather than standing beside it. A class built on no builtin narrows nothing — an instance of a subclass of it may be a string — so it relates to a kind in neither direction.
Literals against other kinds. A literal pins type(x) exactly, so it carries the kind of its constant and is decided against another kind: Literal["a"] is below ~int, and Literal["a"] & Literal["b"] is empty. Literal[1] and Literal[True] are disjoint although 1 == True, because the two pin different types. The rule reads the constant's type and applies only to the builtin scalars, whose equality is Python's own, and to any type that compares by identity -- which an enumeration does unless it says otherwise, so two of its members are two values and a meet of them is empty. An IntEnum says otherwise: its members equal the integers they carry, and a meet of two of them stays conservative.
An enumeration against the union of its members, when every instance of the class really is one of them: an Enum that is not a Flag, carrying at least one member, whose members compare by identity. Then Colour and Literal[Colour.RED, Colour.GREEN] are one set, decided in both directions; the class is still what repr prints and what a failure names. The three exclusions are each a value that would stand against the union:

kind	the value it admits that `list(cls)` never yields
`Flag`, `IntFlag`	`P.A \\| P.B` -- `\\|` builds instances the class never listed
an `Enum` with no members	a member of a subclass, since a memberless enum can still be subclassed
`IntEnum`, `StrEnum`	nothing new, but its members equal the values behind them, so two of them are not two values

Each stays the isinstance atom it was, which is sound for every enumeration and merely less complete. - Divisibility between two moduli, where it holds. Every multiple of a is a multiple of b exactly when b divides a, so the two steps settle the inclusion between them and the size of either is beside the point: MultipleOf(5000) is decided below MultipleOf(2500). The question is Python's %, asked of the two steps, so a divisor of any numeric type reads as the kind it is. The other direction is a refutation and needs a value rather than a rule, which is the conservative entry below. - Refinements. A refinement is a subtype of its base and of a refinement with looser bounds — a tighter numeric or length bound entails a looser one, not only a verbatim-contained constraint set; a bound conjunction that cannot be satisfied — a lower bound above an upper bound, or a minimum length above a maximum — is empty. Where the values are bounded to the integers the bounds count them, so an interval that skips every integer — Annotated[int, Gt(0), Lt(1)] — is empty even though its endpoints are ordered. That holds however the meet is spelled: on one refinement, or across an intersection whose members bound it, since an intersection is a subset of every member. A bool base counts too, because it subclasses int; a float base stays dense, so the same bounds are not empty. A bound over a float base is a set of floats and is decided as one: which side a bound lands on is chosen by the base rather than by the operand's type, so Annotated[float, Gt(0)] carries the integer zero and still orders the floats. nan is outside every interval, which is the comparison Python makes. A base that is neither the whole numbers nor the floats alone stays undecided, because narrowing it to one component would give a smaller set than the schema denotes. - Sequences. Homogeneous, fixed-length, and prefix-plus-tail lists and tuples, with the container as part of the type (a list is never a tuple). Every sequence schema valgebra builds takes this linear shape, so inclusion between two sequence schemas is decided completely — a bare list among them, since it is the sequence node its kind's top spells (above). A fixed-length sequence is also decided against a union of fixed-length ones it splits across, where no single branch contains it: tuple[int | str, int] is below tuple[int, int] | tuple[str, int]. The rule needs a fixed component count, so a homogeneous or variadic sequence — a star, matching every length — is not decomposed. - Sets and frozensets. By element inclusion. - Records and mappings. Closed-record width, depth, and required-ness; pure mappings with several key-pattern clauses (each subtype clause subsumed by a supertype clause); and a record mixed with a catch-all when the subtype carries at least the supertype's fields, or when a field the subtype lacks is optional in the supertype and the subtype's catch-all covers its value type (each extra or optional field covered by a catch-all over all string keys). A closed record is compared against a catch-all mapping by the same rule, so {"x": int} is decided below dict[str, int]. A key the supertype requires and the subtype does not declare refutes the inclusion however open the subtype is: a clause governs the keys a value carries and requires none, so the subtype holds a value without that key, and dict[str, int] is decided not below a record that requires one. A meet of two of them is empty when some key one side requires cannot hold: because the types the two give it share no value, or because the other side is closed and does not declare it. Only a required key can do this — a meet of two mappings, or of two optional fields, always contains the empty dict.

A record is decided against a **union of records it splits across** as well,
which is the same shape one kind over from the fixed sequence above:
`{"a": int | str, "b": int | str}` is below the four records that fix both
keys. No single branch contains it, so the rules decline and the sets
answer, by emptiness of the difference.

A difference written as one complemented union. a ∧ ¬(b ∨ c) and a ∧ ¬b ∧ ¬c are one set, and both are decided where either is: no spelling of a difference is the harder one by construction. That is worth stating because the set representation is bounded — a union of dicts, objects or sets holds at most a fixed number of atoms — and complementing a union of n parts multiplies n complements together, which is a width the answer rarely has. A meet against such a union removes one part at a time, so the width the bound sees is the width of the answer rather than of the widest intermediate.

The bound is still there. A difference wide enough to reach it reaches it, and which of two spellings gets there first depends on the order the parts multiply, so a relation the sets decline under one spelling may be decided under another. What no longer happens is one spelling being systematically the one that declines. - A length bound over a base that takes any length. A string and a bytes take any, so a bound their lengths admit is met by a value: Annotated[str, MinLen(1)] is the non-empty string and is decided to have one. A container takes any length by repeating one element, so its element answers instead: a bound of zero is met by the empty container whatever the element admits, and a longer one by as many copies of an element as it asks for. That decides a fixpoint every unfolding of which needs one more element -- each element is a value of the fixpoint, and no finite value satisfies it. A bound over a fixed position, or over a base whose values have no length at all, is not this shape and stays conservative. - Two schemas that share no value. The inclusion is refuted, whatever either side holds: every value of the subject is outside the supertype. The disjointness read here is the one the concrete types settle -- two distinct builtin scalars, two distinct container kinds -- so list[int] is decided not below tuple[int, int], and a mapping not below a list. A subject with no value is the exception the reading catches: it is below both. A class joins the comparison through the bindings, which read the builtin it derives from: a class built on dict holds mappings and nothing else, since a subclass inherits that layout and cannot lay down a second, so a list is decided not below it. A class built on no builtin is not read this way, and the reason is a value: a class deriving from that one and from str is a string and an instance of it. - A subject outside a base. A refinement is a subset of its base, so a subject the base refutes is refuted against every refinement of it -- the same value settles both. The proof does not carry, since being inside the base says nothing about the constraints, which is why list[int] below Annotated[list[int], MinLen(2)] is left to the set representation while list[str] below it is refuted by a rule. - Inclusion in a complement. A is below ~B exactly when A and B share no value, so the relation is decided wherever emptiness decides disjointness: list[int] is below ~int, and dict[str, int] below ~str. This is the semantic-subtyping reduction applied where no structural rule can help — a complement has no shape on the right to recurse into. - Recursion. Equirecursive schemas compare at their greatest fixpoint; the rule is sound and is witnessed by an independent reference denotation. The sets are inductive — a guarded fixpoint contains the values built by finitely many unfoldings — while the comparison assumes its goal and is coinductive; the two agree because a value is finite. A fixpoint is decided below its own unfolding, so a recursive schema and the body written out around it relate in both directions. - The complement laws, where the constructors reach them. complement cancels a complement, union folds a join carrying a schema beside its own complement, and intersection folds the meet of that pair, all where the schema is built. So complement(complement(int)) is int — one schema, which repr and == report and which a comparison is never asked about — a union covering the universe is anything, and a meet cancelling to nothing is nothing. A predicate and a hooked class are exempt: the law holds of sets, and neither is one. The decision procedure has no rule for either shape and never meets one built this way. A shape the fold does not reach is a different matter and is conservative (below).

from typing import Annotated, Any

import annotated_types as at

from valgebra import complement, intersection, recursive, union, Validator

assert Validator(bool).is_subtype_of(int)  # bool is a subtype of int
assert Validator(1).is_subtype_of(int)  # a literal is a member of int
assert Validator(Annotated[int, at.Ge(0)]).is_subtype_of(int)  # refinement <= base
assert Validator(Annotated[int, at.Ge(10), at.Le(0)]).is_empty()  # no such int
assert Validator(
    Annotated[int, at.Gt(0), at.Lt(1)]
).is_empty()  # no int strictly between
assert not Validator(
    Annotated[float, at.Gt(0), at.Lt(1)]
).is_empty()  # floats are dense
assert Validator({str: int}).is_subtype_of({str: int, int: bool})  # mapping clauses
assert Validator({str: int}).is_subtype_of(
    {"b?": int, str: int}
)  # optional field, catch-all covers it
assert Validator({"x": int}).is_subtype_of(
    {str: int}
)  # a closed record below a catch-all mapping
assert Validator(list[int]).is_subtype_of(
    complement(int)
)  # inside a complement: a list shares no value with an int
assert Validator(tuple[int | str, int]).is_subtype_of(
    union(tuple[int, int], tuple[str, int])
)  # a product splits across branches
assert Validator(
    recursive(lambda t: Annotated[list[t], at.MinLen(1)])
).is_empty()  # every unfolding needs one more element
assert intersection({"a": int}, {"a": str}).is_empty()  # 'a' cannot hold both
assert not intersection(
    {"a?": int}, {"a?": str}
).is_empty()  # the empty dict is in both
assert union(bool, int).is_equivalent(int)  # bool | int is just int
assert intersection(int, complement(int)).is_empty()  # the complement law
assert intersection(
    list[int], complement(list[int])
).is_empty()  # complement law, structurally
assert intersection(
    list[int], set[int]
).is_empty()  # disjoint kinds: a list is never a set
assert intersection(
    Any, complement(Any)
).is_empty()  # Any is the top, spelled, so the law reaches it

json_value = recursive(lambda j: union(None, bool, int, float, str, [j], {str: j}))
assert json_value.is_valid({"a": [1, "x", {"b": None}]})

The one assumption: a class the bindings can read has an instance¶

Every other answer here rests on the value model alone. This one rests on an assumption, and it is the only place a "not_subset" can be wrong. No True can: a proof is a proof, and the assumption is only ever read to believe a refutation.

A class is opaque: what it holds is isinstance, and the library reads the class hierarchy rather than running it. A class whose metaclass leaves isinstance and issubclass alone is taken to hold at least one object, which is what lets A be reported not below B for two classes neither deriving from the other -- the difference A ∧ ¬B is read as holding a value. A class no value can instantiate (a __new__ that always raises, an abstract class with no concrete subclass) is empty, and is below everything; the library reports it not below, because the assumption says otherwise.

It licenses one object, not one per kind. A class that lays down no builtin layout confines its instances to no kind, so it constrains values of every kind: a subclass of it may derive from str as easily as from nothing. That placement is right for inclusion -- Plain is not below the complement of int -- and it is not a value. An integer that is an instance of Plain exists only if some class derives from both, and which classes exist is not something a snapshot of the order can say. So Plain against the complement of a kind is undecided, and the same in reverse:

from valgebra import Validator, complement


class Plain:
    pass


class Laid(str):
    __slots__ = ()


assert Validator(Plain).relation_to(complement(int)) == "undecided"
assert Validator(int).relation_to(complement(Plain)) == "undecided"

# A class laid out as the kind is the case this is not conservative about:
# every instance of it is a string, so it has a value on that line.
assert Validator(Laid).relation_to(complement(str)) == "not_subset"
assert Validator(Laid).relation_to(complement(int)) == "subset"

The assumption is the set representation's open world, which both readings share. Neither decides it; the bindings could not answer it without running a constructor at decision time, which is the same code the pure-metaclass test exists to refuse. What it buys is every relation between two classes decided by a rule, at about a microsecond rather than a hundred.

A declared attribute does not widen this. A class with declared attributes -- a dataclass, a NamedTuple -- compiles to the class beside a record of its fields, and the record narrows the class's instances rather than reaching outside them. So a relation that declines beside one declines for the class: int ≤ ~C is "not proven" for a dataclass and for a class with no fields alike, and a class laid out as a kind decides either way. The record is not a second source of conservatism, and in the one place it tells two schemas apart it makes a refutation reachable that the class alone leaves open. A Protocol is a third thing again: it compiles to a class that answers isinstance itself, which is the decline the section above owns, and carries no record at all.

Sound but conservative¶

Here valgebra is correct but not complete: it may answer False or "not empty" for a relation that does in fact hold.

A negative answer is one of two different things, and the core tells them apart even though the boundary does not. A relation can be refuted -- there is a value of the one schema outside the other, so the answer is False and will stay False however much the procedure improves -- or declined, which is the list below: nothing was found either way, and the same query decides once the representation reaches it. The three relations answer with all three values inside the core and map both negatives to False at the boundary, because False is what the contract promises and a third value at the surface would make every caller handle a case the guarantee does not need. What the split buys is that "not proven" is countable: a rule that begins refuting a relation the procedure declines is a change the tests see rather than one that hides behind an unchanged False.

The list is short, and it is short for one reason. Two representations answer these questions. The rules recurse over the schema tree, and where they decline the descriptor is asked: it holds each kind as a set, so a ≤ b is a ∧ ¬b = ∅ and the answer comes out of the sets rather than out of a rule about the shape. What is left below is what the descriptor cannot hold.

A clause keyed by a complement. The set representation partitions a dict's keys by kind and gives each part its own default, so a clause whose key is a kind or a literal lands in a part. A key written as a complement spans every kind but one, which no single part holds, and the lowering declines rather than spreading it — so a relation about such a map is left to the rules, and a pair the rules do not decide comes back "not proven".

That partition is the model's, not a shortcut around it: the source treats a record as a quasi-K-step function, where K is a predefined finite partition of the key domain and the catch-all is split across its parts. The paper weighs letting key domains overlap and declines it, because comparing two records would then need the machinery for comparing intersections of arrow types. A complement-keyed clause is exactly an overlapping domain, so this decline is the model's shape rather than an unfinished corner of the implementation.
```
from valgebra import Validator, anything, complement

not_str = complement(Validator(str))
free_the_rest = Validator({str: int, not_str: anything})
# The walk is exact: membership never goes through the set representation.
assert free_the_rest.is_valid({"a": 1, 7: "anything at all"})
assert not free_the_rest.is_valid({"a": "not an int"})

# The relation declines. These two admit every dict, by different spellings.
long_way = Validator({str: anything, not_str: anything})
assert long_way.is_valid({7: "x"}) and Validator({object: object}).is_valid({7: "x"})
assert not long_way.is_equivalent({object: object})
```
This is the shape open writes on a mapping: freeing the key-types a clause leaves over means a clause over the complement of the ones it claims. Opening a record stays decided, because the regions it frees and the ones its clauses claim cover every key with one value between them, which is one catch-all clause rather than two.
Recursion, past one unfolding. A fixpoint as the supertype costs a refutation rather than an inclusion, and that is the sharper half. a ≤ b is a ∧ ¬b = ∅, so the supertype is where a schema stands under a complement, and a reference there is lowered to the bottom. The difference then contains the value that refutes the inclusion without being proved to contain it, so the answer is "not proven" where a value says plainly that it is false:
```
from valgebra import Validator, complement, recursive, union

chain = recursive(lambda t: union(None, {"next": t}))
assert not Validator(chain).is_valid("a")  # the walk is exact
assert Validator(complement(int)).is_valid("a")
# and the relation declines rather than refuting
assert Validator(complement(int)).relation_to(chain) == "undecided"
```
What the rules reach is narrower than that and is reached: a branch of a union the subject shares no value with is dropped before the rest is asked, so a chain of records beside a None branch is refuted by the record branch alone. Where every branch goes that way the subject is outside the whole union, which is a refutation rather than a decline as long as the subject holds a value at all. And a fixpoint's own unfolding is below it however its body is spelled: a member that is a meet is not placed by any member of the meet, so the reference is unfolded for it and the meet is read as the branch of the definition it is.
```
from valgebra import Validator, intersection, recursive, union

meet = intersection(int, union(float, bool))
tree = recursive(lambda t: union(meet, list[t]))
assert Validator(union(meet, list[tree])).relation_to(tree) == "subset"
assert tree.relation_to(union(meet, list[tree])) == "subset"
```
Branches are dropped where one of them refutes, which is the answer the narrowing carries back from the branch it leaves. A union no branch of which refutes narrows to a smaller union of declines, so the readings that drop branches -- a meet per branch, on the path already headed for the set representation -- are not spent on it, and the pair goes to that representation instead. What that gives up is the union whose branches the subject shares no value with and which none of them refutes: it is outside the union and is answered "undecided". Reaching for it on every union costs the decision path 36% against 0.14% asked of the unions a branch refutes, measured on the relation matrix.

The other half is the lowering. A reference is a cycle and a finite set representation has no room for one, so a recursive schema is lowered by unfolding its body once and putting a bound where the reference was — the top where the schema is used positively, the bottom under a complement, which is what keeps a difference sound. That decides everything about the kinds a fixpoint admits: bytes shares no value with a JSON value, and bytes is below its complement. What one unfolding does not reach is a relation that needs the body twice — a fixpoint below a differently-written fixpoint whose bodies only agree after two steps — and there the coinductive rule is the whole of the answer.
A length bound over a set or a dict, in the sets. A length is not a word's alone, and two of the kinds that have one state it: a word's length is a pattern over its alphabet, and a sequence's is "any element, that many times", which the automaton holds like any other shape. So Annotated[tuple[int, int], MinLen(3)] is decided empty and Annotated[list[int], MaxLen(0)] is the empty list. A set and a dict have a length their components do not count, and a bound over one of those refuses rather than being lowered as if it did. Whether such a schema has a value is a different question and the rules answer it, since a set of any length is built by repeating one element.
An integer bound outside the 64-bit range. The integer component carries its bounds as i64, so Annotated[int, Ge(2**70)] is held as the widest set the carrier spells rather than as the half-line it names. The schema validates exactly -- membership reads the Python integer -- and a relation between two such bounds declines: Ge(2**70) against Ge(2**70 + 1) is undecided in the direction a value refutes, and subset in the direction the carrier proves. Python's integers are unbounded and the carrier is not, which is a property of the representation rather than of the schema.
A meet of two moduli the representation cannot hold. A MultipleOf becomes a residue class, and a class is materialised per residue up to a recorded period. Two steps meet at the period they share, so MultipleOf(64) with MultipleOf(81) is the multiples of 5,184 -- past the period although both steps are well inside it -- and a relation that turns on that meet declines. A rounded period would be wrong in one direction or the other, so it refuses instead.

The inclusion between two moduli does not go that way and is decided above: the steps settle it between them, whatever their size. What the period still bounds is the refutation. MultipleOf(2) is decided not below MultipleOf(4), because the residues hold both and 2 is a multiple of one and not the other; the same question at MultipleOf(2500) against MultipleOf(5000) declines, because naming that value takes a representation and a rule reading the two steps cannot produce one -- the subject's own other constraints may exclude it.
A schema too large to build. The descriptor is bounded three ways: the nodes it will read, the nesting it will descend, and the work a build may spend. Past any of them it refuses, and the caller keeps the rules' answer. None of these is a statement about the schema -- the same schema decides under a larger bound -- and each exists because building a descriptor beside a verdict the rules already reached is work whose result is discarded. Every bound is a row of the architecture table in the repository, with the gate that measures it beside it.

Where that bites is width. A record whose fields each take two types is the union of the records that fix every field, and the rules have no split rule for a record, so the sets answer it. Three fields against their eight corners is decided; four against their sixteen is refused, because the difference reads more nodes than a lowering builds and costs more work than one spends. The shape is the first an ordinary annotation reaches, so it is the number to know:

from valgebra import Validator, union

pair = {"a": union(int, str), "b": union(int, str), "c": union(int, str)}
corners = union(
    *[
        {"a": a, "b": b, "c": c}
        for a in (int, str)
        for b in (int, str)
        for c in (int, str)
    ]
)
assert Validator(pair).relation_to(corners) == "subset"  # three fields

A fourth field answers undecided, which is the conservative answer and not a claim about the relation: it holds, and proving it takes a larger bound.

A predicate. Its satisfiability is undecidable (below), so neither representation reasons about one -- and that is a statement about the predicate, not about every pair carrying one. A refinement is a subset of its base, so what surrounds the predicate still decides: a bounded integer against a predicate-refined list is refuted by the kinds, a list against its own bounded-and-predicated refinement by the empty list the bound leaves out, and a dataclass against a union with a predicate-refined branch by the kind that branch names. What the predicate costs is the other direction. A refutation stands on a value of the subject, and a subject carrying a predicate is never proven to have one, so the same pair reversed is undecided: Annotated[int, Ge(0)] <= Annotated[list[int], Predicate(f)] is refuted and its converse is not.

tests/test_completeness_ledger.py is where a relation that leaves this list lands: it enumerates what the procedure must decide and fails in both directions, so a relation that regresses to conservatism fails there and one that becomes decided is added there. It also carries a strict expected-failure mark for a relation that holds and is not decided, which names none today -- the last, a fixpoint every unfolding of which needs one more element, became a row of the decided list.

from typing import Annotated, Literal, NamedTuple

import annotated_types as at

from valgebra import (
    Regex,
    Validator,
    anything,
    complement,
    intersection,
    nothing,
    recursive,
    union,
)


class Pair(NamedTuple):
    x: int
    y: int


# A length bound over a set or a dict is opaque: their representations do not
# count one. Over a word or a sequence it is decided.
assert not Validator(Annotated[set[int], at.MinLen(3)]).is_empty()
assert Validator(Annotated[tuple[int, int], at.MinLen(3)]).is_empty()
# A named tuple's positions are its fields, and the schema says so, so the
# relation is structural.
assert Validator(Pair).is_subtype_of(tuple[int, int])
# A recursive schema: the laws reach it, and one unfolding decides the kinds its
# body admits. What one unfolding does not reach is a relation needing the body
# twice -- here, that every value of the integer tree is a value of the list
# tree, which holds and is not proved.
mu = lambda: Validator(recursive(lambda t: union(int, list[t])))  # noqa: E731
assert intersection(mu(), complement(mu())).is_empty()
assert intersection(mu(), str).is_empty()
assert not mu().is_subtype_of(recursive(lambda t: union(int, list[list[t]])))

# Everything else here decides, on the sets rather than by a rule.
pattern = Validator(Annotated[str, Regex("a")])
assert pattern.is_subtype_of(Annotated[str, Regex("ab?")])  # L(a) <= L(ab?)
assert pattern.is_subtype_of(Literal["a"])  # L(a) is exactly {"a"}
assert Validator(Annotated[int, at.MultipleOf(4)]).is_subtype_of(
    Annotated[int, at.MultipleOf(2)]
)
assert Validator(bool).is_subtype_of(Annotated[int, at.Ge(0)])
assert Validator(bool).is_subtype_of(Literal[True, False])
assert Validator({"a": int}).is_subtype_of(dict[Literal["a"], int])

# A respelling denotes the same set, and the sets are what the relation reads --
# even though the laws construction settles do not reach this one. `A | (A & B)`
# is `A` by absorption, which needs a containment to see, and containment is the
# decision rather than a law.
record = Validator({"a": int})
respelled = union(record, intersection(record, Validator(str)))
assert respelled != record
assert record.is_subtype_of(respelled)
assert respelled.is_subtype_of(record)

Two instruments hold this list to the tree. tests/test_completeness_ledger.py carries each relation above as a decided one, written the way a caller writes it rather than built from the other operand — a distinction that matters, because the shortcuts the procedure takes are keyed on two schemas sharing their constants. Its strict expected-failure mark is for a relation that regresses to conservatism, and it names none: the list above is what the procedure decides, so an entry that stops holding is a defect rather than a known gap. tests/test_completeness_probe.py searches a fixed universe for relations answered False that no value refutes and fails when one appears without a written reason, so a gap nobody thought of cannot arrive unnoticed. It reaches a gap only where some atom in its universe reaches it, which is why that universe carries both constraint families, a fixpoint beside its own unfolding, and a record beside a literal-keyed map.

General regular-expression-types inclusion of sequences (a union of sequence languages that splits across branches, or a repeated heterogeneous group) is not implemented, and no schema valgebra builds takes that shape: the sequence node carries the linear prefix-and-tail form and has no syntax for the rest.

Undecidable at runtime¶

These have no decidable runtime membership, so valgebra rejects them with a clear message or treats them opaquely — it never guesses.

Erased generics and type variables. A TypeVar, Generic[T], ParamSpec, or TypeVarTuple is rejected; a runtime value carries no binding for a free type variable.
Abstract-collection generics. Sequence[int], Mapping[str, int], and Iterable[T] are rejected; checking Iterable elements would consume the iterable, and str/bytes are themselves sequences. Use a concrete container — list[int], tuple[int, ...], dict[str, int] — or the bare abstract type for an isinstance check.
Callable signatures. Callable[[int], str] checks only that the value is callable; a function does not expose its argument and return types at runtime.
Predicates. An Annotated[T, predicate] runs the predicate at validation time; its satisfiability cannot be reasoned about (Rice's theorem), so nothing is inferred from it and two refinements relate through a predicate only when they carry the same one.

A decision query may nonetheless call it. Deciding whether a literal is a subtype of a refinement is deciding whether that literal's value belongs to it, and belonging runs the predicate — so is_subtype_of and is_equivalent execute user code, as is_empty executes a rich comparison when it orders two refinement bounds. A predicate with side effects, or one that is slow, is one a type query pays for. - Typing qualifiers. Final and ClassVar are rejected as schemas; they qualify a declaration and carry no value-membership meaning. On a class they are read as what they are: a ClassVar annotates the class rather than an instance, so a dataclass field carrying one is not an attribute the schema asks for, and neither is an InitVar, which names a constructor parameter the instance does not keep.

from collections.abc import Sequence
from typing import TypeVar

from valgebra import Validator

T = TypeVar("T")

for undecidable in (Sequence[int], T):
    try:
        Validator(undecidable)
        raise AssertionError("expected a rejection")
    except NotImplementedError:
        pass  # rejected with a clear message, never a silent wrong validator

The contract¶

A positive answer (is_subtype_of/is_equivalent/is_empty returning True) is a proof. A negative answer is "no, or not yet proven". valgebra never reports a relation it cannot justify, so widening the decided fragment can only turn a conservative False into a True — it can never change an answer that was already correct.

Every decision also runs under a fixed work budget, and exhausting it returns the conservative answer (False, "not proven") rather than running unbounded. This preserves soundness: a bail-out is never a wrong True.

The Python answer is True or False, so a False from an exhausted budget reads the same as a False the procedure decided. Inside the core the two are distinct — emptiness answers empty, inhabited, or neither — which is what lets a test say that a bail-out never claims a proof it does not have. The distinction is not surfaced here because the contract does not change with it: a False is "not proven" either way.

The budget binds where the work is a product rather than a sum. Subtyping distributes over both sides of a union, so relating two unions can cost the product of their member counts, and a Boolean combination nested past a handful of levels demands work exponential in its depth.

One shape avoids the product entirely, and it is the one a contract writes most: a union of nothing but literals. A literal denotes a singleton, so such a union denotes a finite set of values, and inclusion between two finite sets is membership of every value of one in the other. That is decided by lookup rather than by distribution, and it is exact in both directions — every value found is a proof, and one value found nowhere is a refutation, since it is in the subject and outside the other schema. Two tables of ten thousand codes each are decided in a few milliseconds, in either direction, whether they were written out separately or one was built from the other:

from typing import Literal

from valgebra import Validator

codes = Validator(Literal[tuple(range(10_000))])
wider = Validator(Literal[tuple(range(10_001))])
shifted = Validator(Literal[tuple(range(1, 10_001))])
backwards = Validator(Literal[tuple(reversed(range(10_000)))])

assert codes.relation_to(wider) == "subset"
assert codes.relation_to(shifted) == "not_subset"  # 0 is in one and not the other
assert codes.relation_to(backwards) == "subset"  # the same set, written the other way

"However they were written" is a claim about the pools: each validator numbers its constants in the order it met them, relating two validators renumbers one pool into the other, and a table written backwards is renumbered backwards. A member list is read as a set only in the canonical order its constructor leaves it in, so the transform that renumbers one sorts it again (crates/valgebra-core/src/ir/transform.rs, mapped_member_set). Without that sort, two tables agreeing on nothing about where each constant sits fall out of the canonical order and are distributed against each other instead.

The refutation is the bindings' to give: two constants at two pool positions are two values only where their type's equality can be trusted, and a constant that does not equal itself — float("nan") — denotes no value at all, so Literal[float("nan")] is the empty set and is below everything. Where the equality cannot be trusted, the relation stays undecided rather than guessing.

What is left under the budget is the Boolean tower: a deeply nested combination of unions, meets and complements, where subtyping distributes over both sides and the work is a product of the branches. A False there may mean "not proven within the bound" rather than "not a subtype"; on anything else it means the relation is outside the decided fragment above. The bound stands in for a termination argument rather than for a missing optimisation: counted over the decision workloads the goals a query repeats number zero, because the trail absorbs recursion and the per-rule caches absorb the shape where one goal is asked once per field. A table over goals would have nothing to hit.