Formal foundations

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 numbered specification documents (01–11).

The core problem

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

A single accepts or conforms_to cannot answer all of them because Cap URNs have mixed variance across four structural coordinates.

Base domain

Let U be the set of normalized Tagged URNs.

Each element u ∈ 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:

⪯ ⊆ U × U

With meaning:

a ⪯ b  iff  a 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 ∈ U:

Acceptance

accepts(a, b)  :⟺  b ⪯ a

Meaning: a subsumes b. Pattern a accepts instance b.

Conformance

conforms_to(a, b)  :⟺  a ⪯ b

Meaning: a satisfies or refines b. Instance a conforms to pattern b.

Comparability

is_comparable(a, b)  :⟺  a ⪯ b ∨ b ⪯ a

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

Equivalence

is_equivalent(a, b)  :⟺  a ⪯ b ∧ b ⪯ a

Meaning: a and b denote the same semantic position.

Specificity function

Define:

spec_U : U → ℕ

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, ⪯, and spec_U are well-defined by what each tag form means (the set of states its key may be in), with ⪯ the inclusion of those meanings (Predicates). These are proved, not assumed, in tagged-urn/formal.

Reflexivity

∀u ∈ U,  u ⪯ u

Transitivity

∀a,b,c ∈ U,  (a ⪯ b ∧ b ⪯ c) ⟹ a ⪯ c

If these hold, ⪯ is a preorder on U.

Antisymmetry (modulo normalization)

(a ⪯ b ∧ b ⪯ a) ⟹ a ≡ b

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

Cap URNs as product

A Cap URN is a four-coordinate product over the Tagged URN domain:

C = U × U × U × E

For c ∈ C, write:

c = (i, o, y, e)

Where:

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

The in, out, and y dimensions reuse the base domain U and relation ⪯. The effect coordinate is a structural axis with exact matching unless the request explicitly uses the unconstrained ?effect form.

Distinguished media URNs: top and unit

Two media URNs play distinguished roles in the directional axes of C. They are formally distinct elements of U; the rest of the spec relies on this distinction.

Top (media:). The maximum of the media URN order under ⪯:

∀ m ∈ MediaUrn,    m ⪯ media:

A cap’s directional spec set to media: is the top type, read as “any A”: a cap that takes media: takes anything, and one that gives media: promises no particular output.

The top type is not the same as a side left open in a request. A request is a question about caps, and a side it does not establish is an unknown (“some A”, not “any A”) (Dispatch: unknown is not “anything”).

Unit (media:void). A leaf carrying the marker tag void. It is atomic: the parser rejects any combination of void with another tag:

media:void ∈ MediaUrn,    media:void ⪯ media:,    ¬(m ⪯ media:void) for any concrete m

A directional spec set to media:void is the unit type, read as “().” It is not the top, not “invalid,” not “absent.” It is a distinct first-class type whose meaning is “no payload flows on this side.”

The atomicity rule is structural: there is no lattice underneath the unit. media:void;warmup, media:void;heartbeat, media:void;reason=foo are parse errors, not refinements. Distinctions about why or how a void slot is used belong on the cap URN’s non-directional y axis or in cap args, never on the media URN itself. This forecloses an entire family of dispatch ambiguity (different unit values? different effects? different commands?) by refusing the syntax that would express them. See Media URNs: the unit type.

The dispatch relation treats media:void exactly like any other media URN. The fact that it admits a logical reading as the unit type is a property the CapKind classifier exploits to label caps; it never enters the dispatch predicate as a special case.

Cap kinds (logical layer)

The product C admits a five-way classification by inspecting (i, o) and the emptiness of y:

This classification is logical only. The dispatch relation defined in The dispatch relation does not branch on kind; the kind is a description of the resulting morphism, not a routing dimension. See Cap URN structure: cap kinds for the full taxonomy.

Cap specificity

Define:

spec_C : C → ℕ

By:

spec_C(i, o, y, e) = 10_000 * spec_U(o)
                    +    100 * spec_U(i)
                    +          spec_U(y)

The in, out, and y axes go through the same Tagged URN specificity function spec_U for the per-axis sum. Where the axes differ is in their weight in the cap-URN total: two orders of magnitude separate out from in from y, giving a single integer with lexicographic priority (out, in, y). This reflects routing intent: producing different things is the largest semantic difference between two caps, consuming different things is next, and y-axis metadata is least.

Per-tag scoring (the same six-form ladder applied uniformly across every axis):

This is a derived scalar used only for ranking among already valid candidates. See Specificity for full details and worked examples.

The dispatch relation

A candidate is a cap. A request is a query, a question about caps that asks something of each side or leaves it unknown (Dispatch: queries). Dispatch is the request, read as a query, admitting the candidate.

Let:

• candidate p = (i_p, o_p, y_p, e_p)
• request r = (i_r, o_r, y_r, e_r)

Dispatch(p, r)  ⟺  (i_r open ∨ i_r ⪯ i_p)  ∧  o_p ⪯ o_r  ∧  (e_r = ? ∨ e_p = e_r)  ∧  y_p satisfies y_r

where i_r open means the request’s input constrains nothing, and y_p satisfies y_r reads the candidate’s own tags as complete (Predicates: complete things).

This is the primary routing predicate. Underneath it is the typed relation between two caps as descriptions (arrow subtyping):

CapRefines(a, b)  ⟺  i_b ⪯ i_a  ∧  o_a ⪯ o_b  ∧  (e_b = ? ∨ e_a = e_b)  ∧  y_a ⪯ y_b

CapRefines(p, r) ⟹ Dispatch(p, r), and the two agree whenever the request states its input and neither side’s tags ask for an absence.

Interpretation of dispatch

Input admissibility (contravariant)

i_r open  ∨  i_r ⪯ i_p

An input the request has not established asks nothing. Otherwise the request’s input must be at least as specific as the candidate’s accepted input.

Type-theoretic view: Function parameters are contravariant. Candidate may accept more general inputs.

Output admissibility (covariant)

o_p ⪯ o_r

The candidate’s output must be at least as specific as the request’s required output.

Type-theoretic view: Function returns are covariant. Candidate must guarantee at least what request demands.

Behavioral refinement (the candidate’s tags, complete)

y_p satisfies y_r

The request’s non-direction tags are a pattern; the candidate’s are the tags it has. The candidate must have every tag the request asks for, may carry tags the request does not mention, and, because its list is complete, does not have the tags it omits: a request for !x is served by a candidate silent on x.

Variance summary

Dispatch is directional

In general:

Dispatch(p, r)  ⟹̸  Dispatch(r, p)

Dispatch is not symmetric.

A specific candidate can handle a generic request, but a generic request cannot “handle” a specific candidate.

Derived cap-level relations

Using base predicates componentwise:

Cap equivalence

CapEq(c₁, c₂)  ⟺  is_equivalent(i₁, i₂) ∧ is_equivalent(o₁, o₂) ∧ is_equivalent(y₁, y₂)

Cap comparability

CapComparable(c₁, c₂)  ⟺  is_comparable(i₁, i₂) ∧ is_comparable(o₁, o₂) ∧ is_comparable(y₁, y₂)

Useful for discovery, not sufficient for dispatch.

Correct predicate roles

Ranking policy

Ranking is defined only over the valid set:

Valid(r) = { p ∈ C | Dispatch(p, r) }

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

Specificity distance

dist(p, r) = spec_C(p) - spec_C(r)

Typical preference

1. dist = 0 (equivalent), most preferred
2. Smallest positive dist (refinement)
3. Negative dist only as fallback (generic candidate)

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

Fundamental sanity properties

Reflexivity of dispatch

∀c ∈ C,  Dispatch(c, c)

Follows from reflexivity of ⪯.

Transitivity of dispatch

∀a,b,c ∈ C,  (CapRefines(a, b) ∧ CapRefines(b, c)) ⟹ CapRefines(a, c)

Follows from transitivity of ⪯ (capRefines_trans). The composition law is a law of caps as descriptions, and of queries (Query.narrower_trans: a narrower question has fewer answers). It is not a law of Dispatch, which relates a cap to a question: a pdf-only candidate serves a request whose input is open; that request, read as a candidate, serves an image request; and the pdf-only candidate does not serve the image request. Dispatch: properties says where each law lives.

Monotonicity of candidate refinement

If candidate p’ refines p:

• i_p ⪯ i_p’ (more permissive input)
• o_p’ ⪯ o_p (more specific output)
• y_p’ ⪯ y_p (more specific y-tags)

And CapRefines(p, r) holds, then:

CapRefines(p', r)

Refinement preserves standing in (capRefines_monotone).

Contradiction rejection

¬(i_r open ∨ i_r ⪯ i_p) ∨ ¬(o_p ⪯ o_r) ∨ ¬(e_r = ? ∨ e_p = e_r) ∨ ¬(y_p satisfies y_r)  ⟹  ¬Dispatch(p, r)

If any conjunct fails, dispatch fails.

Common failure modes

Using accepts for dispatch

Wrong: Flattens 3-dimensional mixed-variance problem into one direction.

Using conforms_to for dispatch

Wrong: Same reason.

Using is_comparable for dispatch

Wrong: Relatedness is not validity. Two URNs can be comparable but not dispatchable.

Ranking before validity

Wrong: Specificity alone does not imply semantic legality.

Treating cap URNs as one-dimensional

Wrong: Cap URNs are structured product objects with mixed variance.

Separation of validity and preference

The specification distinguishes:

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

These must not be conflated.

Implementation conformance

Any implementation conforming to this specification must ensure:

1. All Tagged URNs normalize into U
2. All dimension-level checks reduce to the same base relation ⪯
3. Cap dispatch uses exactly the mixed-direction rule (Section 10)
4. 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 ⪯
• A specificity score spec_U

Cap URNs are four-coordinate product elements in U × U × U × E.

Dispatch is a request, read as a question about caps, admitting a candidate:

Dispatch((i_p, o_p, y_p, e_p), (i_r, o_r, y_r, e_r))
  ⟺  (i_r open ∨ i_r ⪯ i_p) ∧ o_p ⪯ o_r ∧ (e_r = ? ∨ e_p = e_r) ∧ y_p satisfies y_r

This yields:

• An order-theoretic interpretation
• A type-theoretic interpretation
• Separation of routing, planning, discovery, and exact matching
• A foundation for formal verification