Formal Foundations

Mathematical formalization of URN matching and Cap dispatch

Purpose and Scope

This document provides the formal mathematical foundation for the capdag URN matching and dispatch system. It defines:

The Tagged URN semantic domain
The base relation and derived predicates
The Cap URN product construction
The dispatch relation
Ranking as a separate policy layer
Proof obligations and sanity properties

This is the authoritative formal reference. Implementation details are in the other specification documents.

The Core Problem

Capdag uses URNs as structured semantic descriptors, not merely names. The system must answer distinct questions:

Question	Predicate
Can this provider handle this request?	Dispatch
Are these on the same specialization chain?	is_comparable
Are these semantically identical?	is_equivalent
Can output flow to input?	conforms_to

Previous bugs arose from conflating these questions. A single accepts or conforms_to cannot serve all purposes because Cap URNs have mixed variance across three dimensions.

Base Domain

Let U be the set of normalized Tagged URNs.

Each element $u \in U$ has:

A canonical normalized representation
Well-defined wildcard/value semantics
A specificity score
A base semantic relation

Primitive Relation

Define a binary relation on U:

$$ \preceq \;\subseteq\; U \times U $$

With meaning:

$$ a \preceq b \;\text{iff}\; a \text{ is at least as specific as } b $$

Equivalently: b is at least as general as a.

Lattice orientation:

Lower = more specific (more constrained)
Upper = more generic (less constrained)

Derived Predicates

For $a, b \in U$:

Acceptance

$$ \text{accepts}(a, b) \iff b \preceq a $$

Pattern $a$ accepts instance $b$.

Conformance

$$ \text{conforms_to}(a, b) \iff a \preceq b $$

Instance $a$ conforms to pattern $b$.

Comparability

$$ \text{is_comparable}(a, b) \iff a \preceq b \lor b \preceq a $$

One subsumes the other. They are on the same specialization chain.

Equivalence

$$ \text{is_equivalent}(a, b) \iff a \preceq b \land b \preceq a $$

$a$ and $b$ denote the same semantic position.

Specificity Function

Define:

$$ \text{spec}_U : U \to \mathbb{N} $$

Such that greater specificity yields a greater score. This function is used for ranking only, not for primary semantic validity.

Semantic Obligations on U

The system assumes $U$, $\preceq$, and $\text{spec}_U$ are well-defined by the Tagged URN truth table.

Reflexivity

$$ \forall u \in U,\; u \preceq u $$

Transitivity

$$ \forall a,b,c \in U,\; (a \preceq b \land b \preceq c) \implies a \preceq c $$

If these hold, $\preceq$ is a preorder on U.

Antisymmetry (modulo normalization)

$$ (a \preceq b \land b \preceq a) \implies a \equiv b $$

If this also holds, equivalence classes of U form a partial order.

Cap URNs as Product

A Cap URN is a triple over the Tagged URN domain:

$$ C = U \times U \times U $$

For $c \in C$, write:

$$ c = (i, o, y) $$

Where:

i = input dimension (the in tag value)
o = output dimension (the out tag value)
y = non-direction cap-tag dimension

All three dimensions reuse the same base domain U and relation $\preceq$.

Cap Specificity

Define:

$$ \text{spec}_C : C \to \mathbb{N} $$

By:

$$ \text{spec}_C(i, o, y) = \text{media_tags}(i) + \text{media_tags}(o) + \text{count_non_wildcard}(y) $$

Where:

media_tags(x) = number of tags in media URN x (0 if x = identity media:)
count_non_wildcard(y) = number of y-tags with non-* values

This differs from a naive $\text{spec}_U(i) + \text{spec}_U(o) + \text{spec}_U(y)$ because direction specs are Media URNs (counted by tag presence) while y-tags use binary wildcard/non-wildcard distinction.

The Dispatch Relation

Let:

provider $p = (i_p, o_p, y_p)$
request $r = (i_r, o_r, y_r)$

Define the dispatch relation:

$$ \text{Dispatch}(p, r) \iff i_r \preceq i_p \land o_p \preceq o_r \land y_r \preceq y_p $$

This is the primary routing predicate.

Interpretation of Dispatch

Input Admissibility (Contravariant)

$$ i_r \preceq i_p $$

The request’s input must be at least as specific as the provider’s accepted input. Provider may accept more general inputs.

Output Admissibility (Covariant)

$$ o_p \preceq o_r $$

The provider’s output must be at least as specific as the request’s required output. Provider must guarantee at least what request demands.

$$ y_r \preceq y_p $$

The provider’s non-direction tags must satisfy or refine the request’s constraints. Provider may add tags (refinement) but cannot contradict explicit request constraints.

Variance Summary

Dimension	Variance	Condition	Meaning
Input (i)	Contravariant	$i_r \preceq i_p$	Provider may accept broader input
Output (o)	Covariant	$o_p \preceq o_r$	Provider must produce tighter output
Cap-tags (y)	Invariant/Refinement	$y_r \preceq y_p$	Provider must satisfy constraints

Dispatch Is Directional

In general:

$$ \text{Dispatch}(p, r) \;\not\!\!\implies \text{Dispatch}(r, p) $$

Dispatch is not symmetric. A specific provider can handle a generic request, but a generic request cannot “handle” a specific provider.

Derived Cap-Level Relations

Using base predicates componentwise:

Cap Equivalence

$$ \text{CapEq}(c_1, c_2) \iff \text{is_equivalent}(i_1, i_2) \land \text{is_equivalent}(o_1, o_2) \land \text{is_equivalent}(y_1, y_2) $$

Cap Comparability

$$ \text{CapComparable}(c_1, c_2) \iff \text{is_comparable}(i_1, i_2) \land \text{is_comparable}(o_1, o_2) \land \text{is_comparable}(y_1, y_2) $$

Useful for discovery, not sufficient for dispatch.

Correct Predicate Roles

Purpose	Predicate
Routing / execution	Dispatch(provider, request)
Exact lookup	CapEq(a, b)
Discovery / family analysis	CapComparable(a, b)
Pattern-instance checks	accepts, conforms_to

Ranking Policy

Ranking is defined only over the valid set:

$$ \text{Valid}(r) = \{ p \in C \mid \text{Dispatch}(p, r) \} $$

A ranking policy is any total preorder on Valid(r).

Specificity Distance

$$ \text{dist}(p, r) = \text{spec}_C(p) - \text{spec}_C(r) $$

Typical Preference

dist = 0 (equivalent) — most preferred
Smallest positive dist (refinement)
Negative dist only as fallback (generic provider)

This is policy, not semantics. Dispatch defines validity; ranking defines selection.

Fundamental Sanity Properties

Reflexivity of Dispatch

$$ \forall c \in C,\; \text{Dispatch}(c, c) $$

Follows from reflexivity of $\preceq$.

Transitivity of Dispatch

$$ \forall a,b,c \in C,\; (\text{Dispatch}(a, b) \land \text{Dispatch}(b, c)) \implies \text{Dispatch}(a, c) $$

Follows from transitivity of $\preceq$.

If provider $p'$ refines $p$:

$i_p \preceq i_{p'}$ (more permissive input)
$o_{p'} \preceq o_p$ (more specific output)
$y_p \preceq y_{p'}$ (more specific y-tags)

And Dispatch(p, r) holds, then:

$$ \text{Dispatch}(p', r) $$

Refinement preserves dispatchability.

Contradiction Rejection

$$ \neg(i_r \preceq i_p) \lor \neg(o_p \preceq o_r) \lor \neg(y_r \preceq y_p) \implies \neg\text{Dispatch}(p, r) $$

If any conjunct fails, dispatch fails.

Common Failure Modes

Failure	Problem
Using `accepts` for dispatch	Flattens 3-dimensional mixed-variance problem into one direction
Using `conforms_to` for dispatch	Same reason
Using `is_comparable` for dispatch	Relatedness is not validity
Ranking before validity	Specificity alone does not imply semantic legality
Treating Cap URNs as one-dimensional	Cap URNs are structured product objects with mixed variance

Separation of Validity and Preference

The specification distinguishes:

Semantic validity: Whether a provider may legally serve a request (Dispatch)
Selection preference: Which valid provider should be chosen (Ranking)

These must not be conflated.

Implementation Conformance

Any implementation conforming to this specification must ensure:

All Tagged URNs normalize into U
All dimension-level checks reduce to the same base relation $\preceq$
Cap dispatch uses exactly the mixed-direction rule
Ranking is applied only after dispatch validity is established

Summary

The entire system is defined from a single semantic base:

A Tagged URN domain U
A specificity relation $\preceq$
A specificity score $\text{spec}_U$

Cap URNs are triples in $U^3$.

Dispatch is the mixed-direction product relation:

$$ \text{Dispatch}((i_p, o_p, y_p), (i_r, o_r, y_r)) \iff i_r \preceq i_p \land o_p \preceq o_r \land y_r \preceq y_p $$

This yields:

A clean order-theoretic interpretation
A clean type-theoretic interpretation
Correct separation of routing, planning, discovery, and exact matching
A foundation for formal verification