Argon

Argon is a knowledge-representation language and graph database. You declare an ontology — concepts, the relations between them, and the rules that derive new facts — and Argon compiles it to a content-addressed artifact you can query, reason over, mutate, and serve.

This book is the surface specification: the syntax and meaning of an Argon program — the precise reference, chapter by chapter, in the technical specification and its appendices.

For a guided, motivated tour of the whole language, read The Argon Book, the teaching narrative (spec/book/). To watch real packages compile and run, see Argon by Example (examples/).

Two companion sources of truth sit beside this book:

• The Lean 4 mechanization (spec/lean/) is canonical for the substrate — the type system, reasoning semantics, and decidability results. Where the Lean and this book disagree on something the Lean covers, the Lean wins; the book is the bug.
• RFDs (Part II) record design decisions and their rationale. They are history, not normative spec.

Each chapter leads with a grammar fragment and a worked example before the prose. Cross-references are named links; each names the chapter or section it points to.

Toolchain: installation, channels, and versioning

How Argon is installed, versioned, and switched. oxup is the toolchain manager (rustup-style); ox/oxc/ox-lsp/oxfmt are the tools it dispatches.

Install

curl -fsSL https://install.argon-lang.org/install.sh | sh

Installs oxup into ~/.argon/bin, links the tool shims, and installs the stable toolchain. Ensure ~/.argon/bin is on PATH.

Platforms: macos-arm64, linux-x86_64, linux-aarch64.

Channels

Version strings

X.Y.Z is the in-development line; dev/nightly are prereleases of it (they sort ahead of the last stable). oxup and the toolchain share one version.

Distribution layout

Served from https://install.argon-lang.org (S3 origin behind CloudFront):

/install.sh                                                          installer
/toolchains/<version>/<platform>/argon-<version>-<platform>.tar.gz(.sha256)
/dist/channel-<channel>.toml                                         current version per channel
/dist/index-<channel>.json                                           all published versions
/oxup/latest/<platform>/oxup(.sha256)                                oxup self-update (stable)
/oxup/<channel>/latest/<platform>/oxup(.sha256)                      oxup self-update <channel>
/editors/vscode/<version>/argon-<version>.vsix(.sha256)              editor extension

• /toolchains/<version>/ is immutable. dev/nightly tarballs are pruned 30 days after publish; stable is kept indefinitely.
• index-<channel>.json is newest-first: an array of { version, released, platforms[], sha256, available }. A pruned build stays listed with "available": false.

Toolchain spec

A spec identifies a toolchain to install/use/+<spec>:

oxup commands

oxup use <spec>                            install if needed, then set as default
oxup default <spec>                        alias for `use`
oxup install <spec>                        install without changing the default
oxup uninstall <spec>                      remove an installed toolchain
oxup update [channel]                      re-fetch a channel's latest
oxup list                                  installed toolchains (default marked)
oxup list --available [--channel C] [--limit N]   published versions
oxup search <pattern>                      search published versions across channels
oxup show                                  active toolchain, default, installed
oxup which <tool> [--toolchain <spec>]     resolved binary path
oxup self-update [channel]                 update oxup itself (stable; or dev/nightly)
oxup extension install|uninstall|list      editor extension (matches the active toolchain)

--json is available on list, search, and show (for tooling).

Selecting a toolchain (per invocation)

First match wins:

1. OXUP_TOOLCHAIN=<spec>
2. +<spec> as the first argument — e.g. oxc +nightly build
3. ox-toolchain.toml in the working directory or a parent — [toolchain] channel = "<spec>"
4. ~/.argon/settings.toml — [default] channel
5. the built-in stable

A missing toolchain is fetched automatically on first use.

~/.argon/

~/.argon/
  bin/
    oxup                     the manager
    ox oxc ox-lsp oxfmt      symlinks → oxup
  toolchains/<spec>/
    bin/                     ox oxc ox-lsp oxfmt
    share/std/               bundled stdlib packages
    manifest.toml            version, platform, components
    provenance.toml          source (cdn|local), origin, sha256, install time
  settings.toml              [default] channel, [extension] state

ox/oxc/ox-lsp/oxfmt on PATH are symlinks to oxup; oxup reads argv[0], resolves the active toolchain, and execs ~/.argon/toolchains/<spec>/bin/<tool>.

Tools

Formatter notation policy

Argon’s dual notation (Unicode notation) lets source mix Unicode glyphs (∀ ⊑ → ⊞) with their ASCII spellings (forall <: -> box_plus); both lex to the same token. The formatter can normalize a file to one form, governed by [fmt] notation in ox.toml:

[fmt]
notation = "preserve"  # | "unicode" | "ascii"

• preserve (the default) never rewrites between the two forms — a file is formatted as typed, so mixed notation is left untouched.
• unicode rewrites every ASCII spelling to its glyph (forall → ∀); ascii does the reverse. The rewrite is lossless and round-trips, because both forms produce the identical token.

The policy resolves through a nearest-wins cascade (rustfmt/prettier-style): a package’s own [fmt] overrides a [workspace.fmt] at the workspace root, which overrides the global user config. The notation table itself is the single [[notation]] source shared with the lexer aliases and editor input methods. Notation is policy (a per-project taste call); spacing and layout are the Argon convention and are not configurable.

Editor support

Everything an editor knows about an Argon program comes from one place: the language server, ox lsp. The reason is the meta-calculus. Argon’s surface vocabulary is user-extensible — a package declares its own metatypes, concepts, relations, and constructs, so the set of meaningful words in a file is not fixed by the language. A static grammar can color and brace-match the punctuation, but it cannot know that Obligation is a concept or that owes is a relation; only the resolver that elaborated the package knows that. So all the language-aware behavior — diagnostics, hover, jump-to-definition, the right token colors — lives in the server, and editors are thin clients of it. One server, written once, drives every editor; an editor plugin is just an LSP client plus a syntax floor.

What ox lsp provides

ox lsp speaks LSP over stdio and advertises:

Inlay hints and code lenses are not built yet. Because the diagnostics are the server’s, they always match the toolchain that produced them — there is no second, drifting implementation of the checks.

Installing it

oxup installs and version-locks the editor integration, so the editor support matches the active toolchain:

oxup extension install                         # auto-detect every installed VS Code-family editor
oxup extension install --editor neovim         # or name one explicitly
oxup extension uninstall --editor emacs
oxup extension list                            # detected editors + the installed version

The two editor families install differently because they expose different contracts:

• VS Code family (VS Code, Cursor, VSCodium, VS Code Insiders, and the browser-hosted code-server) have an --install-extension CLI. oxup fetches the .vsix stamped with the active toolchain version from an immutable CDN path, sha256-verifies it (the same fail-closed discipline as the toolchain fetch), and installs it. A user on stable 0.2.2 gets the 0.2.2 extension, not “latest”.
• Neovim, Vim, and Emacs have no extension-CLI contract, so oxup installs them by file placement: it writes the embedded plugin files into the editor’s package directory and adds an idempotent, oxup-managed block to the init file (between >>> argon (oxup-managed) >>> sentinels) that points the client at the active toolchain’s ox lsp. Re-running updates the block in place and leaves everything outside the sentinels untouched; uninstall removes both.

oxup init and oxup update auto-install and refresh the integration after the toolchain is placed (oxup init --no-extension opts out). A failed editor install is a soft, one-line warning — the toolchain is what matters — never a hard error.

The VS Code extension ships the Argon “A” glyph as the .ar file icon. The Neovim and Emacs plugins cannot reuse that SVG (their file explorers draw a Nerd Font glyph, not an image); their READMEs give a suggested glyph-and-color registration keyed on the .ar extension.

Environment

Scope

Argon is a programming language for declaring and reasoning over a richly-typed knowledge graph at the data-system layer. The canonical specification of the language core lives in Lean 4 under spec/lean/; this document specifies the surface in prose. Where they disagree, the Lean wins.

The language is built from five atoms — meta-calculus, constructs, rule, trait, macro — and nothing else. Every surface form lowers to one of them. Argon has no surface for IO, threads, network, or filesystem; those live in the host runtime. Tenancy and multi-tenant orchestration are application concerns, not language concerns.

Lexical structure

Source

UTF-8. Source files have extension .ar. Non-ASCII text is admitted in identifiers (Identifiers, UAX #31), comments (Comments), and string/char literals (Literals). Operators and keywords have a canonical ASCII spelling and an equivalent Unicode form — Lean-style dual notation (Operators): ∀ is forall, ⊑ is <:, → is ->, ⊞ is box_plus. The two are interchangeable surface spellings of the same token, so a program may be written in either (or a mix), and editors enter the Unicode forms through a \abbrev input method (\forall → ∀). Delimiters and the remaining punctuation are ASCII.

Comments

• // — line comment, not extracted by ox doc.
• /// — outer doc comment, attaches to the next item.
• //! — inner doc comment, attaches to the enclosing module.
• /* … */ — block comment, may be nested. Not extracted by ox doc. Comments out arbitrary tokens including //-prefixed lines, useful when temporarily disabling sub-expressions.

Identifiers

Identifiers follow UAX #31: an identifier starts with a XID_Start character or _, and continues with XID_Continue characters. The ASCII subset [A-Za-z_][A-Za-z0-9_]* is the common case and the recommended style. An identifier’s text is its exact source bytes. NFC canonical equivalence (so that a precomposed é U+00E9 and the decomposed e + combining acute U+0065 U+0301 would denote the same name) and a mixed-script confusable warning (UAX #39, Latin A U+0041 vs Cyrillic А U+0410) are the RFD 0034 name-resolution design (Out of scope). Conventions: snake_case for value bindings, fields, and rules (fn, derive, query, mutate, check); CamelCase for types, metatype-introduced concepts, and metarel-introduced relations; lowercase (typically snake_case) for the metatype- and metarel-introducing keywords themselves (kind, role, rel, mediation, …); SCREAMING_SNAKE_CASE for stdlib constants. Conventions are not enforced.

Operators

Top / ⊤ and Bot / ⊥ are type-level constants.

Unicode notation

Each operator/keyword below has an equivalent Unicode glyph; the glyph and its ASCII spelling lex to the same token, so they are fully interchangeable and nothing past the lexer distinguishes them. Glyphs and the editor \abbrevs follow the Lean lean4-input conventions; the metric-modal glyphs (⊞/⊟) follow the DatalogMTL literature. The authoritative table is [[notation]] in compiler/crates/oxc-syntax/grammar.toml, the single source from which the lexer’s aliases and the editor input methods are generated.

=> is deliberately not given a Unicode form: it is match-arm / head syntax, not implication, so ⇒ would mislead. diamond_plus / diamond_minus have no single conventional glyph (the notation is ◇ with a directional marker) and stay ASCII-only for now.

Boolean operator placement. Argon distinguishes two syntactic positions:

• Rule-body position — after :- in derive/check, inside unsafe logic blocks, the from/where clauses of query bodies, subquery bodies (collect/set/one/count/exists), refinement where { … } / iff { … } clauses, and require { … } precondition blocks. Conjunction is ,; NAF is not atom. Disjunction is not inline — write multiple rules with the same head, or combine subquery variants via union / intersect / except.
• Expression position — inside fn bodies, if / match conditions, let initializers, the RHS of comparison atoms inside rule bodies, and atom arguments. Boolean operators are &&, ||, !.

The two are non-overlapping: && is not accepted between rule-body atoms; , is not a Boolean operator in expressions.

Literals

INT      ::= [0-9]+ ( '_' [0-9]+ )*
REAL     ::= INT '.' INT
STRING   ::= '"' chars '"'
TEMPORAL ::= '#' ISO '#'
BOOL     ::= 'true' | 'false'
LIST     ::= '[' (expr (',' expr)*)? ','? ']'
RECORD   ::= '{' (Ident ':' expr (',' …)*)? ','? '}'

A temporal literal is one #…#-delimited form whose inner ISO-8601 / RFC-9557 shape totally determines the carrier (RFD 0067) — there is no per-type prefix and no trailing suffix that silently flips the kind. The shape is decided statically at parse; a malformed or ambiguous inner form is loud-refused, never coerced:

FRAC     ::= '.' [0-9]+
OFFSET   ::= ('+' | '-') HH ':' MM
DATE     ::= '#' YYYY '-' MM '-' DD '#'                    → Date       (civil, day)
TIME     ::= '#' HH ':' MM ':' SS FRAC? '#'                → Time       (civil wall-clock)
DATETIME ::= '#' YYYY '-' MM '-' DD 'T' HH ':' MM ':' SS FRAC? '#'
                                                           → DateTime   (civil, no zone)
INSTANT  ::= '#' … 'T' … (SS FRAC?) ('Z' | OFFSET) '#'     → Instant    (absolute UTC point)
ZONED    ::= '#' … 'T' … (SS FRAC?) OFFSET '[' IANA/Zone ']' '#'
                                                           → ZonedDateTime

The trailing Z denotes an Instant (UTC, absolute), following ISO/RFC-9557 (Z = UTC), not a civil DateTime; a bare #…T…# with no zone marker is the zoneless civil DateTime. There is no mandatory Z. Only Date and civil DateTime are compiler-executable today; the Time, Instant, and ZonedDateTime literal forms are recognized by the surface grammar ahead of the value-layer landing them (issue #1285).

Set/map literals are constructor calls (Set::new(a, b, c), Map::new((k, v), …)); there is no {1, 2, 3} form (Out of scope).

Modules and packages

Structure

Modules take three forms, all equivalent at the symbol table:

• A .ar file is implicitly a module named for its file stem.
• A directory containing mod.ar is a module; sibling .ar files (and subdirectories containing mod.ar) are submodules of it.
• An inline mod Name { … } declaration introduces a nested module in the current file.

A mod Name; declaration with no body has a single meaning — Rust’s child-module declaration: it asserts that a sibling Name.ar (or Name/mod.ar directory module) exists and attaches its contents under the current namespace as Name. A file does not rename itself: a content-carrying file whose mod Name; resolves to no sibling is refused with OE0715 (audit dc-06 retired the legacy “module-header” reading, where the first mod Name; of a file silently relabeled that file’s own declarations as module Name). To set a module’s name, use the file/directory layout — the project entry is module root, and any other .ar file is the module named for its stem; to declare a child, create the sibling Name.ar; to keep declarations where they are, omit the mod line. Explicit mod declarations are required; the compiler emits OW0710 when a sibling .ar file exists but no mod declaration references it.

Both project and package entry default to the root module file — preferring the Cargo-style src/root.ar, falling back to a flat root.ar at the package root. A prelude.ar is not an entry default: a package’s prelude is the manifest [package].prelude import model (the auto-imported use-tails of RFD 0038), and a prelude.ar file is an ordinary re-export module reached through the root — conventionally pub used at the root and imported by dependents via use pkg::prelude::*. The entry’s directory is the source root under which the package’s .ar files are indexed.

visibility ::= 'pub' | 'pub' '(' 'pkg' ')'
mod-decl   ::= 'mod' Ident ';'                                  // file-include
            |  'mod' Ident '{' mod-item* '}'                    // inline
            |  'mod' Ident '=' path '(' expr-list ')'           // functor alias (Functor modules)

Default visibility is module-private, following Rust: a default-visibility item is visible to the module that declares it and every descendant module. A private item declared at the package root is therefore visible package-wide (every module descends from the root); a private item in mod M is visible to M and M’s submodules, but not to the root or to sibling modules. This governs the privacy check only — name resolution is unchanged: a descendant still names an ancestor’s item through pkg::/super::/use (there is no bare-name inheritance from a parent module). pub exposes to dependents; pub(pkg) limits to the package.

Imports

use      ::= 'use' use-tree ';'
use-tree ::= path ('as' Ident)?
          |  path '::' '*'
          |  path '::' '{' use-tree (',' use-tree)* ','? '}'
path     ::= Ident ('::' Ident)*

Rust-style: single-symbol (use std::math::Nat;), brace-list (use std::math::{Nat, Int};), glob (use ufo_foundational::prelude::*; — a third-party vocabulary package), and aliased (use foo::bar::Sym as Other;) forms.

A plain use is a private import — visible only inside the importing module. A pub use re-exports: the imported items join this module’s public surface and are visible transitively to dependents, which is how a package prelude works (pub use pkg::prelude::*).

Re-exports resolve, including renamed. A single-item use M::X where X is re-exported by M (rather than declared there) resolves, and so does a renamed re-export pub use M::X as Y. A renamed re-export is reachable only under the alias Y — the original name X is not brought into scope through it (the same rule a renamed use … as follows). Import-resolution limit. One form parses but does not resolve: a capitalized Self:: type path (lowercase self:: works).

Glob-import shadowing follows the Rust convention. A glob import (use m::*) is the lowest-priority binding: an explicit import (use m::X) and a same-module declaration both silently shadow a glob-imported name of the same spelling — no diagnostic, and the choice does not depend on import order. Two glob imports that bring the same name from different items are ambiguous — using that name is refused (an unused ambiguous name is not an error); import the intended item explicitly, or qualify the reference, to disambiguate. Two globs that resolve to the same item (for example one module re-exporting the other’s) are not a conflict.

The prelude is a package feature, not a compiler default (RFD 0038). A package’s [package].prelude (an array of use-tails in ox.toml) is auto-prepended to every module of that package; it is empty by default and carries no vocabulary. type/rel are not in it unless the package opts them in (prelude = ["std::core::{type, rel}"], or prelude = ["pkg::prelude::*"] pointing at a prelude.ar of pub use re-exports). A module opts out with #![no_implicit_prelude]. There is no auto-imported std::prelude; what is always in scope is the language substrate (step 3 below), which is not a library prelude.

Manifest

ox.toml, Cargo-flavored:

[package]
name = "lease-story"
version = "0.1.0"
edition = 0
# Optional package entry override. Without this, the default search prefers the
# Cargo-style `src/root.ar` and falls back to the flat package root `root.ar`.
entry = "root.ar"

[dependencies]
# PATH dependencies (RFD 0030). The key is the path root the
# consumer uses (`use ufo::endurant::Object;`) and must equal the dependency
# package's `[package].name`.
ufo = { path = "../ufo" }

[lattice]
# Decidability-tier ceiling (Standpoints and modal operators). A declaration whose classified tier exceeds
# this ladder name is refused at `ox check` / `ox build` (OE1230, RFD 0030 D6).
max_tier = "recursive"

[standpoints]
# optional package-boundary declarations

[schema]
# Optional source root for generated or nested package layouts. Entry paths are
# resolved relative to this root when the nested entry exists.
root = "src"

Tooling resolves a package directory entry in this order: [project].entry, [project].main, [package].main, [package].entry, then the conventional defaults. With no explicit entry, the default search prefers the Cargo-style src/ layout and falls back to the flat package root (so existing packages keep resolving): both [project] and [package] try src/root.ar then root.ar. The first that exists wins, and its directory becomes the source root — a package laid out as src/root.ar roots all its .ar sources under src/ with no config (ox new/ox init scaffold exactly this). An explicit [schema].root overrides the source root. When no entry is found, the error names every path it searched.

Dependencies (RFD 0030). Only dep = { path = "…" } resolves: each path dependency’s package is loaded and its pub surface folded into the consumer’s workspace under the dependency name as a path root (see Name resolution). The registry/VCS surface — a bare version requirement (ufo = "1.0") or the version/git/branch/tag/rev/registry keys — is recognized and refused with OE1240 (Out of scope), never silently ignored. The dependency name must equal the dependency’s published [package].name (OE1241 otherwise); a dependency cycle is OE1242; the same name resolving to two different directories is OE1243. There is no ox.lock for a path-only graph (path deps are unlocked, Cargo precedent); ox.lock is reserved for the registry/git graph. Manifest honesty (RFD 0030 D6): an unrecognized section or key surfaces a Cargo-style OW1240 “unused manifest key” warning rather than being silently dropped, and [lattice].max_tier is enforced against the Standpoints and modal operators classifier (OE1230).

Name resolution

Resolution of a bare identifier proceeds in order:

1. Local scope. Definitions in the current module, including the lexical chain of enclosing mod bodies and impl blocks.
2. Imports + package prelude. Items brought into scope by use in the current module, and — unless #![no_implicit_prelude] is set — the package’s prelude ([package].prelude, auto-prepended uses; RFD 0038). The prelude is empty by default and carries no vocabulary.
3. Substrate. The fixed, always-in-scope language primitives — not a library, and not opt-outable: the primordial types (Nat, Int, Real, Decimal, Money, Date, Time, DateTime, Duration, Bool, String, Top, Bot) and the builtin type forms (Option, Result, Ordering, List, Set, Map, Range, Truth4, Truth4Of, Diagnostic, Severity, …).

A qualified identifier (containing ::) is resolved by walking the path. The leading segment selects a root:

• pkg — the current package’s root. This is the sole self-reference anchor: a package never refers to itself by its own name, so internal paths survive a package rename. pkg::a::b::X names item X in module a::b of this package. (Argon has packages, not crates — there is no crate keyword.)
• self — the current module; super — the parent module (repeatable: super::super::X).
• A dependency package name declared in [dependencies] — e.g. ufo::endurant::Object (a path-dependency vocabulary package, RFD 0030). The dependency’s pub surface is folded into this workspace under its name as a path root; ufo::X and use ufo::X; resolve into it. The stdlib root std is always available (std::math::Nat).
• Otherwise the leading segment resolves against the scope chain — a submodule of the current module, or a name brought in by use.

Subsequent segments resolve within the preceding module’s namespace. An item therefore has a single absolute name viewed from outside the package (mypkg::a::b::X); viewed from inside, the equivalent absolute form is pkg::a::b::X.

Contextual introducer identifiers (type, or vocabulary names like kind, role, phase, …) are ordinary identifiers — recognized by an IDENT IDENT shape at declaration position and resolved via the algorithm above against the pub metatype (concepts) / pub metarel (relations) declarations visible in scope: declared in this package, or imported from a vocabulary package (across a [dependencies] path-dependency boundary, RFD 0030). Nothing is ambient here — not even type/rel: a package brings the no-commitment baseline into scope explicitly, via use std::core::{type, rel} or its [package].prelude (RFD 0038), exactly as it brings any vocabulary (appendix A). The compiler emits OE0101 UnresolvedName for general failures, and OE0605 UnknownMetatype / OE0606 UnknownMetarel specifically when a leading identifier at declaration position fails to resolve — at ox check and ox build; no artifact is emitted. A use statement that does not resolve is itself refused with OE0103 UnresolvedUseImport (with a did-you-mean over the visible namespace, RFD 0030 D5) — a broken import is never silently accepted.

Module extraction (tree-shaking)

When a module imports another, the elaborator extracts a ⊥-locality module (Cuenca-Grau–Horrocks–Kazakov–Sattler 2008): the smallest subset of the imported module’s axioms that stays non-trivial once every concept outside the used signature is reinterpreted as ⊥. Extraction is a fixpoint, linear-time per iteration, terminating in at most |B| iterations.

The guarantee is Σ-scoped conservativity: every entailment about the used signature survives extraction. Argon strengthens the classical result for its own semantics — closed-world conclusions are preserved (CWA-conservativity), ghost individuals reachable only through non-Σ concepts are pulled in (domain-conservative extraction), defeasible rules drag in their defeaters (defeat-aware extraction — a classical extractor is unsound under non-monotonic semantics, Bonatti-Faella-Petrova-Sauro 2022), and extraction composes safely across an import chain. All are mechanized at spec/lean/Argon/Locality/.

Extraction is how the substrate composes decidability tiers across heterogeneous modules (Tier ladder): each extracted module is classified independently, and conservativity guarantees no entailment is lost. Failures emit OE0710 (conservativity cannot be proven under the importer’s world assumption) or OE0711 (defeat-aware extraction cannot close the defeat graph).

Meta-calculus atom

Three declarations: metaxis, metatype, metarel. They make the language ontology-neutral by letting packages declare the concept-introducing keywords.

metaxis

metaxis-decl ::= 'metaxis' Ident 'for' target metaxis-body? ';'
target       ::= 'metatype' | 'metarel' | 'individual' | 'macro' | '[' target (',' …)* ']'
metaxis-body ::= '{' enum-body '}' | '=' TypeExpr ('where' refinement)?
enum-body    ::= Ident (',' Ident)*          // unordered
              |  Ident ('<' Ident)+          // totally ordered (chain)

pub metaxis rigidity for metatype { anti_rigid < semi_rigid < rigid };
pub metaxis sortality for metatype { sortal, non_sortal };
pub metaxis identity_provision for metatype { provides, inherits };
pub metaxis dependency_kind for metarel { existential, contingent, none };
pub metaxis ordinality for metatype = Nat;
pub metaxis weight for metatype = Real where _ > 0.0;

A metaxis characterizes the meta level: its values are assigned to metatypes (for metatype) and metarels (for metarel), never to a concrete type directly. The targets name the meta-sort the axis applies to — metatype for the concept tier, metarel for the relation tier — not the type / rel concept introducers. (A future for <DeclaredType> target — a type-specific refinement axis bound to one declared type — is left open by the model but not yet specified.)

Cross-axis constraints are check rules at module level, never embedded in the body.

metatype

metatype-decl ::= 'abstract'? 'fixed'? 'metatype' Ident '=' '{' axis-assign (',' …)* ','? '}' ';'
axis-assign   ::= Ident ':' value
value         ::= Ident | literal

A metatype body is a record of axis values, so each binding reads like a struct field — a single : separates the axis from its value.

pub abstract fixed metatype category = { rigidity: rigid,      sortality: non_sortal };
pub fixed metatype kind     = { rigidity: rigid,      sortality: sortal,     identity_provision: provides };
pub fixed metatype subkind  = { rigidity: rigid,      sortality: sortal,     identity_provision: inherits };
pub metatype role           = { rigidity: anti_rigid, sortality: sortal };
pub metatype phase          = { rigidity: anti_rigid, sortality: sortal };

A metatype name in scope is contextually a concept-introducing keyword: pub kind Person { … }.

Axes are pure user vocabulary. The axis bindings in a metatype body are the declaring package’s own ontology — validated against the declared metaxis domains (RFD 0027 D2), persisted on the wire, and queryable — but the compiler never reads an axis name. No axis assignment changes elaboration, coverage, or mutation semantics; importing a vocabulary cannot alter substrate behavior because its author happened to name an axis rigidity. The metatypes shown above (kind, subkind, role, phase, category) are example declarations of the kind a third-party UFO vocabulary package would ship — they are not language atoms, and no UFO vocabulary ships with Argon or its stdlib. Other vocabularies (BFO, GFO, custom) define their own metatypes with their own axis assignments; the language treats all of them uniformly.

Substrate behavior comes from two ontology-neutral modifiers (RFD 0027 D6) — the operational shadows of the classic meta-property distinctions, with PL precedents rather than ontological commitments:

• abstract — no direct instances. Every type the metatype introduces refuses construction (insert T { … }), direct classification (insert iof(x, T)), and seeded assertion (positive pub fact T(x)) with OE0233; subtypes are unaffected, and pub not_fact T(x) (refuting membership) stays legal. Abstract types are exempt from trait impl-coverage obligations (Resolution) — they structure the hierarchy, and every individual is classified through some non-abstract subtype. abstract may also be declared per-type on a concept declaration (pub abstract type Vehicle { … }, the UML/PL convention); a type introduced by an abstract metatype is abstract with no override semantics.
• fixed — classification decided at construction. insert iof / delete iof against a type introduced by a fixed metatype refuses with OE0234 (mutate); construction itself is unaffected. Dynamic classification is the default — the restriction is the opt-in, the same posture as check. Fixed classification is what makes static modal discharge sound (Modal operators); the Kripke-semantics justification (rigid designation = fixed classification) is mechanized in Argon.Reasoning.StaticDischarge and the mutation-gate theorem in Argon.Runtime.ModifierGates.

A vocabulary author writes both layers together — pub abstract fixed metatype category = { sortality: non_sortal, rigidity: rigid }; — the modifiers carry the behavior, the bindings carry the package’s ontology. Misplaced modifiers (fixed on a concept declaration, either modifier on a struct/enum/relation, duplicates) are refused at parse with OE0008.

metarel

metarel-decl  ::= 'metarel' Ident '(' endpoint-list ')' metarel-body? ';'
endpoint-list ::= endpoint (',' endpoint)*
endpoint      ::= (Ident ':')? Ident          // optional name, then metatype name
metarel-body  ::= '{' axis-assign (',' …)* ','? '}'

pub metarel mediation(mediator: relator, mediated: kind) {
    dependency_kind: existential,
};

pub metarel material(kind, kind) { dependency_kind: contingent };
pub metarel three_way_dependence(kind, kind, kind);

The metarel name is itself a contextual relation-introducing keyword (Relations): pub mediation Involves(m: Marriage, p: Person) declares a relation classified by mediation. The elaborator verifies the relation’s endpoint metatypes match the metarel’s positions. (An alternative decorator-attachment spelling — #[mediation] on a generic relation declaration — was sketched in earlier drafts but is not built: user-declared metarel names are not compiler directives, so the attribute form refuses at the directive registry, OE0705. The introducer form above is the supported surface.)

The stdlib ships a generic metarel for ontology-uncommitted use:

// in std::core — the generic metarel (opt-in via `use std::core::rel`,
// RFD 0038), shown as it is declared inside the stdlib (not a user file).
pub metarel rel<E1: metatype, E2: metatype>(E1, E2);

rel accepts any endpoint metatypes (inferred from the relation’s parameter types). After use std::core::rel;, the modeler can write pub rel ParentOf(parent: Person, child: Person) [1..1] [0..*] for relations without committing to a specific ontological vocabulary. Vocabulary packages may re-export std::core::rel in their prelude as a convenience.

Reflection

Reflective sorts: Entity, TypeRef, Metatype

The substrate exposes three reflective sorts and a fixed lattice over them:

Metatype  <:  TypeRef  <:  Entity

• Entity is the universal sort of all entities — individuals and type-references alike. A type is an entity (so it can itself be classified by a higher-order type; see Higher-order modeling). Entity <: Top.
• TypeRef is the sort whose values are references to declared types (concept / construct / relation / metatype) — a handle into the closed, nominal catalog of declarations, in the manner of OWL-2 punning, Java’s Class<?>, or Haskell’s TypeRep. TypeRef is unsealed, so Metatype remains the only sealed primitive. Because TypeRef denotes a closed catalog of already-declared types rather than an impredicative universe, there is no Type : Type: the reflective layer is a predicative, stratified universe of codes, not a self-membership hierarchy.
• Metatype is the sealed primitive that classifies all metatypes (kind, role, phase, …, and Metatype itself). Since Metatype <: TypeRef, every metatype name in scope is also a TypeRef value.

Type-as-value. A declared type’s name in value position is a TypeRef value — Person, kind, and Metatype are all TypeRef values, distinguished from the type Person by syntactic position. This is the substrate’s type-as-value facility: a field or parameter may be typed TypeRef (or the bounded TypeRef<C>; see Built-in type forms) and carry a reference to a declared type. The runtime carrier is the declared-symbol reference Value::Name; on the wire, a TypeRef/Entity argument is a qualified class-path ("pkg::mod::Type", or {"$typeRef": "pkg::mod::Type"}) resolved to the declared type’s identity — entity refs (#i…) are not accepted for these parameters. See RFD 0023.

Reflection intrinsics

The substrate provides five reflection intrinsics — meta, iof, specializes, extent, and implements (RFD 0026; signature implements(t: TypeRef, tr: TraitRef) -> Bool, materialized as the catalog-closed $implements relation with supertrait closure and <: upward target-coverage, Reflective conformance: TraitRef and implements) — admitted in any rule body without a use declaration. The first three have syntactic-sugar atom forms in Rule-atom grammar; extent and implements are called directly. For meta/iof/specializes/extent, each type-position argument is a TypeRef value — a literal type-reference or a bound variable of sort TypeRef — which is precisely what makes the intrinsics first-class, value-polymorphic predicates: library code can pass, count over, or quantify across type-values (see Higher-order modeling and the unprivileged mlt package, realizing the spec/research/RP-003-mlt-as-library.md GAP-1). implements differs in two deliberate ways: its second argument is TraitRef-sorted (traits are not types and stay off the <: lattice), and because $implements is a finite catalog-closed relation, both of its positions may be free — enumeration is the intended use (Reflective conformance: TraitRef and implements).

meta has the signature meta(x: Entity) -> TypeRef: it returns the immediate classifier of x — its <:-minimal declared type — as a TypeRef value. Under multiple classification (an entity instantiating incomparable types, e.g. a UFO individual that is both a Person and a Customer with neither <: the other), meta(x) is multi-valued: it yields one TypeRef per <:-minimal classifier. (It is a Metatype value only when x is itself a type — e.g. meta(kind) == Metatype — since Metatype <: TypeRef.) x :: T is syntactic sugar for meta(x) == T.

meta() applies only to ontologically-classified concepts (those declared under a vocabulary or stdlib metatype). Calling meta() on a struct/enum-declared value is a category error — language-level data carries no metatype — and emits a diagnostic at elaboration.

Worked examples (each right-hand side is a TypeRef value): meta(Person) == type when Person is pub type Person { … } under std::core::type; meta(Person) == kind when Person is pub kind Person { … } under an imported (or locally-declared) UFO vocabulary; meta(kind) == Metatype; meta(Metatype) == Metatype (sealed self-instantiation). Metatype is the sealed primitive that classifies all metatypes; it is special-cased by the compiler. The classifier kind and the primitive Metatype are TypeRef values because Metatype <: TypeRef.

iof has the signature iof(x: Entity, t: TypeRef) -> Bool. The rule-atom form x : T (Rule-atom grammar type test) is syntactic sugar for iof(x, T). Because the type-position argument t is a TypeRef value, iof is a first-class predicate: it can be passed as a relation argument, counted over, or quantified across — for example, library code building higher-order theories (the unprivileged mlt package, Higher-order modeling, Stdlib (selected)) treats iof as a first-class predicate.

iof is read at two tiers. The individual/ABox tier is membership of an order-0 entity in a type, asserted by a pub fact T(x) ground atom. The catalog/type tier is a declared type×type membership — a type X declared an instance of a higher-order type T via the : T instantiation clause (Vocabulary concepts and the generic type metatype, pub kind USD : Currency). The subject x is itself a TypeRef value (a type used as a higher-order individual), so the same iof relation carries both; which tier a read sits in is decided by whether the subject is an individual or a type, not by a separate relation. The catalog tier is declaration-derived (never an ABox event), so a #[static] check (Rule atom — fn, derive, query, mutate, check) may read it and extent projects it at the type level.

specializes has the signature specializes(t1: TypeRef, t2: TypeRef) -> Bool. The rule-atom form t1 <: t2 (Rule-atom grammar specialization) is syntactic sugar for specializes(t1, t2). Same first-class, value-polymorphic motivation as iof — both arguments are TypeRef values.

iof and specializes apply only to ontologically-classified concepts. Calling them on struct/enum-declared values is a category error and emits a diagnostic at elaboration, parallel to the meta() discipline.

extent has the signature extent(t: TypeRef) -> Set<Entity> (t is a TypeRef value naming the type whose extent is enumerated). Returns the set of entities x such that iof(x, t) holds at the current state. Both function-style (extent(EmperorPenguin)) and UFCS method-style (EmperorPenguin.extent()) are admitted; the method form lowers to the function form.

Worked examples: extent(Person) returns all order-0 entities classified as Person; extent(BirdSpecies) returns all order-1 kinds that are iof-instances of BirdSpecies (e.g., {EmperorPenguin, GoldenEagle, Grouse, Pheasant}); extent(Metatype) returns the set of all metatypes in scope. extent() on a struct/enum-declared value is a category error, parallel to the other reflection intrinsics.

Relation-signature reflection (rel / arm). Two further reflection predicates reflect over declared relations (the relation tier of the reflective catalog, RFD 0031 D2), so a vocabulary package can write relation-level compile-time constraints:

• rel(r: TypeRef, m: TypeRef) -> Bool — r is a declared relation and m its classifying metarel. One catalog row per declared relation.
• arm(r: TypeRef, pos: Int, t: TypeRef) -> Bool — for relation r, pos is a 0-based arm position and t the endpoint type declared there. One row per (relation, position).

Both are catalog-closed (one row per declared relation / arm, never the ABox), so — like $implements — every position may be free and enumeration is the intended use. Since meta is polymorphic over the relation tier, meta(r) == <metarel> is an admitted equivalent spelling of the rel(r, <metarel>) membership test — the two bind against mirrored catalog rows; rel/arm remain the surface for arm-level (endpoint) reflection. rel/arm are abstract reflection primitives, never ontological vocabulary; the metarel/type names a check matches on are user vocabulary, compared by catalog identity. A package-shipped check quantifies over the catalog to enforce an endpoint discipline:

// "an endpoint of a `characterization` relation must be aspect-sorted"
pub check BadCharacterization(r: TypeRef, t: TypeRef) :-
    rel(r, characterization), arm(r, 1, t), meta(t) == kind
    => Diagnostic { severity: Severity::Warning, code: "UFO::W010", message: "..." };

(The metarel introducer itself also verifies its endpoint metatypes at elaboration — metarel, OE0631; $rel/$arm let a package extend or audit that discipline declaratively.)

Lowering. A declared type in value position lowers to the IR primitive Term::TypeRef. This lowering is position-uniform across the surface: rule bodies and imperative bodies (mutate / test / fn) coerce identically, so a relation with a TypeRef-typed endpoint is writable in-language (insert Regards(k, Person)), over the wire ({ "$typeRef": "pkg::mod::Person" }), and readable back through equality dispatch (t == Person) — all three carry the declared symbol reference Value::Name. Binders shadow the coercion (a parameter / let named like a declared type is the local value); the landing is sorted — OE0262 refuses a type-as-value pinned into a variable-expecting rule slot, OE1384 the mutate-body analogue (an entity-declared endpoint or field). iof(x,t) (and x : t) lowers to the Core-IR typeTest atom and meta(x) == T (and x :: T) to the metaEq atom (spec/lean/Argon/CoreIR/RuleIR.lean); specializes(t1,t2)/t1 <: t2 has no dedicated atom and lowers to a reserved-head predicate, and extent(t) to an application of the extent builtin. Beneath Core IR, the reasoner evaluates these against catalog relations it materializes from the declarations — $iof (entity × type, closed under supertypes; this carries both tiers — the individual-tier rows from pub fact T(x) assertions and the catalog-tier type×type rows from each : T instantiation clause, the latter closed upward over the target type’s <: ancestors), $specializes (the reflexive-transitive specialization graph plus the built-in Metatype <: TypeRef <: Entity edges and the sibling TraitRef <: Entity edge; declared relations are first-class nodes of this graph, so $specializes carries the relation tier too — relation × relation rows from each pub rel R(...) <: S edge, closed reflexive-transitively, so specializes(R, S) binds R over the S family and specializes(X, X) holds for every declared relation X — the mechanism the relation-value application selector rests on), $meta (entity × its <:-minimal classifiers, PLUS the relation tier: relation × its declared metarel — meta is polymorphic over relations exactly as over types, so meta(relation) == <metarel> binds and fires against these rows), $implements (type × trait, supertrait closure and <: upward target-coverage folded in — Reflective conformance: TraitRef and implements), and the relation-tier $rel (relation × metarel) / $arm (relation × position × endpoint type) — RFD 0031 D2. OE0212 MetaArgUnbound is the reserved refusal for an unbound argument of the four type-position intrinsics; implements is exempt by design — both of its positions enumerate over the catalog-closed $implements relation, which is the intended use.

Typical use: deriving cross-level properties of higher-order types from their instances.

#[categorizes(Bird)]
pub type BirdSpecies {
    numberOfLivingInstances: Int = extent(self).count(),
    averageHeight: Decimal = extent(self).map(|b| b.height).avg(),
}

The = expr field-default form shown above refuses with OE0237 FieldDefaultUnsupported (see struct and enum — language built-ins (data declarations) for the full disposition). Express cross-level derivations such as EmperorPenguin.numberOfLivingInstances with the from-navigation field form ([RFD 0005, struct and enum field navigation](constructs/struct-and-enum.md)) or an explicit derive/query rule (Rule atom — fn, derive, query, mutate, check).

Constructs atom

Concepts and relations are co-equal first-class entities. The construct atom is layered:

• Language built-ins (lexer-level, always available): struct and enum — pure data declarations with no ontological commitment, no metatype classification, structural equality.
• Stdlib ontological constructors (opt-in, not ambient — brought into scope via use std::core::{type, rel} or a [package].prelude entry, RFD 0038): the generic metatype type introduces ontologically-classified node-concepts (pub type Foo { … }); the generic metarel rel introduces ontologically-classified relations (pub rel R(...)). They are the no-commitment baseline, imported like any vocabulary — nothing is ambient.
• Vocabulary classifiers (require a pub metatype / pub metarel declaration in scope — declared in this package, or imported from an external vocabulary package): metatypes like UFO’s kind, role, phase, category and metarels like mediation, material for richer ontological commitment. No vocabulary ships with the language or the stdlib — a vocabulary is an ordinary external package (e.g. a UFO package authored by the UFO authors), and an introducer that resolves to no visible declaration is refused with OE0605 / OE0606.

All four layers compile to one substrate IR. The distinction lives in the metatype/metarel calculus (Meta-calculus atom); the language itself ships only the calculus, the data-declaration shorthands, and the meta-declaration keywords.

struct and enum — language built-ins (data declarations)

struct-decl ::= attribute* 'pub'? 'struct' Ident generic-params? where-clause? '{' field-list '}'
enum-decl   ::= attribute* 'pub'? 'enum'   Ident generic-params? where-clause?
                  '{' variant (',' …)* ','? '}'
field-list  ::= field-decl (',' …)* ','?
field-decl  ::= attribute* 'mut'? Ident ':' TypeExpr ('=' expr)? ('from' relation-ref)?
variant     ::= Ident ( '(' TypeExpr (',' …)* ')' | '{' field-list '}' )?

pub struct Diagnostic {
    severity: Severity,
    code:     String,
    message:  String,
    range:    Option<Range>,
}

pub enum Severity { Error, Warning, Info, Hint }
pub enum Option<T> { Some(T), None }
pub enum Result<T, E> { Ok(T), Err(E) }
pub enum Shape { Circle, Square, Triangle }

One enum spelling. enum has a single declaration form — the brace list above — matching Rust and the only form that carries payloads. An earlier enum Name = A | B | C pipe spelling is removed (OE0009). Concept cover declarations (Vocabulary concepts and the generic type metatype) take the matching brace form pub kind Name { A, B } (OE0012 on the old = A | B pipe), so no =-pipe surface survives.

struct/enum declarations carry no metatype classification. They are language-level data shapes — structural equality, no fact-store identity beyond storage, no participation in the metatype calculus. They cover stdlib data records (Diagnostic, Severity, Option, Result, Path, Range, Truth4) and user plumbing types. meta() reflection (Reflection) does not apply.

Struct and enum values

A struct value is constructed by naming the type and giving every field: Row { a: 1, b: 2 }. This is an ordinary expression — it can be a let binding, a field value, a function argument, a return value, a list element, or either side of a comparison. The full construction and projection grammar lives in the expression grammar (Expression grammar); this section states the data semantics.

pub struct Point { x: Int, y: Int }

pub fn origin() -> Point = Point { x: 0, y: 0 };
pub fn project_x(p: Point) -> Int = p.x;

Structural equality. Two struct values are equal when their fields are equal, field by field — there is no identity to compare. Field order in the literal does not matter: Row { a: 1, b: 2 } and Row { b: 2, a: 1 } are the same value. Equality is recursive: a struct whose field is itself a struct compares that field structurally too. This is what “pure data” means concretely — a struct is its fields, nothing more.

pub struct Row { a: Int, b: Int }

test "structural equality is field-wise and order-independent" {
    assert Row { a: 1, b: 2 } == Row { b: 2, a: 1 };
    assert Row { a: 1, b: 2 } != Row { a: 1, b: 3 };
}

Immutability. A struct value is immutable: its fields are fixed at construction and never change. There is no in-place update. To produce a struct that differs from an existing one in a few fields, use functional update — the ..base spread — which yields a new value and leaves the base untouched (Expression grammar):

pub struct Row { a: Int, b: Int }

test "spread is a functional update yielding a new value" {
    let base = Row { a: 1, b: 2 };
    assert Row { ..base, a: 9 } == Row { a: 9, b: 2 };   // a overridden, b carried
    assert base == Row { a: 1, b: 2 };                   // base is unchanged
}

Because a struct value is immutable, mut on a struct field is meaningless and is refused — mut field: Type on a struct raises OE0253 MutOnStructField. The mut modifier marks a concept field updatable by an update … set { … } statement inside a mutate body (mutate); that notion belongs to identity-bearing concept individuals, not to value-semantic data.

pub struct Point { mut x: Int, y: Int }

No identity — insert is refused. insert T { … } mints an identity and records an iof classification; it is how concept individuals are born. A struct has no metatype and no identity, so insert on a struct type is refused — OE0252 InsertOfStruct. Construct the struct as a plain value instead (drop the insert). The inverse direction is refused too: a brace literal T { … } whose head names a concept is OE0264 StructLitConceptHead (construct the individual with insert T { … } in a mutate/test body, or declare T a struct for plain data), and an insert written inside a pure fn body is OE0265 FnBodyInsert (construct in a mutate/test body and pass the value in).

pub struct Point { x: Int, y: Int }

pub mutate make() {
    let p = insert Point { x: 1, y: 2 };
}

A struct literal must state every field exactly. A missing field is OE0249 StructFieldMissing, an undeclared field is OE0250 StructFieldExtra, and a field given the wrong type is OE0251 StructFieldTypeMismatch. These are build-time refusals, named to the field, not deferred to runtime.

Enum values. A payloadless variant is written as a path: Severity::Error, Shape::Circle. A payload variant carries one value and is constructed by applying the variant to that value: Msg::Text("hi"). Enum values compare structurally, the same as structs — Msg::Text("hi") == Msg::Text("hi"), and a payload variant never equals a different variant. A payload variant takes exactly one value; any other count is OE0256 EnumPayloadArity.

pub enum Msg { Text(String), Empty }
pub struct Mail { body: Msg }

pub fn greeting() -> Mail = Mail { body: Msg::Text("hi") };
pub fn blank()    -> Mail = Mail { body: Msg::Empty };

User-concept generics are decorative. A user-declared generic enum Opt<T> (or struct) parses, but its type parameters reach no storage slot, so applying it — Opt<Int> — is refused (OE0235). The optional and result shapes used in practice are the library generics Option<T> / Result<T, E> and the optional-field form T?, whose argument shapes the elaborator does interpret. Payload binding for the optional form is the rule-body is Some(a) / is None test (next paragraph) or a value-position match expression (let v = match opt { Some(x) => x, None => d };, below); a payload-binding arm in statement position refuses with OE1319.

Reading an enum payload — is Some(a). Inside a rule body, an optional field’s payload binds with the membership test path is Some(binder), and absence tests with path is None. A present field materializes one row binding the payload; an absent field materializes none, so the surrounding conjunction fails (RFD 0007 Rule-atom grammar):

pub type Person { mut age: Int? }

pub derive Adult(p, a)   :- p: Person, p.age is Some(a), a >= 18;
pub derive HasNoAge(p)   :- p: Person, p.age is None;

Reading an enum payload — value-position match. A match expression in value position — a let right-hand side, a comparison operand, a fn body, a return/require value — binds an enum payload and evaluates. let r = match opt { Some(x) => x, None => 0 }; reads the payload into x and yields the selected arm’s value; this is the idiomatic way to read or consume an enum value. The arm binds exactly one variable positionally; a zero-, multi-, or record-binder arm is OE0257 EnumPayloadPattern (Expression grammar).

pub enum Opt { Some(Int), None }

test "value-position match binds the payload and evaluates" {
    let some = Opt::Some(7);
    let none = Opt::None;
    assert (match some { Opt::Some(x) => x, Opt::None => 0 })  == 7;
    assert (match none { Opt::Some(x) => x, Opt::None => 99 }) == 99;
}

A payload-binding arm in statement position — an effectful arm body inside a mutate statement-match, e.g. match opt { Some(v) => { let _ = insert T { n: v }; }, None => {} } — refuses with OE1319 rather than silently mis-evaluating. Bind the payload in value position (let v = match opt { … };) first, then run the effect. The rule-body is Some(a) form above is the other supported reader; the constant-pattern subset of match (payloadless variants, literals, _) executes in both positions (Pattern matching).

Field defaults. The field-default form field: Type = expr refuses with OE0237 FieldDefaultUnsupported: the parser recognizes the = expr clause and rejects it loudly rather than silently dropping the default. Supply the value at the construction or kind-level binding site, or use the from-navigation form (next paragraph) for a derived value.

Field navigation views — from. Unaffected by the above: a field may carry a from Rel.endpoint navigation-view clause supplying a derived value (RFD 0005, relation subsumption). This form is parsed and elaborated normally; it is the supported way to compute a field’s value from related entities.

Field mutability — mut. A field declaration may carry the mut modifier between any leading attributes and the field name: mut field: Type. Without mut, the field is immutable post-construction — its value is fixed at the construction site (or by #[intrinsic] kind-level binding, or by from-clause derivation) and may not subsequently be re-assigned. With mut, the field admits update-stmt writes inside mutate bodies (mutate).

pub type Person {
    name: String,                          // set at construction; not updatable
    dob: Date,                             // set at construction; not updatable
    #[intrinsic] ssn: String,              // must be set at kind binding; not updatable
    mut current_address: String,           // updatable via `update`-stmt
    mut current_employer: Company?,
    #[intrinsic] mut current_role: Role,   // required at construction AND updatable later
}

mut is orthogonal to the other field-decl modifiers: #[intrinsic] governs construction-time required-ness, not updatability (both can apply); a mut on a from-derived field is contradictory and rejected with OE0822 MutOnDerivedField; a default = expr supplies a fallback at construction; the metatype’s fixed modifier (metatype, mutate) governs whether iof classification can change, not whether fields can, so a fixed kind admits mut fields. The modifier reads identically on struct, enum-variant, and vocabulary-concept fields. Mutations lower to append-only retract/assert event pairs on the axiom log (Storage layer); the proposition’s (entity_id, property_id) identity is stable across edits, so bitemporal queries reconstruct prior values (Temporal substrate).

Vocabulary concepts and the generic type metatype

When a vocabulary metatype is in scope, its name introduces a concept:

// A declaration is terminated by exactly ONE of: its `{ }` body, its `{ }`
// cover, or — when it has NEITHER — a REQUIRED ';' (the same item-termination
// rule as Rust: `struct Foo;` vs `struct Foo { … }`). A missing terminator on
// the bodyless form is `OE0011 MissingTerminator`.
concept-decl    ::= attribute* 'pub'? <metatype-name> Ident generic-params?
                     supertype? refinement-clause? ( cover | body | ';' )
supertype       ::= specialization? instantiation?
specialization  ::= '<:' TypeExpr (',' TypeExpr)*
instantiation   ::= ':' TypeExpr (',' TypeExpr)*
cover           ::= '{' variant (',' variant)* ','? '}' // bare-ident members; self-terminating
body            ::= '{' (field-decl | instance-value) (',' …)* ','? '}'   // self-terminating — no ';'
instance-value  ::= Ident '=' expr                     // see body modes below

A cover and a field/instance body share the { … } surface; the member shape distinguishes them. A cover’s members are bare concept names (a brace whose first entry is an Ident followed by , or }), matching enum’s { Circle, Square } and the complete Parent { A, B } group axiom; a body’s first entry carries a : (a field name: Type), :: (a per-target axis override), or = (an instance-value).

The leading identifier (type, or a vocabulary name like kind, subkind, role, phase, category, …) is contextually a concept-introducing keyword — resolved per Name resolution against the pub metatype declarations visible in scope: declared in this package, or imported from a vocabulary package. type is not ambient — it is the std::core baseline, brought into scope by use std::core::{type} or a [package].prelude entry (RFD 0038). An introducer that resolves to no visible pub metatype is refused with OE0605 UnknownMetatype at ox check and ox build.

use std::core::{type};   // the no-commitment baseline, brought into scope (RFD 0038)
pub type Document { title: String, body: String }

// Vocabulary-classified concepts: the vocabulary must be IN SCOPE.
// Here it is declared in-package (the external-vocabulary-package
// pattern — a real UFO package would ship these declarations and be
// imported instead; nothing UFO-related ships with Argon):
pub metatype kind = { };
pub metatype subkind = { };
pub metatype category = { };

pub kind Person { name: String, age: Nat }
pub subkind Adult <: Person iff { self.age >= 18 };   // defined class: auto-classified (Refinement)
pub category Animal;

pub kind Vehicle;
pub subkind Car         <: Vehicle { license_plate: String }
pub subkind Truck       <: Vehicle { license_plate: String, cargo_kg: Nat }
pub subkind Motorcycle  <: Vehicle { license_plate: String, weight: Real }

A concept cover body (pub kind Vehicle { Car, Truck, Motorcycle }) is parsed but its subkind-threading semantics are not yet implemented — an unconsumed cover refuses loudly rather than silently asserting nothing. Declare the subkinds explicitly (as above), adding a partition/complete group axiom for the covering constraint; the cover form is tracked to do this in one stroke.

pub metatype kind = { };
pub kind Car; pub kind Truck; pub kind Motorcycle;
pub kind Vehicle { Car, Truck, Motorcycle }

Supertype clauses. <: T declares specialization (intra-classification subtyping): Adult <: Person says every adult is a person. : T declares iof-instantiation: pub kind USD : Currency says USD is an instance of the higher-order type Currency. Both clauses are general substrate features — neither commits to any specific higher-order theory. Higher-order theories like MLT (the unprivileged mlt package, Higher-order modeling, Stdlib (selected)) interpret the order arithmetic over :; the substrate itself only enforces that iof is well-founded and acyclic.

Multiple parents on either axis. Both clauses admit a comma-separated list, and both can co-occur on a single declaration:

pub subkind Penguin
    <: FlyingAnimal, AquaticAnimal              // specializes two kinds at order n
    :  Vertebrate_Species, Endangered_Species   // instance of two categories at order n+1
{
    name: String,
    body_plan   = "tetrapod",
    iucn_status = IucnStatus::Vulnerable,
}

When both clauses are present the canonical order is <: then :, mirroring the order arithmetic (specialization parents at the concept’s own order, instantiation parents one above). The order is a style convention, not a rule: both clauses are independent (parents are an unordered set on each axis), so either source order parses and means the same thing — writing : before <: is accepted with the OW0010 style warning (never an error), and oxfmt normalizes it to the canonical order. All parents in a single <: clause must be at the same order; all parents in a single : clause must be at one order above. Unprivileged theory packages (e.g. mlt) enforce additional cross-parent constraints over the iof DAG.

Diamond resolution. When multiple parents (on either axis) declare a field with the same name, the elaborator rejects the declaration with OE0208 AmbiguousFieldFromMultipleParents. The modeler resolves the ambiguity by qualifying the field with its parent:

pub category Vertebrate_Species { habitat: String }
pub category Endangered_Species { habitat: HabitatProtectionZone }

pub subkind Penguin : Vertebrate_Species, Endangered_Species {
    Vertebrate_Species::habitat = "Antarctic coast",
    Endangered_Species::habitat = HabitatProtectionZone::IUCN_II,
}

Field access from instances follows the same qualification when ambiguous: bar.habitat is rejected with OE0208; the modeler writes bar.Vertebrate_Species::habitat to disambiguate. The substrate offers no automatic merge, override-by-position, or last-wins behavior — every collision is resolved explicitly. (This is consistent with how Argon’s trait system handles method-name collisions; see Trait atom.)

Body modes when : T is present. When a concept is declared as an iof-instance of another (pub kind USD : Currency { … }), the body admits two statement kinds:

• field = value — sets the value of a field defined on the target T. This is the kind-as-instance facet: USD is filling in fields that Currency declared on its instances.
• field: Type — declares an instance-level field that the kind itself will carry forward to its own instances. This is the kind-as-kind facet: every USD bill will have its own serial_number.

pub category Currency {
    #[intrinsic] iso_code: String,
    #[intrinsic] decimal_places: Nat,
    symbol: String,
}

pub kind USD : Currency {
    iso_code       = "USD",        // value for the Currency-defined field
    decimal_places = 2,
    symbol         = "$",

    serial_number: String,         // instance-level field on bills
    denomination:  Nat,
}

let my_twenty = USD { serial_number: "L12345678A", denomination: 20 };

#[intrinsic] on a field declares it must be set at kind level by every iof-instance. Cross-level binding diagnostics: OE1901 InstantiationFieldNotInTarget (a = binding names a field absent from the target metatype), OE1902 InstantiationFieldShadows (a : field shadows an inherited one), OE1908 IntrinsicPropertyMissing (a required #[intrinsic] field is left unbound), and OE0208 AmbiguousFieldFromMultipleParents (a field declared by multiple parents, unqualified). Theory-specific cross-level constraints (e.g., MLT’s categorization / partition / subordination / powertype rules) are not compiler diagnostics: a higher-order theory ships as an unprivileged package (e.g. mlt, Higher-order modeling) and authors those constraints as its own rules/checks over the neutral substrate; see appendix C.

Field access through the iof chain. For an instance bar: SomeKind where SomeKind : SomeCat and SomeCat declares field x, the access bar.x is resolved by walking up the iof chain:

1. Instance fields first. If bar has x declared as an instance-level field (via x: Type in SomeKind’s body), return bar’s own value.
2. Kind-level values next. Otherwise, look at meta(bar) = SomeKind. If SomeKind set x = value at its kind level, return that value.
3. Walk further up. If SomeKind itself does not bind x, continue: meta(meta(bar)), etc., until either x is found or the chain bottoms out at an entity with no further : parent.
4. Not found. Error: OE0101 UnresolvedName (or a more specific field-not-found variant).

Three equivalent surface forms reach the same value when x lives at the kind level:

Shadowing across levels. If x is bound at both an instance level and a higher kind level — different types, or the same type with different values — the elaborator rejects the declaration with OE1902 InstantiationFieldShadows. Modelers either rename, or accept the shadow explicitly by writing meta(bar).x / SomeKind.x when they need the kind-level value. There is no implicit override.

Relations

Like concepts, relations are introduced by a vocabulary-defined metarel — there is no built-in rel keyword at lexer level. Stdlib ships a generic metarel std::core::rel<E1, E2>(E1, E2) for ontology-uncommitted relations; vocabulary packages can ship richer metarels (mediation, material, etc.) or re-export the generic.

// Same terminator rule as a concept (Vocabulary concepts and the generic `type` metatype): the `{ }` rel-body self-
// terminates; the bodyless form requires a ';' (`OE0011` if absent).
rel-decl         ::= attribute* 'pub'? <metarel-name> Ident '(' rel-param-list ')'
                      cardinality-list? rel-supertype? ( rel-body | ';' )
rel-supertype    ::= ('<:' | 'specializes') TypeExpr (',' TypeExpr)*
rel-param        ::= 'mut'? Ident ':' TypeExpr        // RFD 0076 — `mut` only in the named form
cardinality-list ::= cardinality+                       // one slot per endpoint
cardinality      ::= '[' range ']'
range            ::= Nat '..' Nat | Nat '..' '*' | Nat '..=' Nat | Nat
                  // In cardinality position, `..` is INCLUSIVE on both ends
                  // (UML convention): `[1..1]` means exactly one, `[0..*]`
                  // means zero or more. Distinct from Rust range semantics.
rel-body         ::= '{' field-list '}'

The leading identifier (after pub) is contextually a metarel-introducing keyword, resolved per Name resolution against the pub metarel declarations visible in scope — declared in this package or imported from a vocabulary package; rel is not ambient — the std::core baseline is brought in by use std::core::{rel} or a [package].prelude entry (RFD 0038). An unresolved introducer is refused with OE0606 UnknownMetarel. The parser disambiguates concept-decl (no (...) after the new name) from relation-decl (has (...)).

Three surface forms (using the std::core baseline, brought into scope via use std::core::{type, rel};):

use std::core::{type, rel};
// Form A — anonymous binary field on a concept
pub type Person { children: [Person] }

// Form B — named relation with optional navigation views
pub rel ParentOf(parent: Person, child: Person) [1..1] [0..*];
pub type Person {
    parents:  [Person] from ParentOf.parent,
    children: [Person] from ParentOf.child,
}

// Form C — n-ary relation with intrinsic property body
pub rel Marriage(spouse_a: Person, spouse_b: Person) [0..1] [0..1] {
    since:  Date,
    status: MarriageStatus,
}
pub rel Transaction(seller: Person, buyer: Person, item: Asset) {
    amount: Money,
    at:     DateTime,
}

Cardinality (positional, UML association-end convention). For a relation with endpoints e₁, e₂, …, eₙ, the i-th cardinality slot bounds the number of distinct eᵢ for each fixed combination of all the other endpoints — the UML association-end multiplicity. (Equivalently: hold every endpoint but the i-th fixed, and the slot bounds how many distinct eᵢ may complete the tuple.) Omitted slots default to 0..*. For binary relations the slots read left-to-right; pub rel ParentOf(parent: Person, child: Person) [1..1] [0..*] reads “each child has 1..1 parents (slot 1 bounds the parents per fixed child); each parent has 0..* children (slot 2 bounds the children per fixed parent).” For n-ary relations the same per-position rule holds against the fixed combination of the others; pub rel Transaction(seller, buyer, item) [0..*] [0..*] [0..1] reads “for each (buyer, item) pair, 0..* sellers; for each (seller, item) pair, 0..* buyers; and for each (seller, buyer) pair, 0..1 items.”

Relation subsumption (<: / specializes). A relation declaration may name one or more superrelations after its endpoints, in either glyph — <: or the keyword synonym specializes (they are exact synonyms; a declaration reads identically under either). A superrelation clause makes the child’s extent flow into the parent’s: every tuple of the child is, by that edge, a tuple of the parent, so the parent’s closed extent (and every navigation view and rule over it) includes the child’s. The clause takes an optional parenthesized filler list stating, for each parent end by name, what fills it — parentEnd = value:

use std::core::{type, rel};
pub type Person;
pub type City;
pub rel Loc(p: Person, c: City);

// Bare form — pair the child's ends onto the parent by position.
pub rel Home(p: Person, c: City) <: Loc;

// Named filler list — each parent end paired, by name, with the child end
// at the same position. This means EXACTLY what the bare form means: both
// record the same identity mapping, and the bare form desugars to this one
// list at a single point, so there is one downstream representation, not two.
pub rel Residence(p: Person, c: City) <: Loc(p = p, c = c);

// `specializes` is the exact keyword synonym of `<:`.
pub rel Domicile(p: Person, c: City) specializes Loc(p = p, c = c);

Each filler is one of three shapes, all keyed by a parent end: parentEnd = childEnd (pair the parent end with a child end); parentEnd = <literal> (a constant pin, fixing that parent end to a value); or parentEnd = childEnd as ParentSort (a cast, widening a child end to a parent supersort). A mapping whose every parent end is paired with the child end at the same position is the identity mapping; anything else — a rename that permutes ends, a constant pin, or a widening — is a non-identity mapping. Both are evaluated: a child tuple contributes its mapped image to the parent’s extent, threading child ends into the parent’s positions by name, filling pinned positions with their constant, and admitting cast ends at the parent sort. The parent’s closed extent — and every navigation, rule, and query over it — sees the mapped image, so the child is a live member of its parent’s family.

A constant pin fixes a parent end the child has no end for. This is the worked example for the whole mechanism. WagesUSA records only a person and an amount; its images join IncomeItem with the currency pinned to USD. ForeignIncome is an identity member alongside it, so the parent family carries both a pinned image and a pass-through tuple:

use std::core::{type, rel};
pub type Person;
pub type Currency;
pub const USD: Currency;
pub const EUR: Currency;
pub rel IncomeItem(mut p: Person, mut amount: Int, mut c: Currency);
// Constant pin: the parent's `c` end is fixed to a literal rather than
// paired from a child end.
pub rel WagesUSA(mut p: Person, mut amount: Int) <: IncomeItem(p = p, amount = amount, c = USD);
// Identity member: every end paired to the child end at the same name.
pub rel ForeignIncome(mut p: Person, mut amount: Int, mut c: Currency) <: IncomeItem(p = p, amount = amount, c = c);

pub fact Person(alice);
pub fact Person(bob);
pub fact Currency(USD);
pub fact Currency(EUR);
pub fact WagesUSA(alice, 500);
pub fact ForeignIncome(bob, 300, EUR);

// The parent-union query over the whole family.
pub derive anyIncome(p, a, c) :- IncomeItem(p, a, c);
// A query that pins the currency: only USD-imaged rows answer it.
pub derive usdIncome(p, a) :- IncomeItem(p, a, USD);

WagesUSA(alice, 500) is an IncomeItem with its currency filled by the pin; ForeignIncome(bob, 300, EUR) passes through unchanged. anyIncome reads the parent family and sees both:

anyIncome(alice, 500, USD)
anyIncome(bob, 300, EUR)

The pinned query IncomeItem(p, a, USD) fixes the currency, so it matches the pinned image but prunes the EUR tuple — usdIncome yields only alice:

usdIncome(alice, 500)

pub const declares a named individual constant. pub const USD: Currency; declares the individual USD with concept sort Currency: when the ascribed type resolves to a declared concept, the ascription lowers to the same classification assertion pub fact Currency(USD); emits, so the constant resolves as a classified individual wherever an individual is written — a constant pin (c = USD), a rule-body value position (s == USD), a fact argument. Individual identity is the global bare-name hash, so writing the explicit pub fact Currency(USD); alongside the const (as the examples here do) re-asserts the same one row — a relation extent is a set, and re-assertion is harmless. A const whose ascribed type is not a declared concept (a primordial like Int, a struct/enum) declares the bare name only; no classification is asserted. The initializer form const X: T = …; does not execute yet and refuses (OE1355).

Retraction runs the mapping in reverse of assertion: delete WagesUSA(alice, 500) withdraws the child, and its USD image disappears from IncomeItem (a two-support image survives until its last contributing child is retracted).

That last clause is worth showing, because a family image is a derived conclusion held by set-union support, not a stored tuple. When two different members pin the same parent tuple, the image carries two independent supports and is one row that survives until the last support is retracted:

use std::core::{type, rel};
pub type Person;
pub type Currency;
pub const USD: Currency;
pub rel IncomeItem(mut p: Person, mut amount: Int, mut c: Currency);
// Two members that both pin the currency to USD — different relations, same image.
pub rel WagesUSA(mut p: Person, mut amount: Int)  <: IncomeItem(p = p, amount = amount, c = USD);
pub rel SalaryUSA(mut p: Person, mut amount: Int) <: IncomeItem(p = p, amount = amount, c = USD);

pub fact Person(alice);
pub fact Currency(USD);
pub fact WagesUSA(alice, 500);
pub fact SalaryUSA(alice, 500);

pub mutate dropWages()  { delete WagesUSA(alice, 500) }
pub mutate dropSalary() { delete SalaryUSA(alice, 500) }

pub derive anyIncome(p, a, c) :- IncomeItem(p, a, c);
pub derive totalIncome(p, t) :- p: Person, t = sum(a for p2 in Person, IncomeItem(p2, a, _), p2 == p);

WagesUSA(alice, 500) and SalaryUSA(alice, 500) both image onto IncomeItem(alice, 500, USD) — one row, two supports:

anyIncome(alice, 500, USD)

Run dropWages: one support is gone, but SalaryUSA still contributes, so the image survives unchanged —

anyIncome(alice, 500, USD)

Then run dropSalary: the last contributing child is retracted, and only now does the image withdraw —

(no rows)

Propositions, not events

A relation extent is a set of propositions, not a log of events. Two child facts whose translations produce the identical parent tuple are the same proposition asserted twice; the family holds it as one row carrying two supports. This is correct set semantics and the single most common source of aggregate surprise, so it is worth pinning precisely with three runs of the IncomeItem model above.

Identical fact twice — one row. WagesUSA(alice, 500) and SalaryUSA(alice, 500) both translate to IncomeItem(alice, 500, USD). An aggregate over the family folds that one row once. totalIncome sums the amount over IncomeItem per person:

totalIncome(alice, 500)

— 500, not 1000, even though two child facts were asserted. That is the right answer for the proposition “alice has USD income of 500”: the two children merge into one row carrying two supports, and (per the retraction above) the row survives until the last supporter is withdrawn.

Distinct amounts — two rows. Change one fact to SalaryUSA(alice, 501). The translations now differ (500 vs 501), so they are two propositions, two parent rows, and the aggregate sums both:

totalIncome(alice, 1001)

Event identity — two rows. If the two children stand for distinct events — two separate payments that happen to share amount and currency — the identical-tuple merge silently undercounts every multiplicity-sensitive aggregate over the family (sum, count, avg; min/max are unaffected because they ignore duplicates). The fix is in the model, not the query: give the parent a distinguishing end (a source or category end, an event id) so the two events map to two different parent tuples. Add an event-id end e to IncomeItem and each member, assert WagesUSA(alice, 500, 1) and SalaryUSA(alice, 500, 2), and the two events stay apart:

totalIncome(alice, 1000)

Pins-merge corollary. Pinning an end away is the usual way a modeler creates a collision: two members that both pin c = USD and expose the same remaining ends have byte-identical translations, so their rows always merge. Two distinct members in exactly this shape — the WagesUSA / SalaryUSA pair above — are flagged by the collision-capable-siblings warning (OW0741): it names both members and the parent and states the one-row merge consequence, so the aggregate surprise is caught at the declaration rather than discovered in a query. It is a warning, not a refusal (the merge is correct set semantics) and is suppressible where the merge is intended; the fix, when it is not, is to keep or add a distinguishing end so the two members stop pinning the distinction away.

The family-query provenance surface — the generalized specializes(k(…), Parent(…)) query and its Parent(…) via k sugar — carries the mapping through φ: a via family query reaches a non-identity mapped member, reads that member’s own extent, and presents the parent-framed rows with the pinned/renamed/cast ends filled and the answering member bound to k. The generalized specializes form with an explicit member frame still refuses (OE1416) for a non-identity member, because that form ties the member frame positionally to the member’s own ends — sound only for an equal-arity identity member; it points the modeler at via. The parent-union query above reads the closed extent and sees the mapped image directly.

A reorder routes the child’s ends to swapped parent ends by name. BackEdge(u, v, w) reverses an Edge’s endpoints:

use std::core::{type, rel};
pub type Node;
pub rel Edge(mut src: Node, mut dst: Node, mut w: Int);
// Reorder: parent end `src` is fed by child end `v`, `dst` by child end `u`.
pub rel BackEdge(mut u: Node, mut v: Node, mut w: Int) <: Edge(src = v, dst = u, w = w);

pub fact Node(n1);
pub fact Node(n2);
pub fact BackEdge(n1, n2, 7);
pub derive anyEdge(s, t, w) :- Edge(s, t, w);

BackEdge(n1, n2, 7) contributes the reversed Edge:

anyEdge(n2, n1, 7)

A cast widens a child end to a parent supersort; it is identity on the value (the value carries no sort tag), admitting the narrower child end at the parent’s declared sort:

use std::core::{type, rel};
pub type Agent;
pub type Person <: Agent;
pub type City;
pub rel Loc(a: Agent, c: City);
// Cast: the child end filling parent end `a` is widened to the supersort.
pub rel Home(p: Person, c: City) <: Loc(a = p as Agent, c = c);

pub fact Person(bob);
pub fact City(paris);
pub fact Home(bob, paris);
pub derive anyLoc(a, c) :- Loc(a, c);

anyLoc(bob, paris)

A filler that names a parent end the parent does not declare refuses with OE1411; a mapping that fills a parent end twice, or leaves one uncovered, refuses with OE1412. A mapping this build cannot yet resolve to parent positions — a filler list against a cross-module parent whose declared ends are not visible in the child’s file — refuses with OE1410 MappedSubsumptionNotYetEvaluable rather than being recorded under-resolved. (The negative-polarity dual — refuting a parent family when a non-identity edge would have to flow the refutation down to the child, which needs the mapping’s ill-defined inverse — is refused separately at the read path with OE1413.)

Why the filler list is keyed by parent end. Prefer the named filler list over the bare form on any relation whose parent ends share a sort — and note that its key names the parent end, not a position. Bare subsumption pairs the child’s ends onto the parent by position, recording that pairing nowhere in the child’s source. When two parent ends have the same sort, reordering them is a change the sort-covariance gate cannot catch — every position still type-checks — and the child declaration is byte-identical before and after, so a bare pairing flips with no diff at the site where the child is declared. Consider a transfer whose ends are both Account:

use std::core::{type, rel};
pub type Account;
// Parent ends both `Account`. Bare pairing sends the child's first end to
// `payer`, its second to `payee` — but that pairing lives only in the
// positions, not in the child's text.
pub rel Transfer(payer: Account, payee: Account);
pub rel WireTransfer(src: Account, dst: Account) <: Transfer;

Reorder the parent’s ends to Transfer(payee, payer) and this same child still compiles: src now lands on payee and dst on payer, silently reversing every transfer’s direction with no change visible at the WireTransfer declaration. The named filler list states the pairing at the child site, keyed to the parent’s end names:

use std::core::{type, rel};
pub type Account;
pub rel Transfer(payer: Account, payee: Account);
pub rel WireTransfer(src: Account, dst: Account) <: Transfer(payer = src, payee = dst);

Because each filler names the parent end it fills, the correspondence is anchored to names, not positions: it re-anchors under a parent-end reorder instead of silently re-pairing. Reorder the parent to Transfer(payee, payer) and payer = src still routes src to payer — the mapping’s meaning is unchanged; only the parent position it resolves to moves. That re-anchored mapping is now a permutation of the parent’s positions, and this stage evaluates it, so the reordered edge compiles clean and its images join the family correctly:

use std::core::{type, rel};
pub type Account;
// Parent ends reordered vs. the block above; the child is byte-identical.
pub rel Transfer(payee: Account, payer: Account);
pub rel WireTransfer(src: Account, dst: Account) <: Transfer(payer = src, payee = dst);

pub fact Account(acc_a);
pub fact Account(acc_b);
pub fact WireTransfer(acc_a, acc_b);
pub derive allTransfers(payer, payee) :- Transfer(payer, payee);

The mechanical guarantee is completed by a meaning guarantee. In the upright parent (Transfer(payer, payee)) WireTransfer(acc_a, acc_b) records acc_a as the payer; reorder the parent to Transfer(payee, payer) with the child byte-identical, and acc_a is still the payer — the filler payer = src re-anchors to the parent’s payer end wherever it now sits, and the evaluator applies the resolved permutation. The stored tuple’s positional layout follows the parent’s new order (so the raw row reads Transfer(acc_b, acc_a) — payee first now), but the account each parent end names is invariant:

# parent declared Transfer(payer, payee):  allTransfers(acc_a, acc_b)   → payer = acc_a
# parent declared Transfer(payee, payer):  allTransfers(acc_b, acc_a)   → payer = acc_a

A same-sort parent-end reorder therefore can never change a mapping’s meaning — not merely “not silently”, but not at all: the mapping is re-anchored by parent end name and evaluated through that re-anchoring, so who the child records as the payer is the same before and after the reorder. That end-to-end invariance is the acceptance criterion for keying fillers by parent end name.

When two paths disagree — the divergent-map diamond. A relation can reach the same ancestor through more than one subsumption path. When every path composes to the same mapping onto that ancestor, the diamond is harmless — a fact frames to one ancestor row whichever path is read — and it compiles. When two paths compose to different mappings, there is no single answering frame, and the declaration is refused. Here D reaches A straight through Left but end-swapped through Right:

use std::core::{type, rel};
pub type Person;
pub rel A(x: Person, y: Person);
pub rel Left(a: Person, b: Person) <: A(x = a, y = b);
pub rel Right(a: Person, b: Person) <: A(x = b, y = a);
pub rel D(p: Person, q: Person) <: Left(a = p, b = q), Right(a = p, b = q);

A D(alice, bob) fact would land at A(x = alice, y = bob) through Left and at A(x = bob, y = alice) through Right — two different ancestor rows — and a family query over A follows only the first path, silently dropping the other. The refusal names the child, the ancestor, and both composed framings in parent-name-keyed filler form:

OE1424: subsumption of `D` reaches ancestor `A` through paths whose composed mappings DIFFER — via D → Left → A: (x = p, y = q); via D → Right → A: (x = q, y = p). A `D` fact would occupy two different rows in `A`, and a family query (`via D`) would silently report only one framing (the closure follows the first path). Fix: reconcile the fillers so both paths compose to the SAME mapping onto `A`, or remove one subsumption edge. If both images are genuinely wanted, that is a feature request — the mapped-relation-subsumption design record keeps both-images open as future work.

Fix it by making the two compositions agree, or by removing one edge; if the child genuinely belongs at both ancestor rows, that is a feature request the design record keeps open as future work.

Relation-end mutability (mut, RFD 0076). Every relation end is immutable unless declared mut — the same rule, and the same modifier placement, as concept fields (RFD 0006): mut is written immediately before the end name, only in the named-end form of a concrete relation declaration. An anonymous-end mut or a mut inside a metarel signature is refused with OE0013 (mutability is declared per concrete relation end; there is no metarel-level mut). The analogy with fields stops at the declaration posture — a relation assertion is an immutable proposition and there is no relation-end update; mut governs which assertion history is legal:

use std::core::{type, rel};
pub type Person;
pub type Organization;
pub type Marriage;

// A material relation: both ends vary over time, so both opt in.
pub rel worksFor(mut employee: Person, mut employer: Organization) [0..*] [0..1];

// A mediation-shaped relation: a particular marriage cannot involve
// different spouses (`spouse` keeps the immutable default), while a
// surviving person may participate in another marriage later. The
// exact `[2]` bracket makes the initialization minimum atomic: because
// an immutable fiber freezes at its first asserting transaction, BOTH
// spouse tuples must be asserted together (`OE1398` refuses an
// under-filled initialization — the frozen set could never grow to
// complete it).
pub rel bindsSpouse(mut marriage: Marriage, spouse: Person) [0..1] [2];

The write path enforces the declaration per endpoint fiber (hold every other endpoint fixed — the same fixed-complement reading as cardinality): a matched delete R(args) on a relation with any effectively-immutable end refuses with OE1402 (deleting one tuple removes one value from every fiber, so direct retraction needs every end mut; an unmatched delete stays an idempotent no-op); for an immutable end, the first transaction asserting a fiber freezes its complete value set, and a later transaction inserting a new value there refuses with OE1403 (re-asserting an active tuple stays idempotent; a fresh dependent context initializes its own fiber). The legal removal of an immutable binding is retracting its dependent context — the individuals at the other positions — whose kernel RetractIndividuals effect cascades the incident relation retractions, refusing with OE1404 when the set would strand an immutable end’s surviving context; the capability-gated forget erasure runs the same dependent-context gate over its target’s incident tuples (on every standpoint plane the erasure sweeps), so physical erasure cannot stand in for a refused cascade. Correcting a mis-recorded binding — one that was never true — is a separate belief-time channel, the capability-gated amend verb (the record-exit, described below); it is distinct from ending a binding whose world changed (the world-exit cascade). Two declaration gates complete the picture: effective mutability is conjunctive over relation subsumption — a child may tighten a parent mut end by omitting mut, but declaring mut where any transitive superrelation keeps the position immutable refuses with OE0268 — and an end may stay immutable only when every member of its dependent context is an identity-bearing individual (a primordial-, value-, or reference-sorted context member has no lifetime whose retraction could release the binding; refused with OE0267, mark that end mut) — and the same OE0267 refuses the sole end of a unary relation, whose dependent context is empty outright (no other position exists, so no retraction could ever release the binding and the fact would be permanently frozen). The reflection plane exposes the effective bit as the total, catalog-closed armMutability(relation, index, is_mut) atom, one row per declared end.

The gates read the closed extent, not just the tuples a statement names. An insert into a subrelation contributes a row to every transitive superrelation, so an immutable parent fiber initialized through one route (a direct parent insert or a child’s) refuses growth from every other route — direct, sibling child, or child under a parent-initialized fiber — with the same OE1403 (a child re-asserting the parent’s already-active value still initializes its own fiber and is admitted). The closure spans planes too: the freeze witness reads the relation’s retained history as a single global extent — folded on the fixed complement with no standpoint axis — so an insert whose value is new for a fiber any plane initialized refuses with the same OE1403, whichever plane the initializing fact lived on. This global reading is strictly stricter than a per-plane witness (it over-refuses a value new only to a different plane, and never admits an illegal one); per-plane scoping of both the freeze witness and the cardinality gate — so a standpoint’s composed view freezes and counts only against its own retained history — is designed but not yet shipped. And a pub derive whose head names a declared relation feeds that relation’s extent, so a premise mutation that would make an immutable derived binding disappear while its dependent context survives, or grow an already-initialized immutable derived fiber, refuses the whole transaction with OE1397 — the transaction’s net rule-derived extent delta is checked atomically before anything commits; declared relation heads do not bypass mutability merely because no source delete/insert names them directly (pure derive/query heads with no relation declaration carry no end-mutability metadata and are unaffected). The initialization set itself remains governed by the declared cardinality: because an immutable fiber freezes at its first asserting transaction, a declared minimum of two or more is decidable exactly there — an initialization establishing fewer distinct values refuses with OE1398 (the frozen set could never grow to complete it) on every route: a direct insert, a subrelation insert initializing the parent fiber, a rule-derived initialization, and a static fact set (refused at ox check / ox build). A mutable end’s minimum keeps the deferred OW1342 recorded-not-enforced posture. And because the ArgUFO audit story rests on armMutability being total, the name is reserved: a user declaration named armMutability refuses with OE0704 — a same-module derive of that name would otherwise mask the catalog rows and let the very module under a forbidden-opt-out audit discharge it vacuously.

A gallery, end by end. mut is read per fiber — fix the other end and ask whether that value set may still change after its first assertion.

pub type Kid; pub type Toy; pub type Person; pub type Passport;

// Transferable ownership — a pure association, like `worksFor`. Giving a
// toy away is a `delete` + `insert`, and `delete` needs every end `mut`.
pub rel ownedBy(mut toy: Toy, mut owner: Kid) [0..*] [0..1];

// Provenance: this toy was made *for* this kid. The recipient is
// constitutive; the kid's side still grows as they receive more toys.
pub rel madeFor(mut toy: Toy, recipient: Kid) [0..*] [0..1];

// Birth: a child's birth-mother never changes; a mother's set of
// children grows with each birth.
pub rel bornTo(mut child: Person, mother: Person) [0..*] [1];

// Issuance: a passport is issued to one person forever; a person
// accumulates passports over a lifetime.
pub rel issuedTo(mut passport: Passport, holder: Person) [0..*] [1];

Fix a child and their birth-mother is one frozen value (immutable mother); fix a mother and her children accumulate (mut child) — the same shape as madeFor and issuedTo, one end constitutive of the tuple and the other accumulating history. A transferable association like ownedBy is all-mut by necessity: rebinding requires delete, and a matched delete removes a value from every fiber. Choosing mut reduces to three questions per relation: (1) will a tuple ever be deleted while both individuals still exist? — then every end is mut (an association: ownedBy, worksFor); (2) otherwise, which end is fixed the moment the tuple exists and which keeps accumulating? — the constitutive end stays immutable, the accumulating end gets mut (bornTo, madeFor, issuedTo, bindsSpouse); (3) is the only honest exit the disappearance of a participant? — then the cascade does the work and the end needs no mut. On these relations the gates read: insert bornTo with a second birth-mother for a recorded child refuses OE1403 (a second birth-mother contradicts frozen information rather than adding to it); delete issuedTo while holder and passport both survive refuses OE1402; retracting the passport cascades the frozen binding and the holder survives; retracting the holder alone refuses OE1404 while the passport’s context survives.

The choice between bindsSpouse and worksFor(mut, mut) is a modeling posture, not two kinds of fact. bindsSpouse reifies the relator — the marriage is an entity whose relata are constitutive, so its ends are immutable and its lifecycle runs through retract-and-cascade — while worksFor(mut, mut) deliberately does not reify: it tracks only the current association, a coarser view whose tuples are rebindable snapshots (history stays queryable bitemporally). A domain that cares about the employment itself declares an EmploymentContract and gives its relation immutable ends, making a job change the retraction of one contract and the creation of another — the marriage’s shape. What this design adds is that the schema now states which posture each relation takes; before, every relation silently behaved like the coarse view.

Correcting the record — amend (RFD 0076). Immutability protects two different things the write path used to conflate: the world cannot rebind an immutable end, and the record cannot be silently rewritten. Ending a binding because a participant ceases is a world-exit — the cascade (retract the dependent context, the incident tuples fall away, history retains the binding, and the vacated value can never be reused). Discovering that a binding was never true — a mis-recorded assertion, false when it was made — is a record-exit, and it is what amend performs: the assertion is withdrawn as false ab initio, releasing the freeze contribution it should never have made, while the bitemporal history retains what-was-believed-when (the correction is auditable, not an erasure). amend R(args); is the primitive (withdraw when the true value is unknown; positive evidence is withdrawn, so the proposition returns to unknown, not refuted); amend R(args) => R(args'); is the atomic composite (withdraw and assert the corrected proposition against one transaction-time view — all-or-nothing). It is a distinct verb from delete on purpose: delete is the valid-time ender (the binding stops being true now), amend is the belief-time corrector (the binding was never true). amend is capability-gated at the source level exactly as forget is: a mutate body using it refuses to build (OE1405 AmendWithoutCapability) unless the enclosing mutate declaration grants #[allow_amend]; correction authority is further authorized per invoking principal, target-scoped, at the serving layer.

pub type Person;
// Birth: a child's birth-mother never changes (immutable `mother`), but a
// mis-recorded mother is corrected at belief time.
pub rel bornTo(mut child: Person, mother: Person) [0..*] [1];

#[allow_amend]
pub mutate correct_birth_mother(child: Person, wrong: Person, right: Person) {
    // The record was wrong from the start: `child` was never born to `wrong`.
    // Withdrawing `bornTo(child, wrong)` releases the frozen `mother` fiber,
    // so the corrected `bornTo(child, right)` is admitted where a plain
    // `insert` would refuse `OE1403`.
    amend bornTo(child, wrong) => bornTo(child, right);
}

#[allow_amend]
pub mutate rescind_birth_mother(child: Person, wrong: Person) {
    // Truth not yet known: withdraw the false assertion alone. The `mother`
    // fiber re-initializes as if it had never been frozen at `wrong`.
    amend bornTo(child, wrong);
}

The amendment gates read one net corrected view of the whole transaction — the retained assert-polarity history minus the tuples this transaction amends, with corrected assertions and any lifecycle effects overlaid — so a correction cannot launder a companion cascade (the corrected tuple is live in the view the dependent-context gate reads). Two amendment-specific refusals complete the surface: amending one of several tuples in a fiber whose declared minimum exceeds one, when the surviving corrected set would drop below that minimum, refuses with OE1407 AmendmentBelowMinimum (distinct from OE1398, which refuses an under-filled initialization — OE1407 refuses an under-filling correction of an already-established fiber); and amend R(args) naming a tuple that is live but has no directly-asserted (or refuted) event — a purely rule-derived conclusion — refuses with OE1406 AmendmentTargetNotAsserted (you amend premises, not conclusions; dependency maintenance recomputes the consequence). On an all-mut relation amend is admitted (its freeze-release is vacuous there, but the false-ab-initio marking still differs from delete’s valid-time close). A tuple with neither an event nor a live row is the idempotent no-op, as an unmatched delete is.

The declaration-plane gates (OE0267/OE0268) are enforced by oxc-check in its end_mutability classifier, run over each relation declaration in the check pass; the write-path gates (OE1402–OE1404) are enforced by oxc-runtime in its end_mutability module.

Anonymous-field cardinality default. A field declared with the inline anonymous-relation form field: [T] (Form A) synthesizes a binary relation with default cardinality 0..* and Set semantics. The bounded spellings — field: [T; n..m], ordered-list opt-in field: [T; n..m, ordered] (lowering to List<T>), and the [T; <=1] singleton hint (OW2402, suggesting T? / Option<T>) — are reserved surface: no enforcement is wired yet, so a cardinality bound on a list type refuses by name (OE0014) rather than being silently discarded. Use a plain [T] until write-path enforcement lands.

Anonymous fields are structural shorthand: they do not engage the metarel calculus. No metarel name is attached; the synthesized relation is accessed only via dot-traversal. This is symmetric with struct/enum, which are likewise language-level structural and carry no metatype. Named relations (Forms B and C) require a metarel-introducing keyword in scope.

[T] on struct vs concept. On a struct or enum field, [T] is plain List<T> — no synthesized relation, no closure traversal, no metarel. On an ontologically-classified concept (declared under a metatype), [T] is Form A — a synthesized binary relation supporting closure traversal (alice.children+(b)). The difference is whether the enclosing declaration is data (struct/enum) or ontology (declared under a metatype — type or a vocabulary introducer).

When to upgrade Form A to Form B or C. Promote an anonymous field to a named relation when any of: (a) the relation needs to be classified under a metarel (mediation, material, …) so the substrate can reason over its properties; (b) the relation carries intrinsic data of its own (since: Date, amount: Money); or (c) the relation must be referenced as a first-class predicate from rule bodies (derive ancestor(d, a) :- ParentOf(d, a), …). When none of those apply, Form A is the right choice.

Generic relation-property characteristics. A named relation (rel or metarel) may carry the standard relation-algebra property characteristics (the OWL object-property characteristics) — PL/DB-neutral, describing the shape of the relation’s extent with enforcement, not an ontological commitment. All four are shipped by the std::rel standard-library package and must be brought into scope — use std::rel::{transitive, irreflexive, asymmetric, functional} (nothing is ambient — Name resolution / RFD 0038). #[transitive] is a genuine declarative macro (it expands to the closure derive). #[irreflexive] and #[asymmetric] are genuine procedural macros (RFD 0040): they re-emit the relation and paste the guarding check’s internal __{rel}_{prop} head via concat_idents. They read the relation’s name, so they apply to a rel; on a metarel they decline (the invocation is refused, OE0723). #[functional] is likewise a genuine procedural macro (RFD 0040 P2): BOTH its rel and metarel arms re-emit the decorated declaration and paste a __{rel}_functional check that fires when a source maps to two distinct targets (OE1361) — the same check-based enforcement as its siblings. A rel whose explicit target cardinality permits more than one target contradicts #[functional] and is refused (OE1378). A characteristic applied without its import is refused — OE0705 for every macro (#[transitive]/#[irreflexive]/#[asymmetric]/#[functional]; OE1362 is retired). Multiple characteristics compose on one declaration (re-emitting $item verbatim, a stacked sibling and the user’s brackets/generics/body all survive).

use std::rel::{transitive, irreflexive, asymmetric, functional};

#[transitive]
#[irreflexive]
#[asymmetric]
pub rel is_proper_part_of(part: Top, whole: Top);

#[functional]
pub rel inheres_in(burden: Aspect, bearer: ConcreteIndividual);  // each aspect inheres in one bearer

Enforcement applies to the declared relation’s own extent. Propagation of a property borne by a metarel to the relations it classifies is out of scope (Out of scope). A characteristic applied without importing it from std::rel is refused — OE0705 for every macro (#[transitive]/#[irreflexive]/#[asymmetric]/#[functional]; all genuine macros, not directives). #[functional] applies to both a binary rel and a binary metarel (each arm pastes the source-maps-two-targets check); #[irreflexive]/#[asymmetric] apply only to a rel and decline on a metarel (the invocation is refused, OE0723). On a non-relation declaration (a concept, a rule) the invocation likewise fails to match and is refused (OE0723). (The ontology-specific relation properties — MLT’s #[partitions], #[categorizes], etc. — are vocabulary decorators and live in their packages, distinct from this generic family.)

impl Type { … } — grouping

impl-block ::= 'impl' generic-params? TypeExpr  '{' impl-item* '}'      // grouping
            |  'impl' generic-params? TypeExpr 'for' TypeExpr '{' trait-impl-item* '}'   // trait impl

The grouping form admits any declaration kind (impl-item); the trait-impl form is restricted to the contract member forms (trait-impl-item: fn / mutate / derive / check / query) and is governed by the conformance obligations of the trait surface and conformance (RFD 0026).

impl Person {
    pub fn greeting(self) -> String = "Hello, " + self.name;       // instance method
    pub fn adult(p: Person) -> Bool = p.age >= 18;                  // associated function
    pub rel ParentOf(parent: Person, child: Person) [1..1] [0..*];  // lexically grouped
    pub query oldest() -> Option<Person> {
        select p from p: Person order by p.age desc limit 1
    }
}

An impl Type block accepts any declaration kind: methods, associated functions, relations, queries, mutations, checks, associated type / const. All declarations inside the block are namespaced under Type::. Methods (items with self first parameter) are additionally accessible via UFCS dot-notation (alice.greeting()); associated functions and relations are reachable only as Type::name(args).

impl Person {
    /// Instance method (has `self`): both `alice.greeting()` and `Person::greeting(alice)` work.
    pub fn greeting(self) -> String = "Hello, " + self.name;

    /// Associated function (no `self`): reached as `Person::adult(p)`.
    pub fn adult(p: Person) -> Bool = p.age >= 18;

    /// Type-associated relation: reached as `Person::ParentOf(a, b)`.
    pub rel ParentOf(parent: Person, child: Person) [1..1] [0..*];

    /// Method-shaped query: `alice.oldest()` and `Person::oldest(alice)` both work.
    pub query oldest() -> Option<Person> {
        select p from p: Person order by p.age desc limit 1
    }
}

A relation declared inside impl Type is not exposed at module level. Choose the placement (module level, inside a topic mod, or inside impl Type) according to the semantic association the modeler intends — see Connecting concepts and relations.

Connecting concepts and relations

A relation is first-class, but where it is declared expresses its semantic association with the participating concepts. Three placements coexist; the modeler picks by intent:

• Module level — a free predicate owned by no single endpoint: pub rel ConnectedTo(a: Node, b: Node) [0..*] [0..*];, accessed as ConnectedTo(x, y) anywhere in the module.
• Topic mod — grouped with related concepts; accessed as family::ParentOf(a, b) after use family::*;.
• impl Type (impl Type { … } — grouping) — conceptually “about” the type, alongside its methods; accessed as Person::ParentOf(a, b) only, not at module level.

Navigation from a concept value to its participations. Three mechanisms link an instance to the relations it participates in.

1. Field-form navigation view (cheapest, declarative):

pub type Person {
    parents:  [Person] from ParentOf.parent,    // alice.parents
    children: [Person] from ParentOf.child,     // alice.children
}

A field may be scalar when the relation is binary and the projected endpoint is functional — its declared cardinality caps it at one ([0..1] / [1..1]). For a binary relation the holder is the sole other endpoint, so a functional value endpoint is a holder→value dependency: one value per holder. The scalar view then yields a single value, not a collection:

pub type Person {
    manager: Person from HasManager.manager,    // a single Person, not [Person]
}

A scalar view over a non-functional endpoint is refused: the endpoint may back several tuples for one holder, so a single value is ill-defined. Declare the field as a collection ([T]) or constrain the endpoint:

pub type Person {
    parent: Person from ParentOf.parent,    // scalar over a [0..*] endpoint
}
pub rel ParentOf(parent: Person, child: Person) [0..*] [0..*];

A scalar view over an n-ary relation is refused even when the value endpoint is [0..1]: the bracket bounds the value per fixed combination of the other endpoints, not per holder, so it is not a holder→value functional dependency. Here [0..1] bounds salary per (person, company) pair, but one person may hold two employments and so two salaries — which a scalar projection would silently collapse. Project the whole set as a collection, or model the dependency with a binary relation:

pub type Company;
pub rel Employment(person: Person, company: Company, salary: Int) [0..*] [0..*] [0..1];
pub type Person {
    pay: Int from Employment.salary,    // scalar over a ternary relation
}

A collection view over an n-ary relation is admitted — it projects the whole endpoint set — provided the holder endpoint is unambiguous. The holder is the endpoint the declaring concept occupies, resolved by type: exactly one non-value endpoint whose type is comparable with the declaring concept. If no non-value endpoint is comparable the holder can never occupy the relation, so the view is statically empty; if two or more are, from Rel.endpoint cannot say which is the holder. Both are refused (OE1376). A binary relation is never ambiguous — its holder is the sole other endpoint — so this only constrains arity ≥ 3:

pub type Item;
pub rel Pairing(buyer: Company, seller: Company, item: Item);
pub type Company {
    deals: [Item] from Pairing.item,    // holder ambiguous: buyer or seller?
}

Each field is a derived view over the relation. The compiler verifies the field type matches the role’s endpoint type and that cardinality is consistent with the relation’s per-endpoint cardinality (a scalar field over a non-functional endpoint, or over any n-ary relation, is refused — OE1370; a collection field over an n-ary relation whose holder is not uniquely type-resolvable is refused — OE1376). The view materializes against the relation’s closed extent: because relation subsumption (Relations) makes a subsumed relation’s tuples tuples of its supersuming relation, a view over Rel.endpoint includes the endpoints contributed by every <:-subsumed relation — so a subtype that refines an inherited collection by projecting from a subsumed relation (SatisfactionAccount.records from satisfactionAccountRecords <: recordAccountRecords) sees exactly its narrower elements.

Filtering the view — where. A navigation view keeps only the projected elements that are iof the field’s element type; a where clause narrows it further. The clause is one expression, not a braced body, and it binds exactly one variable: the projected endpoint, named by the endpoint selector the from clause spells. Module-scope declarations are visible as usual, so a type test, a rule call and a field predicate all resolve:

pub type Drawing {
    circles:    [Circle] from Contains.shape where shape : Circle,      // type test
    bigCircles: [Circle] from Contains.shape where shape.radius > 10,   // field predicate
}

self is not bound here. A refinement body binds self to the individual whose membership is being decided (Refinement), but a navigation-view filter runs over the projected elements, so a filter written against self names nothing and is refused (OE0107) with the endpoint variable it should have named. Nor are the relation’s other endpoints bound — including the holder, the individual whose field is being computed — so a condition comparing a projected element against the holder’s own state cannot be written in the clause; express it as a rule and call the rule with the endpoint variable.

pub type Shape { radius: Int }
pub type Circle <: Shape;
pub rel Contains(drawing: Drawing, shape: Shape);
pub type Drawing {
    circles: [Circle] from Contains.shape where self.radius > 10,    // `self` is unbound
}

2. UFCS method via impl (richer navigation):

impl Person {
    pub query siblings(self) -> [Person] {
        select s from ParentOf(p, self), ParentOf(p, s) where s != self
    }
}

Methods are appropriate when navigation requires filtering, joining, ordering, or aggregation beyond a simple projection. Accessed as alice.siblings().

3. Direct rule-body invocation (always available):

pub derive grandparent(g: Person, c: Person) :- ParentOf(g, p), ParentOf(p, c);

Inside any rule body, the relation is a predicate addressable by name (or by qualified path: family::ParentOf(...), Person::ParentOf(...)).

Inverse declaration (when both sides are field-form):

pub type Country { citizens: [Citizen] }
pub type Citizen {
    #[inverse(Country.citizens)]
    countries: [Country],
}

The compiler verifies cardinality consistency and exposes both navigation directions over a single synthesized relation.

Naming convention. Relation names are CamelCase (per Identifiers) — ParentOf, Marriage, IsCitizenOf — symmetric with the CamelCase of metatype-introduced concepts. The name plus argument order encodes semantic direction; ParentOf(p, c) reads “p is the parent of c.” The convention is the modeler’s responsibility — the language does not enforce it. Use field-form views or methods to expose semantically-named navigation in the opposite direction.

Fact heads resolve in the declaring file’s scope; individuals travel by bare name. A pub fact P(...) head must resolve to a concept or relation in the file’s fact-head scope: the concepts and relations the file itself declares, plus imported ones its use/prelude scope reaches by module-qualified path (use vocab::Executable; and a pub use re-export hub both work). A head that resolves to nothing refuses with OE0220 FactReferencesUnknownPredicate; when the name is declared elsewhere in the workspace, the refusal names the declaring module and the working pattern. That pattern rests on identity: an individual’s identity is the global bare-name hash — alice is the same individual from every module — so the canonical cross-module shape is to mint where the concept is declared (pub fact Person(alice); in the concept’s own module) and reference anywhere by bare name (in rule bodies, mutate bodies, and as relation-fact arguments in other modules).

Facts assert propositions, not events. A relation’s extent is a set: asserting the same pub fact twice — same relation, same arguments — adds nothing, because the two identical assertions are one tuple. A bare proposition is true once, however many times it is written. Because a literal in-file repeat is therefore almost always a copy-paste slip, the compiler warns on a same-file literal duplicate pub fact (duplicate-fact-in-file, a suppressible warning). The remedy is to delete the duplicate; or, if the repeats are meant to record distinct events (a marriage that happened twice, a payment repeated), give each fact its own identity — add an event-id endpoint so the arguments differ and both tuples survive. Duplicates are matched on the canonical encoding of the fact, not its source spelling — whitespace and formatting differences do not matter, and a relation reached through a renamed import (use pkg::Married as Wed;) is the same relation as the original name, so Married(a, b) and Wed(a, b) are one fact and warn. The check is deliberately narrow: it fires only within one file. The same fact asserted in two different files, or re-inserted by a mutate, is legitimate idempotent re-assertion and is never flagged.

Three import postures

A modeler picks an ontological posture per module by choosing what to use. Three cover almost all code:

// Posture 1 — pure data, no ontology. `struct`/`enum` are lexer built-ins.
use std::math::Nat;
pub struct Receipt { lease_id: Nat, paid: Money, at: Date }
pub enum Severity { Error, Warning, Info, Hint }

// Posture 2 — generic ontological commitment via the std::core
// baseline, brought into scope explicitly (RFD 0038).
use std::core::{type, rel};
pub type Document { title: String, body: String }
pub rel Cites(citer: Document, cited: Document) [0..*] [0..*];

// Posture 3 — vocabulary-classified. The vocabulary is an ordinary
// EXTERNAL package — here a hypothetical third-party UFO package;
// nothing UFO-related ships with Argon or its stdlib — or the module
// declares its own `pub metatype` / `pub metarel` vocabulary locally.
use ufo_foundational::prelude::*;   // a third-party vocabulary package
pub kind Person { name: String, age: Nat }
pub rel ParentOf(parent: Person, child: Person) [1..1] [0..*];
pub mediation Involves(m: Marriage, p: Person);

Postures compose and are per-module, not per-package: a module may use the imported std::core baseline (use std::core::{type, rel}, or via the package prelude) alongside another imported (or locally-declared) vocabulary, and a package may ship modules in different postures behind one prelude. The metatype calculus (Meta-calculus atom) distinguishes the declarations by the keyword in declaration position.

Group axioms — disjoint, complete, partition

A group axiom constrains a set of sibling concepts collectively: that they never overlap, that they jointly exhaust a parent, or both. The three forms share one declaration shape — a contextual keyword, an optional parent, and a brace list of member concept paths:

disjoint  { Cat, Dog, Fish }            // pairwise non-overlapping
complete  Animal { Cat, Dog, Fish }     // jointly exhaustive over Animal
partition Animal { Cat, Dog, Fish }     // disjoint AND complete

The keywords (disjoint / complete / partition) are contextual — they lex as ordinary identifiers and bind as group-axiom keywords only in declaration position followed by the group-axiom shape, so they remain available as concept and field names elsewhere. A group axiom introduces no name of its own; it names existing concepts.

disjoint { A, B, C } asserts the members are pairwise non-overlapping: no individual is an instance of two of them at once. Disjointness is instance-level. A write that would classify one individual into two declared-disjoint members is refused (OE0240), so the contradictory state never enters the store. disjoint takes no parent — the members need not share a supertype.

complete Parent { A, B, C } asserts the members jointly cover Parent: every Parent instance is an instance of at least one member. Under the closed-world default (Type system), a Parent instance derivable into none of the members is an uncovered instance, and the write that creates it is refused (OE0241). Each member must be a subtype (<:, transitively) of Parent, checked at elaboration (OE0243 otherwise). Completeness has a second, static half, but it fires only when uncoveredness is provable. The build is refused (OE0242) when the schema declares an instantiable (non-abstract) concept S <: Parent that is provably disjoint from every cover member — so no individual can be both an S and a member (for instance because a disjoint/partition declaration separates S from each member, or because the cover is empty). A subtype that merely fails to be a static subtype of any member is not refused: under multiple classification an S individual can still be classified into a member at write time, so its covering is left to the runtime OE0241 guard. (This is why orthogonal generalization sets over one class — two partitions of Parent along independent dimensions — are admitted: a member of one is not disjoint from the members of the other.) An abstract subtype, having no direct instances, is exempt. This static gate ranges only over the concepts declared in the same file as the group axiom; a subtype introduced in another module is not seen at this point, and — like an in-file subtype that is not provably uncovered — its covering is left to the runtime OE0241 guard rather than refused statically.

partition Parent { A, B, C } is the conjunction: the members are both disjoint and complete over Parent. It imposes the OE0240 overlap guard, the OE0241 covering guard, and the OE0242 / OE0243 static gates together.

A declared disjointness also constrains typed-slot writes, because it makes a slot’s demand unsatisfiable rather than merely unmet. Writing into a relation endpoint, or into a concept-typed field, an individual already classified under a concept declared disjoint from the slot’s declared concept is refused: classifying that individual under the slot’s concept would itself violate the group, so the write can never be satisfied in this state or any later one. The refusal fires at elaboration where the value’s concept is statically known (OE1426 endpoints, OE1434 fields) and at write time against the individual’s real classification (OE1428 endpoints, OE1435 fields). It does not depend on the slot concept’s world assumption — an open world permits membership that is unknown, not membership a declaration forbids. Two concepts with no declared disjointness are unaffected: multiple classification is legal, an individual under one may later also be classified under the other, and the write stands.

Disjointness and covering are enforced as ordinary substrate checks (Rule atom — fn, derive, query, mutate, check) the compiler synthesizes from the declaration — one overlap check per unordered member pair, one negation-as-failure covering check per cover — so a violating write is refused by the same delta-guard that enforces a hand-written check, with no separate axiom machinery. The covering check is closed-world: it fires when no member membership is derivable. Its interaction with a concept’s #[world(open)] assumption is specified in World assumptions (CWA / OWA) (RFD 0045).

A degenerate group axiom synthesizes no runtime check, because it has nothing to guard. An empty disjoint { } and a one-member disjoint { A } have no unordered pair to overlap, so no overlap check is produced and the declaration is accepted in silence. An empty complete Parent { } likewise produces no covering check — but it still meets the static cover gate above, so any instantiable subtype of Parent (including Parent itself, if non-abstract) is then provably uncovered and the build is refused (OE0242).

Types and refinement

Generics

Angle brackets, Rust-aligned:

generic-params ::= '<' generic-param (',' …)* '>'
generic-param  ::= Ident ('<:' TypeExpr ('+' TypeExpr)*)?

Type arguments at call site use turbofish for disambiguation: sort::<Money>(prices).

Subtyping

A <: B declares A is a subtype of B. Two universal bounds frame the lattice: A <: Top and Bot <: A hold for every A.

Beyond the declared <: graph, the substrate has three built-in subtyping sources (oxc-check/src/infer.rs::types_compatible):

• Numeric tower: Nat <: Int <: Real and Nat <: Int <: Decimal. Money is not in the tower — there is no implicit Int → Money; Money only arises through the result-side widening of monetary arithmetic (Numeric tower and coercion), Money ▷ Decimal ▷ Real ▷ Int.
• Covariant collections: List<A> <: List<B> and Option<A> <: Option<B> iff A <: B (written [A]/A?).
• Invariant elsewhere: tuples, fn(…) -> _, and generic applications subtype only by equality.

Real, Decimal, and Money are exact arbitrary-precision rationals (BigRational); source numeric literals parse to exact rationals with no f64 round-trip, so 0.1 + 0.2 == 0.3 (RFD 0016, oxc-reasoning/src/compile/value.rs).

Refinement

refinement-clause ::= ('where' | 'iff') '{' refinement-pred (',' …)* '}'
refinement-pred   ::= D1Pred | D2Pred

A refinement attaches a predicate to a concept. The keyword chooses how the predicate relates to membership — the description-logic split between a primitive class (⊑, necessary conditions only) and a defined class (≡, necessary and sufficient conditions). See RFD 0017.

• where { P } — primitive. P is a necessary condition: every member satisfies it, but a supertype instance that merely satisfies P is not thereby a member. Membership is asserted (by construction or insert iof, mutate); P is enforced as an invariant at each membership write and never widens the extent. This is Rust’s where bound lifted to a concept’s members — a constraint, not a definition.
• iff { P } — defined. P is necessary and sufficient: an instance of the supertype is a member if and only if it satisfies P. Membership is derived — the substrate auto-classifies and rejects manual insert iof (mutate, OE0211). Reads as the membership biconditional: “an Adult is a Person iff age >= 18.”

pub type Adult          <: Person  iff   { self.age >= 18 && self.has_id };   // defined: any qualifying Person is automatically an Adult
pub type ExtinctSpecies <: Species iff   { self.living_count == 0 };          // defined: classification derived from state
pub type VettedVendor   <: Vendor  where { self.risk_score <= 30 };           // primitive: vetting is conferred; the score is a necessary invariant on members

D1Pred (substrate-locked): metaEq, isDet, hasAnc, hasDesc, countGeq, forallC, existsC, plus Booleans. D2Pred: QF-LIA, GNFO, enum equality. The elaborator stages D1 ahead of D2 residual.

Mechanically: D1Pred / D2Pred / MixedPred are inductives at spec/lean/Argon/Decidability/Fragment.lean; the staging theorem stage_correct lives at CrossDomain/Staging.lean; the polynomial bound on D1 evaluation (d1EvalCost n φ ≤ d1Size φ · (n+1)^(d1QuantifierDepth φ)) is proven in Complexity/Bounds.lean. The bound grounds the polytime claim Tier ladder makes for tier:structural and tier:closure.

Three-valued membership under OWA. When the governing world assumption is open (World assumptions (CWA / OWA)), iff-derived membership is three-valued: success requires positive evidence that the predicate holds. A value whose predicate evaluates to unknown does not satisfy the refinement — matching SHACL’s sh:Violation discipline and SQL’s three-valued NULL semantics. Under CWA, unknown collapses to false. The mechanization at TypeSystem/Soundness/CwaOwa.lean proves that CWA-true refinement results survive transition to OWA (monotonic knowledge transfer). The symmetric rule for a primitive where invariant: a membership write is rejected only on positive evidence of violation (P evaluates to a definite false); unknown permits the write (mutate, OE0668). unknown means information absence — a referenced field with no recorded value. A predicate that cannot be evaluated at all (an unsupported form, malformed stored data, or a type-mismatched comparison such as ordering a Date against an Int) is not unknown: unsupported forms are refused at build time (OE0660) — including a predicate whose expression shape is supported but whose field locus is not: an iff projecting a field declared only on the refining concept’s own body (structurally absent from every supertype candidate), or a where projecting a relation-backed navigation field (not evaluable against stored fields at a membership write) — and anything that slips past the gate fails the operation loudly at runtime — never a silent permit (where) or a silently-empty derived extent (iff). Refinement predicates evaluate on the same exact value tower as every other value position (RFD 0016): exact rationals for Real/Decimal/Money, chronological Date comparison, with no value-dependent enforcement.

Built-in type forms

First-class function values include references to declared fns and closures (Expression grammar); both share the fn(T1, T2) -> U type. Higher-kinded types and runtime trait objects (dyn Trait) are out of scope (Out of scope).

Reflective sorts. Entity, TypeRef, and Metatype are the reflective sorts of the meta-calculus (Reflection), ordered Metatype <: TypeRef <: Entity (and Entity <: Top). These are distinct from Top (Subtyping): Top is the <:-greatest type, whereas TypeRef is the sort whose values are references to declared types. The bounded form TypeRef<C> is sugar for the Refinement refinement { t: TypeRef where specializes(t, C) } (RFD 0017, where = primitive/asserted), with TypeRef == TypeRef<Top>. It is covariant — TypeRef<A> <: TypeRef<B> iff A <: B — which follows directly from the refinement ({t | t <: A} ⊆ {t | t <: B}), adding no new structural subtyping rule. Membership is three-valued under OWA (World assumptions (CWA / OWA), RFD 0007): specializes(t, C) unknown ⇒ not a member. Powertype / order / categorization semantics stay in the unprivileged mlt package (Higher-order modeling); TypeRef<C> carries none of them. See RFD 0023.

? propagation

expr? on a Result<T, E>-typed expression unwraps to T on Ok or returns the Err from the enclosing rule. Admitted in fn and mutate bodies, where the enclosing rule’s return type is Result<U, E> for some U. Not admitted in derive (which has no return type — predicates do not fail) or query (whose return type is the projection type, not a Result); check rules emit diagnostics rather than returning Results. Calling ? outside an admitted context is a parse-time error.

Expression grammar

expr            ::= primary-postfix
                      ((arith-op | comp-op) primary-postfix)*
                      (('not')? 'in' primary-postfix)?
                      ('&&' expr | '||' expr)*

primary-postfix ::= unary-op* primary postfix*
unary-op        ::= '!' | '-'
postfix         ::= '.' Ident '(' expr-list ')'                  // n-arg method call
                  | '.' Ident                                     // field access OR zero-arg method call
                  | '[' expr ']'                                  // index
                  | '[' expr? '..' expr? ']'                      // slice
                  | '?'                                            // try (Result propagation)

primary         ::= literal
                  | '_'                                            // wildcard / anonymous binding (rule-atom arg positions only)
                  | '(' expr ')'
                  | list-or-comprehension
                  | if-expr
                  | match-expr
                  | block-expr
                  | meta-call
                  | aggregate
                  | subquery                                       // `query` (count/set/one/collect/exists braces)
                  | call-expr
                  | path
                  | struct-literal
                  | closure

literal         ::= INT | REAL | STRING | DATE | DATETIME | BOOL

list-or-comprehension
                ::= '[' ']'
                  | '[' expr (',' expr)* ','? ']'
                  | '[' expr 'for' Ident 'in' expr ('where' expr)? ']'

if-expr         ::= 'if' expr block ('else' (block | if-expr))?
match-expr      ::= 'match' expr '{' arm (',' arm)* ','? '}'
block-expr      ::= '{' stmt* expr? '}'
block           ::= '{' stmt* expr? '}'

call-expr       ::= path '(' expr-list ')'
meta-call       ::= 'meta' '(' expr ')'

aggregate       ::= ('sum'|'count'|'min'|'max'|'avg')
                    '(' expr ('for' Ident 'in' expr
                              ('where' expr)? (',' rule-atom)*)? ')'   // RFD 0029: trailing atoms refine the fold

struct-literal  ::= path '{' (struct-init-list)? '}'
struct-init-list ::= field-init (',' field-init)* ','?
                   | '..' expr (',' field-init)* ','?            // struct-update spread
field-init      ::= Ident (':' expr)?                            // `name` shorthand or `name: expr`

closure         ::= '|' closure-params? '|' ('->' TypeExpr)? closure-body
closure-params  ::= closure-param (',' closure-param)* ','?
closure-param   ::= Ident (':' TypeExpr)?
closure-body    ::= expr | block

path            ::= Ident ('::' Ident)*
expr-list       ::= (expr (',' expr)*)?

arith-op        ::= '+' | '-' | '*' | '/' | '%'
comp-op         ::= '==' | '!=' | '<' | '<=' | '>' | '>='        // non-chainable

Precedence (tightest to loosest):

1. Postfix (.f(), [i], [a..b], .field, ?)
2. Unary prefix (!, -)
3. Multiplicative (*, /, %) — left-associative
4. Additive (+, -) — left-associative
5. Comparison (==, !=, <, <=, >, >=) — non-associative (a < b < c is rejected; use a < b && b < c)
6. Membership (in, not in) — non-associative
7. Logical AND (&&) — left-associative, short-circuit
8. Logical OR (||) — left-associative, short-circuit

Turbofish disambiguates generic call sites at expression position: sort::<Money>(prices).

Rounding builtins (RFD 0029). A small family of rounding functions is available in expression position — both in rule-body bindings and in the fn/compute plane — operating exactly over the numeric tower (Decimal stays Decimal, never via f64):

round_half_even is the money default: financial rounding rounds half to even to avoid the systematic upward bias of half-away-from-zero. All four return an exact value (integral results collapse to Int). A wrong argument count is refused at compile with OE1333 RoundingBuiltinArity.

The decimal-place count n has a supported scale domain of |n| ≤ 1000. The scale is 10⁻ⁿ, formed as an exact rational, so the bound caps the magnitude of 10^|n| for resource safety; 1000 places is far beyond any real-world money / decimal / scientific quantity (SQL DECIMAL caps scale at 38; IEEE 754 decimal128 carries 34 significant digits). A count outside the domain is refused at evaluation with OE1374 RoundingScaleOutOfRange — a typed client diagnostic, never a silent truncation of the count to a wrong scale.

Closures capture environment by value (Argon is value-semantic; no references). A closure’s type is fn(T1, T2) -> U — interchangeable with declared fn references at any function-typed argument or binding.

Property-style accessors. The paren-less postfix .Ident resolves to a stored field if the receiver type declares one with that name; otherwise to a call of a zero-argument method with that name. This unifies the .field and .zero_arg_method() forms — both read obj.name. The 30.days, 5.minutes, 60.seconds shorthand in Numeric tower and coercion is exactly this affordance over zero-arg methods on numeric types. Methods with one or more arguments always require explicit parens.

Struct-literal evaluation. A struct-literal T { … } evaluates each field initializer and assembles a struct value of type T (the data semantics — structural equality, immutability, no identity — are stated in struct and enum — language built-ins (data declarations)). The literal must state every field: a missing field is OE0249, an undeclared one is OE0250, and a field given the wrong type is OE0251. The field shorthand in field-init (a bare Ident with no : expr) takes the field’s value from a same-named binding in scope.

Functional update — the ..base spread. The ..expr form in a struct-init-list constructs a new struct value from an existing one: it evaluates base, copies every field, then overrides the fields the literal restates. Row { ..base, a: 9 } is base with a replaced by 9 and every other field carried over. The result is a fresh value; base is never modified (struct values are immutable, struct and enum — language built-ins (data declarations)). The spread supplies the fields the literal omits, so the every-field rule is satisfied by the base — a spread literal need only name the fields it changes.

pub struct Row { a: Int, b: Int }

test "spread overrides one field and carries the rest" {
    let base = Row { a: 1, b: 2 };
    assert Row { ..base, a: 9 } == Row { a: 9, b: 2 };
    assert base == Row { a: 1, b: 2 };          // base unchanged
}

Field projection. The postfix .f reads field f off a struct value, by structure. Projection nests — outer.inner.v reads v off the inner struct off outer. A field the struct’s type does not declare is OE0254 StructFieldAccessUnknown.

pub struct Inner { v: Int }
pub struct Outer { inner: Inner, tag: String }

test "projection reads through nested struct values" {
    let o = Outer { inner: Inner { v: 7 }, tag: "x" };
    assert o.inner.v == 7;
    assert o.inner == Inner { v: 7 };
}

Enum payload binding in match. The constant-pattern subset of match — payloadless enum constants, literals, or-patterns of those, and _ — executes (Pattern matching). A payload-binding arm (match opt { Some(x) => …x… }) destructures one payload value into one fresh variable, bound over the arm body. In value position — a let right-hand side, a comparison operand, a fn body, a return/require value — this binds and evaluates: let r = match opt { Some(x) => x, None => 0 }; is the idiomatic way to read an enum payload. The arm binds exactly one variable positionally; a zero-, multi-, or record-binder arm is OE0257 EnumPayloadPattern. A payload-binding arm in statement position (an effectful arm inside a mutate statement-match) refuses with OE1319 rather than mis-evaluating; bind the payload in value position first. The rule-body membership test path is Some(binder) / path is None is the other supported reader (struct and enum — language built-ins (data declarations), RFD 0007 Rule-atom grammar).

Functor modules

A module declaration may take type or value parameters, producing a functor module — a module-valued function:

functor-mod  ::= 'mod' Ident generic-params '{' mod-item* '}'
                                                              // generic functor
              |  'mod' Ident '(' param-list ')' '{' mod-item* '}'
                                                              // value-parameter functor
mod-alias    ::= 'mod' Ident '=' path '(' expr-list ')' ';'  // instantiation

Functor modules are instantiated via the mod Name = path(args); alias form introduced in Structure; the body is re-elaborated per instantiation site with the parameters bound. The substrate guarantees monomorphization at elaboration — there is no runtime module dispatch.

mod TaxJurisdiction<J: Jurisdiction> {
    pub type TaxableIncome <: Money;
    pub derive owes_tax(p: Person) :- p.income: TaxableIncome, p.income > 0;
}

mod us_federal = TaxJurisdiction<USFederal>;
mod california = TaxJurisdiction<California>;

Parametric modules, not parametric concepts. Argon admits parameterization only at the module level. There is no parametric pub type Container<T> { … } form — a metatype-classified concept is always a closed, monomorphic classifier. When a modeler wants Container<Apple> vs Container<Orange>, the answer is either (a) a specialization hierarchy (pub type AppleBox <: Container) when the variation is ontological, or (b) a functor module whose body declares the per-instantiation concepts when the variation is parametric. This restriction keeps the metatype calculus first-order and the inference tier classifier decidable; lifting it would require admitting kind-polymorphism into refinement and standpoint federation, both of which are unsound at present without further machinery.

A functor body admits any module-level item: concepts, relations, rules, traits, macros, sub-mods, and other functor modules. Each instantiation produces a fully elaborated namespace; symbols from one instantiation do not unify with symbols from another (us_federal::TaxableIncome and california::TaxableIncome are distinct types, both <: Money).

Functor modules are the canonical mechanism for vocabulary-parameterized libraries (per D-007).

The Path type

Path<NodeT, EdgeT> is the first-class type produced by path-projecting query forms (query). It appears in the built-in type forms (Built-in type forms) because the compiler synthesizes path values from query results; the value-level API lives in the stdlib (std::path).

A path is an ordered, alternating sequence n₀, e₁, n₁, e₂, n₂, …, eₘ, nₘ where m = length(path) is the number of edges. A path of length zero is a single node. NodeT and EdgeT are the least common supertypes of the node and edge values respectively.

Edge values by relation form. Edge values vary with which relation form (Relations) the path traverses:

• Forms B and C — named relations. Each edge value is the relation tuple-entity itself, carrying any intrinsic properties: path.nth_edge(0)?.distance retrieves the distance field of the first edge when the underlying relation declares it.
• Form A — anonymous fields. Each edge value is the structural placeholder Edge<From, To> { from: From, to: To }. Form A carries no metarel classification and no intrinsic data, so the placeholder exposes only endpoint identities.

Heterogeneous chains. When a path traverses relations with differing endpoint types (e.g., user.knows(friend).works_at(company) where knows: User → Person and works_at: Person → Company), NodeT is the join (least common supertype) of User, Person, and Company, and EdgeT the join of the involved relation types. When no common supertype is in scope, both fall back to Top. Modelers needing precise heterogeneous typing decompose into single-relation queries and join at the modeler level.

Hyperedges. Paths are over binary relations only. n-ary relations (pub rel Transaction(seller, buyer, item)) are queryable but not path-traversable; hypergraph traversal semantics is out of scope (Out of scope).

API. The shape/projection/fold operators (length, nodes, edges, nth_edge, reverse, concat, map_*, …) are stdlib API on impl<N, E> Path<N, E> in std::path — see Stdlib (selected). The type-system-relevant facts: cost(self) -> Real lives in a conditional impl gated on E <: Weighted (the Rust-aligned conditional-impl pattern), so a uniform Path<N, E> admits cost() only when the edge type implements the std::path trait Weighted { fn weight(self) -> Real; }; without it, shortest-path queries rank by edge count. The Form-A edge value is the placeholder pub struct Edge<A, B> { from: A, to: B } — no metarel classification, just a first-class edge for uniform iteration.

Equality. Path<N, E> has structural equality: two paths are equal iff their node and edge sequences match position-by-position. Paths are value-semantic and immutable; all transformations produce new path values.

Temporal substrate

Why bitemporal

The substrate before this section operates on a single state mapping concepts to extents. The mutation grammar (mutate) advances the state from snapshot to snapshot; prior snapshots are not addressable. This section introduces the bitemporal substrate: every fact carries a valid time and a transaction time. Bare queries default to the current snapshot; explicit temporal operators address the past, the future, and the historical record of the system’s beliefs.

The formalism is DatalogMTL (Wałęga et al., IJCAI 2019) with stratified negation (Tena Cucala et al., AAAI 2021) over the integer timeline; the reference reasoner is MeTeoR (Wałęga et al., AAAI 2022).

Valid time and transaction time

Two interval annotations on every fact (and every relation tuple):

• Valid time (VT) — when the fact holds in the world. [VT_start, VT_end], with open-ended [VT_start, ∞] for ongoing.
• Transaction time (TT) — when the system recorded the fact. [TT_start, TT_end], with open-ended [TT_start, ∞] for current belief.

The snapshot view is the projection ${,\mathsf{iof}(x, T),\mid,VT_{\text{start}} \le \mathit{now} \le VT_{\text{end}} ;\wedge; TT_{\text{start}} \le \mathit{now} \le TT_{\text{end}},}$. Bare rule atoms and bare queries default to this view.

The bitemporal extension applies uniformly to all relations, not just iof. A pub rel Enrolment(s: Person, u: University) tuple carries VT and TT just like an iof fact.

Mechanized at spec/lean/Argon/Reasoning/Temporal.lean (BiState as the bitemporal State; TTHistory and TTMonotone for the transaction-time invariant). The bitemporal extension is additive — the termination machinery of Argon.Reasoning.State lifts pointwise without modification.

Retroactive correction and audit

Mutations that close a VT interval retroactively (delete iof(x, T) at #PAST-DATE#) do not erase the prior record. They close its TT interval at now and append a new record with the corrected VT. Audit queries as of TT = #PAST-DATE# reconstruct what the system believed at any past point. The substrate is append-only by default; explicit erasure (forget), crypto-shredding (#[shred_on_forget]), and #[retention(…)] bounds are storage-layer concerns specified in mutate and Storage layer.

Rule validity over time

A rule carries valid time and transaction time just as a fact does. Its valid time is the interval over which the rule is in effect; its transaction time is when the rule was recorded or its text corrected. This is the bitemporal model of any fact — when it holds versus when the system recorded it — applied to rules, with transaction time serving as the shared viewpoint across facts and rules.

A rule’s start-of-validity is written with the same at #DATE# qualifier a fact uses, placed on the head:

pub derive eligible(x) at #2018-01-01# :- enrolled(x), in_good_standing(x);

Without the qualifier a rule has unbounded validity — in effect at every point — so a program that dates none of its rules behaves exactly as one with no validity windows at all. A rule’s record time, when it entered the system, is the separate transaction-time axis and is never folded into its validity: an undated rule is in effect at past points too, not merely from the moment it was written.

Evaluating derived facts at a chosen rule valid-time point selects exactly the rules in effect at that point, by the same valid-time visibility the data plane applies to facts (VT_start ≤ t ∧ t < VT_end). Reading at the present selects every currently-in-effect rule, so present-time evaluation is unchanged by the feature. A reconstruction of what was derived at a past point replays under the rules in effect then, not the rules in effect now.

A prospective retirement closes a rule’s VT_end going forward; it is forward-only: derived facts that held while the rule was in effect stand, and only points at or after the close lose that rule’s support. Retroactive invalidation — removing a rule as if it had never been in effect — is a distinct, transaction-time operation outside this section.

A rule’s validity window is a property of the rule — which rules apply — and is independent of any metric-temporal operator (since, until) appearing inside a rule body, which constrains when within the world timeline a body atom holds.

Three-valued evaluation under OWA

Under open-world assumption, temporal atoms evaluate to Is | Not | Can. The since and until operators (see Temporal rule atoms) lift to three-valued via the strong-Kleene meet/join tables that truth values defines, composed pointwise across the interval. Unknown temporal extent projects to Can, never to Both — there are no conflicting witnesses, just single-source uncertainty.

Temporal sub-tier

Temporal expressiveness is an orthogonal sub-tier on top of the main tier ladder. Every program has a tier pair (main, temporal) — see Tier ladder.

Metric-timeline resolution

The metric temporal operators (since, until, and the box/diamond bounded forms) reason over a discrete integer timeline whose tick is a package-declared resolution, set in ox.toml:

[temporal.metric]
resolution = "week"   # or "day" (default), "hour", "nanosecond", "2weeks", …

The tick is a package-global choice (one metric axis is shared by every rule and fact), mirroring default_world. It lives under [temporal] — the umbrella for temporal-reasoning config — rather than a bare [metric], so the precise word metric stays scoped to the metric-operator family (distinct from the modal box/diamond family) and leaves room for future siblings ([temporal.modal], …). It is a cost/coarsening lever: a metric operator’s work scales with the number of ticks between interval endpoints, so a program reasoning over long spans can declare a coarser tick. Because decidability rests on discreteness — not on the tick equalling a day — any positive-integer tick keeps the metric fragment decidable (see Decidability).

• Snapshot reads are unaffected. “The fact valid at instant t” (see AsOf semantics) stays a full-nanosecond integer comparison; it never consults the tick. The tick governs only the metric operators.
• Bounds are authored in days (.days/.weeks, or a bare integer) and coarsened onto the tick. A bound that is not an integer multiple of the tick loud-refuses rather than rounding — since[3 days] under a week tick refuses (3⁄7 is not a whole number of weeks); since[14 days] is two ticks.
• The default is day, so a package that declares no [temporal.metric] table behaves exactly as before.
• An unrecognized resolution value is a non-fatal manifest warning (it falls back to the day default), per the manifest-honesty convention.

The design record is RFD 0067 §6.

Rule atom — fn, derive, query, mutate, check

Argon distinguishes the definition of derived predicates (derive) from inference tasks over the resulting theory (query). derive populates IDB predicates that other rule modes can join against, contributing to the inductive closure. query consumes them and returns a typed value with no IDB side-effect. The split mirrors IDP’s { … } inductive-definition block vs. propagate/expand inference tasks. fn is pure value computation over its arguments; mutate is the only side-effecting verb; check emits diagnostics observer-only (lowers to Cat3 — never populates the IDB).

Purity ladder

fn and query are cacheable on (args, state_version). derive is stratified fixpoint. mutate is transactional.

fn

fn-decl ::= attribute* 'pub'? 'fn' Ident generic-params? '(' param-list ')' '->' TypeExpr fn-body
fn-body ::= '=' expr ';'                          // single-expression
         |  '{' stmt* expr? '}'                    // block, implicit return
param   ::= 'self' | Ident ':' TypeExpr

self and Self. Argon is value-semantic; there is no reference or borrow form. self is always owned-by-value (no &self / &mut self) and is admitted only as the first parameter of a method inside an impl block or a trait declaration; its type is the enclosing impl’s target. Self resolves to the implementing type in trait declarations, to Type inside impl Trait for Type, and to Type inside bare impl Type { … }.

pub fn rent_per_day(l: Lease) -> Money = l.monthly_rent / 30;

pub fn classify(area: Decimal) -> Size {
    if area < 50.0 { Size::Small }
    else if area < 200.0 { Size::Medium }
    else { Size::Large }
}

pub fn safe_div(a: Money, b: Money) -> Result<Money, Diagnostic> {
    if b == 0 {
        Err(Diagnostic { severity: Severity::Error, code: "Math::DivZero", message: "..." })
    } else {
        Ok(a / b)
    }
}

derive

derive-decl ::= attribute* 'pub'? 'derive' Ident '(' param-list ')'
                  ( ':-' atom-list )? ';'
atom-list   ::= atom (',' atom)*
atom        ::= predicate-call | comparison | type-test | 'not' atom | path-pattern

pub derive ancestor(d: Person, a: Person) :- ParentOf(d, a);
pub derive ancestor(d: Person, a: Person) :- ParentOf(d, p), ancestor(p, a);
pub derive senior(p: Person) :- p: Person, p.age >= 65;

// Ground-fact form (no body, concrete args): the head holds for the named terms.
pub derive iof(Type, Type);                                    // MLT* OL3
pub derive Within(usc26, usc);                                 // seed a derived predicate

Multiple derives with matching head name and arity compose as Datalog union (modulo the stratification check below). not atom is NAF, evaluated under well-founded semantics. A derive with no :- clause is bodiless, and its head arguments decide its reading:

• Concrete arguments → a ground fact. When every head argument is a concrete term — a declared individual (Within(usc26, usc)), an enum constant, an axis value, or a type reference (iof(Type, Type)) — the bodiless derive declares that tuple as a ground fact, equivalent to :- true. This is the sanctioned way to seed ground tuples directly on a derived predicate: the seed tuples union with the head’s other derive clauses and rules over the same relation node (same name, same arity), so a recursive rule reads them and computes their closure (seeds ∪ derived-closure). A non-concrete (free-variable) argument is the error — a bodiless derive has no body to range-restrict it — and is refused with OE1342, the bodiless analogue of OE1303 (below), naming the offending argument and directing you to declare the individual or add a :- … body.
• Type-annotated parameters → an empty predicate. A bodiless head whose arguments are typed parameters (pub derive adult(p: Person);) introduces the predicate with that signature and an initially empty extent — the introduce-empty idiom (Rule-atom grammar). Its rows arrive from later same-head derive clauses.

Every body-carrying rule must be range-restricted (safe): each variable in the head, in a negated (NAF) atom, or in a comparison/compute operand is bound by some positive body atom; an unsafe rule is refused at compile (OE1303), since an unbound variable would silently project Null or mis-evaluate.

Evaluation model. A derive program denotes the tuples its rules derive, under the semantics fixed in Reasoning: the least fixpoint of the positive program, stratified negation layered along the axis dependency graph, and — for a negation cycle no stratification can layer — the well-founded model computed by the alternating fixpoint. The surface consequences a rule author relies on:

• Recursion through negation is accepted. A negation cycle (p :- not q, q :- not p) that strict stratification cannot layer is evaluated under well-founded semantics rather than refused. Cross-stratum, acyclic NAF is ordinary stratified negation. (OE1309 no longer fires from stratification; it survives only as the dispatch seam.)
• Four-valued query surface. WFS is three-valued (true / false / undefined). The engine materializes the definitely-true extent as the head’s rows — a paradoxical atom resolves to undefined and does not fire downstream rules — and the head’s undefined tuples surface on the query/derive read as Can rows, by default (drop-but-count under the opt-in K3 projection; see the envelope contract under well-founded semantics). A rule whose conclusion is genuinely undecided neither fires nor is denied — and the read says so (Can) instead of omitting it.
• #[brave] / stable-model semantics is out of scope (Out of scope).

Parametric (axis-generic) rules. A derive rule may be generic over a set of axes; the elaborator monomorphizes it to a finite set of concrete rules at elaboration, with no change to fixpoint semantics.

Stratified aggregates. Aggregate atoms (count, sum, max, min, avg, set_collect, …; see query) are admitted inside derive bodies when the aggregated predicate sits at a strictly lower stratum than the rule head, where the stratification dimension is a well-founded relation (typically the iof DAG, the specialization lattice, or an explicit user-declared ordering). The classic library use case is computing a derived level function over iof:

pub derive has_order(t: Entity, n: Nat) :-
    n == 1 + max { select m from t': Entity, m: Nat
                   where iof(t', t), has_order(t', m) };

The stratifier accepts this because the inner max aggregates has_order over iof-predecessors of t, and iof is well-founded. Stratified aggregates that would loop through an aggregation step on the same stratum are rejected with OE0510 NonStratifiedAggregate.

Universals over recursive predicates. A common composite pattern — a conjunction is fulfilled iff all of its children are — is a universal over the very predicate being defined:

pub derive Fulfilled(p: Conjunction, t: Instant) :-
    Instant(t), forall c: PC where childOf(p, c), Fulfilled(c, t);

This form is refused (OE1317 RecursionThroughAggregation): the forall lowers to the count-equality aggregate (Rule-atom grammar), and stratified-aggregate semantics (Faber–Pfeifer–Leone) require the aggregated predicate in a strictly-lower stratum — here Fulfilled aggregates over itself, so its SCC crosses an aggregate boundary and has no stratification. No intermediate derive helps: recursion depth follows the data (the part-whole tree), so any helper joins the same cycle. The supported phrasing is negation-as-failure double negation — ∀c.F(c) rewritten as ¬∃c.¬F(c):

pub derive HasUnfulfilledChild(p: Conjunction, t: Instant) :-
    childOf(p, c), Instant(t), not Fulfilled(c, t);
pub derive Fulfilled(p: Conjunction, t: Instant) :-
    Conjunction(p), Instant(t), not HasUnfulfilledChild(p, t);

This converts recursion-through-aggregation into recursion-through-negation, which the well-founded executor evaluates. On two-valued-total data — every child’s Fulfilled status resolves to true or false, as it does over a finite acyclic part-whole tree of leaves with definite status — the double negation derives exactly the universal’s extent, bottom-up through the tree. The honest caveat: where a child’s status is genuinely undefined under WFS, the double-negation form propagates undefined to the parent rather than guessing either way — and the surface reports the parent as a Can row rather than omitting it, per the four-valued projection rule under well-founded semantics. Admitting the forall form directly (structural stratification over a provably well-founded relation) is tracked in issue #185.

Worked example — double-entry accounting (RFD 0029). Derived values and aggregate-as-term together make quantitative domains authorable. The double-entry invariant — within every journal entry, total debits equal total credits — is a check comparing two aggregates; the per-account balance is a derived value, grouped per account (the outer bound variable). The running package is examples/double_entry_v0.

pub type Account { mut name: String, }
pub type Entry   { mut memo: String, }
pub type Posting { mut amount: Decimal, mut side: String, }   // side = "D" | "C"
pub rel postedTo(posting: Posting, account: Account);
pub rel inEntry(posting: Posting, entry: Entry);

// Per-account balance = Σ debits − Σ credits, grouped per `acct`.
pub derive accountBalance(acct, bal) :- acct: Account,
    debits  = sum(p.amount for p in Posting, postedTo(p, acct), p.side == "D"),
    credits = sum(p.amount for p in Posting, postedTo(p, acct), p.side == "C"),
    bal     = debits - credits;

// The double-entry invariant — two aggregates compared, per entry.
pub check EntryNotBalanced(e: Entry) :- e: Entry,
    debits  = sum(p.amount for p in Posting, inEntry(p, e), p.side == "D"),
    credits = sum(p.amount for p in Posting, inEntry(p, e), p.side == "C"),
    debits != credits
    => Diagnostic {
        severity: Severity::Error,
        code:     "Ledger::E001",
        message:  "journal entry is not balanced — total debits must equal total credits",
    };

// A sales-tax line, rounded to cents with banker's rounding (the money default).
pub derive accountTax(acct, tax) :- acct: Account,
    debits = sum(p.amount for p in Posting, postedTo(p, acct), p.side == "D"),
    tax    = round_half_even(debits * 0.075, 2);

Every amount is an exact Decimal: sum folds rationals (no rounding), the balance subtraction is exact, and round_half_even rounds to cents exactly — 150.75 * 0.075 = 11.30625 rounds to 11.31, never an f64 artifact. The EntryNotBalanced check is an instance-level Error, so at runtime it is a delta guard: a mutation that would leave an entry unbalanced is rejected atomically (double-entry is enforced, not merely reported).

Rule-atom grammar

Bodies of derive, query from clauses, check, and unsafe logic blocks are conjunctive sequences of rule atoms. The atom shapes:

rule-body ::= rule-atom (',' rule-atom)*
rule-atom ::=
    // Negation as failure
      'not' rule-atom
    | 'not' '(' rule-atom (',' rule-atom)* ')'
    // Modal (tier:modal)
    | 'box' '(' rule-atom ')'
    | 'diamond' '(' rule-atom ')'
    // Restriction quantifiers — DL ∀R.C / ∃R.C  (tier:expressive)
    | 'forall' '(' field-path ',' type-expr ')'
    | 'exists' '(' field-path ',' type-expr ')'
    // FOL binding quantifiers — admitted at tier:fol (inside unsafe logic)
    | 'forall' Ident ':' type-expr 'where' rule-body
    | 'exists' Ident ':' type-expr 'where' rule-body
    // Aggregate as atom, optionally compared (paren form, Expression grammar)
    | aggregate (comp-op expr)?
    // Subquery as atom, optionally compared (brace form, `query`)
    | subquery (comp-op expr)?
    // Reflection
    | meta-call (comp-op expr)?
    | path '::' Ident                                // sugar for meta(path) == Ident
    // Predicate call with optional outcome / comparison suffix
    | path '(' rule-arg (',' rule-arg)* ')'
        ('is' outcome-suffix | comp-op expr)?
    // Role invocation with closure (+ = transitive, * = reflexive-transitive)
    | field-path ('+'|'*') '(' Ident (':' type-expr)? ')'
    | field-path '(' Ident (':' type-expr)? ')'
    // Type test and `is` sugar
    | field-path ':' type-expr
    | field-path 'is' ('not'? 'unknown' | type-expr | Ident)
    // Specialization
    | field-path '<:' field-path
    // Binding — single `=`, distinct from the comparison `==` (RFD 0029)
    | Ident '=' expr
    // Comparison — RHS is a full expression (Expression grammar)
    | field-path comp-op expr
    // Membership — RHS is a full expression (set, list, or range)
    | field-path 'not'? 'in' expr
    // Bare-path Boolean test
    | field-path

field-path     ::= Ident ('.' name)*
rule-arg       ::= expr | expr comp-op expr
outcome-suffix ::= 'not'? ('ambiguous'|'unknown'|'timeout') ('(' Ident ')')?

The truth qualifier R(arguments) is unknown selects R’s well-founded-undefined tuples. These are tuples left neither definitely true nor definitely false by a recursion-through-negation component (Truth values). The component must finish first: the stratifier places the consumer in a higher stratum and then reads R’s undefined companion. A consumer that feeds back into R’s component is refused with OE1441, because it would inspect an incomplete result. Move that consumer into a separate pub derive that does not feed back into R. is not unknown, payload-binding is unknown(x), and path-headed x is unknown also refuse with OE1441; only a predicate call identifies the companion, and a complement requires an explicit finite domain. The multi-valued suffixes is both(a, b) / is ambiguous(a) / is timeout(a) remain the separate OE1349 refusal. This qualifier does not classify ordinary open-world absence; it reads only the WFS companion materialized by evaluation.

Binding atoms (x = expr, RFD 0029). A rule body may bind a fresh variable to the value of an expression: x = expr (single =) is assignment, distinct from the comparison x == e (double =, a filter). expr ranges over bound variables, literals, field projections (t.income), exact arithmetic over the numeric tower, the rounding builtins (Expression grammar), and aggregate expressions. This is the established Datalog/Soufflé assignment concept and is what lets a rule head carry a derived value:

pub derive Tax(t, owed) :- appliesTo(b, t), owed = t.income * b.rate;

The binding introduces a fresh variable, and is range-restricted. Two distinct refusal paths, never a silent Null:

• Freshness (OE1335 BindingLhsAlreadyBound). The left-hand side x must be a new name. If x is already bound — by a prior positive predicate atom, a head parameter bound elsewhere, a projection, an aggregate result, or an earlier binding — the = would silently degrade into an equality filter (x joined against the computed value) rather than a binding. It is refused, naming x, with the directed hint: use == to compare, or pick a fresh name. This is the path a rebind x = x + 1 takes when x is otherwise bound (e.g. by a body predicate) — the LHS is not fresh.
• Range restriction (OE1303 RuleNotRangeRestricted). x = expr binds x positively iff every variable in expr is itself positively bound. An unbound right-hand-side variable, or a pure self-reference / cycle among binding atoms where the result variable is bound by nothing else (x = x + 1 as the only binder of x; x = y, y = x), leaves x unbound under the binding fixpoint and is refused as unsafe.

So x = x + 1 refuses either way — via OE1335 when x is already bound elsewhere (freshness), or via OE1303 when x has no other binder (range restriction) — and the two codes name the two genuinely different errors.

Aggregates as bindable terms (RFD 0029). Because an aggregate is a bindable expression, comparing two aggregates — the double-entry sum(debits) == sum(credits) invariant — is simply binding each and comparing the bound variables:

pub derive balanced(e) :- e: Entry,
    debits  = sum(p.amount for p in Posting, inEntry(p, e), p.side == "D"),
    credits = sum(p.amount for p in Posting, inEntry(p, e), p.side == "C"),
    debits == credits;

The aggregate source extends the comprehension form: after for x in Source, a comma-separated list of additional body atoms (relation atoms, comparisons, type tests) refines the fold’s domain, and variables from the outer rule body are visible inside. That visibility is the grouping — the group key is the set of outer bound variables free in the aggregate, the standard Datalog reading. pub derive balance(acct, s) :- acct: Account, s = sum(p.amount for p in Posting, postedTo(p, acct)); groups per acct. A binding is not a comprehension trailing-atom form — sum(w for u in T, …, w = u.v) is refused with OE1336 BindingInComprehension, which directs you to project the value into the fold directly (sum(u.v for u in T, …)) or to bind in the outer rule body and aggregate the bound variable. The brace form (sum { … }) stays count/exists-only; a value aggregate in brace form is refused with OE1331 ValueAggregateBraceForm, which directs to the comprehension form. The SQL-ish group by … having is not built; it refuses with OE0007 carrying the binding-form rewrite. (Aggregates evaluate over the definitely-true extent: an aggregate folding over a relation with well-founded-undefined atoms is refused at runtime with OE1332 AggregateOverUndefined rather than silently treating undefined as false. The refusal is whole-relation, not per-group; three-valued aggregate intervals are tracked under issue #250.)

The value aggregates are numeric folds (RFD 0016): sum / avg / min / max lift every projected value into the exact-rational domain — min / max included, so no orderable-but-non-numeric projection (a Date, a String) is admissible either. A projection whose declared type is statically non-numeric — a temporal value, a String, a Bool, an entity or structured value — refuses at ox check / ox build with OE1433 AggregateProjectionNotNumeric, naming the projection expression, its type, and the fold’s numeric domain; a non-numeric value that reaches the fold only dynamically raises the same OE1433 loudly at runtime. count folds cardinality and admits any projection.

Empty-group semantics — a deliberate split. When a group is empty (the fold sees no rows), the aggregators divide by role:

• sum, count, count_distinct emit a value for the empty group — 0. An additive/cardinality fold has a well-defined identity (the empty sum is zero, the empty count is zero), so the grouped row is produced with that identity value.
• min, max, avg drop the row — they have no value over an empty set (there is no least/greatest element, and the mean is 0/0), so no grouped row is produced for an empty group rather than fabricating one.

This split is load-bearing for the double-entry invariant. sum(debits) == sum(credits) must catch an entry that has credits but no debits: because sum emits 0 for the empty debit side, the comparison is 0 == credits, which fails and flags the entry as unbalanced. Were sum to drop the empty group, the row would vanish and the imbalance would pass silently. The examples/double_entry_v0 package relies on exactly this behavior.

Conjunction between atoms uses ,. NAF uses the not keyword. Disjunction is not inline — write separate derive rules with the same head and arity; the union composes structurally. The same-head idiom is derive-only: a check head carries payload identity (its => Diagnostic { severity, code, message } report, its guard classification, its violation relation), so two checks sharing one head would cross-talk and are refused at elaboration (OE1328 DuplicateCheckHead) — rename one check, or express the disjunction through a shared derive predicate whose same-head clauses union, read by a single check. (Trait check members are unaffected: each impl’s monomorphized member rule is qualified by its impl target and keeps a distinct head, Trait atom.) The RHS of comparison atoms is a full expression (Expression grammar); inside that expression context, && / || / ! apply normally.

Payloadless enum constants. In value position, a path of the form EnumName::VariantName denotes the canonical enum value when the variant has no payload. This is distinct from the standalone rule atom sugar path :: Ident above, which means meta(path) == Ident. Payload-carrying variants require constructor semantics and are not constants by themselves.

Predicate resolution. The head of every predicate-call atom (path '(' … ')') must resolve to a declared predicate in scope — a rel, a concept used as a classification predicate, a derive / query head, a trait rule member (qualified Trait::member(...), or bare when exactly one provider is in lexical scope; subject to the coverage gate, Resolution), a pub fact / pub not_fact predicate, a fn, or a reflection intrinsic (iof, specializes, meta, extent, implements). check heads are not consumable: checks are observers only (Purity ladder) — their violation sets never populate the IDB — so a body atom resolving to a check head (module-level or trait check member) is refused with OE1329 CheckHeadConsumed; derive from the underlying body predicates instead (factor the violation pattern into a pub derive head read by both the check and the consuming rule). This applies to the predicate atoms of derive and check bodies and to both the body and head atoms of bridge rules (Bridge rules). An unresolved head is OE0223 RuleReferencesUnknownPredicate, the rule-body analogue of the pub fact obligation OE0220 (RFD 0004). A resolved atom is further checked for arity (OE0225) and — where both the argument’s type and the declared parameter type are concretely known — argument type (OE0226, sound under multiple classification: it fires only on provable disjointness). Entity-typed positions additionally carry a declared-sort discipline (OE1432 RuleAtomArgSortMismatch): a logic variable whose declared sort — its head-parameter annotation, a body sort guard x : T, or a unary concept-membership atom T(x) — is <:-incomparable with the position’s declared parameter concept is refused. This is deliberately not a disjointness proof (multiple classification can still make the join non-empty at runtime); it is the signature-level discipline: an atom whose declared sorts are incomparable can only succeed through a multi-classification the program never states, and in practice compiles to a silently-empty join. Both <: directions pass (a subtype in a supertype slot is subsumption; a supertype in a subtype slot narrows, exactly as an x : T occurrence-typing test narrows), and asserting the second sort in the body (x : T or T(x)) licenses the atom. A predicate declared in several clauses — one per admissible sort — licenses an argument comparable with any clause’s parameter concept at that position, and a clause leaving the position unannotated admits anything there. Sorts a variable merely picks up by occupying other predicates’ argument slots are classification evidence, not declarations, and never trigger the refusal. This is independent of the world assumption: the world assumption governs the truth value of instances of a declared predicate (under the CWA default an unasserted instance is false; under an #[world(open)] concept it is unknown/Can, World assumptions (CWA / OWA)) — it never admits an undeclared predicate name. To introduce a predicate that is intentionally empty until populated, declare it (pub rel P(...), or a bodiless pub derive P(...); head). ox check enforces this, and ox build refuses to emit an artifact for a program containing an unresolved predicate.

Relation-value application. A rule-body variable whose value is proven to range over a finite, exhaustive set of declared relations may itself stand in predicate position — r(p, c) where r is such a variable. The proof comes from the same body: a specializes(r, Parent) atom pins r to the Parent specialization family (relations are first-class citizens of the <: graph, so specializes ranges over declared relations exactly as it ranges over concepts); an equality with a relation literal (r == Home) pins a singleton; rel/arm reflection atoms pin by metarel or endpoint signature. The application lowers to a static dispatch over the proven candidate set — reading the dispatch at selector r equals applying the concrete relation r names.

If you only want the union of a relation family, do not use this — query the parent relation directly. Every subrelation’s tuples flow into each ancestor relation’s extent by declared subsumption (the RFD 0005 closure, materialized at seeding). A rule body naming Loc already ranges over Home, Work, and any member added later, with no dispatch and no domain proof. Relation-value application earns its cost only when the parent query would erase information you need — see the cases below.

pub type Person;
pub type City;

pub rel Loc(p: Person, c: City);
pub rel Home(p: Person, c: City) <: Loc;
pub rel Work(p: Person, c: City) <: Loc;

// UNION — no relation-value application. `Home` and `Work` tuples flow
// into `Loc` by subsumption, so the parent query already unions them.
pub derive anyLoc(p: Person, c: City) :- Loc(p, c);

The motivating case is provenance: you need to know which member of the family a tuple came from. The parent query collapses the family to one relation and erases that; a relation-valued selector keeps it, because specializes(kind, IncomeItem) binds kind to each member and kind(p, a) reads the tuple through it — so kind stands in the output as which relation each row was declared in, kept as a value.

pub type Person;

pub rel IncomeItem(mut p: Person, amount: Int);
pub rel Wages(mut p: Person, amount: Int)    <: IncomeItem;
pub rel Interest(mut p: Person, amount: Int) <: IncomeItem;

pub fact Person(alice);
pub fact Person(bob);
pub fact Wages(alice, 50000);
pub fact Interest(alice, 1200);
pub fact Wages(bob, 30000);

// PROVENANCE — `kind` is a relation-valued output column.
pub derive report(p: Person, kind, a: Int) :-
    specializes(kind, IncomeItem), kind(p, a);

// UNION — the plain parent query; same rows, no `kind` column.
pub derive total(p: Person, a: Int) :- IncomeItem(p, a);

Read what the selector is, row by row. Built as a standalone file and queried with ox derive, report produces (verbatim):

derive(report): 6 tuple(s)
  (#i7582462787275748164, <anonymous>::IncomeItem, 1200)
  (#i7582462787275748164, <anonymous>::IncomeItem, 50000)
  (#i7582462787275748164, <anonymous>::Interest, 1200)
  (#i7582462787275748164, <anonymous>::Wages, 50000)
  (#i8648907253816210642, <anonymous>::IncomeItem, 30000)
  (#i8648907253816210642, <anonymous>::Wages, 30000)

The first column is the Person identity, printed as its stable content-addressed handle — #i7582… is alice, #i8648… is bob. The middle column is the relation each row was declared in — Wages, Interest, IncomeItem are relation values, not strings (a standalone file elaborates its relations under <anonymous>, so a member prints <anonymous>::Wages; inside a multi-module package it is the module path, e.g. model::Wages). Every concrete row also appears under IncomeItem itself: specializes is reflexive (a relation is a kind of itself) and the RFD 0005 closure copies each child tuple up into the parent’s extent, so the family selector legitimately witnesses both the leaf and the ancestor. The plain parent query total produces the same underlying rows without the category column — (#i7582…, 1200), (#i7582…, 50000), (#i8648…, 30000) — and nothing downstream can recover which member each came from once the union has merged them. That recovery is the entire reason to apply a relation-valued selector instead of naming the parent.

For one row per concrete member — dropping the reflexive parent witnesses — exclude the parent in the body (kind != IncomeItem narrows the proven domain; the specializes atom still supplies it, so the finite-domain proof holds):

pub type Person;

pub rel IncomeItem(mut p: Person, amount: Int);
pub rel Wages(mut p: Person, amount: Int)    <: IncomeItem;
pub rel Interest(mut p: Person, amount: Int) <: IncomeItem;

pub fact Person(alice);
pub fact Wages(alice, 50000);
pub fact Interest(alice, 1200);

// Leaf-only provenance: exclude the reflexive parent witness.
pub derive reportLeaf(p: Person, kind, a: Int) :-
    specializes(kind, IncomeItem), kind != IncomeItem, kind(p, a);

reportLeaf drops the IncomeItem rows, leaving one (p, kind, a) per concrete member — (#i7582…, <anonymous>::Interest, 1200), (#i7582…, <anonymous>::Wages, 50000) (again #i7582… is alice).

The generalized family query — each row once, by construction

The kind != IncomeItem idiom above is a workaround for a specific over-return: the bare specializes(kind, IncomeItem), kind(p, a) reads every candidate’s closed extent, and the parent’s closed extent already holds a copy of every member’s tuples (the RFD 0005 closure), so each concrete row surfaces twice — once under its declaring member, once under the reflexive parent. The canonical family query — the via sugar — names the family in one atom and reads each member’s own extent, so every row is returned once, under its declaring relation, by construction — no exclusion idiom, no dedup.

via is the spelling you write; it desugars to a generalized specializes atom that is the same query written out:

Parent( args ) via k   ≡   specializes( k( _… ) , Parent( args ) )

Each example below is shown as a pair — the via form and the equivalent generalized specializes form — with one shared meaning and one shared output; the two spellings produce byte-identical rows (a differential test pins this end to end). Every block parses on this branch; every output is ox build + ox derive, verbatim. The shared fixture:

pub type Person;

pub rel IncomeItem(mut p: Person, amount: Int);
pub rel Wages(mut p: Person, amount: Int)    <: IncomeItem;
pub rel Interest(mut p: Person, amount: Int) <: IncomeItem;

pub fact Person(alice);
pub fact Person(bob);
pub fact Wages(alice, 50000);
pub fact Interest(alice, 1200);
pub fact Wages(bob, 30000);
// A tuple asserted DIRECTLY on the parent relation — it arrives under
// `kind = IncomeItem`, not under any leaf member.
pub fact IncomeItem(alice, 500);

// A second family: engagements between an audit firm and its clients.
pub type Firm;
pub type Company;
pub rel Engagement(firm: Firm, client: Company);
pub rel AuditEngagement(firm: Firm, client: Company)      <: Engagement(firm = firm, client = client);
pub rel ConsultingEngagement(firm: Firm, client: Company) <: Engagement(firm = firm, client = client);
pub fact Firm(deloitte);
pub fact Firm(kpmg);
pub fact Company(acme);
pub fact Company(beta);
// deloitte both audits AND consults for acme; kpmg only audits beta.
pub fact AuditEngagement(deloitte, acme);
pub fact ConsultingEngagement(deloitte, acme);
pub fact AuditEngagement(kpmg, beta);

// ── Provenance: for each income row, also give me the relation it was
//    declared in. `via` (canonical) and its generalized form are one query.
pub derive report_via(p: Person, kind, a: Int) :-
    IncomeItem(p, a) via kind;
pub derive report_gen(p: Person, kind, a: Int) :-
    specializes(kind(p, a), IncomeItem(p, a));

// ── Guard as meaning: the same rows, but exclude tuples asserted directly
//    on the parent relation itself.
pub derive leaf_via(p: Person, kind, a: Int) :-
    IncomeItem(p, a) via kind, kind != IncomeItem;
pub derive leaf_gen(p: Person, kind, a: Int) :-
    specializes(kind(p, a), IncomeItem(p, a)), kind != IncomeItem;

// ── Multi-witness, witnesses DIFFER: the same firm serves the same client
//    under two different engagement categories — a firm may not both audit
//    and consult for one client (auditor independence).
pub derive independence_via(firm: Firm, client: Company) :-
    Engagement(firm, client) via k1, Engagement(firm, client) via k2, k1 != k2;
pub derive independence_gen(firm: Firm, client: Company) :-
    specializes(k1(firm, client), Engagement(firm, client)),
    specializes(k2(firm, client), Engagement(firm, client)), k1 != k2;

// ── Multi-witness, witness JOINS: two different people with income of the
//    SAME category — the witness `kind` is an ordinary join variable, shared
//    across both atoms rather than compared unequal.
pub derive sameCategory_via(p1: Person, p2: Person, kind) :-
    IncomeItem(p1, a1) via kind, IncomeItem(p2, a2) via kind, p1 != p2;
pub derive sameCategory_gen(p1: Person, p2: Person, kind) :-
    specializes(kind(p1, a1), IncomeItem(p1, a1)),
    specializes(kind(p2, a2), IncomeItem(p2, a2)), p1 != p2;

Provenance — for each income row, also give me the relation it was declared in. report_via and report_gen return the same rows: each family tuple exactly once — the three leaf rows and the directly-asserted parent row, under IncomeItem:

derive(report_via): 4 tuple(s)      # report_gen is byte-identical
  (#i7582462787275748164, <anonymous>::IncomeItem, 500)
  (#i7582462787275748164, <anonymous>::Interest, 1200)
  (#i7582462787275748164, <anonymous>::Wages, 50000)
  (#i8648907253816210642, <anonymous>::Wages, 30000)

Guard as meaning — the same, but only rows declared on a leaf member. leaf_via and leaf_gen add kind != IncomeItem and both drop the directly-asserted parent row:

derive(leaf_via): 3 tuple(s)        # leaf_gen is byte-identical
  (#i7582462787275748164, <anonymous>::Interest, 1200)
  (#i7582462787275748164, <anonymous>::Wages, 50000)
  (#i8648907253816210642, <anonymous>::Wages, 30000)

Note what the guard now means. Under the old bare closed-extent read, kind != IncomeItem corrected an artifact — it discarded the reflexive duplicate rows the closure copied up into the parent. Under the own-extent read those duplicates never exist, so the same guard now states a choice: exclude facts asserted directly on the parent relation (they arrive with kind = IncomeItem) and keep only the leaf members. Under the old read the guard corrected an artifact; under the family query it states a meaning — report includes the IncomeItem, 500 row, leaf excludes it.

Multi-witness, witnesses differ — the same firm serves the same client under two DIFFERENT engagement categories — a firm may not both audit and consult for one client. independence_via and independence_gen bind two witnesses over the same firm/client pair and require them distinct; only deloitte/acme qualifies (both audit and consult), kpmg/beta has one engagement kind:

derive(independence_via): 1 tuple(s)   # independence_gen is byte-identical
  (#i7895632145248339177, #i1312706375208229289)

The two handles are deloitte and acme. The parent query cannot express this. Engagement(f, c), Engagement(f, c) is the same union self-joined on itself — it holds whenever the firm has any engagement with the client, and two audit engagements alone would satisfy it. Only the witness distinguishes the categories: k1 != k2 demands two rows from different declaring relations, which is exactly “audit and also consult”.

The independence rule needs a proper-member guard when the parent carries direct facts. via is reflexive: a tuple asserted directly on Engagement arrives in the parent’s own extent with witness = Engagement. The fixture above has no direct-parent engagements, so its output is exact — but on a schema where firms are also recorded through a bare Engagement fact, a firm/client with one real member engagement plus a direct parent fact carries two distinct witnesses (Engagement and the member), and the rule above spuriously flags it though only one real engagement category exists. Add the same “exclude direct parent assertions” guard the reportLeaf example uses — k1 != Engagement, k2 != Engagement — so only genuine member categories count:

pub derive independence_unguarded(firm: Firm, client: Company) :-
    Engagement(firm, client) via k1, Engagement(firm, client) via k2, k1 != k2;
pub derive independence_guarded(firm: Firm, client: Company) :-
    Engagement(firm, client) via k1, Engagement(firm, client) via k2,
    k1 != k2, k1 != Engagement, k2 != Engagement;

With AuditEngagement(kpmg, beta) and a direct Engagement(kpmg, beta), the unguarded rule returns two rows — the genuine deloitte/acme and the spurious kpmg/beta — while the guarded rule returns only the genuine pair:

derive(independence_unguarded): 2 tuple(s)
derive(independence_guarded): 1 tuple(s)

Multi-witness, witness joins — two different people with income of the SAME category. Here the witness is an ordinary join variable — kind is shared across both atoms, not compared unequal. sameCategory_via and sameCategory_gen return the person pairs sharing a category (alice and bob both have Wages; each ordering appears once):

derive(sameCategory_via): 2 tuple(s)   # sameCategory_gen is byte-identical
  (#i7582462787275748164, #i8648907253816210642, <anonymous>::Wages)
  (#i8648907253816210642, #i7582462787275748164, <anonymous>::Wages)

The identity handles: #i7582… is alice, #i8648… is bob; the witness column is the relation each row was declared in, kept as a value (a standalone file elaborates under <anonymous>).

The legacy bare form, for contrast. The pre-existing two-argument specializes(kind, IncomeItem), kind(p, a) reads every candidate’s closed extent — so the parent’s closure copies surface alongside the members, returning each leaf row twice and the direct parent tuples once, seven rows for this fixture:

derive(report_bare): 7 tuple(s)
  (#i7582462787275748164, <anonymous>::IncomeItem, 500)
  (#i7582462787275748164, <anonymous>::IncomeItem, 1200)
  (#i7582462787275748164, <anonymous>::IncomeItem, 50000)
  (#i7582462787275748164, <anonymous>::Interest, 1200)
  (#i7582462787275748164, <anonymous>::Wages, 50000)
  (#i8648907253816210642, <anonymous>::IncomeItem, 30000)
  (#i8648907253816210642, <anonymous>::Wages, 30000)

This is the behavior the via / generalized own-extent form replaces: the three tiers are the bare two-argument form (legacy, closed extents, duplicates), the via sugar (canonical, own extents, each row once), and the generalized specializes form (via’s meaning, written out — identical rows).

Why the member frame is not a user spelling. The generalized specializes(k(memberArgs), Parent(parentArgs)) atom bounds k to the family, applies k in its own argument frame, and constrains the tuple in the parent’s frame; for an identity family the two frames have the same width, shared variables thread a column through both, and the correspondence is the declared subsumption mapping, never visual column position. The parent frame is information-complete — the mapping rules forbid dropped child ends, so every value a member carries is available in the parent frame. A member frame therefore binds nothing the parent frame does not already bind, which is why via plus the parent atom expresses every practical family query and the generalized form appears only as via’s desugar. The member frame becomes independently expressive only if subsumption mappings that drop a child’s ends are ever admitted — an open design question — at which point the general form is already specified and via remains its all-wildcard special case.

Rule of thumb. The parent atom alone is the union; + via k is the union plus which one; the generalized specializes(k(...), Parent(...)) form is the meaning of via, written out.

The via sugar reaches mapped members too — a member joined by a non-identity (argument-mapped) edge, whether a rename, a constant pin, or a subsort cast. A via family query reads such a member’s own extent and presents the rows in the parent’s frame, with the pinned / renamed / cast ends filled by the mapping and the answering member bound to the witness. The generalized specializes form with an explicit member frame still refuses (OE1416) for a non-identity member: that form ties the member frame positionally to the member’s own ends, which is sound only for an equal-arity identity member — it points the modeler at via, which is frame-agnostic. The witness member position must be a plain variable (OE1415 otherwise); the member frame’s width must match the parent’s arity (OE1414) and the parent frame’s width must match the parent relation’s declared arity (OE1418). A via k clause on an explicit specializes(...) atom is a misuse — via is itself the sugar for a specializes query — and refuses with OE1419; write one spelling or the other, not both.

A mapped family reads cleanly through via. With WagesUSA(p, a) <: IncomeItem(p, a, c = USD) (a constant pin), an incomeSource view over the parent family binds each row’s currency through the pin and its witness through the edge — no member-frame spelling, no dispatch:

use std::core::{type, rel};
pub type Person;
pub type Currency;
pub const USD: Currency;
pub rel IncomeItem(mut p: Person, mut amount: Int, mut c: Currency);
pub rel WagesUSA(mut p: Person, mut amount: Int) <: IncomeItem(p = p, amount = amount, c = USD);

pub fact Person(alice);
pub fact Currency(USD);
pub fact WagesUSA(alice, 500);

// Reads the mapped member through φ: `c` is filled by the pin, `kind` by the edge.
pub derive incomeSource(p: Person, a: Int, c: Currency, kind) :- IncomeItem(p, a, c) via kind;

incomeSource(alice, 500, USD, WagesUSA)

The USD came from the pin (the member never stores it), and kind is WagesUSA — the member that answered.

Don’t-care ends in a family query — the anonymous wildcard _. A parent frame does not have to bind every end. When you only want which member answered — not the amount, not the currency — write _ for each end you don’t care about. This is the natural query for provenance: “who has income, and from which kind of source?” ignores the figures entirely. The wildcard is a genuine don’t-care in the family-query frame, one anonymous slot per _, so an all-_-but-one frame is not mistaken for a lower-arity query.

The fixture carries a pinned member (WagesUSA, currency pinned to USD) and an identity member (ForeignIncome, currency passed through):

use std::core::{type, rel};
pub type Person;
pub type Currency;
pub const USD: Currency;
pub const EUR: Currency;
pub rel IncomeItem(mut p: Person, mut amount: Int, mut c: Currency);
pub rel WagesUSA(mut p: Person, mut amount: Int) <: IncomeItem(p = p, amount = amount, c = USD);
pub rel ForeignIncome(mut p: Person, mut amount: Int, mut c: Currency) <: IncomeItem(p = p, amount = amount, c = c);

pub fact Person(alice);
pub fact Person(bob);
pub fact Currency(USD);
pub fact Currency(EUR);
pub fact WagesUSA(alice, 500);
pub fact ForeignIncome(bob, 300, EUR);

// Who has income, and from which kind? Amount and currency are don't-cares.
pub derive whoHasIncome(p, kind) :- IncomeItem(p, _, _) via kind;
// Keep the amount, still ignore the (pinned or passed-through) currency.
pub derive amountAndKind(p, a, kind) :- IncomeItem(p, a, _) via kind;

whoHasIncome drops both figure ends and returns one row per person with the answering member — alice earns WagesUSA, bob earns ForeignIncome:

derive(whoHasIncome): 2 tuple(s)
  (#i7582462787275748164, <anonymous>::WagesUSA)
  (#i8648907253816210642, <anonymous>::ForeignIncome)

amountAndKind keeps the amount and still ignores the currency — useful precisely because the currency is pinned on WagesUSA (the member never stores it) and passed through on ForeignIncome; a single _ reads across both shapes without naming a column that one member fills by a pin and the other by an end:

derive(amountAndKind): 2 tuple(s)
  (#i7582462787275748164, 500, <anonymous>::WagesUSA)
  (#i8648907253816210642, 300, <anonymous>::ForeignIncome)

#i7582… is alice, #i8648… is bob. The wildcard behaves the same in a via family query as in a plain parent atom: it matches any value and binds nothing.

A subsumption edge may not drop a child end — use a derive view instead. A mapping must reference every declared child end (a rename or a cast source; a child end may feed several parent ends — a diagonal — but never none). Dropping one is refused at the declaration with OE1421:

use std::core::{type, rel};
pub type Person;
pub type Currency;
pub type Text;
pub const USD: Currency;
pub rel IncomeItem(mut p: Person, mut amount: Int, mut c: Currency);
pub rel Bad(mut p: Person, mut amount: Int, mut note: Text) <: IncomeItem(p = p, amount = amount, c = USD);
//                                          ^ OE1421 — child end `note` is referenced by no filler

OE1421: subsumption of `Bad` onto `IncomeItem` drops child end `note` — dropping an end inside a subsumption edge would merge distinct `Bad` facts (differing only at `note`) into one `IncomeItem` row, so it is refused. Fix, in order: (1) if `Bad` genuinely belongs to the `IncomeItem` family, reference every child end in the filler list (a rename or a cast source; a diagonal may reference one child end at several parent ends); (2) if a lossy projection is intended, write a derive rule instead — a projection VIEW is not family membership, e.g. `pub derive view(p, a) :- Bad(p, a, _);`

Why every child end must be referenced (φ-injectivity). The mapping φ translates each child tuple to a parent image. A dropped end makes φ non-injective: two child tuples that differ only at the dropped end collapse to the same parent image with no declared meaning for the collapse, and — because a relation’s extent is a set — merge into one parent row that any aggregate over the family then counts once. Worse, the §D4 withdrawal cascade relies on the child identity the dropped end carried — a distinction the collapse erases at the parent image, so the cascade can no longer tell the two child tuples apart. Requiring every child end (each fed to at least one parent end) keeps φ injective on the distinct-child-tuple part of the domain, which is exactly what family membership must preserve. A diagonal is still injective: reusing one child end at several parent ends duplicates a value into the image but discards nothing.

The derive view is the honest spelling of a lossy projection. The OE1421 remedy — pub derive view(p, a) :- Bad(p, a, _); — is a rule, not a family edge, so it is explicit that it forgets note and is not Bad’s membership in a family. It also makes the merge visible where it happens: two Bad facts that agree on (p, a) and differ only in note project to one view row.

use std::core::{type, rel};
pub type Person;
pub type Text;
pub rel Bad(mut p: Person, mut amount: Int, mut note: Text);

pub fact Person(alice);
pub fact Text(memoA);
pub fact Text(memoB);
pub fact Bad(alice, 500, memoA);
pub fact Bad(alice, 500, memoB);

pub derive view(p: Person, a: Int) :- Bad(p, a, _);

view(alice, 500)

One row, not two — the two notes are projected away by the derive, exactly the merge a dropped-end edge would have performed silently. A dedicated projection marker on a subsumption edge (a surface way to declare “this edge intentionally forgets an end”) is a reserved design under consideration in the mapped-relation-subsumption design record and is not yet a surface form; until it lands, the derive view is the spelling.

Multiplicity is a schema choice, and aggregates read it. The merge above is the same set-membership rule an aggregate obeys: whether a family sum double-counts two payments is decided by the schema, not the query. A relation Payment(mut p: Person, mut amount: Int) with two facts Payment(alice, 500) twice holds one proposition and sums to 500; add a distinguishing source end — Payment(mut p: Person, mut amount: Int, mut src: Source) with s1/s2 — and the two payments are distinct rows summing to 1000. This is the same trap the relations chapter draws out for family images; the fix is identical (keep a distinguishing end, do not pin it away). Grouping such an aggregate by the family witness is not yet expressible: a via clause is not admitted inside an aggregate comprehension, and threading the witness through an intermediate derive trips the finite-domain proof on the selector column — so per-witness totals are computed today by aggregating each leaf member directly, not by grouping a parent-family sum on kind.

Two clarifications on the selector. kind is an ordinary rule variable, not a keyword — name it anything (r, src, which). And it takes no type annotation: like every rule variable its type is inferred from where it stands — appearing as the family member in specializes(kind, IncomeItem) constrains it to that family, the compiler establishes the complete closed set of member relations at build time (the finite-domain proof; a selector it cannot pin to a finite exhaustive set is refused with OE1386, below), and refuses the rule if it cannot.

Two further cases need the selector in body position, not the head. Per-member differentiated logic — the same selector applied twice, or joined against a per-member table, so the rule branches on which relation matched (specializes(kind, Loc), kind(p, c), priority(kind, n)). Families not modeled by subsumption — members collected by a rel/arm/meta reflection atom (a shared metarel or endpoint signature) rather than a <: edge, where no single parent relation exists to query. A pinned singleton (r == Home) reads exactly one relation’s tuples and is the degenerate case of the same dispatch:

pub type Person;
pub type City;

pub rel Home(p: Person, c: City);

// Singleton: equality with the relation literal `Home` pins `r`, so
// the application reads exactly `Home`'s tuples.
pub derive homed(p: Person, c: City) :- r == Home, r(p, c);

The candidate set must be statically proven — Argon refuses rather than guess a domain or evaluate an open dispatch. A selector bound only by a constraint that proves no finite exhaustive set (an inequality binds r as a value variable but enumerates nothing) is refused with OE1386:

pub type Person;
pub type City;

pub rel Loc(p: Person, c: City);

// `r != Loc` binds `r` but proves no finite exhaustive relation domain.
pub derive anywhere(p: Person, c: City) :- r != Loc, r(p, c);

A value proven not to denote a relation (pinned to an Int, a String, a struct value, …) applied in predicate position is refused with OE1387:

pub type Person;
pub type City;

pub rel Loc(p: Person, c: City);

// `r` is pinned to the integer 3 — not a relation value.
pub derive anywhere(p: Person, c: City) :- r == 3, r(p, c);

A negated relation-value application must be safe: the selector and every tuple argument must be positively range-restricted outside the negation. An argument (or the selector) bound only inside the not is refused with OE1391:

pub type Person;
pub type City;

pub rel Loc(p: Person, c: City);
pub rel Home(p: Person, c: City) <: Loc;

// `c` appears ONLY inside the negation — the negated dispatch is unsafe.
pub derive unhoused(p: Person) :- p : Person, specializes(r, Loc), not r(p, c);

The remaining refusals in the family are structural, and each guards against a silent misderivation the dispatch would otherwise produce:

• An application whose argument count matches no candidate’s arity is OE1388. With the wrong tuple width there is no coherent pairing of arguments to a candidate’s columns, so a dispatch built anyway would read misaligned columns (or an always-empty relation) — a wrong answer, not an error.
• An argument category-incompatible with a candidate’s declared endpoint is OE1389 (e.g. a text literal against an Int column). Such a candidate can never match the tuple; dispatching over it would either drop rows the modeler expected or force a type-incoherent join, again silently.
• A family containing a relation not lexically accessible from the applying module is OE1390. A dispatch that silently dropped the inaccessible candidate would change the rule’s meaning based on visibility — the family it reads would depend on who is looking, so the whole application is refused rather than narrowed.
• A candidate whose signature metadata (arity, endpoints, visibility) is unavailable to the build — a relation carried by an artifact too old to record it — is OE1393. The dispatch cannot be proven sound without that metadata, so Argon refuses rather than guess it (App. C).

pub fact targets a base predicate, never a derived one. A derive / query head is a valid rule-body atom (it is in the resolution set above), but it is not a valid pub fact target. pub fact asserts into an extensional relation (a concept-as-classification or a pub rel); a derived predicate’s extent is intensional — computed by rule derivation. A pub fact P(...) whose P is a pub derive / pub query head is refused with OE0239 FactReferencesDerivedPredicate: the asserted seed tuple would key a different relation node than the rule head reads, so it would silently drop out of the rule’s fixpoint — the derive would evaluate to a result that omits the asserted tuples (no error, wrong answer). To give a derived predicate ground tuples that participate in its derivation, use one of two sanctioned forms, and OE0239’s help names both:

• A bodiless pub derive P(args); clause over concrete arguments (derive). The seed tuple is itself a derive clause on P, so it shares P’s relation node and participates directly in P’s fixpoint — the simplest way to seed P itself.
• A base relation the rule reads — declare pub rel Base(...), seed it with pub fact Base(...), and add a clause pub derive P(...) :- Base(...). Use this when the seed tuples are themselves a reusable extensional predicate.

Either keeps P a single-origin intensional head (the same rule Build pipeline and .oxbin enforces for a foreign-placed-vs-derived relation, OE1246). (A pub fact over a check head is the ordinary OE0220 — a check head is observer-only, not a predicate at all.)

Build loud-gate. More broadly, ox build refuses (writing no .oxbin) any derive / query rule the engine does not evaluate — an unsupported quantifier shape, a nested or non-count-class aggregate, not <aggregate>, an unsupported type-test or meta-eq (OE1311–OE1315). Argon refuses rather than emit an artifact that would silently mis-derive; see Build pipeline and .oxbin.

Modal atoms (box(...), diamond(...)) carry Kripke-frame semantics over the standpoint and classification frames described in Modal operators. The elaborator statically discharges the common case (type-classification atoms whose target is introduced by a fixed metatype — membership constant, RFD 0027 D6) and routes the remainder to a modal reasoner over std::kripke. Modal atoms are admitted only at tier:modal; lower tiers reject them.

Restricted universals (forall v: T where Body, Head). In the where body the last atom is the consequent (Head) and all preceding atoms are the domain restriction (Body). The quantifier holds iff every domain element also satisfies the consequent — it lowers to the count-equality count{ v : Body, Head } == count{ v : Body } (the domain-and-consequent count equals the domain count). The type annotation T is the static sort of v; the runtime domain comes from the where Body, so the Body must restrict v with a membership or predicate atom (e.g. member(g, v) or v in g.items) — Body, not T, bounds the count. An empty domain (count{ v : Body } == 0) makes the universal vacuously true (0 == 0), deriving the head — classical restricted-∀ semantics. The encoding needs at least a domain atom and a consequent (≥2 where atoms); the paren restriction form forall(path, T), the exists-binder form, and a single-atom where refuse with OE1315 (App. C).

Allen interval relations (before, meets, overlaps, during, starts, finishes, and their reciprocals) are not substrate operators. They are provided by the std::allen library (RFD 0024), defined over the Date / Duration value layer (Temporal substrate) — ordinary predicates over interval endpoints, not parser-level syntax.

Three atom shapes in the grammar above parse-refuse rather than silently mis-derive:

• Role closure field-path ('+'|'*') '(' … ')' (e.g. p.knows+(q: Person)). The base role-invocation form field-path '(' Ident (':' type-expr)? ')' is accepted; the transitive (+) / reflexive-transitive (*) closure suffix refuses with OE0001. Express transitive reachability through a recursive derive head.
• Axis sugar path '::' Ident (x :: T, i.e. meta(x) == T). Write the meta(x) == T comparison atom directly; the :: rule-atom shorthand refuses. (In value position EnumName::Variant is unaffected — see the payloadless-enum-constant note above.)
• Range membership field-path 'not'? 'in' <range> (p.v in 1..10). The set/list RHS of in is accepted; a lo..hi range RHS refuses (OE0001 on ..). Write the two-sided comparison p.v >= 1, p.v <= 10 instead.

Temporal rule atoms

Argon’s bitemporal substrate (Temporal substrate) admits metric temporal operators in rule bodies — the DatalogMTL fragment with stratified negation over the integer timeline.

Any atom may be qualified by a valid-time point or interval: atom at t (a single VT point), atom during [t1, t2] (a closed VT interval), atom since t (the open interval [t, ∞]).

Six prefix metric operators address past and future. Their interval bounds are durations (0, N with a unit ns…y, or inf/∞):

box_minus     [a, b] (φ)         // φ held at every past point in [a, b]
diamond_minus [a, b] (φ)         // φ held at some past point in [a, b]
box_plus      [a, b] (φ)         // φ holds at every future point in [a, b]
diamond_plus  [a, b] (φ)         // φ holds at some future point in [a, b]
since         [a, b] (φ, ψ)      // φ has held since ψ within [a, b]
until         [a, b] (φ, ψ)      // φ holds until ψ within [a, b]

Two shortcuts expand to [0, ∞] intervals: ever atom (some past or future point; needs tier: expressive for the disjunction) and always atom (every point; tier: recursive).

Side-by-side modal (box/diamond) and metric temporal atoms in one body compose additively. Nesting one family inside the other is refused at tier: recursive and routed to tier: fol — see Tier ladder for the decidability rule (OE0712).

query

query-decl ::= attribute* 'pub'? 'query' Ident '(' param-list ')' '->' TypeExpr
               ('across' '[' standpoint (',' …)* ']')?
               '{' query-body '}'
query-body ::= ('with' Ident '=' query-body ';')*
               'select' projection
               'from' rule-body                                    // Rule-atom grammar
               ('optional' 'from' rule-body)*
               ('where' rule-body)?                                // additional atoms
               ('group' 'by' expr ('having' expr)?)?
               ('order' 'by' expr ('asc' | 'desc')?)?
               ('limit' Nat ('offset' Nat)?)?
projection ::= expr | '{' struct-init-list '}' | 'path' Ident | aggregate
role-step  ::= Ident quantifier? ('(' role-binders ')')? ('as' Ident)? mode-spec?
quantifier ::= '+' | '*' | '{' expr (',' expr)? '}'                // expr of type Nat
mode-spec  ::= 'mode' ('walk' | 'trail' | 'acyclic' | 'simple')
            |  'shortest' | 'all-shortest' | 'any' | 'k-shortest' Nat

Role-step path-traversal chains (a.role+(b), c.ParentOf{1, n}(p: Person)) are admitted as predicate-call atoms in the rule-atom grammar (Rule-atom grammar) and are not separately defined here.

The evaluated query-body is select … from … (where …)?. Every other form parse-refuses loudly with a feature-named code — never a generic OE0001, never silently ignored: the result-shaping clauses (group by … having, order by … asc|desc, limit … offset) with OE0007; the with CTE clause with OE1344; the graph-/path-traversal projections (select shortest path …, select path …, … as <name> mode …) with OE1345; optional from with OE1346; and the result-table set operators (union / union all / intersect / except) with OE1347.

pub query active_leases_for(t: Person) -> [Lease] {
    select l from l: Lease, l.tenant == t where is_active(l)
}

pub query ancestors_within(p: Person, n: Nat) -> Set<Person> {
    select a from p.ParentOf{1, n}(a: Person)
}

pub query shortest_route(a: City, b: City) -> Path<City, Road> {
    select shortest path r from a.road+(b) as r
}

pub query avg_age_by_dept() -> Map<Department, Real> {
    select { dept: avg(p.age) }
    from p: Person, p.works_in(dept: Department)
    group by dept
}

pub query rich_friends_of(p: Person) -> Set<Person> {
    with rich = select x from x: Person where x.net_worth > 1_000_000;
    select f from p.knows(f: Person) where f in rich
}

pub query agreed_across(p: Person) -> Truth4Of<Bool>
    across [LegalGround, MedicalGround]
{
    select consents(p)
}

Subquery forms. Brace-bracketed inner queries used as expressions:

subquery      ::= subquery-kind '{' rule-body '}'                   // Rule-atom grammar; no `from` keyword
subquery-kind ::= 'collect' | 'set' | 'one' | 'count' | 'exists'

The subquery body is a bare rule-atom list — there is no from keyword inside the braces (that prefix belongs to the top-level query-body only; an inner from parse-refuses with OE0001).

The cardinality-fold kinds count and exists evaluate over the bare atom list above (count { p: Person }, exists { p: Person }). The projection-carrying kinds collect / set / one parse but refuse at ox check / ox build (OE1312); they never silently lower to a cardinality fold. Use a derive head plus a top-level query projection.

Set operations on result tables: union, union all, intersect, except.

Subquery aggregates (admitted as aggregate projections inside subquery bodies and as the subquery-form <aggregate> { atoms }): count, count distinct, sum, avg, min, max, collect, set_collect, string_join, percentile. The expression-level comprehension form sum(expr for x in coll where pred) (Expression grammar) admits a subset (sum, count, min, max, avg) for non-subquery contexts.

Default lattice context: K3. With across [...]: FDE.

mutate

mutate-decl ::= attribute* 'pub'? 'mutate' Ident '(' param-list ')' ('->' TypeExpr)?
                '{' mutate-body '}'
mutate-body ::= ('require' '{' expr (',' …)* '}')?
                stmt*
                ('return' expr ';')?
stmt        ::= 'let' Ident (':' TypeExpr)? '=' expr ';'
             |  'match' expr '{' arm (',' …)* '}'
             |  insert-stmt | update-stmt | delete-stmt | upsert-stmt | amend-stmt
             |  'detach' 'delete' expr ';'                                  // ‡ refused, OE1353
             |  emit-stmt
             |  'for' Ident 'in' expr '{' stmt* '}'
             |  'if' expr '{' stmt* '}' ('else' '{' stmt* '}')?
             |  expr ';'
insert-stmt ::= 'insert' TypeExpr '{' field-init-list '}' ';'              // typed-literal insert
             |  'insert' TypeExpr '{' '..' expr (',' field-init-list)? '}' ';'  // spread: seed from a struct value
             |  'insert' Ident ':' TypeExpr '{' field-init-list '}' ';'   // ‡ named typed-literal — OE0001
             |  'insert' Ident 'into' expr ';'                             // insert binding into collection
             |  'insert' predicate-call '{' field-init-list '}' ';'        // relation insert with body
             |  'insert' predicate-call ';'                                // relation insert, no body
update-stmt ::= 'update' (Ident | pattern) 'set' '{' field-assign (',' …)* '}' ('where' expr)? ';'
field-assign ::= Ident ('=' | '+=' | '-=') expr
delete-stmt ::= 'delete' predicate-call ';'                                // delete iof(…) / delete Rel(…)
             |  'delete' (Ident | pattern) ('where' expr)? ';'             // ‡ entity / bulk delete — OE0001
upsert-stmt ::= 'upsert' pattern ('as' Ident)? upsert-clause+ ';'          // ‡ refused, OE1352
upsert-clause ::= 'on' 'insert' '{' field-assign (',' …)* '}'
               |  'on' 'update' '{' field-assign (',' …)* '}'
emit-stmt   ::= 'emit' Ident '{' expr '}' ';'
amend-stmt  ::= 'amend' predicate-call ';'                                 // belief-time withdrawal (RFD 0076)
             |  'amend' predicate-call '=>' predicate-call ';'             // atomic withdraw + correct

pub mutate sign_lease(t: Person, p: Property, rent: Money, term_days: Nat) -> Lease {
    require { rent > 0, term_days > 0 }
    let l = insert Lease(t, p) {
        monthly_rent: rent,
        start:        today(),
        end:          today() + term_days.days,
        status:       Pending,
    };
    emit AuditLog { LeaseSigned { lease: l, at: now() } };
    return l;
}

pub mutate hire_or_raise(p: Person, o: Organization, salary: Money) {
    upsert p.works_at(o) as emp
        on insert { emp.start_date = now(), emp.salary = salary }
        on update { emp.salary = salary };
}

pub mutate rebrand(old: String, new: String) {
    update c: Company set { name = new } where c.name == old;
}

An update of a bound target writes its mut fields directly. The ('where' expr)? filter (and the bulk/pattern target forms it implies, as in rebrand above) is refused at ox check / ox build (OE1318), never silently dropped.

The grammar shapes marked ‡ are loud refusals, not silent no-ops. Named typed-literal insert (insert l: Lease { … }; use let l = insert Lease { … } instead) and entity/bulk delete of a bound target or pattern with an optional where refuse with OE0001 — only delete predicate-call (delete iof(…) / delete Rel(…)) is admitted. detach delete refuses with OE1353 and upsert with OE1352.

delete Rel(…) and insert Rel(…) additionally pass the relation-end mutability gates (RFD 0076, Relations): a matched delete on a relation with any effectively-immutable end refuses at the write path with OE1402 (an unmatched delete stays an idempotent no-op), and an insert adding a new value at an immutable end whose endpoint fiber an earlier transaction already initialized refuses with OE1403 — checked before the OE1341 cardinality cap, atomically, so a refused body commits nothing. The gates read the closed extent: an insert into a subrelation is gated against every superrelation’s fiber too (still OE1403), and a premise write whose rule-derived consequences would vary an immutable-ended declared relation’s extent — retract a derived binding whose dependent context survives, or grow an initialized derived fiber — refuses the whole body with OE1397, even though no statement names that relation. The initialization set itself remains governed by the declared cardinality: on an immutable end the fiber’s value set freezes at its first asserting transaction, so a declared minimum of two or more is decidable exactly there — a body that initializes such a fiber with fewer distinct values refuses with OE1398 (the frozen set could never grow to complete it), whichever route initializes it: a direct insert, a subrelation insert, a rule-derived initialization, or a static fact set at build. A mutable end’s minimum keeps the deferred OW1342 posture.

The relation-end mutability write gates — the ones that admit or refuse a delete R(…) / insert R(…) against an immutable end, and the individual retraction that would strand an immutable-ended binding (OE1402–OE1404) — are enforced by oxc-runtime in its end_mutability module; see relations for the rule they enforce.

The rebrand example assumes name is declared mut on Company. Per struct and enum — language built-ins (data declarations), fields are immutable post-construction unless explicitly marked mut:

pub type Company {
    #[intrinsic] founded: Date,    // construction-required; not updatable
    mut name: String,              // updatable via `update`-stmt
}

update-stmt admits writes only to mut fields. A field-assign targeting a non-mut field is rejected with OE0820 UpdateImmutableField. The elaborator validates each field-assign against the entity’s field-decl mut flag; rejection surfaces at build time, not at mutation invocation.

Insert from a pre-built value — the ..v spread

Concept construction is fused to insertion: there is no bare construction expression of concept type. Constructor machinery therefore lives in fns over struct values (struct and enum — language built-ins (data declarations)) — and the spread form lets such a value feed an insert without re-spelling every field:

pub type Person { name: String, age: Int }
pub struct PersonSeed { name: String, age: Int }

pub fn seed() -> PersonSeed = PersonSeed { name: "Ada", age: 36 };

pub mutate admit() -> Person {
    let v = seed();
    return insert Person { ..v, age: 37 };   // seed's fields, age overridden
}

The base v must evaluate to a struct value; its fields seed the field-init set by exact field name against the target’s declared fields (the whole <: chain — an inherited field is a match), and the explicit field: value initializers override same-named seeds, in either textual order. The merge happens before the construction gates, so the spread is field-init sugar and nothing downstream can tell the forms apart: required- field completeness (OE0207), primitive-refinement invariants (OE0668), abstract-type refusal (OE0233), fixed classification (OE0234), the value/individual boundary (OE0248), and declared-field validation all fire over the merged set exactly as the longhand spelling, and identity is still minted only by the event log at insert. There is no first-class unpersisted individual: the struct value is pure data (no identity) until the insert constructs the concept individual from it.

Field-name matching is total and loud, never lossy:

• A required target field that neither the base nor an explicit initializer supplies refuses with OE0207, same as omitting it longhand.
• An optional target field (T?) the base does not carry simply stays absent — no phantom write.
• A source field with no declared target field (on the concept or any <: ancestor) refuses with OE0261 InsertSpreadFieldUndeclared: data the source value carries never silently vanishes on insert.
• A base that is not a struct value — a scalar, an individual, an enum constant — refuses with OE0260 InsertSpreadSourceNotStruct.
• More than one spread in one init list refuses at ox check / ox build with OE0263 StructLitMultipleSpreads (a second spread has no defined merge order); the same refusal governs the value struct literal’s functional-update spread. Combine the sources into one struct value first, then spread that.

The base is an ordinary body value position: a deductive read there refuses with OE1371 and an unbound name with OE1383, exactly as a field initializer would. mut on a target field is orthogonal — construction may set mut and non-mut fields alike, spread-fed or explicit.

The relation-insert-with-body form (insert P(a, b) { … }) does not take a spread while that host form itself refuses (OE0001); the field-init merge extends to it when the body form lands.

Field updates lower to append-only event pairs on the underlying property axiom (Storage layer): a retract event for the prior value and an assert event for the new. The proposition’s logical identity is the (entity_id, property_id) pair; the value is what changes. Bitemporal queries reconstruct prior values per Temporal substrate.

Mutations are transactional within the body; the kernel may reject mutations that violate refinement, consistency policy, or stratification — rejection surfaces to the caller as Result<T, Diagnostic> from the host runtime.

Dynamic reclassification — insert iof / delete iof. Because iof is a first-class predicate (Reflection), mutate bodies can dynamically classify and declassify entities by inserting or deleting iof tuples through the existing insert predicate-call / delete predicate-call forms:

pub mutate enrol(p: Person) {
    insert iof(p, Student);                  // p is now a Student
}

pub mutate expel(s: Student) {
    delete iof(s, Student);                  // s is no longer a Student
}

The single-type insert iof(x, T) / delete iof(x, T) forms above classify and declassify an entity, subject to the gates below. Inserting an iof tuple over a relation concept — insert iof((p, into), EnrolledAt) for a named relation EnrolledAt — refuses: the tuple-argument form parse-refuses with OE0001 rather than silently doing nothing.

The substrate enforces two constraints on insert iof(x, T):

1. Refinement gate (enforced). If T carries a defined refinement iff { … } (Refinement) — for example, pub type ExtinctSpecies <: BirdSpecies iff { self.numberOfLivingInstances == 0 } — the predicate is the substrate’s source of truth for membership: the modeler updates the underlying state (here, numberOfLivingInstances) and the substrate derives the iof classification automatically, so explicit insert iof(x, ExtinctSpecies) emits OE0211 IofInsertOnDefined and the mutation is rejected. If instead T carries a primitive refinement where { … }, membership is conferred by assertion, so insert iof(x, T) is permitted — but the predicate is a necessary invariant: an x that positively violates it (definite false, World assumptions (CWA / OWA)) is rejected with OE0668 RefinementInvariantViolated. The same invariant is checked when a primitive-where member is created by construction (insert T { … }) or when an update writes a field the predicate reads.
2. Modifier gates (enforced — RFD 0027 D6). Re-classification is governed by the ontology-neutral fixed modifier on the target’s introducing metatype (metatype), never by any axis name: insert iof(x, T) / delete iof(x, T) where T is fixed-introduced is refused with OE0234 FixedReclassification — classification under such types is decided at construction (insert <T> { … } remains legal; construction is not re-classification). Admission is the absence of fixed: dynamic classification is the default, and a vocabulary opts its rigid metatypes into the restriction explicitly (pub fixed metatype kind = { … };) — an axis assignment like rigidity::anti_rigid is inert user vocabulary and grants nothing by itself. Likewise insert iof(x, T) against an abstract type — a direct instance — is refused with OE0233 AbstractTypeConstruct; non-abstract subtypes are unaffected. Both gates fire at ox check / ox build where the target is statically known and at the runtime write path otherwise, rejecting the whole mutation atomically. The membership-constancy theorem (Argon.Runtime.ModifierGates.runMutation_fixed_iof_constant) is what grounds static modal discharge over fixed-introduced types (Modal operators).
3. Compatibility gate. x’s existing classification chain must include some supertype that T specializes (e.g. Student <: Person requires x: Person).

After insert iof(x, T), the entity x is classified under both its prior types and T. After delete iof(x, T), x is no longer classified under T but retains all other classifications. The substrate maintains a single global iof relation; insert/delete operate transactionally.

Bitemporal mutation forms. Per the temporal substrate (Temporal substrate, Effective-dating: valid time and the two as_of axes), an insert may carry an explicit valid-time at <date> qualifier — the assertion’s valid time begins on that civil day (RP-004 mutate). This form executes, on every insert arm: the write threads the date onto the event’s bitemporal extent, and an as_of <#date#> query reads it back. A typed-literal insert (insert T { … } at <date>, with or without the ..v spread) stamps the constructed individual’s membership and every field assertion with the same valid time, and an op-level qualifier wins over the call-level default valid-time an embedder supplies for the whole mutation (explicit intent over the per-call backdate).

pub type T;
pub type Evt { tag: String? }
pub mutate enact(x: T, effective: Date) {
    insert iof(x, T);                        // [VT: now → ∞]  [TT: now → ∞]  — atemporal default
    insert iof(x, T) at effective;           // [VT: effective → ∞]            — effective-dated
    insert Evt { tag: "x" } at effective;    // membership + fields, all [VT: effective → ∞]
}

The window form during [t1, t2] and a valid-time-qualified delete (bitemporal retraction — closing a valid-time interval rather than opening one) refuse loudly (OE1330) rather than silently applying at all valid times; the since <date> open-interval form executes on inserts, equivalently to at (an open interval from the anchor):

pub type T;
pub mutate retro(x: T) {
    insert iof(x, T) during #2020-09-01#;   // window VT
}

Explicit erasure — forget. For compliance scenarios (GDPR right-to-erasure, sensitive-data redaction), forget removes the underlying tuple including its bitemporal history — removed from every served read and every write gate; the durable-replay journal retains the erased bytes closed (see the gate-and-read surface below):

forget x;                                               // bound individual; capability-gated

Only the bound-individual form forget <expr> is admitted; the forget iof(x, T) and bulk forget … where … shapes refuse with OE0001.

forget is capability-gated at the source level: a mutate body containing forget refuses to build (OE0730 ForgetWithoutCapability) unless the enclosing mutate declaration grants #[allow_forget]. Cascading derived facts are revised via DRed overdelete.

Erasure is measured at the gate-and-read surface: after forget x, no assert-polarity event on any plane or polarity introduces or references x (relation arguments are walked into nested collection values), and x’s pre-existing closing retractions are erased with their asserts. Each erased live event leaves one freshly-minted extent-closing retraction event — a body clone whose closed assert no longer exists, the receipt the durable-replay journal needs so a reopened store drops the re-added assert instead of resurrecting it — and the durable journal retains the erased history closed rather than expunging bytes. Neither replay artifact is served by a read or consulted by a write gate.

The capability does not exempt forget from the relation-end mutability gates (RFD 0076): erasing an individual bound at an effectively-immutable relation end while that end’s dependent context (the individuals at every other position) survives the transaction refuses with OE1404 — erasure may not stand in for the refused cascade. The dependent may cease in the same transaction through either channel (a logical retraction or another forget), and the gate reads every standpoint plane, exactly the planes the erasure sweeps. Erasing the dependent individual itself is the legal direction and takes its incident bindings with it.

Reasserting a tuple after retraction produces distinct VT intervals on the underlying store — the substrate does not coalesce on adjacent boundaries. Historical retract/reassert is queryable via audit projections.

Individual retraction — retract. retract ends one or more individual lifetimes and cascades their incident relation bindings. Two source forms lower to the kernel RetractIndividuals effect (RFD 0076):

retract x;              // a single individual
retract {x, y};         // an atomic set — one cessation set, one coverage gate

Every retract (and forget) target in a body joins ONE transaction-wide cessation set, gated once for immutable-end coverage: for a both-immutable binary relation, retracting only one endpoint refuses OE1404 (the surviving endpoint is its dependent context), while retract {x, y}; — or two separate retract statements naming x and y — covers both. A retract inside an if branch, a for body, or a match arm joins that same union. Re-introducing a retracted individual later in the same body — a re-classification, a relation endpoint, or a property write — refuses OE1400; an assert-then-retract nets clean and is admitted. Duplicate targets are idempotent.

Belief-time correction — amend. delete ends a binding’s valid time (it stopped being true); amend corrects the record (it was never true — a mis-recorded assertion, false ab initio). The two are deliberately distinct verbs so a correction can never be mistaken for a valid-time deletion. amend withdraws the assertion as false ab initio, releasing its contribution to any relation-end freeze (RFD 0076), while the bitemporal history retains what-was-believed-when — an auditable correction, not an erasure:

pub type Person;
pub rel bornTo(mut child: Person, mother: Person) [0..*] [1];

#[allow_amend]
pub mutate rescind(child: Person, wrong: Person) {
    amend bornTo(child, wrong);                          // withdrawal — truth unknown
}

#[allow_amend]
pub mutate correct(child: Person, wrong: Person, right: Person) {
    amend bornTo(child, wrong) => bornTo(child, right);  // atomic withdraw + correct
}

The primitive amend R(args); withdraws positive evidence (the proposition returns to unknown, not refuted). The composite amend R(args) => R(args'); withdraws and asserts the corrected proposition against one transaction-time view, all-or-nothing (a refused corrected assertion commits nothing). Like forget, amend is capability-gated at the source level: a mutate body using it refuses to build (OE1405 AmendWithoutCapability) unless the enclosing mutate declaration grants #[allow_amend]; correction authority is further authorized per invoking principal, target-scoped, at the serving layer. Amendment is validated against one net corrected view of the transaction (withdrawals subtracted, corrected assertions and lifecycle effects overlaid), so it grants no coverage exemption to a companion cascade. Amending an established immutable fiber below its declared minimum refuses with OE1407; amending a purely rule-derived tuple (no asserted event to correct) refuses with OE1406. The composite corrects a fact of one relation: its withdrawal and correction must name the same relation, so a cross-relation amend R(old) => S(new) refuses at build with OE1409 (to change facts across two relations, delete one and insert the other). Correcting a refutation (not_fact) is deferred to the negative-facts mutation surface; amend here corrects positive relation assertions. An amendment releases exactly the one assertion it named — an assertion is an event, not a value-for-all-time — so a later re-assertion of the same tuple is a fresh initialization that re-freezes its immutable fiber: after amend R(a); insert R(a); a subsequent insert R(a') refuses (OE1403) exactly as it would with no amendment, whereas amend R(a); insert R(a'); directly (no intervening re-assertion) admits.

Body semantics

A mutate body lowers to the Operation IR and runs with all-or-nothing atomic commit: a failed require guard, or any error, emits nothing (RFD 0015). require preconditions, let bindings, typed-literal entity construction with system-minted identity, projection navigation (a.b.c) over committed state, collection inserts (insert … into …) with for iteration, sum / count aggregate guards over comprehensions, index projection (coll[i]), and effectful if/else (control flow is expression-valued; branches are blocks) all execute, returning the body’s tail value.

Name resolution in value positions. A bare identifier in a body value position — a relation-tuple argument, a constructor or update … set field value, a let right-hand side, a require guard operand, or the tail — resolves in order: a parameter or let / loop / match binder in scope first; then a declared type name (concept / trait / metatype / metarel / relation), which lowers to a TypeRef value exactly as it does in a rule body (Type-as-value) — the write side produces the same reference the read side dispatches on and the wire accepts as { "$typeRef": … }; then a module-declared individual (one introduced by a pub fact, resolved to its content-addressed identity). A binder therefore shadows both a declared type and a declared individual of the same name. A name that resolves to none of these is refused at ox check / ox build with OE1383 (no identity is ever synthesized for an unbound name), rather than building green and failing at the first run. A type-as-value LANDS only in a write position declared to hold one — a TypeRef / Metatype / TraitRef-typed relation endpoint or field; landing it in an entity/value position is refused with OE1384 at build where the declared signature is visible, and by the identically-worded runtime write gate otherwise. The same rules govern test bodies.

match in bodies. A value-position match (a let RHS, an update … set value, a tail / return value, or a require guard) matches over constant patterns (payloadless enum constants, literals, or-patterns, _; Pattern matching) and desugars to the same IfExpr chain a value if uses, with exhaustiveness enforced at ox check (OE0203). A statement-position match (arms running effects — the BPMN-gateway dispatch match d { Disposition::Clean => { update … }, Disposition::BreaksFound => { insert … }, _ => {} }) lowers to a right-nested Operation::If chain over the arm blocks’ operations (RFD 0015 Amendment 2): the same ordered first-match semantics, constant-pattern subset, and OE0203 exhaustiveness as the value desugar; arm blocks and if branches admit the full mutate statement set at any nesting depth. upsert, emit, and detach delete in a body refuse by name rather than dying generic or doing nothing silently: emit with OE1318, upsert with OE1352, and detach delete with OE1353.

Mutate-body arithmetic is exact (RFD 0016 / RFD 0029): require guards and let / field expressions route through one canonical evaluation core — pure-Int operands stay checked integers (overflow is a loud error, never a wrap), and any Real / Decimal / Money operand promotes to an exact rational (/ is the field operation, no truncation), so 0.1 + 0.2 == 0.3 holds exactly in a mutate body where it would fail in f64.

Reads see committed state. A body’s projections (a.b.c) read the store as committed before the mutation; a body does not observe its own not-yet-committed constructions. One consequence: constructing a collection-valued field and then insert … into that same field in a single body does not compose (the append seeds from committed state).

Deductive reads are iterands, not value terms. A pub query / derived-predicate deductive-plane read is set-valued. Its sole admissible use in a mutate body is as the iterand of a for x in <query> { … } loop, which binds each projected row in turn (lowered to a reasoner snapshot read over committed state, the same no-read-your-writes plane as above). A nullary read (for r in applicable()) iterates the whole extent; a parameterized read (for r in applicable_for(arg)) passes its bound arguments as the query’s sideways read-goal bindings, iterating only the rows the parameters select.

pub mutate mark_all() {
    for r in applicable() {
        insert iof(r, Done);
    }
}

A deductive read in a non-iterand term/value position — a let right-hand side, a require guard, an update … set value, a field value, or the tail — has no scalar value and is refused at ox check / ox build with OE1371 MutateQueryTermNotExecutable rather than passing the static gates and dying at the first runtime call:

pub mutate mark_term() {
    let x = applicable();
}

check

check-decl ::= attribute* 'pub'? 'check' Ident '(' param-list ')' ':-' atom-list '=>' diagnostic-expr ';'

pub check no_overlapping_leases(t: Person, p: Property) :-
    count { from l: Lease where l.tenant == t, l.property == p, is_active(l) } > 1
    => Diagnostic {
        severity: Severity::Error,
        code:     "Lease::E001",
        message:  format!("Tenant {} has overlapping active leases on {}", t.name, p.address),
    };

A check is a denial rule over the well-founded model: the body is the violation pattern, the => Diagnostic payload is the per-violation report. Checks never contribute facts (Cat3 — observers, not derivers). check is the only producer for the diagnostic stream from user code.

Discharge — the body’s vocabulary decides, not the author

You never declare a check “compile-time” or “runtime.” Discharge is staged by what the body reads (RFD 0025), the same staging discipline as refinement predicates (Refinement) and modal static discharge (Modal operators):

Catalog-level checks are the user-extensible compiler-diagnostic mechanism: a theory package ships its modeling constraints (OntoClean-style rigidity lints, MLT well-formedness, trait conformance) as check rules and they surface at ox check, ox build, and live in the editor — the LSP runs the same discharge — like any compiler diagnostic, under the package’s own codes.

The #[static] convention. Compile-time-intent checks carry #[static] by convention. The attribute does not change where discharge happens (the vocabulary does); it asserts the intent — if the body later drifts to instance vocabulary, the build fails with OE1322 instead of silently reclassifying the check to runtime discharge.

A firing Severity::Error check at build is a build failure: ox build writes no artifact, same discipline as every other loud gate. Warning/Info render and pass.

Runtime semantics — guard on the delta

At each mutation boundary the runtime evaluates the instance-level checks on the committed state (pre) and on the transaction’s overlay (post = committed + the body’s buffered events, mutate):

• Severity::Error guards: if the mutation creates violations — violations(post) ∖ violations(pre) is non-empty — the whole body is rejected atomically (nothing flushes, mutate’s atomicity) and the rendered diagnostics return to the caller. This generalizes the built-in write gates (OE0668 refinement invariants, OE0211 defined-concept inserts) to user-authored constraints.
• Pre-existing violations never block. A violation that predates the mutation (a stricter artifact over old data) is reported through the observe channel but does not reject writes — the guard is over the delta, not the absolute state.
• Warning/Info observe: collected and surfaced — on mutation results, in dispatch responses (the diagnostics section), and on demand. #[observe] on an Error check opts out of guarding (report-only, legitimate during migration).

The mechanized contract is spec/lean/Argon/Reasoning/Checks.lean: static_discharge_sound (a catalog-closed body evaluates identically at build and against any store extending the catalog) and guard_iff (the guard passes iff violations(post) ⊆ violations(pre)).

The Diagnostic payload

Diagnostic and Severity are check-surface syntax interpreted by the compiler (like the #[default] defeat-plane directive) — no import declares them. Exactly three fields, validated at ox check (OE1323); code: and message: are always required, and severity: is required unless the check implements a trait member whose signature pins it (check Member(Self) => Severity::…; — Trait atom, RFD 0026 amendment, issue #230), in which case omitting severity: inherits the pinned one (a divergent restatement is OE0676):

• severity: — Severity::Error | Severity::Warning | Severity::Info (closed set).
• code: — a string literal, namespaced: ::-qualified ("Lease::E001", "OntoClean::C1"), with the compiler’s OE/OW prefixes reserved (OE1324).
• message: — a string literal, or format!("…{}…", args) with positional {} placeholders only; each argument is evaluated per violation tuple and must resolve against the body’s bindings (OE1325). {{/}} escape literal braces.

at: is reserved for span attribution and refused.

Three-valued honesty

Check bodies evaluate over the well-founded model in K3 and fire on definite (is) violations only — undefined does not fire. Precisely: a violation requires the body to be well-founded true, so a negated body atom not p(x) contributes only when p(x) is well-founded false (definitely absent), not merely not-true — an undefined p(x) arising from recursion-through-negation does not satisfy the negation. A body that would have fired only because a NAF subject was undefined is surfaced on the observe channel marked [undefined], never as a violation and never to the delta guard, regardless of the check’s declared severity. Negation in a check body is negation-as-failure over the well-founded model (the CWA default, World assumptions (CWA / OWA)): not statute(c.cite) means “no derivably known statute,” not a claim about reality. Surfacing can-grade (possible) violations is out of scope.

Documentation gap — the in-body determinedness test is implemented but not yet specified here. The compiler accepts two check-body atoms, determined(A) and undetermined(A), over a membership atom A: they read the converged model and hold when A’s verdict there is definite, respectively not definite. A verdict is left indefinite by a well-founded standoff (can) or — for a concept marked #[world(open)] — by absence of evidence that nothing refutes, the same two cases the four-valued assert [not] derivable verdict distinguishes (World assumptions (CWA / OWA)); under the closed-world default absence is definite-false and only the standoff remains. They let a check body dispose of an undecidable membership per path instead of taking a severity-derived default. Outside a check body they are refused (OE1431), and a check body that uses either while leaving some membership atom’s can path unrouted warns (OW0744) — see Diagnostic codes. No chapter specifies them yet, and this section does not: two surface questions in the design record (RFD 0090) are open — whether the test generalizes to per-atom granularity inside a compound membership or stays at whole-membership granularity, and what surface the per-check inferred-disposition report takes (build-time inventory, ox subcommand, or both). A chapter written before those settle would document a form that is expected to move. The chapter also owes the underlying gate the tests build on: how a blocking check disposes of a membership it cannot decide, which is likewise unspecified here today. Until then the mechanized denotation is the reference: undeterminedAtom / determinedAtom in spec/lean/Argon/Reasoning/Checks.lean.

Delivery contract: a fired check is an emission to the reserved typed sink Diagnostics: Diagnostic (Sinks). The => Diagnostic { … } consequence is exactly => emit Diagnostics { Diagnostic { … } } — the Diagnostics-channel spelling of the general => emit Sink { … } rule consequence (emit) — and check is its sole producer (the diagnostic stream is never fed by a hand-written emit Diagnostics). Each firing carries polarity (Firing): a new violation binding emits an Asserted diagnostic and a violation resolved by a later mutation emits a Retracted one — the diagnostic clears, the dual of the delta guard above. Delivery is direct — the build diagnostic stream for static discharge, mutation results and the dispatch-response diagnostics section for runtime discharge.

emit from any rule mode

emit publishes a typed value to a sink — a named, write-only egress channel. It is the language’s hook into the system’s pub/sub layer: a published value flows to whatever external observers a sink is wired to, and nothing else happens to the knowledge graph. An emit adds no axiom, derives no tuple, and can never change the queryable extent — it is an observation, not a mutation. Because it is extent-neutral, emit is admitted in every rule mode (fn, query, derive, mutate, check), not only the side-effecting one; a fn that emits is still pure in the sense the purity ladder cares about — its return value and the extent are unchanged.

Sinks

A sink is the typed publication channel emit targets. It names a channel and the type of value that channel accepts; it carries no body and no target:

sink-decl ::= attribute* 'pub'? 'sink' Ident ':' TypeExpr ';'

pub sink AuditLog: LeaseEvent;
pub sink HitlQueue: ReviewTask;
pub sink Notify:    Notification;

There is exactly one sink form. A brace-bodied form pub sink Name { … } is not a sink declaration (a sink has no in-language body — where a value is delivered is configuration, not source); it is refused with OE1356. Delivery — log file, webhook, message queue, HITL ticket — is a runtime concern configured outside the source (the egress dual of the read-side placement routing); the language guarantees only that an emitted value matches the sink’s declared type.

Two spellings, one mechanism

emit means the same thing everywhere — publish value v to sink S — but the rule modes come in two body shapes, so it has two surface spellings.

Imperative bodies (mutate, fn block) have a statement position, so emit is a statement:

emit-stmt ::= 'emit' sink-path '{' expr '}' ';'
sink-path ::= Ident ('::' Ident)*

pub type Person { name: String }
pub sink AuditLog: String;

pub mutate sign_lease(t: Person) {
    // … the write …
    emit AuditLog { t.name };
}

Declarative bodies (derive, query, check) are clause bodies (select … from …, head :- atoms) with no statement position, so emit rides a consequence arrow => — the same arrow check already uses. In fact check’s => Diagnostic { … } is an emit to the reserved Diagnostics sink; it is the Diagnostics-channel special case of the general consequence form:

pub type Person { age: Int }
pub sink SeniorFeed: Person;

// derive: publish on each newly-derived tuple (the signed derivation delta)
pub derive senior(p: Person) :- p: Person, p.age >= 65 => emit SeniorFeed { p };

A check’s => Diagnostic { … } payload is the same construct: it is sugar for => emit Diagnostics { Diagnostic { … } }, an emit to the reserved typed sink Diagnostics: Diagnostic (check). emit Diagnostics { … } is otherwise reserved — the diagnostic stream is produced only through check, never by a hand-written emit. As a check consequence it carries polarity like any other derive-class sink: a new violation emits an Asserted diagnostic and a resolved violation emits a Retracted one (the diagnostic clears).

Firing — once per fresh delta, with polarity

A sink is fed once per fresh firing, where the firing unit is the natural one for the mode. Re-deriving, a cache hit, or re-reading an unchanged result does not re-emit. Each firing carries a polarity: Asserted (a value newly published) or Retracted (a previously-published delta withdrawn).

So mutate/fn/query fire per execution/evaluation and derive/check fire per binding — but in every case the rule is “fire on each fresh occurrence, deduplicated by the cache/delta,” which is why the published stream tracks the system’s evolution rather than how often something is asked.

The delta model. The two delta-firing modes carry both signs. A derive sink sees Asserted on the +1 delta when a head tuple becomes true and Retracted on the −1 delta when a previously-true tuple becomes false; a re-derivation that nets to zero emits nothing. A check sink sees Asserted on a new violation binding and Retracted when a previously-firing violation is resolved. Emitting only the positive delta and dropping retractions would be a silent egress lie: a consumer would learn that an entitlement was granted but never that it was revoked. Polarity closes that — the egress stream is faithful to the extent’s evolution in both directions.

The imperative and pull modes are Asserted-only by construction, not by omission. A mutate emits per committed write and a committed write is never un-happened — an abort emits nothing rather than a later Retracted. A fn emits per fresh evaluation, and query is pull-based: a pull produces a result, never a standing delta there is anything to withdraw. There is no retraction to carry because these modes have no negative delta, so they are complete.

Emission and delivery

An emission is a triple { sink, value, polarity }. The value is the evaluated typed value — the same value carrier the language uses for struct and enum values, so a sink’s payload type is an ordinary type and the emitted value is checked against it. The polarity is the firing sign above.

Emissions ride the commit’s observation channel — the same receipt channel that carries #[observe] and Warning / Info check diagnostics — not the axiom/event log of facts (Storage layer). This is why emit is model-neutral: an emission is never an axiom, so it cannot enter the well-founded model, and its durability does not change the queryable extent.

Delivery is at-least-once with idempotency — effectively-once effect, not effectively-once delivery, which is unattainable across an independent process boundary (the two-generals impossibility). The mechanism is a transactional outbox over the append-only commit log (Richardson, Microservices Patterns; the partitioned-store reasoning of Helland, “Life beyond Distributed Transactions”): an emission is recorded atomically with the commit that produced it, then delivered; a redelivery after a crash or timeout is deduplicated downstream by an idempotency key derived from the emission and its originating commit. A consumer that applies emissions idempotently observes each effect once.

Routing is configuration. Which physical destination a sink’s values reach — a log file, a webhook, a message queue, a human-in-the-loop ticket — is runtime configuration (ox.toml), the egress dual of the read-side [placement] routing. It never appears in source: a sink declaration names the channel and its payload type and nothing more, and emit guarantees only that the value matches that type.

Status

emit is settled surface and executes in all five rule modes. The mutate and fn statement forms publish per fresh execution/evaluation — Asserted, nothing on abort, and a fn cache hit on (args, state) does not re-emit. The derive => emit consequence publishes the signed derivation delta at the commit boundary: Asserted on a newly-true head tuple, Retracted when a previously-true one becomes false, nothing on a net-zero re-derivation. The check => emit consequence publishes from the violation delta (Asserted on a new violation, Retracted when one resolves). The query => emit consequence publishes one Asserted value per fresh evaluation (a cache hit does not re-emit). Every position type-checks the value against the sink (OE0201 on a mismatch), refuses an undeclared sink (OE0101), and refuses the reserved Diagnostics sink to a hand-written emit (OE1368 — the diagnostic stream is produced only through check’s => Diagnostic { … }). An emit-bearing fn inlined into a rule body is refused (OE0227 — a rule body has no egress surface). A check => emit that fires at ox check / ox build has no receipt at build, so it surfaces a non-blocking OW1369 (its egress is a runtime-only effect, never silently dropped). Egress is model-neutral throughout: it asserts no axiom and never changes the queryable extent — emissions ride the commit’s observation channel (mutate / derive / check on the mutation receipt) or the read’s dispatch response (query), never the axiom log. Delivery and routing (log file, webhook, message queue, HITL ticket) are runtime configuration — the egress dual of read-side placement. The one sink-declaration form is pub sink Name: Type;; a brace-bodied pub sink Name { … } is refused by name (OE1356) — a sink has no body.

Pattern matching

match-expr ::= 'match' expr '{' arm (',' …)* ','? '}'
arm        ::= pattern ('if' expr)? '=>' expr
pattern    ::= '_'
            |  literal
            |  Ident                                    // binder
            |  TypeExpr '(' pattern (',' …)* ')'        // variant
            |  TypeExpr '{' field-pattern-list '}'      // record
            |  Ident ':' TypeExpr                       // type test
            |  'is' reasoning-outcome
            |  pattern '|' pattern                      // OR
reasoning-outcome ::= 'unknown'
                  |  'ambiguous' '(' Ident ')'
                  |  'timeout'   '(' Ident ')'
                  |  'both'      '(' Ident ',' Ident ')'

pub fn classify(l: Lease) -> Status =
    match l {
        ResidentialLease(r) if r.bedrooms > 4 => Status::Large,
        ResidentialLease(_)                   => Status::Standard,
        CommercialLease(_)                    => Status::Commercial,
        _: TerminatedLease                    => Status::Closed,
        is unknown                            => Status::Pending,
        is ambiguous(x)                       => Status::Ambiguous(x),
        _                                     => Status::Unknown,
    };

Exhaustiveness checked; non-exhaustive matches require _ or fail with OE0203.

Match semantics

match evaluates — in value position and statement position — as ordered first-match over constant patterns:

A value-position match (a fn body, a rule-body comparison operand, a mutate let RHS / update … set value / return value / require guard) desugars at elaboration to a right-nested conditional chain over scrutinee == constant tests — if s == P1 { v1 } else if s == P2 { v2 } else { v_last } — so it executes on the existing IfExpr paths in the reasoner and the mutate runtime; semantics are first-match in arm order, and the final arm’s value is the else-branch. Exhaustiveness is required: a final _ arm, or full coverage of the scrutinee’s enum variants when statically known — otherwise OE0203 at ox check. Statement-position match (arms running effects inside a mutate body) executes with the same semantics (RFD 0015 Amendment 2): the arms are blocks running mutate statements (update / insert / delete / forget / require / nested for / if / match), the match lowers to a right-nested Operation::If chain over the arm blocks’ operations — ordered first-match, exactly one selected arm’s effects run, the arm value is discarded — and the same exhaustiveness rule applies (_ => {} with an empty block is the idiomatic catch-all; OE0203 otherwise). Or-patterns expand to consecutive conditions sharing the arm’s operations.

A single-binder payload destructuring (Some(v) => …) executes in value position — let r = match opt { Some(v) => v, None => 0 }; and every value-position site above: the arm’s condition tests the variant tag and its body sees the binder substituted by the decoded payload. A payload-binding arm in statement position (an effectful arm inside a mutate statement-match) refuses with OE1319: bind the payload in value position first (let v = match opt { … };), then run the effect. A bare binder Ident, a type test, an is-outcome arm, and an arm guard refuse with OE1319 in both positions.

Rule-body arm projections must be total. In a rule body (derive / check / query / bridge), the relational lowering hoists every field projection inside the conditional chain — including arms the scrutinee never selects — into an eager, unconditional $field:: join, because the relational plan has no lazy join. $field::<f> has no row when an individual lacks f, so an arm projecting an optional (T?) field would silently filter out every row missing that field, even rows whose matching arm never touches it. Rather than mis-evaluate, ox check / ox build refuse such a rule with OE1320: every field projected inside a conditional arm (a value-if branch or match arm — both lower identically) must be total, i.e. declared required on every visible type that declares it. Workarounds: split the conditional into one rule per arm (each joining only the fields that arm needs), or declare the field required. Projections in always-evaluated positions (the rule body proper, the outermost condition / scrutinee test) and fn / mutate bodies (which evaluate branches lazily) are unaffected.

Trait atom

A trait is a behavioral contract: a named bundle of obligations over a Self type, discharged by impl Trait for Type blocks. The boundary with the concept lattice is doctrinal: concepts say what something is (ontologically); traits say what something can do — trait hierarchies never enter the <: concept lattice, traits cannot be specialized or inherited, and classification never belongs in a trait (Modeling guidance: traits versus phases and categories). The full design is RFD 0026; the trait surface lands in stages, and what runs end-to-end is exercised by the packages in examples/.

Surface

trait-decl  ::= attribute* 'pub'? 'trait' Ident generic-params?
                   (':' TypeExpr ('+' TypeExpr)*)?            -- supertraits (requires-constraints)
                   ('{' trait-item* '}')? | ';'               -- empty body = marker trait
trait-item  ::= fn-signature ';'                              -- invocation-plane member ('self' leads)
             |  'mutate' Ident '(' 'self' (',' member-params)? ')' ';'   -- invocation-plane member
             |  'derive' Ident '(' member-params ')' ';'                    -- rule-plane member
             |  'check' Ident '(' member-params ')'
                   ('=>' 'Severity' '::' Ident)? ';'          -- rule-plane member; optional
                                                              -- severity pin (issue #230)
             |  'query' Ident '(' member-params ')' '->' TypeExpr ';'       -- rule-plane member
             -- 'type' Ident ';' / 'const' Ident ':' TypeExpr ';' remain reserved

impl-block      ::= 'impl' generic-params? TypeExpr ('for' TypeExpr)? ('{' … '}')? | ';'
trait-impl-item ::= fn-decl | mutate-decl                     -- full bodies
                 |  derive-decl | check-decl | query-decl     -- full bodies (rule body; select
                                                              -- body for query), Self admitted

When 'for' TypeExpr is present the construct is a trait impl (impl Renewable for Lease) and its items are trait-impl-items; when absent it is a bare impl (impl Lease { … }), whose items parse per impl Type { … } — grouping but are gated at elaboration (OE1326) until inherent members execute. Conformance (Conformance) governs trait impls only. Impls of either form are standpoint-global: declaring one inside a standpoint { … } block is refused at elaboration (per-standpoint impls are an open design question RFD 0026 deliberately does not decide).

• Self resolves only inside trait and impl bodies: in a trait item it is the obligation’s type parameter; in an impl item it denotes the impl’s target type. Misuse is OE0675. A trait member signature must mention Self in at least one parameter position (a member that is not about the implementing type belongs at module level — OE0675 says so). Multiple Self positions are legal.
• Supertraits use : (pub trait Repaintable: Drawable), Rust’s spelling, because they are Rust’s semantics — requires-constraints, not subsumption (Resolution). <: is reserved for the concept lattice.
• Generic parameters remain unbounded-only (Generic parameters); generic members, bounded generics, and trait-side default bodies refuse loudly, never dropped.

Member semantics: two planes

Members split by how they are consumed; both planes elaborate by monomorphization — each impl member lowers to an ordinary rule (Self ↦ target type) flowing through the standard pipeline (classifier, stratifier, evaluability gate, reasoner) with no new evaluation machinery.

Rule plane (derive, check, query) — clause union

The trait declares the predicate; each impl contributes a type-guarded clause:

pub trait Adulthood {
    derive Adult(Self)
}
impl Adulthood for USPerson     { derive Adult(p: Self) :- p.age >= 18 }
impl Adulthood for GermanPerson { derive Adult(p: Self) :- p.age >= 18, p.has_residence }

elaborates to two ordinary rules with one head, Adulthood::Adult — Datalog unions same-head rules natively, and the head-parameter guards close over <: (World assumptions (CWA / OWA)). Dispatch is derivation: an atom Adult(p) in

pub derive CanVote(p: Person) :- Adult(p), p.registered

holds per-individual under whichever impl covers the individual’s actual type — the relational transposition of dyn dispatch, with the no-overlap rule (Conformance) keeping the selection single-valued per declared type (per-individual multiple classification is defined in Conformance). A query member carries the full query signature — Self in parameter positions, a Self-free return type (return-position Self is OE0675: it would need union types or bounded generics) — and each impl provides a full select … from … body; the trait signature fixes the projection shape. Query members are declared, conformance-checked, and lowered per impl, and they surface through the same per-impl query dispatch top-level queries use — each impl’s clause is queryable under its per-impl identity Trait::member@Target. They are not rule-body atoms: a query-member atom in a derive/check body is refused loudly at ox check, the same envelope discipline fn members get (Resolution) — top-level queries are not rule-body predicates either, and the member form inherits exactly that. A single dispatch endpoint returning the union of per-impl results is reserved. A check member monomorphizes to ordinary RuleMode::Check rules; discharge, payload, and delivery follow RFD 0025 unchanged. A check member’s signature may pin its severity with the payload-arrow suffix (check OverLimit(Self) => Severity::Error; — RFD 0026 amendment 2026-06-11, issue #230): the pin makes blocking behavior part of the trait contract. Under a pin, an impl’s Diagnostic { … } payload may omit severity: (it inherits the pinned one), may restate the same severity (harmless), and is refused with OE0676 when it states a different one — a contract whose blocking behavior varies by implementor is a weak contract. Only the severity is pinnable: code: and message: stay per-impl, and a full Diagnostic { … } payload on the trait-side signature is refused (OE1323). An unpinned member keeps per-impl severity freedom. #[observe] on an impl member whose pinned severity is Error remains legal (a discharge-mode opt-out, not a severity change).

Invocation plane (fn, mutate) — receiver resolution

A body is a single value or a single transaction; resolution is to exactly one impl. An invocation-plane member leads with the self receiver — its first parameter must be self (OE0675 otherwise; further Self-typed parameters are admitted after it) — because the receiver is what dispatch selects on. A mutate member —

pub trait Closable {
    mutate close(self, reason: String);
}
impl Closable for SavingsAccount {
    mutate close(self, reason: String) {
        update self: SavingsAccount set { status = "closed" }
    }
}

— monomorphizes per impl (full RFD 0015 imperative bodies; self is the receiver variable inside the body, Self splices to the target type) into the mutation catalog under the per-impl identity Closable::close@SavingsAccount, callable as Closable::close: invocation dispatches on the receiver individual’s actual committed type to the unique covering impl (<:-aware — an impl for Account covers a SavingsAccount receiver). An ambiguous receiver — classified under two <:-incomparable covered targets — and a receiver with no covering impl are both loud runtime refusals naming the impls / the receiver’s types (Conformance), never an arbitrary pick. Invocation flows through the standard mutation-dispatch surface (CLI harness / serve / SDK); the receiver is passed as the self argument (an individual reference), exactly like any RFD 0019 entity-ref parameter. fn members elaborate and dispatch the same way through the compute surface (Resolution has the precise execution envelope). Mutations do not call mutations; member mutates do not change that.

Generic parameters

Unbounded generics parse and travel the wire; bounded generics are rejected (OE0667). The conditional-impl coherence theorem (Argon.TypeSystem.Conditional) is mechanized.

Resolution

Calling convention (rule plane). Trait::member(args) qualified is always legal. Bare member(args) is legal when exactly one provider of that name and arity is in lexical scope; ambiguity is an error naming the candidates. There is no postfix p.member() sugar in rule bodies — p.x is field-access space (Rule-atom grammar).

The coverage gate. A bare member atom requires the argument’s static type to be fully covered — you cannot call what isn’t implemented, statically. Coverage is computed over the workspace-closed catalog via the abstract modifier (metatype, RFD 0027 D6): a static type T is fully covered iff every instantiable (non-abstract) declared S ⊑ T (including T itself when non-abstract) is ⊑ some impl target. Abstract types admit no direct instances (OE0233 refuses construction) — every individual is classified through some non-abstract subtype — so they need no covering themselves; their non-abstract descendants do. The instantiability oracle is a pure wire-flag read (Argon.TypeSystem.Conformance. instantiableOfAbstract); no axis vocabulary is consulted — a sortality::non_sortal binding is the package’s own ontology and exempts nothing by itself. The default is instantiable: an unmodified declaration (the neutral std::core::type baseline, any pub metatype m = { };) obligates coverage — the gate can only over-refuse, never silently admit a vacuous member call, and the exemption is the explicit abstract opt-in. Partial coverage is legal only under an explicit conformance guard:

pub derive CanVote(p: Person) :-
    implements(meta(p), Adulthood),     -- the visible branch
    Adult(p), p.registered

Uncovered or unguarded-partial atoms are OE1327, whose help names the uncovered types and offers both fixes (add the impl, or write the guard). Dispatch that can fail is always visible in the source. Under multiple classification meta(p) is multi-valued (Reflection); the guard is existential by construction — meta is a relation and the conjunction is a join, so the guard holds iff some <:-minimal classifier of p is covered, and the clause that fires is the one whose target that classifier satisfies.

Invocation-plane dispatch. Invocation-plane members are end to end through the execution surfaces Argon has — the dispatch surfaces, where the only type information is the receiver individual’s committed classification:

• A member is invoked by its callable name Trait::member (qualified path, or any unambiguous ::-suffix — the same resolution rules as mutations and rule heads; ambiguity is an error naming the candidates), or pinned to one impl by its per-impl identity Trait::member@Target. The pinned form is an explicit escape hatch: it bypasses receiver dispatch and does not re-verify that the receiver is covered by that impl’s target (parity with ordinary mutations, which do not re-verify update x: T against x’s classification).
• The self argument carries the receiver individual; dispatch selects the unique impl whose target covers the receiver’s actual committed type (<:-aware). No covering impl, and a receiver under two <:-incomparable covered targets (the Conformance residual), are loud refusals naming the types / the impls — never an arbitrary pick.
• mutate members run through every mutation surface (the CLI demo harness, serve’s /v1/dispatch/mutation, the generated SDK’s member endpoint); fn members run through the compute surface (/v1/dispatch/compute, SDK) — exactly the surfaces where top-level fn declarations execute.

Source-level call sites are not an execution surface — for any fn. Top-level fn declarations cannot be called from rule bodies or from fn/mutate bodies (term-position user-function application does not resolve); method-call syntax x.foo() parses but has no semantics — the call expression builds, resolves to nothing, and derives nothing (the same silent-vacuity bucket as term-position application; tracked for a loud gate). fn members inherit exactly that envelope — they are declared, conformance-checked, lowered, and dispatchable wherever top-level fns are, and nowhere else. Source-level calls bind to the rules this section reserves: build-time resolution (first x’s inherent impls, then trait impls; one concrete body, no vtables), Trait1::foo(x) (UFCS) on collision, bare calls legal where exactly one trait in scope provides the member, and the receiver’s static type subject to the same coverage gate.

Supertraits are requires-constraints. pub trait Renewable: Resource makes impl Renewable for Lease well-formed only if impl Resource for Lease exists (OE0674). Nothing is inherited — no member bodies, no identity, no lattice position.

Orphan rule. An impl Trait for Type must live in the package declaring Trait or the one declaring Type (OE0672), so every workspace’s impl set is unambiguous.

Conformance

Enforced at ox check and ox build over the closed catalog (elaboration-time diagnostics, not check rules):

No-overlap (OE0673) instantiates the mechanized coherence contract by construction — a nominal target is a TraitBound with satisfied T := T ⊑ target — so at most one impl covers any declared instantiable type and there is never a specificity question. Both arms matter: impl Adulthood for Person + impl Adulthood for USPerson is OE0673 (the “default + override” pattern is rejected by design — write disjoint targets, or one impl whose body branches), and impl T for Person + impl T for Customer is OE0673 when some pub type Employee <: Person, Customer is declared (the common descendant would sit under two clauses). One residual cannot be closed statically — the set of an individual’s runtime classifications is not known at compile time: an individual dynamically classified under two <:-incomparable covered targets with no declared common descendant. Its semantics is defined, not accidental — in the rule plane the clauses are independent sufficient conditions (both may fire; the union is their disjunction); in the invocation plane an ambiguous receiver is a loud runtime refusal.

Reflective conformance: TraitRef and implements

• TraitRef is a reflective sort parallel to TypeRef (RFD 0023): values are handles to declared traits (carrier Value::Name). It is a sibling sort under Entity — deliberately not on the Metatype <: TypeRef chain, because traits are not types.
• implements(t: TypeRef, tr: TraitRef) -> Bool is the fifth reflection intrinsic (Reflection), materialized as the RT-closed reserved-head relation $implements from impl declarations, with supertrait closure and <: upward target-coverage folded in (an impl for Person covers USPerson, World assumptions (CWA / OWA)-coherent).
• $implements is catalog-closed, so not implements(…) is stratification-safe, and — unlike the type-position arguments of the other four intrinsics — both positions of implements are exempt from OE0212 and may be free: enumeration is relational (implements(t, Adulthood) with free t yields the implementing types; implements(meta(p), tr) with free tr yields the traits of p’s type). The expression plane gets the boolean form (if/match scrutinees) and implementors(Trait) -> Set<TypeRef>.
• Conformance checks are catalog-level vocabulary under RFD 0025 D1 as amended by RFD 0026 (catalog-level iff every variable is reflective-sorted: TypeRef, TraitRef, or Metatype), so they discharge statically at ox check:

#[static]
pub check EveryPersonKindHasAdulthood(t: TypeRef) :-
    specializes(t, Person),
    not implements(t, Adulthood)
    => Diagnostic {
        severity: Severity::Error,
        code:     "Onto::E001",
        message:  format!("{} must implement Adulthood", t),
    }

Wire and Lean correspondence

Member rules are emitted as ordinary RuleDecl/QueryDecl events; invocation-plane members as ordinary MutationDecl/ComputeDecl events keyed Trait::member@Target — no new AxiomKind. TraitDeclBody.methods carries member signatures (all five planes); ImplDeclBody.items carries member provenance (both fields carry it — the wire is built for this). spec/lean/Argon/Substrate/Trait.lean carries the @[language_interface] shapes; Argon.TypeSystem.Conditional states the coherence contract that OE0673 enforces. The Lean obligations for this design (monomorphization conservativity on the Reasoning/Datalog/ spine; coherence instantiation; structural-tier conformance) are listed in RFD 0026.

Modeling guidance: traits versus phases and categories

If it classifies, it is a concept; if it obligates behavior, it is a trait. “Adult” as a classification is an anti-rigid phase of Person — model it as pub type Adult <: Person iff { age >= 18 } and the substrate derives membership. Reach for a trait when otherwise-unrelated types must satisfy a common contract of derivations or operations (Closable, Auditable, per-jurisdiction rule families) — the contract is about what the types provide, not what their instances are. A trait carrying a single unary Self-member named like a classification is usually a phase in disguise.

Examples

-- Marker trait.
pub trait Renewable;

-- Rule-plane contract; per-jurisdiction clauses.
pub trait Adulthood {
    derive Adult(Self)
}
impl Adulthood for USPerson     { derive Adult(p: Self) :- p.age >= 18 }
impl Adulthood for GermanPerson { derive Adult(p: Self) :- p.age >= 18, p.has_residence }

pub derive CanVote(p: Person) :-
    implements(meta(p), Adulthood), Adult(p), p.registered

-- Invocation-plane contract. The receiver leads; invocation passes
-- `self` (an individual ref) and dispatches on its actual type.
pub trait Closable {
    mutate close(self, reason: String);
}

-- Supertrait as requires-constraint (Rust's `:`). Return-position
-- `Self` is OE0675 (it would need union types / bounded generics);
-- return a concrete type.
pub trait Repaintable: Drawable {
    fn repaint_cost(self, color: Color) -> Int;
}

-- Bare impl (inherent grouping): parses per `impl Type { … }` — grouping, but its members are
-- OE1326-gated at elaboration — inherent members do not execute yet
-- (the RFD 0026 invocation plane covers trait members only).
impl Lease {
    fn extend(self, days: Nat) -> Lease;
}

Macro atom

The macro atom is the fifth substrate atom (meta-calculus, constructs, rule, trait, macro) and the extensibility layer the ontology-neutral doctrine depends on: it is how a vocabulary library grows the surface without a compiler change. Its design is settled by RFD 0037; this chapter is the surface specification.

The declarative expansion engine — pub macro declarations expand at EXPAND (hygiene, repetition, attribute/decl-position invocation, cross-module imports), and their output re-elaborates through the ordinary path to events. The procedural layer (#[procmacro] pub fn, Procedural macros) provides concat_idents, quote/${} antiquotation, decl-reflection, and a total non-recursive body — the mechanism that re-homes #[irreflexive]/#[asymmetric]/#[functional] from compiler builtins to library procedural macros (#[functional] was the last builtin retired, Migration: re-homing the hard-coded surface).

The shape of the design. A macro expands to surface syntax, which is re-parsed and re-elaborated through the one existing path to events — never to events directly. Expansion is a phase between parse and resolve, run to a fixed point; the resolver, type checker, Name resolution ontology-neutrality gate, and decidability-tier classifier all run on the post-expansion program, so a macro is invisible to none of them. The declarative layer (pub macro, pattern→template) is the foundation; the procedural layer (#[procmacro], computation over reflected syntax) is layered on top (Procedural macros).

Declarative macros

macro-decl    ::= attribute* 'pub'? 'macro' Ident '{' macro-rule (';' macro-rule)* ';'? '}'
macro-rule    ::= '(' macro-pattern ')' '=>' '{' template '}'
macro-pattern ::= /* token tree with $name:SPEC metavariables and $(...)* / $(...)+ / $(...)? repetitions */

A declarative macro is a sequence of (pattern) => { template } rules. A pattern matches a token tree; metavariables are tagged with a fragment specifier that fixes the syntactic category matched and the binding space the bound name lives in. The template is surface syntax, with metavariable substitution and $( … )*/+/? repetitions (optional separator: $( … ),*).

pub macro vec {
    () => { Vec::empty() };
    ($head:expr $(, $tail:expr)*) => { /* … */ };
}

let xs = vec!(1, 2, 3);

Fragment specifiers. The syntactic categories $x:expr, $t:ty, $i:ident, pat, stmt, block, item, literal, path, tt; plus four Argon-specific specifiers, each a binding-space-targeted parse — $c:concept parses a concept-introducing declaration and binds in the concept space, $r:rel a relation declaration (rel space), $m:metatype a metatype introducer, and $u:rule a rule-body atom (carrying its own rule-variable sub-bindings). The set is closed; a standpoint specifier and a user-extensible registry are out of scope (Out of scope). Because a concept/metatype specifier only binds — the Name resolution gate runs later, at resolution (Hygiene) — and no specifier carries a tier, ontology-neutrality and tier-honesty hold by construction.

The expansion model

Expansion is a distinct compilation phase:

lex → parse → expand* → resolve → check → instantiate (lower to events) → tier-classify → discharge

• Expand to surface, re-elaborate. A macro produces surface syntax that is spliced into the module and re-parsed; it then flows through the same resolve → check → lower path as hand-written source. The content-addressed AxiomKind event wire is produced only by the unchanged lowering, so a macro inherits the substrate’s identity and drift guarantees for free. A macro never emits events directly.
• Fixed point. A macro whose output contains further invocations re-expands until none remain, bounded by a fuel cap that errors on exhaustion.
• Emit into the invocation module. A macro expands at its use site and its output lands in the invoking module, where rules it emits compose with the user’s by the same-module same-head union (derive). It cannot contribute to another module’s heads.
• Classifier-last gives tier-honesty. The decidability-tier classifier runs after expansion on the lowered events, so the program lands on its true tier — a macro that emits a recursive rule is classified exactly as if the rule were hand-written, and cannot smuggle the program across a tier boundary.
• Determinism. The declarative layer is strongly normalizing by construction, has no I/O, and emits collections in a canonical order. Rule variables are alpha-canonicalized at lowering (Hygiene), so a macro’s choice of fresh variable names never affects the .oxbin content hash. Expansion is therefore a deterministic function of its input, and reproducible builds need no author discipline.

Hygiene

Macro-introduced binders neither capture nor are captured by names at the use site, across all of Argon’s binder namespaces (rule variables, concept/type, rel/metarel, metatype/metaxis + axis values, individuals, trait members). The model is scope-sets with binding spaces (Flatt 2016 + Racket binding spaces): each namespace is an interned scope inside one scope-set, resolved by the unchanged maximal-subset rule. Hygiene is white-box — the quotation applies a fresh macro scope to the identifiers a macro introduces.

The Name resolution ontology-neutrality gate composes as a commuting pass: scope-set resolution (syntactic) produces a candidate binding, then the gate (semantic) checks that a macro-introduced concept resolves to a visible pub metatype — it may reject, but never re-points a reference. Macro-introduced vocabulary is not exempt from the gate.

Two regimes follow from what reaches event identity:

• Rule variables are clause-local and alpha-canonicalized at lowering, so hygiene need only guarantee non-capture; their names are irrelevant to identity.
• Introduced vocabulary (a concept/relation a macro declares) has a semantic, referenceable name, so hygiene gives it a content-derived, stable identity.

Macros are hygienic-only: there is no unhygienic!. A $crate-style self-reference plus syntax-parameter keywords cover the real needs; any future raw escape must name the binding space it breaks into.

Imports and the shared #[…] namespace

A pub macro foo { … } declaration occupies a single symbol in the module namespace. use mod::foo; brings it into scope; foo!(args) invokes it at expression position and #[foo(args)] at declaration position. The ! and #[…] sigils are invocation markers, not separate-namespace tags — there is no distinct macro namespace, and no #[macro_use] form; macro imports follow ordinary item-import rules (Imports).

User macros and compiler-known directives share the #[…] namespace. Resolution is by uniqueness at registration: a name resolves to exactly one implementation, and a user macro colliding with a built-in directive is an OE0705-class error, never a silent shadow (matching the loud-refusal discipline of the directive registry, Directive surface and the MLT decorator path). Identity is keyed to a stable handle, not the spelling, so re-homing a directive (Migration: re-homing the hard-coded surface) does not change how a #[name] resolves.

Procedural macros

A procedural macro computes its expansion by running code, rather than rewriting a pattern into a template. It is not a fn over a TokenStream: the procedural layer is a total, structurally-recursive meta-language over reflected syntax, not general-purpose computation. Totality is what the substrate’s own doctrine requires — it is strongly normalizing and deterministic by construction, and (being a total function over an inductive syntax type) mechanizable in Lean (Lean correspondence).

A procedural macro is a #[procmacro] pub fn in the one macro namespace:

#[procmacro]
pub fn irreflexive(item: Decl) -> Syntax {
    let head = concat_idents("__", item.name, "_irreflexive");
    quote {
        $item;
        pub check $head(x: $item.params[0].ty) :- $item.name(x, x)
          => Diagnostic { severity: Severity::Error, code: "Argon::OE1359",
               message: "relation `${item.name}` is #[irreflexive] but relates an element to itself" };
    }
}

The body is a total, non-recursive fragment: let bindings over the construction builtins and reflection projections, then a trailing quote. The surface is:

• quote { … } — a QUOTE_EXPR; its body is re-parsed through the ordinary elaboration path (never emitted as events directly). Splices: $name (a let-bound value), $item (the whole reflected declaration, re-emitted verbatim), and the reflection projections below.
• Reflection projections — the declaration’s resolved structure, complete and client-agnostic. On the item: item.name, item.kind ("rel" / "metarel" / "type" / "metatype"), item.arity (decimal string; "0" for a non-relation), item.attr, item.arg, item.param_list (verbatim), item.params, item.fields. Per parameter p (in $( for p in item.params ) repetitions): p.name, p.ty, p.is_list, p.is_optional, p.is_last. Per field f (in $( for f in item.fields ) repetitions): f.name, f.ty, cardinality f.is_list / f.is_optional, the from-clause source f.rel / f.role (empty when the field has no from clause), modifiers f.is_mut / f.is_pub / f.is_intrinsic, the verbatim attribute text f.attrs, and f.is_last. ${ if <bool> { … } else { … } } is a total conditional over the boolean projections. Field defaults are deliberately not reflected: a field default is refused at parse (OE0237), so no well-formed default node exists to project.
• Resolved-schema projections — the declaration’s structure resolved across the package: item.all_fields (own and inherited fields via the <: chain, nearest declarer first, de-duplicated so the most-specific declarer wins; item.fields stays own-only), item.stored_fields / item.nav_fields (the same set partitioned on whether the field carries a from clause), and per field f.declaring_concept, f.has_from, and f.is_forward (endpoint direction: true iff the projected role is not the backing relation’s first endpoint — the bit that decides scalar wiring vs a loop over the reverse endpoint in a constructor). These resolve from a parse-only, cycle-safe schema graph over the current package’s module tree (EXPAND precedes name resolution, so no elaborated types are consulted; a <: cycle is folded once, matching the substrate’s concept-cycle semantics). An ancestor or backing relation declared outside the package is beyond the phase’s visibility: a macro consuming item.all_fields on such a declaration declines the whole expansion loudly (a residual invocation, OE0723, no artifact) — it never silently omits an out-of-package ancestor’s fields.
• ${expr} antiquotation — an in-string splice (e.g. inside a diagnostic message:), resolved by the macro renderer at EXPAND. It is render-time, not runtime string concatenation (the runtime has no Text + Text — that is a separate arc).
• concat_idents(a, b, …) (paste) — builds a raw definition-site identifier from pieces; the single capability the splice-only declarative layer lacks. The result is not freshened — the macro intends it as the stable public head (__{rel}_{prop}); splices are substitution barriers carrying their own use-site identity.

Bodies are non-recursive (trivially total). #[procmacro] resolves as a macro (DefKind::Macro), runs at EXPAND by a dedicated evaluator, and its #[procmacro] directive executes at fn-decl position. #[irreflexive] and #[asymmetric] (Migration: re-homing the hard-coded surface) are genuine procedural macros written exactly this way.

Full structural recursion over reflected Syntax — a totality checker and the classify ∘ expand tier-honesty theorem — is out of scope (Out of scope). Field reflection and resolved-schema reflection (inherited fields and relation endpoint direction, the projections above) are in scope and shipped; the resolution scope is the current package, with out-of-package ancestors refusing loudly as described above.

Directive surface and the MLT decorator path

Every #[…] attribute must resolve to a registered compiler directive or an in-scope pub macro (e.g. #[transitive], re-homed to std::rel, Migration: re-homing the hard-coded surface / RFD 0037 D8 — brought in by use). The directive registry (oxc-instantiate’s DIRECTIVE_REGISTRY) is the single declarative table of every directive the toolchain reads or reserves, with its argument shape, valid positions, and status. There are no silently-ignored attributes: an attribute that is neither a registered directive nor an in-scope macro refuses with OE0705 UnknownDirective (nearest-known suggestion), documented-but-unbuilt directives with OE0706 DirectiveReservedUnimplemented, misplaced directives with OE0707 DirectiveInvalidPosition, argument forms on bare-form directives with OE0709 AttributeArgsNotYetImplemented, and conflicting families with OE0714 DirectiveConflict.

The relation-property directives are library macros, split by mechanism (Migration: re-homing the hard-coded surface):

• Relation-property directives (RFD 0031) — #[transitive] is a declarative pub macro in std::rel (closure derive R(x, z) :- R(x, y), R(y, z) into the relation’s own head); #[irreflexive]/#[asymmetric]/#[functional] are genuine procedural macros (#[procmacro], RFD 0040) that re-emit the decorated declaration ($item) and paste a guarding check via structural reflection. #[functional] dispatches on item.kind then item.arity: BOTH a binary rel and a binary metarel re-emit $item and paste a __{rel}_functional check that fires when a source maps to two distinct targets (OE1361). It is binary-only — a functional object property is binary by definition, so a non-binary #[functional] matches no arity arm and the invocation is refused (OE0723; #1273). A rel whose explicit target cardinality permits more than one target contradicts #[functional] and is refused (OE1378). All three re-home from compiler builtins (#[functional] was the last, so OE1362 is retired and an unimported #[functional] refuses as OE0705, like its siblings); each formats Argon source and re-parses it through the ordinary derive/check pipeline.
• MLT decorators — #[categorizes(T)], #[partitions(T)], #[subordinate_to(M)], #[power_type_of(T)], and #[order(N)] are no longer compiler directives at all. They are genuine library #[procmacro]s in the unprivileged mlt package (not std): each re-emits the decorated declaration and emits a MetaProperty on the metarel (or, for #[order], the metaxis) it shares its name with — reading the argument’s name (or, for #[order], an integer), not its structure. Nothing is ambient: a consumer lists mlt in ox.toml and imports the vocabulary (use mlt::*; / use mlt::{categorizes};), and an unimported decorator is an unknown attribute macro, refused by the no-silent-attribute gate (OE0705). The emitted MetaProperty is re-checked at the emission boundary and again at load — #[order]’s value is validated against the mlt::order metaxis’s declared Nat where { _ <= 16 } domain by the self-validating .oxbin load re-check (OE0623), so the bound holds without any compiler privilege. The reasoner-side enforcement of the MLT closure rules over the emitted metaproperties is authored as the mlt package’s own rules/checks over the neutral substrate (Phase 2).

Directives as library macros

The hard-coded directive surface is library macros, with the user-facing syntax byte-identical to a privileged-path synthesis (RFD 0009 RP-003 GAP-3). The mechanism is decided by the directive’s emit target:

• Relation-property emits ordinary rules (which have surface), so it lives in std::rel, split by what each member needs:
  • #[transitive] is a declarative pub macro: the macro template produces lowered events byte-identical to a direct synthesis (verified differentially).
  • #[irreflexive] / #[asymmetric] are genuine procedural macros (#[procmacro] pub fn … -> Syntax, RFD 0040): each re-emits the decorated declaration ($item) and pastes a pub check whose head is concat_idents("__", item.name, "_{prop}") — the unique ident the splice-only declarative layer cannot build. Their import gate is OE0705 (a bare unimported #[irreflexive] is an unknown attribute macro, like transitive).
  • #[functional] is a genuine procedural macro (#[procmacro], RFD 0040 P2, importable from std::rel, OE0705 if not — retiring the last #[builtin] and its OE1362). It dispatches on item.kind then item.arity; BOTH the rel and metarel arms re-emit $item and paste a __{rel}_functional check that fires when a source maps to two distinct targets (OE1361) — the same check-based enforcement as #[irreflexive]/#[asymmetric] (#1377 A2, retiring the former [0..1]-cap reconstruction that silently dropped stacked siblings, user brackets, generics, and bodies). It is binary-only: a non-binary relation matches no arity arm and the invocation is refused (OE0723; #1273), because a functional object property is binary by definition. A rel whose explicit target cardinality’s upper bound exceeds one contradicts the constraint and is refused (OE1378).
• MLT emits MetaProperty events. Its surface is the unprivileged mlt package (RFD 0043): every decorator — the relational #[categorizes]/#[partitions]/#[subordinate_to]/#[power_type_of] and the metaxis-valued #[order(N)] — is a genuine #[procmacro] emitting a re-checked MetaProperty through the emission boundary (Procedural macros). There is no compiler builtin, no std::mlt, and no reserved MLT diagnostic code; the expander is the package’s own procmacro, not a privileged compiler path. MLT is one higher-order type theory among several (potency, ML2, powertype), so the substrate stays neutral about which one a model commits to.
• std::temporal / std::lifecycle become declarative library macros; whether each operator ships native or library is a scoping choice once the engine exists.

// std/temporal.ar — a declarative desugaring to rule-body atoms (no computation)
pub macro since {
    ( $lhs:rule since [ $lo:literal , $hi:literal ] $rhs:rule ) => {
        @meta_window($t, $lo, $hi), $rhs at $t, holds_throughout($lhs, $t, now)
    };
}

Lean correspondence

The substrate at spec/lean/Argon/Substrate/Macro.lean mechanizes the shape of macro declarations — MacroAtom = declarative MacroDecl | procedural ProcMacroDecl as @[language_interface] carriers policed by the drift gate. Per RFD 0037 D7, the substrate boundary is held at the typed AST: macro expansion is untrusted and Rust-side, and assurance comes from re-checking its output — the tier classifier runs last, the content hash is re-derivable, and the drift gate covers the MacroAtom shape. Mechanize the re-checker, not the producer.

The tier-honesty theorem — that classify ∘ expand lands a program on the same decidability class as its expansion — is statable only once expand is a total Lean object over an inductive Syntax type (RFD 0040 D7). The scope-set hygiene algebra and a full expansion-preservation theorem are out of scope.

The MLT-relational kinds — instanceOf, specializes, categorizes, partitions, subordinates — live in spec/lean/Argon/MetaCalculus/MLTKinds.lean, with the round-trip theorem classify_declOfKind; the elaborator emits canonical metarel_decl events via declOfKind.

Testing

A test declares an in-language unit test: a named imperative block run against a fresh world by ox test. Its name is a string literal; its body is the mutate-body statement set (mutate) plus the assert statement. An assert mirrors require, except a failed assert records a pass/fail outcome and execution continues (rather than aborting). Three assertion forms exist: the value/boolean form assert <expr>;; the derivability form assert [not] derivable F(args);, which tests membership / non-derivability of a fact against the materialized extent with world-honest four-valued outcomes keyed on the tuple’s truth value — present unrefuted (is) ⇒ PASS/FAIL, explicitly refuted (not) ⇒ FAIL/PASS under either world, well-founded-undefined (can) ⇒ a loud INCONCLUSIVE for BOTH polarities (an undefined atom is never a definite not; the exact pin is a scenario truth = "Can" expect row), asserted-and-refuted (both) ⇒ PASS/FAIL (positive support exists), absent under closed-world ⇒ FAIL/PASS, absent under open-world ⇒ a loud INCONCLUSIVE (absence is unknown, not false, World assumptions (CWA / OWA)); and the rejection form assert rejects [( Pkg::Code )] { … }, which asserts that a write block is refused by a write-path guard (a where-invariant, a check delta-guard, a group axiom, …) — a genuine guard rejection PASSes (matching a pinned code if given), an accepted write FAILs, and a non-guard error ERRORs loudly so a broken test never masquerades as a passing rejection. derivable and rejects are contextual keywords (leading position only). The runner, the full assertion semantics — including reads over the deductive plane, the outcome tables, and the guard-vs-non-guard classification — isolation, and the scope are specified in The test atom — ox test.

test-decl ::= attribute* 'test' String '{' test-stmt* '}'
test-stmt ::= mutate-stmt            // `mutate`: let / insert / update / delete / for / require / calls
           |  'assert' expr ';'
           |  'assert' 'not'? 'derivable' IDENT '(' (expr (',' expr)*)? ')' ';'
           |  'assert' 'rejects' ('(' path ')')? '{' mutate-stmt* '}' ';'

(The fixture / expect block forms are reserved and do not parse.)

pub type Account { name: String }

// A test constructs a world top-to-bottom and asserts over it; `ox test`
// runs each test against its own fresh store and reports PASS / FAIL / ERROR.
test "a constructed account carries its name" {
    let cash = insert Account { name: "Cash" };
    assert cash.name == "Cash";
}

Discovery. ox test runs test declarations from mod-reachable modules and auto-discovers every *.ar anywhere under the package’s tests/ directory (recursive, any depth — so no test under tests/ silently fails to run), elaborating them as part of the package — so a test placed in the reserved tests/ directory runs without mod-wiring, symmetric with scenarios/*.toml. This is test-mode only: tests/*.ar never enters ox build’s artifact. See Runtime contract.

Isolation. Each test runs against its own fresh store seeded with the package’s declared facts; no test sees another’s writes, so test ordering is unspecified and irrelevant. Within a test, the body’s writes are visible to later assertions, including the facts they derive (read-your-writes over the committed + deductive state). See Runtime contract for the ox test runner and the assertion semantics in full.

Scenario harness — ox run-scenario

An .ar package declares the ontology; it does not carry data. So a built .oxbin queried with no fixtures answers against an empty store. A scenario is a small .toml script that seeds the store and then reads it back, so a model ships with realistic, reproducible state — and, with assertions, with executable checks.

A scenario file lists an ordered sequence of steps. Each [[step]] is tagged by do:

[[step]]
do   = "mutate"                  # invoke a declared mutation
path = "norms::register"
args = { p = "alice", age = 25 }

[[step]]
do     = "query"                 # run a declared query, print its rows
path   = "norms::findEmployeeNamesOfCompany"
args   = { c = "acme" }
label  = "employees of acme"     # optional, echoed in the output

[[step]]
do      = "derive"               # dump a derived predicate's extent
name    = "spouses"              # the rule head's short name
explain = true                   # optional: annotate each tuple with its proof tag

[[step]]
do    = "compute"                # invoke a declared `fn`, print its single result
path  = "norms::getSpouse"
args  = { p = "alice" }

Document order is execution order. A scenario interleaves writes and reads: populate, look, mutate again, look again — each read sees the state at that point. The four kinds map to the same operations as the standalone commands: a mutate step runs a declared mutation (with the same check-guard handling as a write over HTTP); a query step runs a declared pub query and prints its rows; a derive step dumps a derivation’s extent by its rule-head short name, the read ox derive <oxbin> <rule> performs (with explain = true adding the Rule atom — fn, derive, query, mutate, check proof tag per tuple); a compute step evaluates a declared pub fn and prints the single value it returns.

A query step’s args is what makes a parameterized declared query do a keyed lookup. A pub query findEmployeeNamesOfCompany(c: Company) -> … whose body binds c looks c up only when c is supplied; with no args, the parameter degrades to a free join variable and the query enumerates the whole extent. A derive step takes no args — a derivation has no parameters, so it always dumps the full extent.

Argument typing

Each args table maps a parameter name to a TOML value, typed into the runtime’s value space by one shared rule (the same path expect tuples use, below):

A bare string defaulting to an individual is the load-bearing convention: the same name in the source and in the scenario refers to the same entity. Array values and a non-finite float are rejected with a clear diagnostic.

Assertions — expect

Add an expect table to a step and it stops being a printer and becomes a test: its result is diffed against the expectation and a PASS/FAIL verdict is reported. Which sub-keys apply depends on the step kind:

[[step]]
do     = "query"
path   = "norms::findEmployeeNamesOfCompany"
args   = { c = "acme" }
expect = { equals = [ [{ text = "Dave" }], [{ text = "Alice" }] ] }

[[step]]
do     = "derive"
name   = "isDisenfranchised"
expect = { empty = true }

[[step]]
do     = "compute"
path   = "norms::getSpouse"
args   = { p = "alice" }
expect = { value = "dave" }      # a single expected value

[[step]]
do       = "mutate"
path     = "norms::register"
args     = { p = "bob", age = 12 }
expect   = { rejected = "Norms::E001" }   # assert a check guard rejects it

• A query or derive step takes the row-set sub-keys: rows = N (exact count), contains = [tuple, …] (every listed tuple is present, count-sensitive), equals = [tuple, …] (the result set matches exactly, order-insensitive multiset equality), empty = true (no rows).
• A compute step takes value = <toml value>: a single expected value.
• A mutate step takes rejected = "<CODE>": assert the mutation is rejected by a check guard carrying that user code. A rejection by that code is a PASS and the run continues (the rejected transaction committed nothing); a success or a rejection by a different code is a FAIL. Without rejected, a guard rejection halts the scenario.

The correctness crux is that an expected value is typed through the same rule as the step args, and the diff is by value identity — never by rendered string. So an entity-valued result column matches a bare-string or { individual = "…" } expectation, but never a { text = "…" } one; a Text "dave" is never equal to the individual dave. A sub-key applied to the wrong kind (value on a query, rows on a compute, an unknown key) is a loud scenario error, not a silent no-op.

Files, discovery, and running

A package carries scenarios as a sibling demo.toml and/or any number of files under a scenarios/ subdirectory:

ox run-scenario <pkg>                       # run every discovered scenario
ox run-scenario <pkg> --scenario voting     # run scenarios/voting.toml (or a sibling voting.toml)
ox run-scenario <pkg> --scenario path/to.toml
ox run-scenario <pkg> --extent norms::Voter  # also print a concept extent after the run

With no --scenario, run-scenario discovers every scenario — the sibling demo.toml plus every scenarios/*.toml, filename-sorted for determinism — and runs them all. Each scenario runs against its own freshly-loaded, freshly-seeded store re-derived from the artifact bytes, so a mutation in one scenario cannot leak into another’s reads and the order across files is irrelevant. --scenario runs exactly one: a path verbatim, or a bare name resolving to scenarios/<name>.toml then a sibling <name>.toml. --extent <concept> prints that concept’s extent once the scenario has run.

run-scenario collects every failed assertion (it does not stop at the first) and exits non-zero if any assertion — or any scenario — failed, naming the offending file. A scenario therefore doubles as a CI-usable check.

A single file uses either [[step]] or the older flat [[mutate]] list (a pure population script, applied in order), never both — the whole point of [[step]] is interleaving, which a split across two arrays cannot express. The flat [[mutate]] form is also what ox query and ox derive apply when they find a sibling demo.toml: they seed from [[mutate]] fixtures, then run their own read. A [[step]] scenario beside one of those commands is not run by them (they have nowhere to surface the interleaved reads); they print a warning pointing at ox run-scenario.

The scenarios/ directory is the integration-.toml surface, distinct from tests/, which holds the in-language test atom (The test atom — ox test). The two are complementary: scenarios/ scripts the runtime from outside the language with a .toml harness; the test atom expresses checks inside the language.

The test atom — ox test

A test is a named imperative block, run top-to-bottom against a fresh store. Its name is a string literal; its body is the mutate-body statement set (let / insert / update / delete / for / require and declared mutation/fn calls — mutate, RFD 0015) plus the assert statement:

test "accountBalance derives the posted amount per account" {
    let cash = insert Account { name: "Cash" };
    let rev  = insert Account { name: "Revenue" };
    let e    = insert Entry { memo: "sale 1" };
    postPair(cash, rev, cash, rev, e, 100.50);
    assert accountBalance(cash) == 100.50;   // reads the derived value
    assert accountBalance(rev) == -100.50;
}

An assert mirrors require exactly, with one difference: a failed require aborts the body; a failed assert records a pass/fail outcome and execution continues. true is a PASS, false a FAIL, and an evaluation error (an unbound reference, a non-boolean result, a missing field, a value not derivable in the current state) is an ERROR (the test errors; it never panics). Setup and assertions interleave naturally, so there is no separate fixture block.

Asserting over the deductive plane. A condition that names a derived predicate or a declared pub query — accountBalance(cash), or the nav-method form x.active_leases() — is evaluated against the reasoner’s materialized extent at the fixpoint of the current committed state, the same read path ox query / ox derive and the for x in <derive> snapshot use. A keyed call (accountBalance(cash)) selects the row whose leading columns match the argument and returns its head-carried value; with no matching row the assert ERRORs (the value is not derivable), and an ambiguous match is a loud error too. Scalar comparisons, field access, arithmetic, and aggregates evaluate as in a require guard. This is the point of testing a reasoning system: an assert checks what the rules derive, not just what was stored.

Asserting derivability — assert [not] derivable F(args). The value-read assert above answers what value a keyed derive carries; the derivability form answers whether a fact holds at all — membership and, crucially, non-derivability. assert derivable F(a, …) passes when a row whose leading columns equal the resolved args is in F’s materialized extent; assert not derivable F(a, …) is its negation. The predicate F resolves the same way the value-read assert and for x in <derive> do — a derive head, a declared pub query, or a base rel. The predicate slot accepts a qualified path (assert derivable students::adult(p), assert not derivable pkg::accounts::adult(p)), resolved by the same ::-suffix matching the rest of the runtime uses: a bare leaf resolves when it is unambiguous, and qualifying disambiguates a name carried by two heads in different modules — that case stays a loud ERROR for the bare form, naming every candidate, so qualification is the way to pick one. Partial args test prefix membership (derivable amtOf(acme) over amtOf(account, money) = “some row has account == acme”); zero args test extent non-emptiness (derivable F()). A predicate that names nothing is a loud ERROR, not a silent outcome. derivable is a contextual keyword — recognized only in leading position after assert / assert not, so it stays usable as an ordinary identifier everywhere else.

The outcome is world-honest and four-valued: the read consults the matching tuple’s truth value — the definite extent, the head’s well-founded-undefined companion, and the explicit refutation extent (pub not_fact) — and only a tuple absent from all three falls to the predicate’s world assumption (World assumptions (CWA / OWA)):

The can row is the load-bearing case on the deductive plane. An atom the well-founded semantics leaves undefined (a recursion-through-negation standoff, truth values) is neither definitely true nor definitely false — so neither polarity is assertable: a definitely-false atom and an undefined one must never be conflated at this surface, and assert not derivable over an undefined atom is a distinct, loud INCONCLUSIVE, never a silent pass. The teaching detail names the value and the exact-pinning vehicle — a scenario expect row { tuple = [ … ], truth = "Can" } (Scenario harness — ox run-scenario), which pins the third truth value where the polarity form cannot. The both row is the opposite discipline: an overdetermined atom is not unknown — positive support exists, so derivable passes and not derivable fails, the detail naming both. The not row reads an explicit refutation as definite-false under either world assumption: a refutation is present evidence, not open-world absence. The per-tuple classification joins the extents exactly as federation’s information-join does (truth values, can ⊕ not = not): an explicitly refuted standoff is not — the refutation supersedes the undefined companion (and it is not both: a standoff supplies no definite positive support). When a partial-args (prefix) assertion matches several rows, an unrefuted positive match keeps the assertion at plain is (a contradictory sibling row does not mask definite support), and a refutation decides the prefix claim only as far as it reaches: a full-arity refutation refutes exactly the asserted tuple (definite not under either world), while under an open-world predicate a refutation of one tuple beneath a partial prefix leaves the remainder unknown — assert not derivable F(prefix) stays INCONCLUSIVE, the detail naming the near-miss (under a closed world the remainder’s absence is already definite, so the prefix decides).

The open-world absent row is the same soundness case it always was. Under the open-world assumption absence of evidence is not evidence of absence: a missing row is unknown, not false, so closed-world non-derivability is not assertable and must never silently pass. The runner reports a distinct, loud INCONCLUSIVE carrying a teaching detail that names the open-world cause and the two ways forward (assert a positive outcome instead, or mark the concept #[world(closed)] if it should be closed). This composes with the world-honest negation-as-failure of the rule engine: a derivability assert reads the same world each negated atom does.

Asserting rejection — assert rejects [( Pkg::Code )] { … }. Argon is a constraint language; a model’s most important property is which writes its where-invariants and check delta-guards turn away. The two forms above assert positive outcomes — the negative-enforcement half is assert rejects { <mutate-body-stmts> }, which asserts that the block’s write is refused by a write-path guard. The block admits the full mutate-body statement set (insert / insert iof / update / delete / mutation calls); it runs against an isolated copy of the test world, so it commits nothing back regardless of outcome. An optional code pin assert rejects(Pkg::Code) { … } requires the rejection to carry that exact diagnostic code. Like derivable, rejects is a contextual keyword — recognized only in leading position after assert — so it stays usable as an ordinary identifier elsewhere.

The outcome is three-valued, and the guard-vs-non-guard distinction is load-bearing:

A guard rejection is a genuine constraint refusal on the write path — a where-invariant violation (OE0668), a check delta-guard refusal (which is also how a group axiom — disjoint / complete / partition — surfaces, carrying the check’s own Pkg::Code), an insert iof onto a defined (iff) concept (OE0211), a write onto an abstract or fixed-introduced type (OE0233 / OE0234), a construction-completeness refusal (OE0207 / OE1014), a property write to an unclassified individual (OE0238), a relation write over a non-existent endpoint or past a declared cardinality (OE0232 / OE1341), or a typed-slot write whose individual is classified under a concept a declared disjoint / partition group makes disjoint from the slot’s declared concept — refused on both slot planes, a relation endpoint (OE1428) and a concept-typed field (OE1435), because classifying that individual under the slot’s concept would itself violate the group, so the write can never be satisfied in this state or any later one (Group axioms). Only these satisfy rejects.

The declared-disjointness pair is admitted at its write-time codes only. The same disjointness is also refused one plane earlier, at elaboration, wherever the written value’s concept is statically known — the annotated-parameter spelling, where a mutation parameter’s declared concept already contradicts the slot’s (OE1426 endpoints, OE1434 fields). Those build-plane refusals are not observable through rejects at all, and no widening of this set could make them so: they refuse at ox check, so the package produces no artifact and the test run never happens. A reader who spells the disjoint write with an annotated parameter and expects a passing rejection test gets a compile error instead — the fix is to write the block over a value whose conflicting classification is only knowable at write time (an individual bound by an earlier insert in the test body, as the runtime codes above describe), or to pin the build-plane refusal the way every other ox check refusal is pinned, as a refusal fixture rather than a test. A non-guard error — a typo, an unbound reference, a type error, an unevaluable term, a stray require failure — is reported as a loud ERROR, never counted as a rejection: a broken test must never masquerade as a passing rejection test. An accepted write is a FAIL (and is rolled back, like any other block outcome, so it does not pollute the rest of the test). Use the positive forms to test that a legal write is accepted.

Isolation. Each test runs against its own fresh store seeded with the package’s declared facts (the same fresh-store-per-run discipline as the scenario harness, Scenario harness — ox run-scenario). No test sees another’s writes, so tests are order-independent. Within one test, the body’s writes are flushed and the read-model maintained before each assert, so an assert observes every earlier write — including the derived facts they entail (read-your-writes over the committed + deductive state).

Discovery + running. ox test runs every test from two sources, unioned: (1) any test declaration in a mod-reachable module (e.g. tests/mod.ar reached by mod tests;), and (2) every *.ar anywhere under <pkg>/tests/, which ox test auto-discovers (recursive, any depth — a nested tests/sub/foo.ar is discovered too, so no test under tests/ silently fails to run — filename-sorted) and elaborates as part of the package, so each sees the package’s full vocabulary. This mirrors how ox run-scenario auto-discovers scenarios/*.toml: a test placed in the reserved tests/ directory runs without mod-wiring. A tests/ file that is also mod-reachable is folded exactly once (its tests never double-run). A discovered tests/foo.ar references package items by their package-absolute path (pkg::…). This discovery is test-mode only: ox build / ox check and the shipped .oxbin never include tests/*.ar — tests do not ship. Tests are inert at query / serve time; only ox test enumerates and runs them:

ox test <pkg>                 # build the package (+ tests/), run every test, report
ox test <pkg> --filter NAME   # run only tests whose name/path contains NAME

A tests/*.ar with a parse or resolve error fails loudly (ox test aborts with the diagnostic), never a silent skip; a package with genuinely no tests anywhere prints “no tests found” and exits 0.

ox test builds the package (so the run reflects current source), runs every discovered test, and prints a PASS / FAIL / ERROR / INCONCLUSIVE line per test — a failed or inconclusive assertion shows its rendered source text and why it could not pass — followed by an N passed, M failed, K errored, I inconclusive summary. A test’s rollup status takes the strongest of its assertions in the precedence Error > Fail > Inconclusive > Pass. It exits non-zero if any test fails, errors, or is inconclusive (a test you cannot decide is not green), so ox test doubles as a CI-usable gate (like ox run-scenario).

Assertion forms. Three forms are admitted. The value/boolean form is assert <bool-expr>; — scalar comparisons (==, !=, <, <=, >, >=), field access on bound entities (x.field, chained x.a.b), arithmetic on those, the aggregate/comprehension forms, and the deductive-plane reads above (a derived-predicate / pub query keyed call, and the nav-method x.method() form). The derivability form is assert [not] derivable F(args); with the world-honest four-valued semantics above. The rejection form is assert rejects [( Pkg::Code )] { <mutate-body-stmts> } — the negative-enforcement half above. All three are test-only: a stray assert (any form) in a mutate / fn body lowers to an unsupported form and ox check / ox build refuse it up front with OE1318 (the runtime also rejects it, as defense-in-depth) — it is never a silent no-op.

Only the three assert forms above are admitted; anything else is a loud refusal, never a silent pass.

Truth values

Types

Two related types, exported from std::core and in the prelude:

pub enum Truth4 { Is, Not, Can, Both }                              // substrate, no payload
pub enum Truth4Of<T> { Is(T), Not, Can, Both(T, T) }                  // parameterized lift

The unparameterized Truth4 is the substrate bilattice carrier — what the Lean spec mechanizes and what Federation.infoJoin, Consistency.append, and Projection.project operate over. The parameterized Truth4Of<T> is the stdlib presentation type used at query-result boundaries that have already produced typed projections — Is(T) carries the witness for the is verdict; Both(T, T) carries the two disagreeing witnesses.

Locked-substrate semantics (per Foundation/Truth4.lean, Standpoint/Consistency.lean, Standpoint/Federation.lean):

• K3 single-standpoint queries return projections containing only Is, Not, Can.
• FDE across [...] queries may return Both(a, b) when standpoints disagree.
• #[consistency(paraconsistent)] standpoints admit Both internally.

Default visibility and K3 projection

Default query return type is the projection type (e.g., Bool, [Lease]); Truth4Of<T> is introduced only when:

• The query has across [...].
• The return type is explicitly Truth4Of<…>.
• A paraconsistent standpoint admits internal Both.

K3 fail-closed projection. When a single-standpoint K3-context query projects to a non-Truth4 type, Can is folded into the projection per Pietz–Rivieccio Exactly-True semantics:

• Boolean projections: Can → false. Only Is(true) is designated.
• Set / list / record projections: Can-valued cells are omitted from the result set.
• Scalar projections: Can collapses fail-closed (omitted for collection-shaped results, false for Boolean predicates).

To preserve the distinction between Not and Can at the surface, declare the return type as Truth4Of<T> explicitly.

The compiler emits Info-level diagnostics on every across query reminding the modeler that Both may arise.

World assumptions (CWA / OWA)

A world assumption governs how the absence of evidence is interpreted:

• Closed (CWA) — if a fact isn’t derivable, it’s false. Negation-as-failure is total.
• Open (OWA) — if a fact isn’t derivable, it’s unknown. Negation requires positive disproof.

The blessed default is CWA; OWA is a live per-concept opt-in. Every concept Argon evaluates is closed-world unless it carries a #[world(open)] mark: negation-as-failure over the stratified / well-founded fixpoint (Rule atom — fn, derive, query, mutate, check, truth values) treats an unmarked concept’s absent membership as definite-false. The package-level default_world (CWA unless a manifest sets it otherwise) governs every concept without an explicit mark. This default is a deliberate choice: an Argon program is a data system whose extents are the authority for what is true, and CWA is the regime that makes “not in the extent” mean “false”. A modeler who wants the OWL/DL open-world reading for a specific concept opts that concept in with #[world(open)], described below (RFD 0045, #787/#796).

CWA is the operative default because Argon’s primary use is application data — counts, payments, schedules, classifications — where the stored extent is the closed world. Concepts that model genuinely-incomplete knowledge (where “absent” means “unknown”, not “false”) opt into the open-world reading per the surface below.

Per-concept OWA opt-in (#[world(open|closed)]) — live. The surface is a #[world(...)] attribute on an ontologically-classified concept:

#[world(open)]
pub type LegalAgent { mut name: String }   // OWA — `unknown` is distinct from `false`

The world directive is executed (RFD 0045 D2): the elaborator reads the policy word — open or closed, any other word is a loud refusal — records the concept’s world assumption on the per-concept world map (keyed by qualified concept path), and the reasoner stamps that map onto every evaluation catalog so each negated concept-membership atom is read under its own concept’s world. The attribute is concept-only (OE0707 on other placements). Concepts without the attribute inherit the package default_world (CWA by default).

The OWA semantics. The world a concept declares changes how the substrate reads its absence:

Interaction with negation-as-failure (Rule atom — fn, derive, query, mutate, check). Under CWA, not P succeeds whenever P is not derivable. Under OWA, an absent P(x) is unknown, not a definite not — so a closed-world not H whose derivation depends on an open-world negation does not get to read that unknown as false. Rather than silently over-asserting the head, the substrate refuses that genuinely-unsound shape at ox check / ox build (OE1367 NegatedOpenWorldDerived): mark H’s concept open-world too (so not H tolerates the unknown), or restructure so the open-world negation does not flow into a closed-world-negated head. This is world-honest negation-as-failure: the engine honors default_world and each concept’s mark instead of evaluating closed-world unconditionally. R(args) is unknown reads R’s completed well-founded-undefined companion; it does not turn ordinary open-world absence into rows. Recursive companion reads refuse with OE1441.

Interaction with the write side. A concept’s world governs its compiler-synthesized structural checks. Under the closed-world default a complete/partition covering check fires when no member membership is derivable (OE0241) and a disjoint overlap check refuses a double-classification (OE0240). Under an open-world concept the covering check softens to refuse-on-K3-not — refuse only on a definite violation, tolerating the merely-unknown case — while disjointness stays world-invariant (a positive overlap is definite under any world). This is the RFD 0045 D1/D2 design.

Interaction with the test atom. assert [not] derivable F(x) (The test atom — ox test) is four-valued: it reads the matching tuple’s truth value first, and F’s world only for a tuple absent from every extent. A present, unrefuted row is is (PASS for derivable, FAIL for not derivable); an explicitly refuted row (pub not_fact) is not — definite-false under either world, a refutation being present evidence rather than absence; a well-founded-undefined atom is can — neither polarity is assertable, so the runner reports INCONCLUSIVE for both and points at the scenario truth = "Can" pin; an asserted-and-refuted row is both — positive support exists, so derivable passes. Only genuine absence falls to the world assumption: under CWA it is definite non-derivability (FAIL for derivable, PASS for not derivable); under OWA it is unknown, so closed-world non-derivability is not assertable — the runner reports a distinct, loud INCONCLUSIVE, never a silent pass.

Interaction with refinement (Refinement). The world a concept declares makes iff-derived membership three-valued — unknown does not grant membership, and a primitive where invariant is the dual where only a definite false denies a write — whereas under CWA unknown collapses to false in both directions. The three-valued refinement field-access discipline is a separate mechanism: a refinement predicate reading a field with no recorded value evaluates to unknown rather than failing — the K3 fail-closed boundary of Refinement, orthogonal to the concept-level world assumption. A missing field makes a predicate unknown; the world assumption then decides whether that unknown collapses to false (CWA) or is preserved (OWA).

Required-field completeness under CWA. Under the closed-world default a required field that is unasserted is a schema violation, not an unknown. OE1014 RequiredFieldUnasserted fires for the in-body construction case — a mutate body that classifies an individual with insert iof and populates its fields in the same body — at body end / commit time (see mutate). The construction-time gate for brace construction (insert T { … } missing a required field, OE0207) is unconditional. Under an #[world(open)] concept an unasserted required field is unknown rather than a violation.

Cross-world conservativity (mechanized). A CWA-true result lifts safely into an OWA consumer — positive evidence stays positive when more information may yet arrive. The base transfer theorem is mechanized at TypeSystem/Soundness/CwaOwa.lean (cwa_owa_transfer): a refinement membership established under CWA remains valid when re-evaluated under OWA, and cwa_isCwa_preserved_under_info_increase extends this to a more-informative consistent (K3) state. The reverse is provably not sound (owa_to_cwa_not_sound): a CWA conclusion that holds only via the closed-world collapse of an unknown to false does not transfer. The module is deliberately parameterized over the WorldAssumption — the CWA default is a surface/engine policy, not a substrate theorem, so the mechanization arbitrates the relationship between the two regimes without privileging either. The bitemporal lift of the transfer is in Locality/Temporal.lean.

Module-extraction interaction. Cross-module imports preserve CWA conclusions about the imported signature via ⊥-local module extraction; the Σ-scoped conservativity theorems are in Module extraction (tree-shaking) (Locality/ScopedConservativity.lean, Locality/DomainConservative.lean).

Per-(standpoint, concept), not per-(concept, time). A world assumption is declared per-(standpoint, concept), never per-(concept, time). A modeler needing different closure disciplines across valid-time would declare two or more standpoints with VT-scoped activation conditions and compose them via standpoint federation (Standpoints and modal operators); the substrate WA-map signature has no time argument. Attempting a per-concept closure with an explicit VT scope without standpoint decomposition is refused with OE0810 WorldAssumptionTemporalIndex.

Reasoning

A derive program is a set of rules (derive); its meaning is the set of tuples those rules derive. This chapter fixes that meaning: the least-fixpoint model of the positive program, the stratification that orders negation, the well-founded semantics that handles recursion through negation, and the defeasibility layer that compiles overrides onto all of it. The surface — what a derive rule looks like and what each clause is allowed to say — is in derive; this chapter is what the engine computes from it.

Least-fixpoint model

A positive derive program (no negation, no aggregation) denotes a single model: the least fixpoint of its immediate-consequence operator. Start from the ground facts, apply every rule once to derive new tuples, repeat until nothing new appears. Over a finite domain this terminates, and the result is unique — independent of the order rules fire. Multiple derive clauses with matching head name and arity union into one relation node, so a seed tuple and a recursive clause over the same head share a fixpoint (seeds ∪ derived-closure).

Aggregation extends the operator without breaking uniqueness, provided each aggregate reads a strictly lower stratum than its head writes (the stratification below). The aggregate fold then sees a converged input relation before it runs, so the fixpoint over the layered program is still unique.

Stratified negation

Negation breaks the monotonicity the least fixpoint relies on: a tuple that adds to a positive relation can remove a tuple that a not atom guarded. Stratification restores order. The rules are partitioned along their axis dependency graph — which axes a rule’s body reads against which axis its head writes — and each layer is evaluated to fixpoint before the layer above it reads its negation. A rule’s body negation must read a relation already converged in a lower stratum.

The graph must be acyclic for this layering to exist. The Lean substrate proves (Theorem 2) that a cycle in the axis dependency graph admits a Cat1/Cat2 rule pair whose stratified fixpoint is order-dependent — there is no canonical layer assignment, so the program has no single stratified model. Cross-stratum, acyclic negation is ordinary stratified negation and is evaluated by this layering.

A negation cycle that no stratification can layer — p :- not q, q :- not p — is not rejected. It is dispatched to the well-founded semantics below. (The diagnostic that once rejected such a cycle, OE1309, no longer fires from stratification; it survives only as the dispatch seam.)

Well-founded semantics

Negation reads against the well-founded model, computed by the Van Gelder–Ross–Schlipf 1991 alternating fixpoint. WFS is the default because the well-founded model always exists and is unique — every program has exactly one, with no choice for the engine to make. The headline consequence: recursion through negation is accepted. A negation cycle that strict stratification cannot layer is evaluated by the alternating fixpoint rather than refused.

The alternating fixpoint is three-valued: every atom is true, false, or undefined. The engine materializes the definitely-true extent as the head’s rows, and an atom the alternating fixpoint cannot pin to true or false — a genuine standoff — is carried alongside as the head’s undefined extent. The query surface is four-valued: a definitely-true tuple is an Is row, and an undefined tuple surfaces as a Can row, by default — never silently omitted, because an omitted standoff is byte-indistinguishable from a definite Not (the epistemic failure the Truth4 discipline exists to prevent). A rule body still joins only against definite rows — an undefined atom does not fire downstream rules; propagating undefined-ness through body joins is the engine-level three-valued lift, tracked separately.

For conditional obligations this keeps the sound projection while restoring the honesty: an obligation whose trigger is genuinely undecided neither fires nor is denied — and the read says so (Can) instead of omitting it.

The envelope contract: the four-valued agent view carries Can rows inline and counts them in hidden.can; the human fail-closed K3 projection (opt-in) drops Can rows from the row list but still reports them in hidden.can — drop-but-count, never a silent collapse. ox derive prints the undefined extent after the definite tuples (silent when empty). The defeat-plane evaluator is two-valued wherever the defeat graph is acyclic — where no defeat target depends back on its own attacker, every head is definitely true or definitely false and contributes no undefined extent. A genuine mutual-defeat cycle — a target whose attacker’s derivation depends in turn on that same target (a rule-dependency cycle through the attacker’s derivation, not a defeat-graph identity cycle, which OE0718 refuses at build time) — has no stable two-valued answer: those heads are undefined under the well-founded model, surfaced as Can like any other undefined extent, and are never resolved by evaluation order. The legacy strength-stratified evaluator remains two-valued by contract.

#[brave] / stable-model semantics — multiple two-valued models, with credulous and skeptical readings — is out of scope (Out of scope). WFS is the single evaluation discipline.

Defeasible reasoning

Real ontologies have exceptions and overrides; classical Datalog does not. Argon’s defeasibility (RFD 0028) makes them first-class without letting any rule lie about what it derives. The design has three commitments:

1. Honest heads. A rule derives exactly what its head says. An unmarked derive rule is strict — classical Datalog, exactly as derive; its conclusions cannot be overridden.
2. The attack is a directive, not grammar. Whether one rule displaces another is a statement about rules, carried in the directive plane above the rule, never a clause inside its body.
3. Strategy is a compilation scheme. The meaning of a defeasible program is the meaning of its compilation onto the core stratified/WFS semantics. No separate reasoner runs; the engine stays strategy-blind.

The directive vocabulary

The canonical example — adults can vote by default, felons are disenfranchised, special-class members vote regardless — reads true at every line:

// strict = unmarked: special-class members vote, period (unattackable)
pub derive can_vote(p) :- SpecialClass(p);

// the overridable default
#[default]
#[label(adult)]
pub derive can_vote(p) :- Adult(p);

// the exception: an honest head, and the attack as a directive
#[defeats(can_vote(p))]
pub derive disenfranchised(p) :- Felon(p);

No rule spells the head it denies. The exception lives under its own name (disenfranchised); the attack rides the directive plane. The pure “block without asserting” defeater (Governatori’s ⇝) is the degenerate case — a #[defeats(…)] rule whose head no one reads.

Targeting

A #[defeats] target is resolution-checked at elaboration (goto-def-able); an unresolvable target refuses loudly. A target resolves over the attacking module’s import-scoped catalog — its own rules plus the pub rules reachable through its use imports (RFD 0082), so an exception can live in another file and name what it overrides under its own honest name. Scope follows ordinary name resolution exactly: importing the rule (a use leaf, glob, or alias) puts its bare short name in scope; importing only its module binds the module name, so its members are addressable by the qualified-path spelling, not by bare name. Three targeting forms ship, plus qualified-path disambiguation:

• Head-level — #[defeats(can_vote(p))]: attacks every #[default] clause of that head.
• Clause-level — #[defeats(can_vote.adult(p))]: attacks exactly the clause labeled adult. This is lex specialis — the specific rule defeating the general clause’s label, an explicit module-stable edge rather than a pair of magic priority integers.
• Trait-qualified — #[defeats(Vote::can_vote(p) @ A)]: attacks a trait member’s clause at a given impl target, using the qualified catalog naming (Rule-atom grammar).
• Qualified-path disambiguation — #[defeats(other_module::can_vote(p))]: when a bare short name is visible from more than one imported module it is ambiguous and refuses (OE0736); the qualified path resolves the head against exactly the named module. An own-module declaration shadows imported ones, like every other resolution position.

Cross-module targeting has three bounds. Defeat visibility equals ordinary name visibility (OE0737): a rule the attacking module cannot name is not a legal target — a non-pub rule is attackable only from its own module and that module’s descendants (the ordinary descendant-private rule), never from a distance. #[default] is the consent token: a rule can be overridden from another file only if its own author marked it #[default] (OE0717, unchanged). The edge stays inside one package (OE0738): a package is a trust and versioning boundary, and a dependency update must not silently change a program’s conclusions — cross-package composition goes through ordinary use of public predicates (honest heads), never through a defeat edge.

Arguments resolve against the decorated rule’s variables. #[defeats(can_vote(p))] on disenfranchised(p) blocks can_vote exactly for the p the attacker derives — per-tuple blocking, not head-wide suppression. A #[defeats] argument that binds in neither the head nor the body of the rule is a loud error (OE0721), never a fresh variable.

Discipline

• Strict conclusions are unattackable (OE0717). A #[defeats] target resolving to a head or clause not marked #[default] refuses: adding rules to a classical program can only add conclusions.
• Defeat-graph cycles are refused (OE0718). The graph over resolved rule identities is acyclic by build-time check; cyclic attack structures are where the well-behaved compilation stories diverge, and Argon refuses rather than picking one silently.
• Defeated defeaters are legal — a #[defeats] rule may itself be #[default] and be attacked in turn (the exception to the exception), as long as the chain bottoms out.
• Team defeat, ambiguity blocking. A tuple is in the head’s extent iff some clause not attacked on that tuple derives it — an unbeaten teammate keeps the conclusion. A blocked tuple is simply absent from the extent; it does not propagate a third truth value downstream. This clean present/absent verdict holds wherever the defeat is acyclic. It does not hold on a genuine mutual-defeat cycle — a target whose attacker’s derivation depends back on that same target (a rule-dependency cycle, distinct from the defeat-graph identity cycle OE0718 refuses) — where the tuple is neither definitely present nor definitely absent but undefined under the well-founded model (surfaced as Can, above); there is no order-of-evaluation answer.
• Downstream rules read warranted extents. Once a tuple is blocked, every later positive body atom reads the post-defeat extent, including through any number of strict intermediate heads. Marking a downstream reader #[default] makes that reader overridable; it does not switch its inputs back to the pre-defeat support catalog. If no rule attacks that reader, it derives the same tuples as an otherwise identical strict reader.
• Duplicate labels per head refuse (OE0719); labels are per-head identities.

Worked: acyclic defeat vs a mutual-defeat cycle

When the attacker’s own derivation never reads back through its target, every head settles — two-valued, no third truth value anywhere. A defaulted discount, attacked by a fraud hold whose body reads only base facts:

#[default]
pub derive discount(o) :- Large(o);

#[defeats(discount(o))]
pub derive fraud_hold(o) :- Flagged(o);

A flagged large order’s discount is definitely false — absent from the extent, not undefined. The hold fires, the default is blocked, and nothing downstream ever sees a Can.

Now let each attacker’s body read the other default’s head:

#[default]
pub derive keys_a(p) :- Employee(p);

// a's disqualifier holds exactly when b's access does
#[defeats(keys_a(p))]
pub derive conflict_a(p) :- keys_b(p);

#[default]
pub derive keys_b(p) :- Employee(p);

// ... and b's disqualifier reads a's access back
#[defeats(keys_b(p))]
pub derive conflict_b(p) :- keys_a(p);

The defeat graph itself is still acyclic — conflict_a attacks keys_a, conflict_b attacks keys_b, no attacker is anyone’s target — so the program is admitted, not refused. But the rule-dependency graph now cycles through negation: keys_a holds unless conflict_a blocks it, conflict_a holds exactly when keys_b does, and symmetrically back. Neither head can settle: granting keys_a blocks keys_b, which withdraws the very conflict that would have blocked keys_a — and the mirror-image assignment is equally supported. There is no stable two-valued answer, and no evaluation order is allowed to invent one. Both keys_a and keys_b surface undefined (Can) for every employee, per the envelope contract above.

Because undefined is a defined outcome here — not an error — the elaborator does not refuse this program; it warns. OW0740 (mutual-defeat-cycle-undefined) fires at elaboration whenever the resolved defeat plane forms such a rule-dependency cycle through defeat, naming the mutually-defeating public heads (here keys_a and keys_b) so an author who expected a definite verdict learns those heads read Can. The lint is representation-independent — it inspects the resolved defeat edges and the lowered rule bodies, not whether the plane is compiled to strict rules or evaluated by the runtime resolver — and fires only for this shape: never for the OE0718 identity cycle (refused earlier), never for a defeat-free recursion-through-negation cycle (the ordinary well-founded treatment above), and never for the acyclic stratified-defeat fragment (provably two-valued). To recover a definite classification, break the cycle: remove or redirect one attack so no attacker’s derivation reads back through its own target. A strict base clause is a partial remedy only — it settles the tuples it covers (those become definite, and definite verdicts cascade around the cycle for them), but the heads stay cyclic for every other tuple and the warning stands.

Strategy #1: Governatori with explicit superiority

The strategy is Governatori-style defeasible logic with explicit superiority and ambiguity blocking, specified as its Maher-2021 three-stratum compilation onto the core stratified/WFS semantics:

1. Support — run every clause (strict + default, plus the attacker rules’ own honest heads) to fixpoint over the materialized base, and attribute each clause’s contribution over that converged catalog — a recursive clause sees its own prior tuples, so transitive closure does not under-derive.
2. Blocking, from surviving attackers — project each attacker’s surviving extent (resolved in defeat-graph topological order, which exists because the graph is acyclic) through its edge argument binding to the blocked target tuples (per-tuple). A defeated defeater contributes nothing — it no longer blocks on the tuples where it was itself defeated.
3. Team-defeat fold — strict clauses contribute unconditionally; a default clause contributes the tuples no surviving edge blocks.

Clause attribution composes these strata rather than exposing raw support as a downstream read model. When attributing one defeasible head, the evaluator keeps that head’s own converged support available for recursive clauses, replaces other defeasible heads with their warranted extents, and recomputes strict intermediate heads over those warranted extents. This preserves recursive closure without allowing a downstream default clause to recover a tuple defeated upstream.

The strategy id is recorded in the .oxbin so an artifact is honest about which compilation gave it its meaning. Future strategies (default logic, courteous LP, argumentation, ASP preferences) arrive as use-imported macro-vocabulary packages selected per module; the engine never changes.

Proof tags

Every derived fact carries one of four tags (Rule-atom grammar), surfaced through the provenance channel (ox derive --explain):

• +Δ definitely provable — supported by a strict (unattackable) clause.
• −Δ definitely refuted.
• +∂ defeasibly provable — a surviving #[default] clause supports it after defeat resolution.
• −∂ defeasibly refuted — every supporting clause was attacked.

$ ox derive examples/legal_norms_can_vote can_vote --explain
  +Δ (dave)     // strict special-class clause
  +∂ (alice)    // surviving adult default

For an artifact whose defeat plane was compiled at elaboration (the strict-WFS lowering recorded in the artifact’s defeat-provenance section), --explain additionally prints the compilation header. The header is artifact-scoped — the carrier records the whole module’s compiled plane, whatever rule is queried — and lists the strategy that gave the compiled rules their meaning and, per source clause, its #[default]/strict kind, #[label], emitted internal support relation, and the #[defeats] edges that clause declared (a clause-level target keeps its .label grain):

artifact: defeat plane COMPILED at elaboration (strategy: Governatori with explicit
superiority); 2 source clause(s) lowered to strict WFS rules
  #[default] m::can_vote #[label(adult)] → support $defeat::support::m::can_vote::adult
  strict m::disenfranchised → support $defeat::support::m::disenfranchised::#0
      defeats m::can_vote.adult

The Lean substrate proves the defeat algebra over each clause’s converged contribution: the team-defeat fold realizes the declarative per-tuple warranted set (Argon.Reasoning.Defeasibility.Transform.compiled_extent_eq_warranted), strict conclusions are unattackable (strict_clause_unattackable), ambiguity blocking holds (all_supporting_clauses_attacked_absent), and — modelling the blocking sets as derived from the attackers’ surviving extents rather than as opaque inputs — a defeated defeater no longer blocks (defeated_defeater_does_not_block, block_mono_in_survivors, pardoned_target_survives). The safe interaction with occurrence typing carries over — only narrowings established by strict (non-#[default]) rules are preserved under defeasible attack (Argon.TypeSystem.Soundness.Defeasibility).

Migration from the strength triple

The pre-RFD-0028 surface — #[strict] / #[defeasible] / #[defeater], #[priority(N)], and pub priority blocks — is removed, and refuses loudly (OE0722) with no silent aliasing. The map:

• #[defeasible] → #[default].
• #[defeater] (which spelled the head it denied) → an ordinary rule under its own honest head carrying #[defeats(target(args))]; the targeted clause must be #[default].
• #[strict] → delete it; unmarked rules are already strict.
• #[priority(N)] / pub priority → an explicit #[defeats] edge. Lex specialis is the specific rule defeating the general clause’s #[label]. Derived superiority (lex posterior over enactment dates) belongs to a future strategy vocabulary that derives edges.

Standpoints and modal operators

Standpoint declaration and federation

standpoint-decl ::= attribute* 'pub'? 'standpoint' Ident ('<:' TypeExpr (',' …)*)?
                     '{' mod-item* '}'

pub standpoint USFederalTax {
    pub type TaxableIncome <: Money;
    pub derive owes_tax(p: Person) :- p.income: TaxableIncome, p.income > 0;
}

pub standpoint California <: USFederalTax {
    pub derive state_owes_tax(p: Person) :- /* … */;
}

pub standpoint ContestedClaims { /* … */ }

A standpoint is a namespace-bearing module: items declared inside are accessible as StandpointName::ItemName (e.g., USFederalTax::owes_tax). The <: relation between standpoints declares lattice membership (federation ancestor for across [...] queries), not namespace inheritance — a child standpoint does not automatically see the parent’s items; explicit use is required to bring items into scope. Cross-standpoint federation via the across [...] annotation on queries; results may carry Truth4 values.

Nested standpoint declarations are not admitted — lattice edges come from <:, not from textual containment. Submodules (mod) and impl blocks inside a standpoint are permitted.

Federation conflict policy is chosen per query, not per standpoint: a federated across [...] query is paraconsistent by default — disagreement surfaces as Both (see truth values) — and may request strict projection. Conflict policy is a per-query projection, not a standpoint-level declaration.

Visibility composition. Facts are scoped by where they are asserted. A fact/not_fact declared inside a standpoint s { … } block is local to s; one declared at file/module scope, outside any standpoint block, sits in the DEFAULT (unscoped) layer. The two compose by the sheaf reading (Sheaf-theoretic semantics for standpoint federation):

• The DEFAULT layer restricts into every view. An unscoped assertion is visible to an unfederated query, to every standpoint-scoped query, and to every standpoint in an across [...] federation — it is the broadest perspective, and the sheaf restriction maps carry it into every stalk.
• A standpoint-scoped fact is invisible outside its standpoint. It does not appear in an unfederated (unscoped) query, nor in a query scoped to a different standpoint. Reading a scoped fact requires explicitly selecting its standpoint — via across [...], box/diamond (Modal operators), or a bridge rule (Bridge rules).

So an unfederated query (pub query q() -> P;) reads exactly the DEFAULT layer; a single-standpoint federation (across [s]) reads the DEFAULT layer unioned with s’s own facts; a multi-standpoint federation info-joins those per-standpoint views (Sheaf-theoretic semantics for standpoint federation). Derive rules, checks, and the mutation delta-guard all evaluate over the DEFAULT-layer (base) view — a scoped fact never silently becomes global truth. A federated query that names a standpoint with no declaration is refused (OE1103 UndeclaredStandpointInAcross) rather than contributing an empty extent that would mask the typo. Mechanized at spec/lean/Argon/Standpoint/Visibility.lean: view_of_base_eq_default_layer (base = DEFAULT layer), scoped_view_eq_default_union_own (scoped = DEFAULT ∪ own standpoint), default_visible_everywhere, scoped_invisible_to_base, and scoped_invisible_to_other.

Modal operators

box(P) and diamond(P) are rule atoms (Rule-atom grammar) admitted at tier:modal. They are interpreted over a Kripke frame; the frame is determined by the surrounding context.

Frames. Argon recognizes two intrinsic frames:

• Standpoint frame. Worlds are standpoints; the accessibility relation is the reflexive-transitive closure of <: over the standpoints in scope (extended by the explicit set of any enclosing across [...] clause). box(P) at standpoint s holds iff P holds at every s' reachable from s along the frame.
• Classification frame. Worlds are configurations in which an individual exists (store states reachable by mutations). A type introduced by a fixed metatype (metatype, RFD 0027 D6) carries forward rigidity: once an individual is a member, the mutate mutation gate preserves that membership forward along accessibility (Argon.Runtime.ModifierGates.runMutation_fixed_iof_constant). This is one-directional, not two-way constancy — a current non-member can still later be constructed into a fixed type, so fixed pins membership going forward but says nothing about future gains. A type introduced by an unmodified (dynamic) metatype carries no such guarantee. This is the standard Guizzardi/UFO modal characterization of rigidity, realized operationally by the ontology-neutral fixed bit rather than by reading any vocabulary’s rigidity axis.

diamond(P) is dual: it holds when P holds in at least one accessible world.

Static discharge. When P is a positive type-classification atom over a target introduced by a fixed metatype, forward rigidity preserves membership across accessible worlds and the elaborator can discharge the modal at compile time without consulting a reasoner (Argon.Reasoning.StaticDischarge.box_fixed_discharge). The discharge is polarity-asymmetric: forward rigidity grips box(x : T) but gives no grip on the negation box(¬(x : T)), since a current non-member may still be constructed into the type later (Argon.Reasoning.StaticDischarge.isRigidIn_does_not_discharge_box_neg).

Atoms that survive static discharge are routed to a modal reasoner over the std::kripke carrier; the choice of backend (tableau, resolution, bounded model-checking) is implementation-defined.

std::kripke. Exported from the stdlib for explicit modal modeling — e.g., writing forall w: World where accessible(current, w), P@w inside unsafe logic { }. The carrier is minimal:

// in std::kripke
pub struct World;
pub struct Entity;
pub fn iof(e: Entity, t: Top, w: World) -> Bool;            // instance-of-in-world
pub fn accessible(w1: World, w2: World) -> Bool;            // frame accessibility
pub fn current() -> World;                                   // the current world

The surface operators box(P) and diamond(P) are syntactic forms — not function calls — and desugar to FOL over World:

Where P@w denotes the rule atom P evaluated at world w (i.e., relativized to w’s extension). Modelers using only the surface operators need not import std::kripke directly; the desugaring threads through the elaborator. There are no Box / Diamond runtime functions — modal operators reduce to quantification over worlds.

Federation interaction. Inside a query annotated across [s₁, s₂, …], the standpoint frame is extended to the named set; box(P) reads “P holds in every listed standpoint” and may return Both, Can, or Not per truth values when the standpoints disagree. Classification-frame box/diamond atoms compose with federation by being evaluated independently at each listed standpoint, then info-joined via the FDE lattice.

Lowering. box(P) and diamond(P) lower to AtomIR::Modal and classify at tier:modal. Cross-nesting a modal with a temporal operator is refused by the tier classifier. examples/modal_box_diamond.ar exercises both operators end-to-end.

Bridge rules

Bridge rules thread information explicitly between standpoints. Where across [...] composes standpoints lattice-wise (FDE info-join over <:), a bridge rule is a directional, named, typed inference that moves a conclusion from one standpoint to another, optionally applying a domain mapping.

Status. pub bridge is refused at ox check / ox build with OE1102 (audit doc-04 / issue #151). Bridge rules parse, lower to wire events, resolve, and pass well-formedness checks — but the federation fixpoint never fires them, so a built artifact’s bridge bodies would silently never contribute to their target standpoint. Rather than ship that inert surface, a bridge declaration is refused loudly; model the cross-standpoint inference with an explicit derive / pub fact for now. Bridge evaluation is the post-stable flagship standpoint deliverable: the parse / lower / wire / decode surface is retained intact (Module::bridges_targeting, the BridgeDecl codec) so the work resumes without a grammar or wire-format change. The semantics below is the committed design.

bridge-decl ::= attribute* 'pub'? 'bridge' Ident
                  '(' standpoint-ref '->' standpoint-ref ')'
                  '{' bridge-rule (';' bridge-rule)* ';'? '}'
bridge-rule ::= rule-body '=>' bridge-head
bridge-head ::= predicate-call                           // direct assertion into target
             |  predicate-call 'mapping' mapping-clause  // with domain map
mapping-clause ::= '{' (Ident '=' expr (',' …)*)? '}'    // src-var ↦ dst-expr
standpoint-ref ::= path                                  // resolves to a standpoint

pub bridge USCitizens(US::Tax -> International::Legal) {
    Person(p), p.citizenship == "US"
        => LegalEntity(q) mapping { q.jurisdiction = "US", q.person_ref = p };
    Person(p), p.passport != null
        => Verified(p);
}

The -> between standpoint references in the bridge head encodes the direction; existing -> operator (function return arrow) is reused with no new lexer token.

Directionality (key property). A bridge from s₁ to s₂ does not imply a bridge from s₂ to s₁. The asymmetry is what makes bridges different from equality / equivalence axioms; without it, bridge composition would collapse standpoints and destroy their contextual scoping. This is the standard discipline across DFOL (Ghidini-Serafini), DDL / C-OWL (Borgida-Serafini-Bouquet), and MCS (Brewka-Eiter) — see the vault notes on bridge-rule semantics for the comparative landscape.

Body and head. The rule body uses the standard rule-atom grammar (Rule-atom grammar) evaluated at the source standpoint. The head is a predicate call evaluated at the target standpoint. If source and target have different domains (e.g., a tax-jurisdiction Person vs. an international-law LegalEntity), an explicit mapping { … } clause specifies how source variables map to target-domain values; without a mapping clause, the bridge is identity (source variable = target argument).

Negation-as-failure in bridge bodies. Bridge bodies admit NAF (not atom) over the source standpoint’s predicates — matching the MCS form. The bridge graph (nodes = standpoints; edges = bridges) must be stratified for the federation fixpoint to be unique; cycles in the bridge graph emit OE1101 BridgeCycle.

Composition with across [...]. A query annotated across [s₁, s₂] composes lattice federation (via <:) and any bridges between s₁ and s₂ in scope. Both contributions are info-joined via the FDE lattice; conflicts surface as Both per truth values.

Mechanization. The standpoint-frame sheaf semantics (Sheaf-theoretic semantics for standpoint federation) treats bridges as restriction maps on the perspectival sheaf — see that section. Diagnostic codes for malformed bridges live in the OE11xx range (Standpoints / perspectival config).

Bridges under temporal extent (Temporal substrate). When bridges cross modules with bitemporal extent, the substrate admits only temporal-uniform bridges at tier: recursive: a bridge rule consults facts only at the same valid-time at which it fires. Bridges that consult facts at different times (bridge m s t reading s _ t' with $t’ \ne t$) require tier: fol and an explicit temporal-bridge-monotonicity axiom in the module’s prelude. The sheaf-equivalence theorems of Sheaf-theoretic semantics for standpoint federation lift pointwise under temporal-uniform bridges with no new axioms; non-uniform bridges require a new axiom and are out of the conservativity envelope. Diagnostic: OE0720 NonUniformBridgeRefused. Mechanized at spec/lean/Argon/Locality/Temporal.lean (sheaf_equivalence_bitemporal_uniform).

Sheaf-theoretic semantics for standpoint federation

The standpoint lattice carries a sheaf-theoretic semantics — the formal grounding of why across [...] federation, bridge rules (Bridge rules), and box/diamond modal operators all compose coherently.

The sheaf. Treat the standpoint lattice as a base for a Grothendieck topology: open sets are downward-closed subsets of the <: lattice. The perspectival sheaf 𝓕 assigns to each open set U a stalk 𝓕(U) — the local knowledge (set of derivable facts, three-valued atoms, evidence accumulations) available to the standpoints in U. Restriction maps 𝓕(U) → 𝓕(V) for V ⊆ U encode how broader perspectives specialize to narrower ones; explicit bridge rules (Bridge rules) lift to additional restriction maps wherever the bridge graph reaches.

Substrate theorems. The correspondence is proved over a finite model at spec/lean/Argon/Locality/SheafEquivalence.lean — no axioms, no sorry: bottom_up_is_equilibrium, equilibrium_is_global_section, and equilibrium_is_minimal_section. Stated informally: the bottom-up evaluation of the federated standpoint system produces an MCS-style equilibrium, and that equilibrium is a minimal global section of the perspectival sheaf. The full categorical construction — a genuine Grothendieck topology with general restriction maps — is open research (it would unify two independent formalizations of perspectival reasoning; see the vault note “Topology of Understanding”). The finite-model theorems are the substrate commitment.

Consequence (H¹ interpretation). When across [s₁, s₂] yields Both(a, b) (the FDE conflict outcome), the first cohomology H¹(𝓕) carries a non-trivial generator. The two witnesses a, b are cohomologically distinct — they witness an irreducible perspectival disagreement that no global section can unify. This is the formal content behind the #[consistency(paraconsistent)] policy: the substrate makes the disagreement explicit rather than collapsing it.

Consequence (sheaf cohomology as diagnostics). Future tooling may surface H¹(𝓕) generators as a diagnostic class — “your federation disagreement is reducible (cohomologous to zero, fixable by a bridge rule) or irreducible (a non-trivial cohomology generator, requiring paraconsistent acceptance).” This is research-grade; the substrate axioms are the commitment.

Lift under bitemporal extent. When the standpoint federation runs over modules with bitemporal extent (Temporal substrate), the three sheaf-equivalence theorems lift pointwise without new axioms — provided bridges are temporal-uniform (Bridge rules). The bitemporal BeliefAssignment, BridgeEval, and LocalFixpoint become time-indexed functions; at each time slice, the canonical theorem applies. Mechanized at spec/lean/Argon/Locality/Temporal.lean (bottom_up_is_equilibrium_bitemporal, equilibrium_is_global_section_bitemporal, equilibrium_is_minimal_section_bitemporal, bundled as sheaf_equivalence_bitemporal_uniform). Non-uniform bridges (consulting facts at different VTs) require a new temporal-bridge-monotonicity axiom and are out of the conservativity envelope.

Decidability

Tier ladder

Default module tier: structural.

Temporal sub-tier (orthogonal axis). Every program has a tier pair (main, temporal). The temporal sub-tier ladder:

The classifier accepts a program if both axes are tractable and the program respects additive composition between modal (box/diamond) and metric temporal operators — no nesting of one family inside the other. Cross-mixed nesting box(box_minus[a,b](C)) is refused at tier: recursive (OE0712 ModalTemporalCrossNestRefused) and routed to tier: fol. The grounding is Demri-Wałęga 2024 (Standpoint LTL): satisfiability is EXPSPACE-complete unrestricted, with a PSPACE fragment under interplay restriction that Argon’s rigidity-of-standpoints commitment satisfies.

Annotation:

#[dec(tier: recursive, temporal: stratified)]
mod my_module { … }

If only one axis is annotated, the other is inferred from the module’s content.

Mechanized at spec/lean/Argon/Decidability/Temporal.lean (TemporalSubTier lattice + additiveComposition predicate + admitsAt_admits soundness lemma).

Annotations

#[dec(tier:<name>)]
#[budget(heartbeats: Nat)]
#[scope(max: Nat)]
#[brave]                  // stable models (reserved)
#[coinductive]            // greatest fixpoint
#[constructive]           // required at tier 5+ for non-ground NAF
#[shape(<recognized-shape>)]
#[lattice(K3 | FDE | Boolean)]
#[consistency(strict | paraconsistent)]    // on standpoint
#[world(open | closed)]                     // on concept (World assumptions (CWA / OWA); live — marks the concept's world, default CWA)
#[default]                                  // on derive — overridable clause (Defeasibility, RFD 0028)
#[defeats(target(args))]                    // on derive — declares an attack (Defeasibility, RFD 0028)
#[label(name)]                              // on derive — clause identity, head.label (Defeasibility)
#[intrinsic]                                // on iof-body field
#[unproven] / #[assumed]                    // on test
#[language_interface]                       // on Lean-spec-bound items

Theory-specific annotations (e.g., #[order(N)] from the mlt package, #[potency(N)] from a potency package) are library macros in unprivileged theory packages, not language-level attributes — see Higher-order modeling and Stdlib (selected).

Reserved attribute names. The compiler-known attribute names listed above are reserved. A user pub macro <name> { … } or #[procmacro] pub fn <name>(…) declaration whose name collides with the reserved set is rejected at the declaration site with OE0708 ReservedAttributeName. The full reserved set:

brave, budget, coinductive, consistency, constructive, dec, default,
defeasible, defeater, defeats, derive, intrinsic, inverse, label,
language_interface, lattice, managed, no_implicit_prelude, priority,
procmacro, scope, shape, unproven, assumed, world

(defeasible, defeater, priority are removed surfaces — they stay reserved so a typo refuses with a migration hint, RFD 0028 D9 — and default, defeats, label are the replacements.)

This list is fixed; adding to it requires an edition bump (the edition = N field in ox.toml). Theory-specific attribute names (categorizes, partitions, subordinate_to, power_type_of, order, complete, potency, @n, …) live in their own unprivileged theory package (mlt, potency, …) as #[procmacro] / pub macro declarations, not as language-reserved attributes — see Higher-order modeling and Stdlib (selected).