The Metatype Calculus

Chapter 2.1 introduced the four declaration forms — pub metaxis, pub metatype, pub metarel, pub decorator — that user packages compose to declare an ontology. This chapter is the engine underneath: the meta-property calculus the compiler runs over those declarations.

The calculus is a stratified Datalog-like fixpoint over a three-valued lattice. Given a concept hierarchy and a vocabulary’s metatype declarations, it computes for every concept its full meta-property profile across every axis the vocabulary declares; classifies declared metatypes against the inferred profile; runs the structural-rule constraints the package ships; and dispatches user decorators that match canonical FOL shapes onto fast-path implementations in the reasoner.

This chapter goes deeper than the surface needs. The audience is ontology engineers and language designers — readers who want the formal grounding behind ch02-01’s declaration forms, the cross-package composition rules, and the recognizer table that makes user-declared decorators run as fast as built-in ones. Working programmers can skim or skip; the surface in Part 2 is enough.

The chapter draws directly on Guizzardi’s UFO axiomatization (rigidity / sortality / identity-provision originated in Guizzardi 2005, refined in Guizzardi & Wagner 2010 and Guizzardi et al. 2018). The principal results below — termination, uniqueness, and necessity of acyclicity — are stated as theorems and accompany the engine that evaluates them.

The four foundational axes (UFO as worked example)

UFO declares four axes that the rest of its foundational vocabulary builds from. We use UFO here because it is the most-developed worked example; BFO, GFO, DOLCE each declare their own axes via the same substrate.

Rigidity

A concept is rigid if every instance falls under it in every world the instance exists in. A Person is rigid: an entity that is a person here is a person in every counterfactual world where that entity exists at all. A Student is anti-rigid: an entity may be a student in this world and not in another. A Mixin is semi-rigid: rigid for some classifications, anti-rigid for others.

Rigidity is the foundational axis in UFO and is operationalized as A.rigidity ∈ { rigid, anti_rigid, semi_rigid } in the meta-property state.

Sortality

A concept is sortal if it carries an identity criterion — a principle for telling when two instances are the same. A Person is sortal (we have a notion of which person is which). A Red Thing is non-sortal (red is a classifier, not an identity-provider).

In UFO, sortals must trace through their supertype chain to a Kind — the metatype that provides identity. OW0207 (“sortal missing Kind ancestor”) is the structural-rule check that surfaces a violation.

Identity-provision

A concept provides identity if instances classified by it gain an identity criterion from it. Kind provides identity. Role does not (it inherits identity from the role-playing concept’s Kind). Subkind does not (it inherits from the parent Kind).

This axis is what makes kind and subkind semantically distinct even though both have the same { rigid, sortal } profile on the rigidity-and-sortality axes alone. The third metatype dimension provides_identity ∈ { yes, no } separates them.

Provides-mediation

A concept provides mediation if it exists to connect other concepts. Relator provides mediation; that is the whole point of the metatype. Kind does not.

Lease is a relator: it has no business existing on its own; it exists to connect a Tenant, a Landlord, and a property. The structure traces back to Hohfeld (1913), who analyzed legal relations as bundles of right-duty / power-liability pairs that bind multiple parties — a tenant’s right to occupancy is paired with a landlord’s duty not to interfere, a landlord’s power to terminate is paired with a tenant’s liability to vacate, and so on. Each pair lives in the relator, not in the parties. UFO’s relator (Guizzardi 2005, §6.4) is the foundational-ontology generalization: a category of entities whose existence consists in mediating other entities.

OW0211 (“role has no mediation path to relator”) is the structural-rule check that fires when a role concept has not been wired to any concept that provides mediation.

The axis dependency DAG

A pub metaxis declaration may depend on other axes through a condition clause. UFO’s identity_provision axis declares:

pub metaxis identity_provision for type {
    provides,
    inherits,
    condition: rigidity == rigid and sortality == sortal
}

The condition says: identity_provision only ranges over concepts that have already been classified as rigid and sortal. The calculus reads this as a dependency edge in the axis DAG: rigidity → identity_provision and sortality → identity_provision. The fixpoint iterates axes in topological order so that, by the time it computes identity_provision, the predecessor axes have completed.

Two constraints follow:

1. Acyclicity. A vocabulary whose dependency edges form a cycle is rejected at vocabulary-load time. Without acyclicity the fixpoint admits two evaluation orders that disagree at termination — the result depends on the order, not the input. Argon refuses such vocabularies; a package author must structure axis dependencies as a DAG.
2. Topological evaluation. With acyclicity, the calculus runs the axes in topological order. Within an axis, the calculus runs three strata (below); across axes, the strata of axis B may read the completed state of axis A. This makes condition clauses load-bearing: they let one axis express its applicability in terms of another.

The DAG is per-vocabulary. Two unrelated vocabularies (UFO with rigidity/sortality, BFO with temporal-status/dependence) compose to two disjoint DAGs that evaluate independently. A vocabulary that extends another (a domain package declaring enforceability whose condition depends on UFO’s rigidity) extends the DAG with new edges to UFO’s existing axes; the result must remain acyclic, and the combined fixpoint over multi-package axis sets is well-defined under that condition.

The three strata

The engine runs each fixpoint pass in three strata, in this order. Strata are stratified in the technical sense: each stratum reads from the previous strata’s completed state, never from an in-progress one.

Formally, let $C$ be the set of concepts, $A$ the set of axes, and $V_a$ the value set for each axis $a\in A$. The meta-property state is a function $\sigma :C\times A\times V\to \{\mathsf{IS},\mathsf{NOT},\mathsf{CAN}\}$ where $V={\bigcup }_a{V}_a$. The lattice on values is the information ordering $\mathsf{CAN}⊑\mathsf{IS}$ and $\mathsf{CAN}⊑\mathsf{NOT}$; $\mathsf{IS}$ and $\mathsf{NOT}$ are incomparable.

Stratum 0 — IS propagation

Stratum 0 is a set of monotone rules of the form

$$\frac{\sigma (c_1,a_1,v_1)=\mathsf{IS}\cdots \sigma (c_k,a_k,v_k)=\mathsf{IS}}{\sigma (c,a,v)\mapsto \mathsf{IS}}$$

Each rule reads only IS premises and produces an IS conclusion. The set of rules is run to fixpoint: ${\sigma }_{n+1}=T({\sigma }_n)$ where $T$ is the immediate-consequence operator over the rule set. Because $T$ is monotone in the information ordering and the lattice has finite ascending chains, the iteration terminates.

If a concept is declared as a kind, the metatype’s profile materializes as starting IS facts: $\mathsf{IS}(c,rigidity,rigid)$, $\mathsf{IS}(c,sortality,sortal)$. Subtype propagation rules give $\mathsf{IS}(s,a,v)$ from $\mathsf{IS}(s^{\prime },a,v)$ when $s⊑s^{\prime }$ in the type hierarchy.

The composition of Stratum 0’s rules is monotone in the information ordering, and the lattice has finite ascending chains, so the iteration’s least fixed point exists, is reached in finitely many steps, and is unique.

Stratum 1 — NaF (negation-as-failure)

Reads the completed IS-state ${\sigma }_0^{\ast }$ and adds NOT facts where the absent-condition holds:

$$\frac{{\sigma }_0^{\ast }(c,a,v)\ne \mathsf{IS}\forall v^{\prime }\in V_a.v^{\prime }\ne v⟹{\sigma }_0^{\ast }(c,a,v^{\prime })\ne \mathsf{IS}}{{\sigma }_1(c,a,v)\mapsto \mathsf{NOT}}$$

This is classical Clark NaF semantics, restricted to a single direction (negative) so the calculus stays stratified. Stratum 1 reads completed Stratum 0 state, so the negation cannot circle back.

Stratum 2 — constraint checks

Reads both IS and NOT states. Emits diagnostics: structural rules (OW0207 through OW0214 plus more), rigidity / sortality consistency checks, sibling-axiom partition completeness checks. Stratum 2 never modifies the meta-property state — it is a one-way producer of diagnostics. A violation is a warning or error; the calculus’s IS / NOT state is unchanged.

The three-valued state

Each (concept, axis, value) triple lands in one of four states:

• IS — Stratum 0 placed it there. Rigorously inferred.
• NOT — Stratum 1 placed it there. The concept is not at this value.
• CAN — neither IS nor NOT applies. The state is genuinely indeterminate.
• (absent) — the axis is not in scope for this concept.

The CAN state is the load-bearing one. Under open-world assumption — which is Argon’s default for ontology work — the absence of evidence is not evidence of absence. CAN says: “the model has not committed to a value; further axioms may pin it.” The fourth theorem below pins this down formally: CAN at fixpoint completion really is genuine indeterminacy — not “we forgot to check.”

This three-valued state is essential for the refinement-type fragment (Chapter 2.6) and the standpoint world-assumption interaction (Chapter 5.4).

Sibling-axiom propagation and structural rules

The calculus is the engine. The structural rules — UFO’s R01–R37 (Barcelos et al. 2023) — are the content: constraint rules a vocabulary package declares to enforce well-formed modeling. They are the second-and-third strata’s main customers.

They land in the source as pub strict error or pub warning declarations:

pub strict error rigid_specializes_anti_rigid(A, B) :-
    A specializes B,
    A.rigidity == rigid,
    B.rigidity == anti_rigid

This is UFO’s R02 in source: “a rigid type cannot specialize an anti-rigid type.” The body reads the meta-property state populated in Strata 0 and 1; the head emits a diagnostic at Stratum 2. The rule does not mutate state — it only signals.

The full UFO ruleset (R01–R37) covers hierarchy constraints (rigidity-lattice descent), identity constraints (every sortal traces to a Kind ancestor; no two independent identity providers), mixin heterogeneity (semi-rigid mixins must aggregate at least one rigid and one anti-rigid descendant), phase constraints (every phase is in a partition), role constraints (every role has a mediation path to a relator), and anti-pattern detections (non-sortal aggregating sortals from a single Kind — likely a Subkind in disguise).

A different vocabulary ships a different ruleset. BFO’s structural rules carve continuant-vs-occurrent disjointness, independent-vs-specifically-dependent disjointness; cofris carves financial-quantity invariants; ccf carves accounting-equation invariants. The machinery is the same: rules read the calculus’s IS/NOT state, emit diagnostics at Stratum 2.

The reason structural rules are first-class — not decorative documentation — is that the calculus runs them at every ox check. UFO’s R02 is not a comment in a paper; it is a rule the elaborator applies, and a violation is a compile-time event. The structural-rule diagnostic codes (OE0204 for hard errors, OW0207–OW0214 for warnings) are documented in Appendix C; each fires on a specific axiom and ox explain long-forms the underlying rationale.

Recognizer dispatch — fast-path for canonical shapes

A user package declares decorators like @[transitive], @[symmetric], @[functional] on relations. The decorator’s semantics: body is FOL — a formula the reasoner could in principle evaluate via Datalog with negation. In practice that is slow: a transitive-closure rule fires O(n^2) times in the worst case under naïve Datalog, and a Functional cardinality check naïvely materializes all pairs.

The compiler avoids both costs through the recognizer table: ten canonical FOL shapes that the reasoner has fast-path implementations for. When a pub decorator body matches one of these shapes, the compiler routes the application to the fast-path; when it does not, the body falls through to generic Datalog evaluation.

The ten shapes:

Transitive { rel }
Symmetric { rel }
Asymmetric { rel }
Reflexive { rel }
Irreflexive { rel }
Functional { rel }
InverseFunctional { rel }
QualifiedCardinality { rel, on_class, min, max }
DisjointClasses { class_a, class_b }
CoveringClasses { parent, children }

Recognition runs against the FOL body after six normalization passes — alpha_rename → flatten_associative → push_negations_inward → implications_to_disjunctions → canonicalize_equality → sort_conjuncts. Per-rule overhead stays under 5ms in a 100-rule package; the matching is exact, not heuristic. A body that recognizes routes the relation through a built-in fast-path (enable_transitive_closure_for, enforce_functional, …); a body that does not lowers to Datalog atoms and runs through the generic evaluator.

A user decorator can pre-tag its expected shape:

pub decorator transitive() on rel = {
    semantics: forall x y z. r(x, y) and r(y, z) -> r(x, z),
    lowers_to: Transitive
}

The lowers_to: Transitive annotation tells the compiler “I expect this body to recognize as a Transitive shape.” If the body does not match the declared shape, the compiler emits OE0232 RecognizedShapeMismatch. Without the annotation, the compiler runs the recognizer and uses whatever shape matches; with the annotation, it cross-checks. Pre-tagging is documentation that the compiler enforces.

The recognizer also feeds into tier classification. A rule whose body recognizes as Transitive collapses from the syntactic tier:fol to the structural tier:closure — its effective tier is min(syntactic, recognized). A user who writes a transitive-closure body inside unsafe logic { ... } (which is always tier:fol ambient) can still benefit from the fast-path and the lower effective tier, provided the body recognizes.

Chapter 5.3 covers tier classification end-to-end; the recognizer table is the substrate’s bridge to the reasoner’s fast-path layer.

Cross-package metatype composition

The substrate composes across packages. UFO declares rigidity, sortality, identity_provision. cofris (the financial-resources foundational ontology) declares its own axes — say, liquidity and convertibility. A domain package can declare a metatype that depends on both:

use ufo::prelude::*;
use cofris::prelude::*;

pub metatype MarketableAsset = {
    rigid,
    sortal,
    provides,
    liquid,
    convertible
}

The compiler resolves each axis name against the union of in-scope pub metaxis declarations from both packages and validates that every axis the metatype binds is satisfied. The dependency DAG extends naturally: UFO’s edges, cofris’s edges, and any new edges the metatype’s axes induce. The combined DAG must remain acyclic.

Three composition results matter here:

• Disjoint non-interference. If two vocabulary packages share no axes, their rule sets evaluate independently. UFO’s structural rules cannot affect cofris’s classification, and vice versa. This is the common case for orthogonal foundational ontologies.
• Shared-axis confluence. If two packages share an axis (both declare rigidity, say), the calculus runs the union of their rule sets and the result is well-defined provided the rule sets are jointly stratified — that is, the axis’s rules from one package do not cyclically depend on the axis’s rules from the other.
• Combined-fixpoint convergence. The combined fixpoint over multi-package axis sets terminates and is unique under acyclicity.

A practical consequence: a project can mix foundational ontologies (UFO + cofris + ccf, the canonical Argon stack) without the compiler’s behavior depending on import order. The semantics is fixed by the union of declarations, not the iteration order through them.

Bidirectional reasoning

The engine exposes three operations:

Forward is the obvious direction: given the modules, fill in every concept’s IS / NOT / CAN triples.

Reverse synthesis is the more unusual one. Given a meta-property profile (say { rigid, sortal, provides_identity: yes }), the engine returns the list of metatype names whose definition matches that profile. It is the answer to “given how this concept actually behaves, what metatypes should we consider for it?” — useful when porting concepts from one foundational ontology to another, or when the modeller knows a concept’s behavior but is uncertain about the right metatype label.

Verification is the consistency check: the user declared pub kind Person and the engine infers Person’s profile. If the inferred profile contradicts kind’s declared profile, the engine emits a diagnostic. The check is the foundation for the structural-rule warnings and the four-variant OE0605 UnknownMetatype hint.

Termination, uniqueness, and the indeterminacy guarantee

The fixpoint terminates because the axis-dependency graph is acyclic. With no cycles, the fixpoint runs the strata in topological order and finishes in $\mathcal{O}(|C|\cdot |A|\cdot |R|)$ time per pass, where $R$ is the rule count.

Four results carry the calculus.

Termination. For any stratified rule set $\mathcal{R}$ over a finite concept hierarchy, the fixpoint iteration of the strata reaches a fixed point in finitely many steps.

Uniqueness. For any stratified rule set $\mathcal{R}$, the fixpoint ${\sigma }^{\ast }$ is unique: any two evaluation orders that respect the strata produce the same final state.

Necessity of acyclicity. Acyclicity of the axis-dependency graph is necessary for fixpoint uniqueness — a cyclic dependency graph admits two evaluation orders that disagree at fixpoint.

Genuine indeterminacy of CAN. If ${\sigma }^{\ast }(c,a,v)=\mathsf{CAN}$ at fixpoint completion, then no monotone extension of the input determines whether $\sigma (c,a,v)$ should be IS or NOT. CAN at completion is genuine indeterminacy — not “we forgot to check.”

The fourth result is the load-bearing one for refinement-type semantics: when Chapter 2.6 admits a refinement-type predicate only when its meta-property atoms are IS, the CAN cases left out are formally indeterminate, not arbitrarily excluded.

When a metatype declaration goes wrong

Six classes of error worth knowing:

• OE0603 MetaxisValueTypeMismatch — a pub metatype binds an axis to a literal whose type does not match the axis’s declared value_type. Writing pub metatype kind = { rigidity = "rigid" } against pub metaxis rigidity { rigid, anti_rigid } triggers this — the axis values are atoms, not strings.
• OE0605 UnknownMetatype — a pub <name> X { ... } concept declaration whose <name> does not resolve to an in-scope metatype. The diagnostic carries a four-variant hint: the name might resolve to something other than a metatype (NotMetatype); a matching metatype might exist in an unimported package (AvailableNotImported); multiple matching metatypes might exist across packages (MultipleAvailable); or no matching declaration exists anywhere (NotDeclared).
• OE0606 MetaxisRefinementViolation — a value supplied to a typed-domain metaxis fails the axis’s where { _ <pred> } refinement. A metarel that binds cardinality_floor = 0 against a metaxis declared Nat for rel where { _ > 0 } triggers this.
• OE0225 UnknownMetarel / OE0226 MetarelEndpointMismatch — a relation declared :: foo whose foo does not resolve to an in-scope metarel, or whose source/target endpoints do not satisfy the metarel’s declared metatype constraints.
• OE0229–OE0234 (decorator family) — unresolved name, arity mismatch, target mismatch, tier-clause divergence, argument-type mismatch on a decorator application, plus OE0232 RecognizedShapeMismatch when a body’s lowers_to annotation diverges from what the recognizer matches.
• OE0204 and the OW0207–OW0214 family — UFO’s structural rules (rigid specializing anti-rigid, sortal missing Kind ancestor, role missing mediation path, etc.) firing as either errors or warnings depending on the rule’s declared severity. These are vocabulary-side — UFO authors them, the compiler runs them. A different vocabulary ships a different family.

The first five classes are diagnostics from the substrate itself: they fire when a vocabulary package’s declarations are malformed. The last family is diagnostics from the vocabulary’s content: they fire when user code writes concepts that violate the vocabulary’s structural constraints. Both are run by the same calculus at Stratum 2.

A worked verification

Take the lease tutorial’s metatypes:

use ufo::prelude::*;

pub kind Person { ... }
pub role Tenant : Person { ... }
pub relator Lease { tenant: Tenant, ... }

The engine, given this input:

• Stratum 0 propagates IS(Person, rigidity, rigid), IS(Person, sortality, sortal), IS(Person, identity_provision, provides) from kind’s profile. Subtype propagation gives IS(Tenant, sortality, sortal) and IS(Tenant, rigidity, anti_rigid) from role’s profile (overriding what would have inherited from Person’s rigidity, because the role declaration pins the value). Same for Lease — relator’s profile carries rigid, sortal, provides_identity.
• Stratum 1 completes the negative facts: NOT(Tenant, rigidity, rigid), NOT(Person, rigidity, anti_rigid), NOT(Lease, sortality, non_sortal), etc. Every (concept, axis, value) triple where Stratum 0 placed nothing and no other value of the same axis was placed for the concept lands as NOT.
• Stratum 2 runs the structural checks. Tenant: anti-rigid + sortal → must trace to a Kind ancestor → does, via Person → OW0207 does not fire. Tenant: relationally dependent → must have a mediation path to a relator → does, via the tenant field on Lease → OW0211 does not fire. Lease: provides_identity → checks the partition rule (no two independent identity providers in the ancestor chain) → passes.

All clean. The lease tutorial’s ox check reports zero structural-rule warnings, which means the metatype graph the modeller wrote is internally consistent against UFO’s structural axioms.

For a worked example of Stratum-0 IS propagation across an independent foundational vocabulary — i.e. one with axes that have nothing to do with UFO’s rigidity/sortality — see argon/examples/bfo-smoke/. The smoke test declares BFO’s temporal_status and dependence axes, four BFO metatypes (continuant, occurrent, independent_continuant, specifically_dependent_continuant), six BFO concepts (MaterialEntity, Process, Quality, …), and two BFO structural rules (continuant-occurrent disjointness, independent-dependent disjointness). Running ox check exercises every stratum of the calculus end-to-end against BFO; running it alongside argon/examples/dolce-lite/ exercises the disjoint-non-interference composition result. The dedicated _catalog/rule-meta-coloncolon/ workspaces additionally exercise the four-arm endpoint resolver from RFD-0031 — relations declared :: <metarel> whose endpoints reference concepts, metatypes, or wildcards.

If the user had instead written pub kind Tenant : Person { ... } (asserting Tenant is rigid), Stratum 0 would propagate IS(Tenant, rigidity, rigid). Verification — the third bidirectional operation — would then report that Tenant’s declared metatype kind carries the profile {rigid, sortal, provides}, while the inferred profile from the surrounding ontology (Tenant playing a role on Lease) says it should be {anti_rigid, sortal, relational}. The engine emits a diagnostic explaining the disagreement.

Why this matters

Four things, taken together, make the meta-property calculus more than just an implementation detail:

It makes vocabulary substitution real. Switching the lease tutorial from UFO to BFO is not a rewrite — it is a different use line and (potentially) a different set of axis declarations. The concepts, relations, and rules in lease.ar and rules.ar are the same. The metatype labels and structural rules are different, because that is what changes between foundational ontologies.

It makes structural rules first-class. UFO’s structural axioms (R01 through R37 in the foundational papers) are not documentation — they are constraint rules in the engine, with diagnostic codes and ox explain long-forms. A structural violation is a compile-time event.

It makes the recognizer a public surface. A user who declares @[transitive] knows that the body recognizes as a Transitive shape and routes to the reasoner’s fast-path. A user who declares a custom decorator with a body that recognizes as Functional gets the same fast-path treatment — without convincing the compiler maintainers to special-case their decorator. The substrate’s recognizer is a finite menu of canonical FOL shapes; users dial decorators against that menu.

The metatheory is closed. Termination is not “we hope so,” uniqueness is not “in practice, yes.” The four results above are theorems about the calculus, not observations about the implementation; that is a stronger statement than “the implementation seems right.”

What’s next

Chapter 5.2 covers the defeasibility layer that builds on top of the calculus — @[default], @[override], @[defeat], the Governatori three-stratum compilation. Chapter 5.4 covers standpoints, which interact with the meta-property state through per-(module, predicate) world assumptions. The tier ladder treats meta-property lookups as tier:structural reasoning — the cheapest possible derivation, polynomial in the size of the calculus, and the floor onto which recognized-shape decorators collapse from the FOL body language.