A legal deontic vocabulary package

Area: Vocabulary & packages Teaches: how to publish a vocabulary — a package whose pub surface is upper-ontology concepts, introducer metatypes, an endpoint-constrained metarel, and catalog checks that a consumer gets for free when it imports the package. Prerequisites: UFO constraints (metarel endpoints, meta, specializes), and the meta-calculus. Run: ox build examples/legal_vocab_v0 && ox check examples/legal_vocab_v0 --codes

Ontological vocabulary is never built into Argon and never in std — a modeler ships it as an ordinary package and a consumer depends on it by path. This is the deontic counterpart of vocab_pkg_v0: a UFO-L modeler ships the deontic concepts, the directed-obligation relation, and the audits a legal modeler inherits. Its consumer is legal_catalog_v0.

What to read in root.ar

An axis orders the modalities. deontic_force is pure user vocabulary — the compiler never reads a force name — ordering the three modalities by the strength of the constraint each imposes:

pub metaxis deontic_force for metatype { permission < obligation < prohibition };

Introducer metatypes become the consumer’s declaration keywords. A consumer writes pub obligation PayRent <: … and the §3.4 introducer gate resolves the keyword across the dependency boundary. Each binds its force on the axis:

pub metatype permission  = { deontic_force::permission,  legal_kind::norm };
pub metatype obligation  = { deontic_force::obligation,  legal_kind::norm };
pub metatype prohibition = { deontic_force::prohibition, legal_kind::norm };

The deontic relation constrains both endpoints. A directed obligation runs from a debtor to a creditor — both party-sorted, never a contract or a bare individual. The endpoint metatypes are verified at elaboration; a relation declared with this introducer whose endpoint is not party-sorted is refused (see legal_catalog_bad_v0):

pub metarel directed_obligation(debtor: party, creditor: party);

The vocabulary ships its own checks. Every variable is TypeRef-sorted, so each #[static] check discharges at the consumer’s ox check, reading meta(k) / specializes. OrphanObligationConcept flags a norm-tagged concept that anchors to nothing in the vocabulary:

#[static]
pub check OrphanObligationConcept(k: TypeRef) :-
    meta(k) == obligation,
    not specializes(k, TimedObligation)
    => Diagnostic {
        severity: Severity::Warning,
        code:     "UFOL::W002",
        message:  "an `obligation` concept does not specialize `TimedObligation` — anchor it so its deadline discipline is inherited",
    };

Running it

The vocabulary itself checks clean — the checks fire on a consumer’s catalog, not on the vocabulary’s own declarations:

$ ox check examples/legal_vocab_v0 --codes
ok

The “free checks” property — that an imported check actually runs on the importing package — is demonstrated by the consumer legal_catalog_v0, where OrphanObligationConcept fires UFOL::W002 on the orphan norm concept.

This example is compiled in CI; the corpus auto-discovery parses and resolves it, and a corpus test (oxc-runtime/tests/examples_corpus.rs) pins the package surface, so it can’t drift from the language.