Foreword

There has long been a gap between the languages we use to think about a domain and the languages we use to run code over it. On one side, ontology engineers reach for OWL, OntoUML, or hand-rolled formalisms in the description-logic tradition: precise, mechanically reasonable, but awkward to compose, package, or evolve like real software. On the other side, programmers reach for Python, TypeScript, or Rust: ergonomic, well-tooled, but almost defenseless against a domain whose constraints really do live in the type system.

Argon is an attempt to close that gap from the programming-language side.

It is a programming language whose primary subjects are concepts, relations, and rules. It compiles. It has a package manager. It has an LSP, an editor extension, and a registry. It also has refinement types, a decidability tier ladder, bitemporal axes, standpoint-aware queries, and a mechanically-verified core. The same source can model a residential lease, a regulatory regime, and the events that move money between them — and the compiler can tell you, before you run anything, whether your rules are decidable, whether your refinement is satisfiable, and whether your invariants follow from your axioms.

This book is the path into that language. It moves atoms-to-molecules, the way The Rust Programming Language does for Rust, and it does so against a single running example — a residential-lease ontology that we build up piece by piece across the chapters. By the end of Part 3, the reader has a working, queryable, validated model of a non-trivial legal domain. Part 5 covers the formal foundations: the meta-property calculus, the seven-tier decidability ladder, defeasibility semantics, and the bitemporal + standpoint runtime. Where the chapters say “mechanically verified,” they state the result and the math behind it — termination, uniqueness, soundness, decidability — and let the reader inspect the engine the result is about.

Argon is not finished. The team is in the middle of a measured redesign: cleaning up vocabulary, unifying body shapes, collapsing a few item kinds into more general primitives. The book teaches today’s syntax and flags every place where the language is moving. Migration notes point forward, and Appendix D is the lever that will keep the book honest as the redesign rolls out.

The audience the book imagines first is the foundational-ontology research community: people who already know UFO, BFO, DOLCE, OntoUML, OWL — what an ontology is, what reasoning is, why decidability matters. The book skips that preamble and goes straight to what is distinctive: how Argon turns an ontology into a program you can ship.

If you arrive from the other side — Rust, TypeScript, Haskell, a working programmer who has never touched description logic — the book still works. The early chapters teach the formal vocabulary as it goes. You will not be asked to read a paper before the first compile.

— the Argon team, 2026

Introduction

Argon is a programming language for declarative ontology modeling with first-class reasoning. Its purpose is to let you describe a domain — its concepts, the relations between them, the rules that hold over them — in a single, typed, packageable language and then run things against that description: queries, mutations, simulations, regulatory checks, diagrams.

This chapter answers four questions: what Argon is, who it is for, what is distinctive about it, and how it relates to the tools you already know.

What Argon is

A working Argon program contains four kinds of items.

Concepts are the things in your domain. A Person, a Lease, a Property, a Mortgage. A concept declaration introduces a type and the fields that go with it. Concepts form hierarchies: a ResidentialLease is a Lease, a Tenant is a Person.

Relations connect concepts. They can be binary (HasResidence(person, residence)) or carry their own structure (a Lease mediates a Tenant, a Landlord, and a property — and has its own dates and rent).

Rules derive new facts from existing ones. derive ActiveLease(l) :- l.start_date <= today(), l.end_date > today() reads as “a Lease is ActiveLease when these conditions hold.” The reasoner picks an evaluator per rule type — structural saturation for the cheap fragment, Datalog for the recursive one, an event-driven engine for reactive rules — and the same evaluators run at compile time and at runtime. Every derivation carries provenance.

Operations do work over the model. compute items are pure functions. query items return bindings. mutation items change the world and emit typed events into a bitemporal log. Each kind picks the body shape that fits its job: = expr, :- body, or { stmts }.

A package collects these items, ships them through a registry, and lets other packages import them. The toolchain — oxup for installing, ox for building/testing/running, ox-lsp for editor integration — is shaped like Cargo’s, intentionally.

Why Argon

A few things that working ontology engineers have asked of their tools, and that Argon tries to answer.

Compose like software. Foundational ontologies (UFO, BFO, DOLCE) and domain ontologies live in different repositories, evolve at different rates, and need to compose. Argon packages do that. There is no monolithic schema; there are libraries, and a manifest, and a lockfile.

Reason at compile time when you can. Most rules are decidable. A few are not. Argon’s tier ladder makes the line explicit: rules at tiers 0–3 execute; rules at tiers 4–6 parse and elaborate but do not run, so the compiler tells you up front when you have written something the engine cannot evaluate. @[theorem] marks a derive as a theorem claim and preserves the marker through to the kernel for a future mechanical-verification pipeline (the pass itself is not yet active). Refinement types are a decidable fragment with a polynomial-time decision procedure.

Carry time with you. Every fact has a valid time (when it is true in the world) and a transaction time (when the system learned it). Mutations publish typed events into an append-only log. Queries can dial in a standpoint, a fork, or a historical timestamp. You do not bolt this on; it is built in.

Show your work. Every result carries why-provenance. Every diagram is generated from the same source the rest of the language reads. Tests live next to the model.

Who Argon is for

The book imagines two readers.

The first is a foundational-ontology researcher or a domain modeller who has been building in OntoUML, OWL, or hand-rolled DL formalisms. You know what a relator is, what a sortal is, why disjointness and completeness matter, why decidability is not a curiosity. What you have wanted is a language whose ergonomics, packaging, and tooling let you ship a model the way a Rust crate ships a library.

The second is a working programmer — Rust, TypeScript, Haskell, OCaml — who has been hand-rolling typed domains and finally wants to declare them once. You may not yet know the term relator; you have certainly written one many times by hand and watched the runtime checks pile up.

Either way, the book starts at the toolchain and walks you through to a compiled, tested, queryable, visualizable lease ontology. Read straight through and it should take a long afternoon.

What is distinctive

Several pieces of Argon, taken individually, exist elsewhere. The synthesis is what is unusual.

• Vocabulary-neutral by construction. Argon’s language core ships zero foundational metatypes. kind, subkind, role, phase, relator, category — these are not keywords. They come from a vocabulary package (UFO, BFO, your own). The reserved-keyword set is small; almost everything composes from packages.
• Three computational modes, one type system. compute for pure functions, derive/query for declarative reasoning, mutation for state-changing operations. Refinement types and the metatype calculus apply uniformly to all three.
• Decidability tier ladder. Seven named tiers from tier:structural (polynomial, the cheapest) through tier:fol (full first-order logic) up to tier:mlt (multi-level theory). The compiler classifies every rule. Tier-cap enforcement at the module level keeps a package’s effective fragment honest.
• Bitemporal + event-sourced + standpoint-aware. The runtime is built around an append-only axiom-event log with valid-time and transaction-time axes; standpoints discriminate views; forks branch the world.
• Mechanically verified core. Refinement-fragment decidability (PTIME), occurrence-typing soundness, and meta-property-fixpoint termination + uniqueness are stated and proven in Part 5.

How Argon compares

A short, comparative sketch — useful if you have spent time with any of these.

A finer-grained feature matrix:

You do not have to pick a side. An Argon project can import an OntoUML-flavored UFO package, emit OntoUML JSON for visual tools, target OWL where downstream consumers need it, and still keep a typed compile-and-test loop the rest of the time.

What this book covers

The book covers Parts 1 through 5: getting started, foundations (concepts, relations, rules, computations and mutations, the type system), composition (patterns, state machines, tests, diagrams), packages and tooling, and the advanced material — the metatype calculus, defeasibility, the tier ladder in detail, standpoints and bitemporal. Where the language is still moving, the chapters flag it inline; the full migration trajectory lives in Appendix D.

The shortest path to a working ontology is to read Chapter 1 end-to-end, then Chapter 2, then Chapter 3.4. That gets you to “concepts, relations, rules, and a diagram of what you have built.”

What’s in argon/examples/

The repository ships with a library of runnable example packages alongside this book. Each is a complete Argon workspace — ox.toml, src/prelude.ar, sometimes a README.md — that you can cd into and exercise with ox check. The book draws on them throughout; this is the canonical index.

Tutorial:

• lease-story/ — the residential-lease ontology built up through Chapters 2–3. The book’s running example.

Foundational ontology ports (each is a minimal smoke test, useful when you want to see a vocabulary stand on its own):

• bfo-smoke/ — Basic Formal Ontology. Declares temporal_status and dependence axes, four BFO metatypes, six BFO concepts, two BFO structural rules.
• dolce-lite/ — DOLCE-Lite. A second independent foundational vocabulary, used in the book to demonstrate disjoint-non-interference composition with BFO.

Domain ontologies (each is a port of a published ontology, faithful to the source):

• pizza/ — the Manchester pizza ontology. The canonical OWL classroom example, ported to Argon. Exercises five relation characteristics (@[transitive], @[symmetric], @[asymmetric], @[functional], @[inverse-functional]) across a class lattice with multiple inheritance.
• time/ — OWL-Time. All 13 Allen relations as first-class pub rel declarations, ~25 datatype properties, DayOfWeek and MonthOfYear enums.
• foaf/ — Friend Of A Friend. The social-graph ontology.
• skos/ — Simple Knowledge Organisation System.
• wine/ — the wine ontology (Hendler / McGuinness OWL teaching example).

Composition demos:

• ontology-tour/ — a registry consumer that pulls pizza, foaf, and wine into a single project and declares a tour_role metaxis for type. Useful as a worked example of cross-package composition.

Beyond these, argon/examples/_catalog/ holds ~530 minimal mini-workspaces — one per (feature, variant) pair — that exercise each atomic feature of the language in isolation. The catalog is the reference companion to the book; see argon/examples/_catalog/README.md for the index.

Open a terminal. The next chapter installs the toolchain.

Getting Started

This part takes you from no toolchain to a running Argon program in one sitting. Three short chapters:

• 1.1 Installation — install oxup, get a toolchain, point your editor at it.
• 1.2 Hello, Argon — the smallest meaningful program, type-checked and run.
• 1.3 Hello, ox.toml — the same code, but as a proper package the rest of the book builds on.

By the end of this part you have a working installation, you have run an Argon program, and you have the skeleton of the lease tutorial that threads through the rest of the book.

Installation

You install Argon by installing one binary: oxup. From there, oxup fetches the rest of the toolchain and keeps it up to date, the way rustup does for Rust.

What gets installed

A complete Argon toolchain bundles six things:

• oxc — the compiler.
• ox — the project manager: ox check, ox build, ox test, ox query, ox mutate, ox diagram, and the package commands.
• ox-lsp — the language server, used by the editor extension.
• std — the standard library bundle.
• tree-sitter-argon — the grammar, compiled to a dynamic library.
• shell-completion scripts.

A single oxup binary does the work of oxup, ox, oxc, and ox-lsp by inspecting argv[0]. The proxy binaries in ~/.argon/bin/ are symlinks back to the same oxup binary, so installing a new toolchain version is a single atomic flip of the active symlinks.

Install via Homebrew

$ brew tap sharpe-dev/tap
$ brew install argon
$ oxup init
$ oxup install stable

Four commands, in order:

• brew tap sharpe-dev/tap — register the Argon Homebrew tap.
• brew install argon — install the toolchain.
• oxup init — first-run setup. Provisions ~/.argon/{bin,toolchains,extensions} and adds ~/.argon/bin to your shell rc inside a guard block.
• oxup install stable — download the latest signed toolchain and make it the default.

The shell-rc edit is bounded — it lives between two clearly-marked comment lines that oxup controls. Running oxup uninstall later cleanly removes the edit along with everything else oxup manages.

Note: the tap is private to sharpe-dev while Argon is in pre-public-release. brew tap will prompt for GitHub authentication; oxup auth login configures the token oxup itself uses to fetch toolchain release assets.

Verifying the install

Open a fresh shell and check the four commands report a version:

$ oxup --version
$ ox --version
$ oxc --version
$ ox-lsp --version

If any of them fail, run oxup doctor. It checks that ~/.argon/ exists and is writable, that the proxy symlinks resolve, that the active toolchain manifest is intact, and that the shell-integration block is present in your rc-file.

$ oxup doctor

oxup doctor --json prints the same diagnostic in machine-readable form; oxup doctor --fix applies auto-fixable repairs.

Editor extension (VS Code / Cursor)

The editor experience is the canonical UX for Argon. Install the extension via oxup, which reads the bundled VSIX from the active toolchain and hands it to your editor’s CLI:

$ oxup extension install

Pass --editor vscode or --editor cursor to override auto-detection. oxup extension status reports the installed extension version. oxup extension uninstall removes it (with --editor all to uninstall from every detected editor at once). For dev-cut toolchains that ship no release asset, oxup extension install --path ./argon-dev.vsix installs a locally-built VSIX while still recording the install in oxup’s state.

The extension brings: LSP-driven hover, semantic highlighting, inlay hints, palette commands for ox query / ox mutate / ox diagram / ox test, an output channel for compiler messages, and the InfoView panel. Use it. The book’s later chapters reference InfoView output directly.

Updating

$ oxup update

Updates the default toolchain to the latest channel build. Pass a specific version to update just that one: oxup update 0.4.0.

To roll back to a previously-installed toolchain: oxup default <version>. To list installed toolchains: oxup toolchain list. To remove a specific version: oxup toolchain remove <version>. To garbage-collect older toolchains while keeping the active one: oxup toolchain gc [--keep N] [--keep-active] [--dry-run]. To check authentication status: oxup auth status. To update or uninstall oxup itself: oxup self update / oxup self uninstall. To uninstall everything oxup manages (including the shell-rc edit): oxup uninstall.

Channels

oxup resolves toolchains through four channel forms (oxup/src/channel.rs::Channel):

• stable — the newest non-prerelease tag.
• nightly — the newest nightly-YYYY-MM-DD tag.
• nightly-YYYY-MM-DD — a specific dated nightly.
• An exact version string — 0.4.0, 0.4.0-rc.1, etc.

Pin a channel:

$ oxup install nightly
$ oxup default nightly

Or pin to an exact version:

$ oxup install 0.4.0
$ oxup default 0.4.0

What’s next

Open a terminal in a fresh directory. The next chapter writes the smallest meaningful Argon program and runs it through the compiler.

Hello, Argon

Argon programs start the same way Rust programs do: with the smallest piece of code that compiles. We will write that piece first and then walk through what every line means.

The smallest program

Argon does not have a single-file mode. The smallest meaningful unit is a project — a directory with an ox.toml manifest and a src/ tree of .ar modules. Set one up:

$ mkdir -p hello-argon/src
$ cd hello-argon

Write a manifest at ox.toml:

[project]
name = "hello-argon"
version = "0.1.0"
edition = "2025"
entry = "root.ar"

[schema]
root = "src"

[package]
name = "hello-argon"
version = "0.1.0"
edition = "2025"

[dependencies]

Chapter 1.3 explains the manifest’s two-section structure ([project] for the perspectival-composition layer; [package] for the registry layer); for now treat it as boilerplate.

The program we are about to write declares its metatype machinery inline so you can see Argon’s substrate forms (pub metaxis, pub metatype) at work. In a production project you would normally write use ufo::prelude::* and pull in a vocabulary package’s catalog (kind, subkind, role, …) instead — kind is not a built-in keyword, but a metatype declared by the UFO package on top of the same substrate. Either way, the substrate is what the language actually ships; Chapter 2.1 covers it in full.

Then write src/root.ar:

use std::math::String

pub metaxis rigidity for type {
    rigid,
    anti_rigid
}

pub metaxis sortality for type {
    sortal,
    non_sortal
}

pub metatype kind = { rigid, sortal }

pub kind Person {
    name: String,
}

pub derive HasName(p: Person) :-
    p: Person,
    p.name != ""

pub query AllNamedPersons() -> [Person] :-
    ?p: Person,
    HasName(?p)
    => ?p

The use std::math::String line at the top is required: Argon ships no implicit prelude, so any primitive a module references — String, Nat, Int, Real, Bool, Date, DateTime, Duration, Decimal, Money — needs an explicit import path. Bare primitive names without a use produce OE0101 UnresolvedIdentifier with a hint at the right import.

Run the type-checker:

$ ox check
ox hello-argon v0.1.0 (./ox.toml)
ox 1 modules resolved from entry point
ox 1 standpoints: default
check passed

Clean. We have an Argon program.

Walking through the program

Eight things happen in twenty-odd lines. Take them in order.

pub metaxis rigidity { rigid, anti_rigid }

Argon ships no foundational metatypes in its language core. The keywords kind, subkind, role, phase, relator — none of them exist as built-in concept-keywords. They are defined by user packages.

A metaxis declares a dimension along which metatypes vary. rigidity is one such dimension; its values are the IDENT atoms rigid and anti_rigid. The mechanism is open-ended — domain modellers in finance, biology, or law can declare their own axes (sortality, criticality, regulability, …) without changing the language.

rigidity and sortality together are enough to define the metatypes Hello, Argon needs. The axes capture (loosely) Guizzardi’s UFO classification: rigidity distinguishes “instances belong to the type permanently” from “instances belong contingently”; sortality distinguishes “the type provides identity criteria” from “the type classifies but does not individuate.” Chapter 5.1 covers the calculus formally.

pub metatype kind = { rigid, sortal }

A metatype declaration introduces a concept-keyword and pins its position along the axes. kind is now a name the rest of this file can use to declare concepts: a kind is rigid (instances belong to it for as long as they exist) and sortal (it supplies its own identity criteria).

This is the line that makes kind exist. If you delete it, the next line stops parsing.

Note: in production code you would normally use ufo::prelude::* (or similar) and pull in a curated metatype catalog instead of declaring axes and metatypes inline. This chapter shows the mechanism in full so you can see what use would otherwise hide.

pub kind Person { name: String, }

A concept declaration. Person is the name; kind is the metatype (the IDENT before the name); the body lists fields with their types. The trailing comma is allowed — keep it on, since the next chapter’s version of Person will grow more fields.

String is one of Argon’s primitive types. The full set is Nat, Int, Real, Decimal, String, Bool, Date, DateTime, Duration, and Money. Each lives in std::math and reaches a module via explicit use.

pub derive HasName(p: Person) :- p: Person, p.name != ""

A rule. HasName is the head; (p: Person) is its argument list with a single typed binding; :- separates the head from the body; p: Person, p.name != "" is the body.

A few mechanics worth pinning down:

• Head parameters bind bare names. p in the head is the binding; the body’s atoms reference it without a prefix. The ? prefix is reserved for body-fresh variables — those introduced by an aggregate’s iteration clause or a query’s body when no head parameter is in scope. Head parameters never carry ?.
• Comma is the conjunction separator for rule bodies. There is no && and no and keyword inside a body — just commas.
• Type tests bind. p: Person is the body’s first atom; it both tests p’s type and re-asserts p’s binding for the rest of the body. Subsequent atoms see p narrowed to Person.

Reading the rule in English: “for any Person p, HasName(p) holds when p.name is non-empty.”

pub query AllNamedPersons() -> [Person] :- ... => ?p

A query is a first-class item: declared, type-checked, callable from the runtime by name. AllNamedPersons takes no arguments and returns a list of Person. The body looks like a rule body. The optional => head_expr after the body says what the result row is.

Because the query head takes no parameters, the body introduces a fresh variable ?p. That is the one place the ? prefix appears: query bodies (and aggregate sub-comprehensions) introduce body-fresh variables explicitly.

Read in English: “return every Person ?p for whom HasName(?p) holds.”

The [Person] syntax is a collection type: a list of Person. We will see cardinality-constrained variants like [Tenant; >= 1] (at least one tenant) in Chapter 2.3.

Running the query

Type-check is ox check. To actually evaluate the query, we need a fact in the world. The runtime command is ox query:

$ ox query AllNamedPersons
   No facts asserted; result set is empty.

That is correct. We have declared a kind, a derive rule, and a query — but we have not yet asserted any Person facts. Once we have a package and a test scaffold (Chapter 3.3), asserting facts and seeing query results will be straightforward.

What you noticed

Three things, probably.

No semicolons, but commas matter. Field lists are comma-separated; rule bodies are comma-separated; argument lists are comma-separated. Trailing commas are allowed. Statements inside imperative blocks (we have none yet — they appear in mutation bodies) do not need separators.

Whitespace is friendly, not significant. You can split a long rule body across lines or keep it on one. The compiler does not care.

Every item is opt-in to export. The default visibility is module-internal — file-scoped. Adding pub makes an item reachable from another module. There is no third tier (no per-package or per-workspace visibility); just the two.

Edge cases worth knowing

• Rule bodies want a typed binding for every variable. p.name != "" reads p’s name field, but the body needs at least one atom that pins p’s type — typically a leading type test like p: Person. The compiler rejects rules whose bodies reference identifiers no atom binds.
• derive with no asserted instances will not fire. pub derive Always(p: Person) :- p: Person only derives Always(p) for asserted Person instances; declaring a kind does not by itself create instances.
• Type errors land at ox check, not at runtime. Misspelling name as nme in the body of HasName raises an error at the field-access; the query never reaches the runtime.

Putting it in the running example

The next chapter promotes this code into the lease tutorial — the running example the rest of the book extends. The metatypes we declared inline here will move into a small metatypes.ar module you write once and never re-think.

Hello, ox.toml

A single .ar file is fine for hello-world. Anything beyond that wants to be a package: a directory tree with a manifest, a stable public surface, and a lockfile so the same code resolves to the same dependencies tomorrow.

This chapter promotes the Hello-Argon program into a proper package — lease-tutorial — which the rest of the book extends.

We continue to declare metatypes inline (this time in a dedicated metatypes.ar module, shown below). A real project would replace that module with use ufo::prelude::* and pull in UFO’s catalog of kind, subkind, role, phase, relator, etc. Whichever path you take, kind is a metatype declared via Argon’s substrate, not a language built-in; Chapter 2.1 covers the substrate end-to-end.

Setting up a package by hand

The toolchain doesn’t yet ship a cargo new-style scaffolder; you create the two files yourself. From a fresh directory:

$ mkdir -p lease-tutorial/src
$ cd lease-tutorial

The package needs a manifest at the root (ox.toml) and a schema-root directory (src/) holding the .ar source files. The next two sections build them.

The manifest

A working ox.toml for the tutorial:

[project]
name = "lease-tutorial"
version = "0.1.0"
edition = "2025"
entry = "root.ar"
default-world = "open"

[schema]
root = "src"

[package]
name = "lease-tutorial"
version = "0.1.0"
edition = "2025"
description = "Running example for The Argon Programming Language"
license = "CC-BY-4.0"
max_tier = 3

[dependencies]

Four sections. They will accumulate as the package grows. Two of them — [project] and [package] — repeat the package’s identity; that is intentional, and the next subsections explain why.

[project] — the perspectival-composition layer

[project] is what ox check, ox build, ox query, and ox mutate read when they need to know how to compose your modules into a world the reasoner can execute over. Required fields:

• name and version — the same name and version the package reports.
• edition = "2025" — the language edition this source is written in. Editions are parse-time only; no runtime split. "2025" is current.
• entry = "root.ar" — the entry-point module under src/. Idiomatic packages name it root.ar; the file lists use … ::* for every submodule the project should see.
• default-world = "open" | "closed" — the world assumption applied to every module that does not override it. Open-world is the default for ontology work.

Optional siblings include [modules], [standpoints], [defeat], and [tree-shaking] — covered in Chapter 5.4 and Chapter 4.1 respectively.

[schema] — where the source lives

[schema]
root = "src"

Every path under [project] (notably entry) is resolved relative to [schema] root. The default is "." (the manifest’s directory); the convention is "src".

[package] — the registry / dependency layer

[package] is what ox install, ox publish, ox audit, ox tree, and ox why read. It is the Cargo-shaped registry surface:

• name, version — must match [project] for hybrid manifests.
• edition = "2025" — the registry’s view of the edition. Inherited from [workspace.package] via edition.workspace = true when the package belongs to a workspace.
• description, license, authors, repository, homepage, documentation, readme, keywords, categories — registry-facing metadata.
• max_tier = N — caps the decidability tier the compiler will let your rules sit at. Tier 3 (full Datalog with stratified negation) is the typical cap; lower it to be conservative, raise it if you have invariants in higher tiers that you intend to verify with @[theorem] rather than execute. Chapter 5.3 covers the full ladder.
• default_world — the default world assumption for items declared in this package’s modules (overridden by [modules].default-world per-module).

Package names match ^[a-z][a-z0-9_-]*$; hyphens and underscores are both legal at the manifest level and canonicalize to underscores in use paths (so lease-tutorial becomes lease_tutorial).

[dependencies]

Empty for now. We will fill this in Chapter 4.1 when we start pulling in foundational vocabulary. A few shapes of dependency entry:

[dependencies]
ufo = "0.2.1"                              # registry, semver
cofris.workspace = true                    # inherit from workspace
my-local = { path = "../my-local" }        # local path

The source tree

Lay down two files under src/. First, the project entry — a root.ar that pulls every submodule into the module graph:

$ tree src
src
├── prelude.ar
└── root.ar

// lease_tutorial::root
//
// Project entry — pulls every submodule into the module graph so
// `ox check`, `ox test`, `ox build`, and `ox diagram` see the full
// project. Add `use foo::*` here when you create `src/foo.ar`.

And a curated prelude.ar — the library surface consumers will reach for:

// lease_tutorial::prelude
//
// Re-export the package's public surface here. Use `pub use foo::*`
// to thread items through. Internal modules left out of the prelude
// stay private — refactor without breaking downstream.

Both are empty for now. We will fill them in shortly.

Every .ar file under src/ is a module. The path under src/ becomes the qualified module path: src/party.ar is lease_tutorial::party, src/prelude.ar is lease_tutorial::prelude, and so on.

Adding a module

Promote our hello-world into a real module. Create src/metatypes.ar:

pub metaxis rigidity for type {
    rigid,
    anti_rigid
}

pub metaxis sortality for type {
    sortal,
    non_sortal
}

pub metatype kind = { rigid, sortal }

Then src/party.ar:

use metatypes::*

pub kind Person {
    id: String,
    name: String,
}

Wire both into the project. Edit src/root.ar to pull them in:

use metatypes::*
use party::*

And expose them through the prelude as the package’s public surface. Edit src/prelude.ar:

pub use metatypes::*
pub use party::*

pub use re-exports — items pass through prelude to consumers as if prelude had defined them itself. This is the canonical pattern: root.ar makes everything reachable for compilation; prelude.ar curates what consumers see.

The directory now looks like this:

src
├── metatypes.ar
├── party.ar
├── prelude.ar
└── root.ar

Type-check it:

$ ox check
ox lease-tutorial v0.1.0 (./ox.toml)
ox 3 modules resolved from entry point
ox 1 standpoints: default
check passed

The package compiles. We have a working skeleton.

What ox.toml is doing for you

Three things, mainly.

Resolution. ox install reads [dependencies], walks the dependency graph against the registry, picks compatible versions, and writes ox.lock. The lockfile is bivalent: it records both a content hash (byte-identical fetches) and a Merkle root over construct signatures (semantic identity — what the package actually contains). Chapter 4.2 covers the lockfile in detail.

Visibility. Two-tier: pub exports across module boundaries; the default is module-internal — file-scoped. There is no per-package or per-workspace third tier. The pub use re-export pattern in prelude.ar is how you make a package’s surface intentional rather than accidental.

Direct-dependencies rule. A package can use only items reachable through its own [dependencies], not items reachable transitively through some dependency’s dependencies. If you want to use a transitive package, add it explicitly to your manifest.

Workspace flavor

A workspace is a root ox.toml whose [workspace] section names member packages:

[workspace]
members = ["packages/lease-tutorial", "packages/lease-tests"]
resolver = "1"

[workspace.package]
edition = "2025"
license = "CC-BY-4.0"

[workspace.dependencies]
ufo = "0.2.1"

Workspace members inherit version pins via ufo.workspace = true and shared metadata via edition.workspace = true. The lockfile lives at the workspace root and is shared across members. We will use a workspace once the model has grown enough to want a separate test package.

Running things

Three commands you will use constantly inside a package:

$ ox check                    # Type-check + meta-property + package constraints
$ ox build                    # Compile to kernel types + Datalog
$ ox test                     # Run test blocks (Chapter 3.3)

Two more once there are queries and mutations to run:

$ ox query <name> [--explain]
$ ox mutate <name> --principal <id> [--dry-run] [--explain]

ox check is the fastest of these — it skips reasoning by default. Pass --reason to invoke the saturation engine; you will need it when an invariant depends on the reasoner having classified the TBox.

Edge cases worth knowing

• root.ar versus prelude.ar. root.ar is the project entry declared in [project] entry; the toolchain starts module discovery from it. prelude.ar is the library surface — what consumers see when they use lease_tutorial::prelude::*. The convention is for root.ar to use foo::* every internal submodule, and for prelude.ar to pub use foo::* only the curated public surface.
• Module names canonicalize. lease-tutorial becomes lease_tutorial for use paths. If you start with hyphens in your package name, expect underscores everywhere else.
• Editions are strings. Edition "2025" is current. Editions are parse-time only; no runtime split.

Putting it in the running example

What you have now is the skeleton the rest of the book extends:

lease-tutorial/
├── ox.toml
└── src/
    ├── metatypes.ar       # the small set of metatypes we need
    ├── party.ar           # Person (and soon Tenant, Landlord)
    ├── prelude.ar         # curated re-exports — public surface
    └── root.ar            # project entry — pulls submodules in

Chapter 2.2 extends party.ar and adds lease.ar. By the end of Part 2 the package has rules, queries, computes, mutations, and refinement types. By the end of Part 3 it has a state machine, tests, and diagrams. The complete running version lives in examples/lease-tutorial/ alongside this book.

Summary

A working Argon package is ox.toml plus a src/ tree of .ar files. The manifest names the package, pins dependencies, and configures reasoning. Modules are files; the prelude curates the public surface; pub use re-exports propagate. ox check keeps you honest. The next part teaches what to put into those modules.

Foundations

This part is the atoms. By the end of it you have written enough Argon to model a domain end-to-end: the substrate that lets a vocabulary package declare metatypes in the first place, then concepts, relations, rules, computations, and a type system over them.

We start with the substrate because every other chapter in this part uses metatypes — kind, role, phase, relator — that come from a vocabulary package (UFO, in our case) built on the substrate. Knowing what those declarations actually are makes the rest of Part 2 about modeling rather than memorizing keywords.

Chapter by chapter:

• 2.1 The Argon Substrate — pub metaxis, pub metatype, pub metarel, pub decorator. The four declaration forms a vocabulary package uses.
• 2.2 Concepts and Hierarchies — Person, Tenant, Landlord, Lease, ResidentialLease, CommercialLease. The hierarchy.
• 2.3 Properties and Relations — fields, multi-valued fields, binary relations, the relator pattern, refinement-typed fields.
• 2.4 Rules and Reasoning — derive, assert, the three-engine pipeline, the tier ladder.
• 2.5 Computations and Mutations — compute for pure functions, mutation for state changes, events into the bitemporal log.
• 2.6 The Type System — primitives, generics, refinement types, subtype reasoning.

By the end of Part 2 the reader has a working, queryable, validated lease model with derived state, mutations for signing and expiry, and refinement types that catch bad data at compile time — and an understanding of which keywords are language primitives and which are package declarations.

The Argon Substrate

Argon’s compiler ships with zero foundational ontology content. It does not know what a kind is, what rigidity means, or what a relator does. The keywords kind, subkind, role, phase, relator, category, mixin — all the vocabulary the introduction promised was not built in — are exactly that. Identifiers, declared by user packages, brought into scope by use.

What the compiler does ship is the substrate that lets a vocabulary package declare them. This chapter is that substrate: the four declaration forms — pub metaxis, pub metatype, pub metarel, pub decorator — that turn a Markdown-flat universe of names into a typed metaontology where the compiler can check Person : Kind, route a transitive decorator to a recognized fast-path, or refuse pub kind X : Role because rigid cannot specialize anti-rigid.

The rest of Part 2 uses UFO’s metatypes (kind, role, …) as if they were primitives, because UFO is the most established vocabulary and the chapters need something to model with. This chapter is what makes that legitimate. UFO is one user package built on the substrate. BFO is another. So is whatever your team needs that doesn’t yet exist.

Why a substrate

Foundational ontologies do not agree.

UFO carves the world along rigidity (does the type apply necessarily, or contingently?) and sortality (does it carry an identity criterion?). BFO carves along temporal status (continuant vs. occurrent) and dependence (does the entity require a specific bearer?). DOLCE has its own axes, GFO its own. They overlap in places, contradict in others. None is wrong; each is a different commitment about what categories are foundational.

A language that bakes one of these in cannot host the others. Make rigidity a built-in keyword and BFO no longer fits — BFO does not commit to rigidity at the upper level. Make temporal_status built-in and you have privileged BFO over UFO.

Argon’s solution is to ship the machinery — axes, metatypes, metarels, decorators — and let the foundational ontology supply the content. UFO declares rigidity; BFO declares temporal_status; both packages run on the same compiler. A project picks one (or several, if their axes do not collide) by writing use.

The four declaration forms

pub metaxis, pub metatype, pub metarel, pub decorator. They are language primitives — the compiler parses each as a top-level declaration form, like fn in Rust or data in Haskell. Everything else in an ontology package — the kinds, the roles, the transitive decorator — is built from these four.

pub metaxis — declare an axis

A metaxis (short for meta-axis) is a dimension along which metatypes vary. Rigidity is one. Sortality is another. Temporal-status is another. A metaxis declaration names the axis, scopes it to the kind of declaration it qualifies (type, rel, or dec), and supplies its value space.

The simplest form is a finite enumeration:

pub metaxis rigidity for type {
    rigid,
    anti_rigid,
    semi_rigid
}

rigidity qualifies type declarations. Its value set is {rigid, anti_rigid, semi_rigid}. The values are atoms — bare identifiers carving the axis into points.

A metaxis can also be a typed domain. Instead of an enumeration, it admits values from a primitive type, optionally narrowed by a refinement predicate:

use std::math::Nat;

pub metaxis cardinality_floor : Nat for rel where { _ > 0 }

The values are natural numbers; the refinement requires positivity. A metarel that binds cardinality_floor = 0 triggers a refinement violation at elaboration time. Typed-domain axes admit Nat, Int, Real, Bool, and String, with promotion Nat → Int → Real.

A package may declare any number of axes. The constraint is one of acyclicity: the meta-property calculus that runs at elaboration time builds a dependency DAG over axes (axis B reads axis A), and a cycle is rejected at vocabulary-load time. Within that constraint, axes are free.

pub metatype — declare a metatype

A metatype is a bundle of axis values. Where a metaxis says “here is an axis,” a metatype says “here is a point in axis space.” kind lives at { rigid, sortal, provides_identity }. role lives at { anti_rigid, sortal, relational }. The declaration form is a record literal over in-scope axes:

pub metatype kind = {
    rigidity = rigid,
    sortality = sortal,
    identity_provision = provides
}

(In practice, packages often elide the axis names when the values themselves are unambiguous: pub metatype kind = { rigid, sortal, provides }. Either form is accepted; the compiler resolves each value against in-scope axes.)

A metatype’s name is the surface keyword. After

pub metatype kind = { rigid, sortal, provides }

writing

pub kind Person { ... }

is a concept declaration whose metatype is kind. The grammar position where a metatype name appears — between pub and the concept’s identifier — accepts any in-scope pub metatype. There is nothing privileged about kind in the parser.

If the resolver cannot find a pub metatype matching that name, the compiler emits OE0605 UnknownMetatype with a four-variant hint: the name might be unimported, ambiguous across packages, declared as something other than a metatype, or genuinely undeclared.

pub metarel — declare a relation metatype

Concept declarations describe individuals. Relations describe how individuals connect: mediates, componentOf, inheresIn. Just as concepts have metatypes that classify them (a Person is a kind), relations have metarels that classify them (a mediates is a material_relator_relation). A metarel declaration ties a relation kind to its endpoint constraints, default cardinalities, and any decorators it implies:

pub metarel mediates = {
    source: relator,
    target: kind,
    cardinality_default: { source: [0..1], target: [1..*] },
    properties: { irreflexive, asymmetric }
}

mediates is a relation whose source must be a relator and whose target must be a kind; by default a relator mediates one or more kinds. The properties set lists structural-property names that apply to every relation tagged with this metarel. The body is record-shaped (= { ... }) — the same shape pub metatype and pub decorator use.

When user code writes pub rel teaches(t: Course, s: Student) :: mediates, the compiler validates the endpoints (Course must be a relator-typed concept, Student a kind-typed concept) and applies the cardinality defaults if the rel does not specify its own. Endpoint mismatches emit OE0226 MetarelEndpointMismatch; an unknown metarel name is OE0225 UnknownMetarel.

pub decorator — declare a decorator

Decorators are reusable annotations that lower to compiler behavior. @[transitive] on a relation tells the reasoner to compute the relation’s transitive closure. @[theorem] on a derive rule marks the rule as a theorem claim — at the current cut, the marker is preserved through emission and surfaces in the kernel’s runtime so a future verification pipeline can target it; the compile-time pass does not yet attempt mechanical verification. The decorators themselves are user-declared:

pub decorator transitive() on rel = {
    semantics: r(x),
    lowers_to: transitive_closure
}

A decorator declaration carries:

• a parameter list (transitive is zero-arg; inverse(of: rel) takes one);
• a target (on rel, on type, on dec, on field, on individual, or on frame);
• a semantics body — a Datalog atom that anchors the decorator’s compile-time intent. The body’s logical content rides on the lowers_to: recognized shape, not on the surface atom itself; conventionally semantics: is a stub atom and the recognizer table picks up the shape;
• an optional lowers_to: <shape> hint that pre-tags the decorator with a recognized canonical shape (more on this below).

When user code writes @[transitive] on a relation, the compiler binds transitive against in-scope decorator declarations, validates arity / target / argument types, and lowers the application. A mismatch emits one of OE0229 UnknownDecorator, OE0230 ArityMismatch, OE0231 TargetMismatch, OE0234 ArgumentTypeMismatch.

The lowers_to hint is the substrate’s bridge to the recognizer table — a set of canonical FOL shapes (transitive, symmetric, functional, disjoint-classes, qualified-cardinality, …) that the compiler can route to a fast-path implementation in the reasoner. A user decorator whose body matches a recognized shape gets the fast-path treatment for free; one that does not falls through to generic Datalog. Chapter 5’s Metatype Calculus covers the recognizer in detail.

How user packages compose this

UFO declares its core axes and metatypes using these four forms — nothing else. Here is the start of UFO’s prelude.ar, which ships with the package:

pub metaxis rigidity for type {
    rigid,
    anti_rigid,
    semi_rigid,
    order: anti_rigid < semi_rigid < rigid
}

pub metaxis sortality for type {
    sortal,
    non_sortal
}

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

pub metatype kind     = { rigid, sortal, provides }
pub metatype subkind  = { rigid, sortal, inherits }
pub metatype role     = { anti_rigid, sortal, relational }
pub metatype phase    = { anti_rigid, sortal, intrinsic }
pub metatype relator  = { rigid, sortal, provides }
pub metatype category = { rigid, non_sortal }

That is the entire mechanism. UFO publishes this file (and a much larger one for relations, decorators, and structural-check rules); user code writes use ufo::prelude::*; from that point kind, role, phase are in scope as identifiers the parser can dispatch.

BFO is a peer package that publishes a different prelude:

pub metaxis temporal_status for type {
    temporal,
    atemporal
}

pub metaxis dependence for type {
    independent,
    specifically_dependent,
    generically_dependent
}

pub metatype continuant                       = { temporal }
pub metatype occurrent                        = { atemporal }
pub metatype independent_continuant           = { temporal, independent }
pub metatype specifically_dependent_continuant = { temporal, specifically_dependent }

BFO declares temporal_status and dependence; UFO declares rigidity, sortality, identity_provision. Zero shared source. A project that imports use bfo::prelude::* writes pub independent_continuant Object {} instead of pub kind Person {} — the same compiler, the same substrate, a different vocabulary on top.

A project can also import both, provided the axes do not collide. The meta-property calculus treats two non-overlapping vocabulary packages as independent — one’s rules do not see the other’s facts. A shared axis (both packages declare rigidity) requires a confluence check, which the calculus runs at vocabulary-load time.

Two runnable example packages exercise the substrate from opposite ends. argon/examples/bfo-smoke/ is the minimal BFO smoke test — declares two BFO axes (temporal_status, dependence), four BFO metatypes (continuant, occurrent, independent_continuant, specifically_dependent_continuant), six BFO concepts, and two BFO disjointness rules. Zero shared source with the UFO package; both compile against the same oxc. argon/examples/dolce-lite/ does the same for DOLCE-Lite.

For the four substrate declaration forms tested in isolation, the catalog ships:

// _catalog/metarel-keyword/composition/ — exercises pub metarel
// with concept-reference endpoints (RFD-0031). Three rels use the
// same metarel; the compiler validates each endpoint against the
// concept-typed source/target via the four-arm endpoint resolver.

pub metaxis dependence_axis for type { independent, dependent }
pub metatype kind = { independent }
pub metatype mode = { dependent }

pub concept Aspect <: ConcreteIndividual

pub metarel characterization = {
    source: Aspect,           // concept reference (RFD-0031 Arm 3)
    target: ConcreteIndividual,
}

pub rel inheres_in(s: IntrinsicMode, t: Quality) :: characterization

Variants: _catalog/metarel-keyword/{minimal,composition}/ and the dedicated decorator workspaces under _catalog/decorator-{theorem,monotone,cache,chain,defeat,scope,complexity,unproven}/.

What you can do with this

The practical takeaway: you are not limited to the metatypes UFO ships.

A regulated-systems project that wants to distinguish Regulation from Norm from Procedure — three concepts UFO does not separate — declares its own axis and metatypes:

pub metaxis enforceability for type {
    enforceable,
    advisory,
    informational
}

pub metatype regulation = { rigid, sortal, enforceable }
pub metatype norm       = { rigid, sortal, advisory }
pub metatype procedure  = { rigid, non_sortal, informational }

These metatypes can layer on top of UFO’s (the rigid and sortal values come from UFO’s axes) or stand alone (declare your own foundational axes; ship them in your own package). User code in the regulated-systems project then writes:

use std::math::{String, Date};

pub regulation TaxRegulation12 {
    statute_id: String,
    effective_date: Date,
    text: String
}

The compiler treats regulation exactly the way it treats kind: it resolves the metatype, propagates its axis profile to TaxRegulation12, runs the meta-property calculus, fires whatever structural rules the package declared, classifies the concept against the inferred profile, and admits the declaration if everything is consistent. There is no compiler change. There is no special case. The substrate is the mechanism; the package is the content.

The same pattern applies at the relation and decorator level. A medical project might declare a treats(source: treatment, target: disease) metarel; a legal project might declare a @[binding] decorator that lowers to a custom Datalog rule. The substrate handles both because both are built from the same four forms.

Where we go next

This chapter taught the surface of the substrate — what the four declaration forms look like, how they compose, what OE0605 and OE0226 and OE0229 are checking for. The rest of Part 2 uses metatypes from UFO to teach concepts (2.2), relations (2.3), rules (2.4), computations (2.5), and the type system over them (2.6). When those chapters write pub kind, pub role, pub relator, you now know where the keywords come from.

The deeper machinery — the IS / CAN / NOT three-valued semantics, the stratified fixpoint with its termination and uniqueness results, cross-package metatype composition, the recognizer table’s shape-dispatch rules, and the structural-check error class — lives in Chapter 5.1: The Metatype Calculus. That chapter is the place to go when you start declaring your own axes and want to understand exactly what the engine does with them.

Concepts and Hierarchies

A concept is the unit of meaning in an Argon ontology. Concepts are the things in your domain — Person, Lease, Property. They have names, fields, and supertypes. Most everything else in the language hangs off them.

This chapter teaches concept declarations from one-line forms up to multi-level hierarchies, and starts the lease tutorial in earnest. The metatype keywords used below — kind, subkind, role, phase, relator — come from the UFO package, declared via the substrate forms covered in Chapter 2.1; they are not language built-ins.

The smallest concept

pub kind Person {
    id: String,
    name: String,
}

Three things to notice.

First, kind is not a keyword — it’s an identifier that resolves to an imported metatype declaration. We met that mechanism in Chapter 1.2. For the rest of this chapter we will assume metatypes::* is in scope, which is the case in our running tutorial because prelude.ar re-exports it.

Second, the body is a comma-separated list of name: Type field declarations. Trailing comma is allowed; use it.

Third, pub is opt-in. Without it, Person is visible only inside the file. With it, Person is part of the package’s exported surface (assuming prelude.ar re-exports the module, as ours does).

Subtypes

A concept declares a supertype with <: (the specializes operator), or : as a documented sugar:

pub subkind ResidentialLease <: Lease {
    bedrooms: Int,
}

Read in English: ResidentialLease specializes Lease. It inherits all of Lease’s fields and adds one more, bedrooms. The typeset alias ⊑ is also accepted (pub subkind ResidentialLease ⊑ Lease) — useful when rendering ontology source for academic publication.

Sugar: : in supertype slots. Argon also accepts : here:

pub subkind ResidentialLease : Lease { bedrooms: Int }

The two forms produce identical compilation. Why both? Argon’s two primitive relations are instantiates (: at the atom level — alice : Tenant) and specializes (<: at the atom level — Tenant <: Person). In a supertype slot the only coherent reading is specializes (you cannot instantiate a type from a type at the same metalevel), so : is admitted as a sugar for the <: of that position. New code is encouraged to use <: for clarity; existing :-form code remains valid indefinitely.

The metatype you use carries semantic weight:

• A kind is rigid (instances belong to it for as long as they exist) and sortal (it supplies its own identity criteria). Person is a kind.
• A subkind is a proper subtype within a hierarchy that still supplies identity. ResidentialLease is a subkind of Lease.
• A role is anti-rigid — a thing plays it temporarily, not permanently. Tenant is a role someone plays for a while.
• A phase partitions the lifecycle of its parent kind. We meet phases in Chapter 3.2.
• A relator is a concept whose whole purpose is to mediate other concepts. Lease is a relator — it connects a Tenant, a Landlord, and a Property.
• A category is rigid but non-sortal — a cross-cutting umbrella. LegalEntity might be one.

The metatype of a concept is its kind in the type-theoretic sense: it tells you what kinds of statements about identity, persistence, and instantiation hold for instances. We get to the formal calculus in Chapter 5.1; here we use the metatypes idiomatically.

Migration note: the team is exploring moving sibling-disjointness — the rule that says distinct subkind siblings cannot share an instance — from explicit partition axioms onto the subkind metatype itself, via axioms { siblings_disjoint } blocks in metatype declarations. Today’s code does not write partition axioms in this book’s tutorial because we do not need them; the constraint will become implicit when the redesign lands. See Appendix D.

Multi-level hierarchies

Concepts compose through inheritance. The lease model has two levels:

pub kind Person {
    id: String,
    name: String,
}

pub role Tenant : Person {
    contact_email: String,
}

pub role Landlord : Person {
    payout_account: String,
}

A Tenant is a Person who plays the tenant role. A Landlord is a Person who plays the landlord role. Both inherit id and name; each adds its own role-specific fields.

In a richer foundational ontology you might add a layer in between — say, LegalSubject : Person and have Tenant : LegalSubject — but the tutorial keeps this flat. The tradeoff is the usual one: more layers, more semantic precision, more to maintain.

The relator pattern

Some concepts exist precisely to connect other concepts. The lease itself is the canonical example:

pub kind Property {
    id: String,
    address: String,
}

pub relator Lease {
    id: String,
    tenant: Tenant,
    landlord: Landlord,
    property: Property,
    start_date: Date,
    end_date: Date,
    monthly_rent: Money,
}

A Lease does not exist independently of the parties it connects. Its identity comes from the Tenant, Landlord, and Property it relates, plus the time interval. The relator metatype marks this kind of “this-is-a-connection” concept distinctly from kind, which marks an independent existent.

You will recognise the pattern from foundational ontologies (UFO calls these relators; OntoUML uses the same name). Argon does not bake UFO into the language, but the pattern is naturally expressible because we have the metatype mechanism.

Note: the Money field type lives in std::math alongside the other primitives. A use std::math::Money at the top of the module brings it into scope; bare Money without an import produces OE0101.

Specializing the relator

Just as Tenant : Person specializes Person, leases specialize:

pub subkind ResidentialLease : Lease {
    bedrooms: Int,
}

pub subkind CommercialLease : Lease {
    permitted_use: String,
}

A ResidentialLease is a Lease (so it carries all the lease fields plus its own). The two siblings — ResidentialLease and CommercialLease — are intended to be disjoint: a single lease is residential or commercial, not both. Today that disjointness is not enforced by the metatype itself, so a partition assertion would express it explicitly. The redesign captured in Appendix D folds the disjointness into subkind’s sibling-axiom, which is what the rest of the book treats as the default reading.

Variations

A few common shapes worth knowing.

Concept without a body

The body is optional. A concept with no fields declares a name and a metatype:

pub kind LegalEntity { }

Often you do this when the concept is a parent type whose instances always pick a more specific subtype.

Concept with multiple supertypes

: admits a comma-separated list:

pub kind LawyerTenant : Tenant, Lawyer { }

Use this when a concept is genuinely both — a thing that plays the tenant role and the lawyer role. The compiler builds the closure over the supertype set.

Concept body extension

You can add fields, derives, and asserts to an existing concept from a different module via extend:

extend Person {
    email: String,

    derive HasEmail(?p: Person) :- ?p.email != ""
}

extend blocks admit only fields, derives, and asserts — not mutations, queries, or computes. The intent is structural extension (data shape, derived facts, invariants), not behavioural extension. We will use extend sparingly in the tutorial; it is mostly useful when adding a small amount of structure to a concept defined in a dependency.

Cross-package extend is a common shape: a downstream package adds optional fields to an upstream concept without forking it. The _catalog/concept-extend/cross-package/ workspace ships a two-package example — base-ontology exports Person; contact-extension extends it with phone-number fields and a derive rule classifying which contacts are reachable. Variants: _catalog/concept-extend/{minimal,composition,cross-package,idiom,anti-pattern,negative-orphan,negative-bad-member}/.

The cross-package variant looks like this in source:

// In base-ontology/src/prelude.ar:
pub kind Person {
    id: String,
    name: String,
}

// In contact-extension/src/prelude.ar:
use base_ontology::*

extend Person {
    primary_phone: String,
    secondary_phones: [String; >= 0],

    derive Reachable(?p: Person) :- ?p.primary_phone != ""
}

A downstream consumer that uses both packages sees a single Person concept with the union of declared fields and rules. The negative-orphan/ variant attempts to extend a Person the package does not have in scope — OE0805 OrphanExtend fires.

Edge cases worth knowing

• Trailing comma in field lists. Allowed everywhere a comma-separated list lives. Use it; it makes diffs cleaner.
• pub is per-item, not per-module. Each concept declares its own visibility.
• No anonymous concepts. Every concept has a name. Inline structural types like { name: String, age: Int } are not concept declarations — those are structural records, used only in narrow positions.
• Field types can be other concepts. tenant: Tenant (above) types the field as a Tenant instance. Argon handles the reference automatically; you do not write &Tenant or Box<Tenant>. There is no notion of borrowing in the language.

Putting it in the running example

Two new files in the lease tutorial:

src/party.ar:

use metatypes::*

pub kind Person {
    id: String,
    name: String,
}

pub role Tenant : Person {
    contact_email: String,
}

pub role Landlord : Person {
    payout_account: String,
}

src/lease.ar:

use metatypes::*
use party::*

pub kind Property {
    id: String,
    address: String,
}

pub relator Lease {
    id: String,
    tenant: Tenant,
    landlord: Landlord,
    property: Property,
    start_date: Date,
    end_date: Date,
    monthly_rent: Money,
}

pub subkind ResidentialLease : Lease {
    bedrooms: Int,
}

pub subkind CommercialLease : Lease {
    permitted_use: String,
}

Update src/prelude.ar to re-export both:

pub use metatypes::*
pub use party::*
pub use lease::*

Then:

$ ox check
   Checking lease-tutorial v0.1.0
    Finished in 0.10s

The hierarchy compiles. We have a structural skeleton — concepts, supertype relations, fields. What we do not yet have is constraints over those structures (ranges, multiplicities, refinement predicates) or rules that derive new facts. Those come in the next two chapters.

Summary

Concepts are the primary unit of meaning in Argon. They have a name, a metatype, an optional supertype list, and a field block. Hierarchies form via the supertype relation. Different metatypes — kind, subkind, role, phase, relator, category — mark different ontological commitments. The lease tutorial now has a Person/Tenant/Landlord hierarchy and a Lease relator with two subtypes. Next we attach properties and relations to it.

Properties and Relations

Concepts on their own describe a vocabulary. To say what holds between things in that vocabulary, you need properties (data attached to a concept) and relations (links between concepts).

In Argon, properties are concept fields — we have already seen them. Relations are a separate item kind, with two surface forms. This chapter teaches both, plus multi-valued fields, the relator pattern, and refinement-typed fields. The relator pattern uses UFO’s relator metatype, declared in UFO’s prelude with the substrate forms from Chapter 2.1.

Single-valued fields

We have written these. The shape is familiar:

pub kind Person {
    id: String,
    name: String,
}

Each field declares a name and a type. Types can be primitives (Nat, Int, Real, Decimal, String, Bool, Date, DateTime, Duration, Money — all in std::math) or other concepts (Tenant, Lease, Property).

A field of concept type holds a reference to an instance — Argon handles the indirection automatically. There is no notion of borrowing or ownership; fields read like values.

Multi-valued fields

Sometimes a concept needs to hold more than one of something — a property with several rooms, a lease with several tenants. Use the collection-type syntax [T]:

pub kind Property {
    id: String,
    address: String,
    rooms: [Room],
}

rooms: [Room] reads “an unordered collection of Room.” Argon does not commit you to a list-versus-set semantic at the surface; the runtime stores collections without duplicates by identity.

Cardinality constraints

A bare [T] admits any count, including zero. To pin the count, add a cardinality clause:

pub relator Lease {
    tenants: [Tenant; >= 1],
    landlord: Landlord,
    property: Property,
    start_date: Date,
    end_date: Date,
    monthly_rent: Money,
}

The >= 1 constraint says “at least one tenant.” Argon admits three operators in this position:

There is no < or >. If you find yourself wanting strict inequality, use >= N + 1 or <= N - 1 and pre-compute the bound, or model the constraint as a refinement type instead (see Chapter 2.6).

Tip: put the cardinality constraint on the field, not in a separate assert. The compiler can use the field-level cardinality during type-checking and reasoning; an assert that re-states the same constraint is redundant and will be flagged as such.

Examples

pub kind Square {
    sides: [LineSegment; == 4],
}

pub kind Committee {
    chair: Person,
    members: [Person; >= 3],
}

pub kind OptionalAddress {
    line_one: String,
    line_two: [String; <= 1],
}

Relations

Argon has a dedicated item kind, rel, for binary relations whose presence at the call site you want to be explicit. There are two shapes.

Binary form

pub rel HasResidence: Person -> Residence

A binary relation between two concepts. The arrow is ->. The relation name reads as a predicate at rule positions:

pub derive ActiveResident(p: Person, r: Residence) :-
    HasResidence(p, r),
    r.is_occupied

Binary relations can also carry attributes via a body:

pub rel Owns: Person -> Asset {
    acquired_on: Date,
    purchase_price: Money,
}

Treat the attached attributes as fields on the relation instance.

A worked example with decorator characteristics, from argon/examples/pizza/src/prelude.ar (the Manchester pizza ontology, ported faithfully):

// Transitive ingredient inclusion: every Margherita is a Pizza,
// every Pizza is a Food, every Food has ingredients, transitively.
@[transitive]
pub rel hasIngredient: Food -> Food

// Functional + asymmetric base: every Pizza has exactly one PizzaBase,
// and a base never "has" a pizza.
@[functional]
@[asymmetric]
pub rel hasBase: Pizza -> PizzaBase

// Functional spiciness: a topping has at most one Spiciness value.
@[functional]
pub rel hasSpiciness: PizzaTopping -> Spiciness

The pizza workspace exercises five relation characteristics — @[transitive], @[symmetric], @[asymmetric], @[functional], @[inverse-functional] — across class lattices with multiple inheritance. Read it end-to-end as a 200-line tour of relation-shape modeling without a foundational-ontology dependency. The argon/examples/wine/, argon/examples/skos/, and argon/examples/foaf/ workspaces show the same relation patterns at different domains.

Reified form

When a relation is rich enough that “binary plus attributes” feels strained — for instance, when the relation has its own subtypes, or participates in further relations — promote it to a concept of its own:

pub relator ResidentialLease : Lease {
    bedrooms: Int,
}

This is precisely the relator pattern from Chapter 2.2. The relator is a concept; its participants are fields on it; its identity is the tuple of its participants over a time interval.

The choice between rel and relator is mostly pragmatic: use rel when the relation is genuinely binary and lightweight; use a relator concept when it has substantial structure of its own. The lease in our running example is a relator because it carries dates, rent, subtypes, a lifecycle, and so on.

Composition

Binary relations can declare a composition chain over other roles:

pub rel composes_to: Agent -> Resource = role1.role2

The = a.b clause says composes_to is the composition of a and b — a derived relation, not a primitive one. We use this rarely in the tutorial; it is most useful when integrating with a foundational ontology that ships role compositions.

Inverses

If you want both directions of a relation explicitly, declare them both:

pub rel TenantOf: Tenant -> Lease
pub rel HasTenant: Lease -> Tenant

A derive rule can keep them synchronized:

pub derive HasTenant(l: Lease, t: Tenant) :- TenantOf(t, l)

Argon does not have a built-in inverse keyword. The pattern above is the idiom; it is explicit, which means the type-checker and reasoner both see the bidirectional structure.

Refinement types and field invariants

Argon admits refinement types — sub-types carved by a predicate over the metatype calculus. They live on a concept-decl’s where { ... } clause and are used at field positions like any other type:

pub subkind RigidLease : Lease where { A.rigidity == rigid }

pub kind LeaseAccount {
    lease: RigidLease,
    balance: Money,
}

The body of a refinement type is a conjunction of axis-predicates — A.rigidity == rigid, A.sortality == sortal, etc. — over the meta-property calculus, not instance-level field comparisons. The compiler proves this fragment decidable; Chapter 2.6 covers the surface in full.

Instance-level invariants — “monthly rent must be positive,” “grace days must be between zero and fourteen” — live on assert items in Chapter 2.4, not on field declarations. The two mechanisms compose: a refinement type narrows by metatype; an assert narrows by instance value.

Note: the refinement fragment is decidable in PTIME with respect to the size of the concept hierarchy and axis count. Membership uses Kleene’s strong three-valued semantics ($K3$) under the open-world assumption with the Pietz-Rivieccio “Exactly True” designation: unknown does not satisfy refinement membership; only true does. We will revisit the OWA implications in Chapter 2.6.

The Top type

Sometimes a field can hold “anything.” Argon’s top type is ⊤ (the Unicode character; the ASCII alias Top parses too):

pub kind Annotation {
    target: ⊤,
    note: String,
}

A field of type ⊤ accepts any concept instance. The trade-off is the obvious one: refinement, dispatch, and reasoning on the field are limited because the compiler does not know what to assume about it. Use ⊤ sparingly — for genuinely heterogeneous data like comment annotations or metadata blobs.

Putting it in the running example

Update src/lease.ar to use cardinality and refinement:

use metatypes::*
use party::*

pub kind Property {
    id: String,
    address: String,
}

pub relator Lease {
    id: String,
    tenant: Tenant,
    landlord: Landlord,
    property: Property,
    start_date: Date,
    end_date: Date,
    monthly_rent: Money,
}

pub subkind ResidentialLease : Lease {
    bedrooms: Int,
}

pub subkind CommercialLease : Lease {
    permitted_use: String,
}

For the tutorial we keep the lease single-tenanted (one Tenant, not [Tenant; >= 1]); a richer model would relax that. The refinement on monthly_rent will land in Chapter 2.6, where we introduce the dedicated refinement-type item.

$ ox check
   Checking lease-tutorial v0.1.0
    Finished in 0.10s

The model still compiles. We have a small but well-typed structural skeleton. Next chapter: rules.

Edge cases worth knowing

• Cardinality versus comparison. The >= / == / <= inside [T; …] are cardinality operators, separate from value-comparison operators of the same spelling. The compiler tracks them in different enums precisely so this distinction is visible. You will not accidentally cross them.
• Underscore separators in counts. [String; >= 1_000_000] works; underscores are stripped before the integer parses.
• Multi-supertype fields. A field whose type is LawyerTenant (a concept with multiple supertypes) carries the closure of all its supertypes’ fields. The compiler enforces field-name uniqueness across the closure; if two parents declare a field with the same name and different types, you get a type error and must either rename or override.
• Cyclic field types are fine. Person { friends: [Person] } works. The compiler builds a graph, not a tree.
• No anonymous concepts in field positions. A field of type { name: String } (an inline record) is not admitted; declare a named concept instead.

Summary

Fields attach data to concepts; multi-valued fields use [T] with optional cardinality clauses; relations come in binary (rel name: A -> B) and reified (relator) shapes; refinement-typed fields sharpen the field’s type with a boolean predicate. The lease tutorial now has properties and relations enough to model a typical residential agreement. What it lacks is rules: the engine that turns this static structure into derived facts. That is the next chapter.

Rules and Reasoning

Rules are where Argon stops looking like Rust and starts looking like its own thing. A rule says “whenever this body is true, this head holds.” The compiler turns rules into reasoning — given some facts, it derives more facts mechanically, with provenance for every conclusion.

This chapter teaches the rule grammar, the assertion variant, the three-engine reasoning pipeline, and a first look at the decidability tier ladder (Chapter 5.3 covers it in depth). References to kind / role / phase throughout the chapter are UFO metatypes — user-declared on top of Argon’s substrate per Chapter 2.1, not built-in keywords.

A first rule

pub derive ActiveLease(l: Lease) :-
    l: Lease,
    l.start_date <= today(),
    l.end_date > today()

Read in English: “for any Lease l, ActiveLease(l) holds when l’s start date has passed and its end date has not.” Whenever the engine has a Lease instance, it checks the body; if every atom holds, it derives ActiveLease(l) as a new fact.

Five things to notice:

1. derive introduces a rule item. The head is ActiveLease(l: Lease). The body follows :-.
2. The body is a conjunction. Each atom must hold for the rule to fire. The separator between atoms is , — there is no && and no and keyword inside a body.
3. Head parameters bind bare names. l in the head and body refers to the same binding. The first body atom (l: Lease) gives l its type; subsequent atoms reuse the binding. The ? prefix is reserved for body-fresh variables — those introduced by an aggregate’s iteration clause or a query’s body when no head parameter is in scope. Head parameters never carry ?.
4. <= and > are comparison operators, not subtype operators. We will meet specializes later for subtype tests.
5. today() is a context-supplied date function intended to return the date for the current evaluation context. It is referentially transparent for any given query — calling the same query at the same wall-clock instant should produce the same result. Status: the call parses and elaborates today, but a registered runtime evaluator is on the roadmap; in the current toolchain expressions involving today() are accepted by ox check and ox build but evaluation against a real wall clock is not yet wired. Use a Date literal (#2026-06-15#) when you need a concrete value to test against today.

Type-check it:

$ ox check
ox lease-tutorial v0.1.0 (./ox.toml)
ox 11 modules resolved from entry point
OI0804 ... derive rule `ActiveLease` classified at Tier 3 (value predicates)
check passed

The OI0804 info diagnostic is the tier classifier reporting where this rule landed on the seven-tier ladder. Three is the highest of the executable tiers — comparisons over value-typed fields put us in QF-LIA territory.

Body atoms — the small vocabulary

A rule body is a comma-separated list of rule atoms. Argon admits roughly a dozen atom shapes; in practice, most rules use four or five.

Type test

l: Lease

“l is a Lease.” Narrows l to instances of Lease (or a subtype). When you want to narrow further, use a more specific type:

l: ResidentialLease

The narrowing is sound — the compiler tracks that subsequent atoms see l at the narrower type. This is occurrence typing; the soundness result is stated in Chapter 5.1.

Comparison

l.end_date > today()
p.age >= 18
n == 0

The comparison operators are ==, !=, <, <=, >, >=. They lift to rule-atom position naturally; both sides can be expressions over bound variables and constants.

Status note: comparison operand-type rule. Today’s elaborator does not type-check comparison operands against each other — p.age < "twenty" where p.age: Int and the right side is a String literal is accepted silently. The operand-type rule for comparison atoms is part of the upcoming Appendix B operator audit (“Reserved for the second edition”). Tracked at sharpe-dev/orca-mvp#412.

Predicate call

HasName(p)
ActiveLease(l)

Calls a derive head as an atom. If the call’s arguments unify with a derived fact, the atom holds. This is how rules compose: one rule’s head is another rule’s body.

Negation

not Expired(l)

“There is no derivation of Expired(l).” Argon uses negation as failure under stratified semantics (Apt, Blair & Walker, Towards a Theory of Declarative Knowledge, 1988); the engine refuses to compile cyclic negation (OE0501).

Aggregate

count(t for t in lease.tenants where t: ActiveTenant) >= 1
sum(p.amount for p in payments where p.month == #2026-01-01#)

Five aggregate functions: sum, count, min, max, avg. The for ... in path clause binds the iteration variable; where atom filters per row. The result is an expression you can compare against a constant.

Status note: aggregate carrier-type rule. The carrier-type rule for sum, min, max, avg (count is intrinsically type-agnostic — it counts witnesses regardless of type) is part of the upcoming Appendix B operator audit. Today’s elaborator does not reject sum(e.note for e in entries) where e.note: String; tracked at sharpe-dev/orca-mvp#412.

The atom families above cover the everyday surface. Five more atom shapes round out the rule-body grammar; each gets its full treatment in Chapter 5, but a short example here makes them concrete. Every example below has a matching workspace under argon/examples/_catalog/ you can cd into and run.

Advanced atoms — a brief tour

Modal — box(...) necessity, diamond(...) possibility. box(<atom>) reads “in every accessible Kripke world, this atom holds”; diamond(<atom>) is its possibility dual. Both wrap any rule-body atom (type tests, comparisons, predicate calls, even other modal atoms). Today’s elaborator accepts both and preserves the wrapper in the IR; the planned tier:modal semantics evaluates them per-world. See Chapter 5.4.

pub derive BoxedPerson(p: Person) :-
    box(p: Person)

Variants: _catalog/rule-modal-box/{minimal,composition,idiom}/, _catalog/rule-modal-diamond/{minimal,composition,idiom}/.

Allen interval relations. Argon admits the thirteen Allen relations (Allen 1983) as binary infix operators between interval-shaped values: before, after, meets, met_by, overlaps, overlapped_by, during, contains, starts, started_by, finishes, finished_by, equals. Each operator classifies the rule at tier:temporal (Tier 4); execution backed by DatalogMTL is on the roadmap.

pub derive Precedes(x: E, y: E) :-
    x: E, y: E,
    x.interval before y.interval

Variants: _catalog/rule-allen-relations/ — the multi-allen variant exercises all thirteen operators in one workspace; the idiom variant shows the canonical “no-double-booking” temporal-invariant pattern.

Quantifiers — forall and exists binding forms. Binding-form quantifiers introduce a fresh-bound variable and lift the rule to tier:fol. They live inside unsafe logic { ... } blocks and require a @[budget] annotation for fairness once tier-6 execution lands.

unsafe logic {
    @[budget(heartbeats: 1000)]
    pub derive SomeLeaseHasEmptyId() :-
        exists l: Lease where l.id == ""
}

Description-Logic-style bounded restrictions (exists(path, Type), forall(path, Type)) classify at lower tiers and don’t need unsafe logic; see Chapter 5.3. Variants: _catalog/rule-quant-{exists,forall}/.

Hypothetical reasoning — hypothetical { ... } blocks. A hypothetical { ... } block declares a counterfactual scenario: a forked knowledge state in which axioms get overridden, the reasoner re-saturates, and ox check --reason reports the diff against the baseline.

let alice: Person = { id: "alice", salary: 100000 }

pub hypothetical alice_double_salary {
    let alice.salary: Int = 200000
}

Plain ox check only confirms the block parses and elaborates; the reasoner-side fork lands at ox check --reason time. Variants: _catalog/hypothetical-block/{minimal,composition-with-derive,idiom}/.

Reflection — meta() and the is-family. meta(X) returns X’s metatype as a value; the intrinsic lowers to a CoreRuleAtom::Meta and surfaces one of the IS-facts the meta-property calculus’s Stratum 0 propagates from each declaration’s metatype profile (Chapter 5.1).

pub derive person_is_kind(p: Person) :-
    p: Person,
    meta(p) == kind

The Person :: kind form is sugar for meta(Person) == kind. The companion is-family of pattern shapes (is unknown, is ambiguous(x), is timeout(x)) handles Argon’s three-valued query outcomes at match-arm level — Chapter 3.1. Variants: _catalog/rule-meta-coloncolon/, _catalog/rule-is-reasoning-outcome/.

A worked derivation

Before running the engine on the lease tutorial, walk through what the saturator does step by step. Suppose the knowledge base contains one Lease fact:

Lease(id="lease-001", start_date=2026-01-01, end_date=2027-01-01,
      tenant=alice, landlord=bob, property=p1, monthly_rent=9500)

and the rule

pub derive ActiveLease(l: Lease) :-
    l: Lease,
    l.start_date <= today(),
    l.end_date > today()

Today’s date is 2026-06-15. The engine performs forward-chaining saturation:

The engine stops at iteration 2: nothing new is derivable. The set of derived facts is the least fixed point of the rule’s immediate-consequence operator over the input facts. This is the standard fixed-point construction from Datalog; the result is unique and independent of the order in which the engine considered candidate bindings.

Why-provenance traces the result back: ActiveLease(lease-001) was derived by the rule ActiveLease/1 from the input fact Lease(lease-001, …) at the body’s three satisfied atoms. ox query active_leases --explain prints this tree.

Multiple bodies, one head

Two rules with the same head form a disjunction: the head holds if any of the bodies fires.

pub derive ExpiredLease(l: Lease) :-
    l: Lease,
    l.end_date <= today()

pub derive ExpiredLease(l: Lease) :-
    l: Lease,
    Terminated(l)

A lease is ExpiredLease if its end date has passed or if it has been explicitly terminated. The compiler treats the two rules as a single Datalog disjunction at the engine level. The provenance you get back when querying tells you which body fired.

Asserts — invariants

A rule with derive produces facts. An assert declares an invariant: a body that, if it ever fires, signals a violation.

assert positive_rent(l: Lease) :-
    l: Lease,
    l.monthly_rent <= 0
    => error("monthly_rent must be positive")

Three differences from derive:

1. The body is the violation condition. The body fires exactly when something is wrong. Read the rule above as “if a Lease exists with non-positive monthly_rent, that is the bad case.”
2. The consequence is mandatory. => error("…") — no optional consequence. The string is the error message.
3. No pub. Asserts are module-scope invariants, not exported.

Migration note: the team is exploring unifying assert and derive under a single rule shape with explicit event consequences (=> Error(...), => Warn(...), => FactDerived(...)). Today’s assert keyword stays the idiomatic form; the unified shape will land additively. See Appendix D.

Optional consequences on derive

A derive rule can carry a non-default consequence:

pub derive borderline_case(c: Case) :-
    c: Case,
    c.confidence < 0.7
    => flag_for_review("low confidence", c.id)

The escalate consequence sends a structured event to a human reviewer rather than tagging the case for asynchronous review:

pub derive low_confidence_decision(d: Decision) :-
    d: Decision,
    d.confidence < 0.5,
    not d.override_recorded
    => escalate("low-confidence decision", d.id, d.confidence)

Variants: _catalog/derive-escalate-consequence/ (minimal, composition-with-assert, idiom) and _catalog/derive-flag-for-review-consequence/ (same shapes).

The four consequence forms today:

Most rules use the implicit form. The explicit forms are for when the head’s purpose is communication or fallback, not just fact derivation.

Migration note: the consequence forms above are being unified with the assert mechanism into a single event-typed => Event(...) system, so that escalate, flag_for_review, error, and warn become user-defined event types rather than keyword forms. The semantics stay; the surface tightens. See Appendix D.

Running the reasoner

ox check does not invoke the reasoner by default. It type-checks and runs the meta-property calculus, but full saturation is opt-in:

$ ox check --reason
ox lease-tutorial v0.1.0 (./ox.toml)
   Reasoning over 4 rules + 2 asserts...
   2 derivations
check passed

The trade-off is speed: type-check is sub-100ms; reasoning takes longer because it actually saturates the rule set. You typically run ox check in editor-loop mode and ox check --reason before commits or releases.

To actually evaluate a query against a populated knowledge base:

$ ox query active_leases
   1 result.
   Lease(id="lease-001", tenant=Tenant(id="t-1"), …)

ox query --explain adds the why-tree — the chain of facts and rule firings that produced each result.

The three-engine pipeline

Argon’s reasoner is not a single algorithm. Three engines tune themselves to different rule types:

• Nous+ saturation — for tier:structural classification: subsumption, role hierarchies, partition. The Baader-style structural saturator (Baader et al., Pushing the EL Envelope, IJCAI 2005) lives in crates/nous. One implementation; two drivers — oxc::reason runs it at compile time, the Kernel runs it at runtime against the same evaluator.
• DataFrog — for tier:closure through tier:recursive: derive rules, asserts, stratified negation, disjunction (Apt, Blair & Walker 1988). One implementation in crates/datalog; two drivers — oxc::reasoning::datalog_bridge at compile time, the Kernel at runtime.
• DomainRuleEngine — for event-driven reactive rules and computations. Lives in the Kernel; runtime-only today (a compile-time driver is a development gap).

Above tier:recursive, rules parse and elaborate but do not execute. tier:fol is gated behind unsafe logic { … }; tier:modal and tier:mlt are syntax-only today.

The dispatch is automatic — you almost never have to think about which engine owns a rule. The classification surfaces through OI0804 if you want to see it.

The saturator follows a monotone-inflationary pattern: every derive rule’s body defines a monotone function on the fact set; the iterator applies the composition until quiescence. The fixpoint is finite (the lattice has finite ascending chains over a finite concept hierarchy) and unique (any two evaluation orders that respect stratification produce the same final state). Chapter 5.1 states the termination, uniqueness, and indeterminacy results in full.

The decidability tier ladder

Argon’s most distinctive design choice is making decidability a graded property, not a binary one. Every rule is classified at compile time into one of seven tiers:

The key thing: tiers 4–6 still parse and elaborate. The compiler checks them syntactically and runs the type-system; @[theorem] annotations are preserved through to the kernel as theorem markers for a future verification pipeline. What it does not do is run them at query time, because the engines for those fragments are either not yet shipped (tiers 4 and 5) or undecidable (tier 6); mechanical theorem verification itself is not yet active.

A package-wide cap lives in ox.toml’s [package] section:

[package]
name = "lease-tutorial"
version = "0.1.0"
max_tier = 3

The compiler refuses to elaborate any rule that classifies above this tier (OE1405). It is the package’s most general statement of “I will not surprise you with a query that takes forever.” The lease tutorial sits comfortably at tier 3.

Chapter 5.3 covers the full ladder, the formal classification function, @[theorem], unsafe logic, and the #[unproven] / #[assumed] test markers.

Edge cases worth knowing

• Variables must be bound. Every variable in a body needs at least one atom that binds it (a type test, a relation atom, a path traversal). Query heads with unbound variables emit OE1409; derive bodies with unbound identifiers fail name resolution.
• Order does not matter inside a rule body. Rule bodies are declarative — l: Lease, l.end_date > today() and l.end_date > today(), l: Lease mean the same thing. The engine picks an evaluation order that works.
• Rule heads cannot share a name with computes. pub derive ActiveLease(...) and pub compute ActiveLease(...) would collide. The compiler tells you up front (OE0206).
• Asserts run in ox check --reason and in tests. They do not run on every ox check (which skips reasoning for speed). Either run --reason or write a test that invokes the relevant assertion.
• today() versus --as-of-valid. Inside a query, today() resolves to the valid time at which the query is asked. To time-travel, pass --as-of-valid <RFC-3339> to the runtime. The same rule body will fire or not depending on the temporal frame (Chapter 5.4).

Putting it in the running example

Add src/rules.ar:

use lease::*

pub derive ActiveLease(l: Lease) :-
    l: Lease,
    l.start_date <= today(),
    l.end_date > today()

pub derive ExpiredLease(l: Lease) :-
    l: Lease,
    l.end_date <= today()

assert valid_dates(l: Lease) :-
    l: Lease,
    l.start_date >= l.end_date
    => error("lease start_date must be before end_date")

assert positive_rent(l: Lease) :-
    l: Lease,
    l.monthly_rent <= 0
    => error("monthly_rent must be positive")

And src/queries.ar:

use lease::*
use rules::*

pub query active_leases() -> [Lease] :-
    ?l: Lease,
    ActiveLease(?l)
    => ?l

pub query expired_leases() -> [Lease] :-
    ?l: Lease,
    ExpiredLease(?l)
    => ?l

pub query active_residential_leases() -> [ResidentialLease] :-
    ?l: ResidentialLease,
    ActiveLease(?l)
    => ?l

Notice: queries’ bodies use ?l because the head is empty (active_leases()) — ? introduces the body’s fresh variable. Derives’ heads carry the binding name explicitly (ActiveLease(l: Lease)), so the body reuses l without ?.

Update prelude.ar:

pub use metatypes::*
pub use party::*
pub use lease::*
pub use rules::*
pub use queries::*

Then:

$ ox check --reason
   Reasoning over 2 rules + 2 asserts...
check passed

The model now derives lease state and enforces lease invariants. We have the engine running over our model.

Summary

Rules are declarative: a head holds when its body’s atoms all hold. derive produces facts; assert declares invariants. Bodies use a small vocabulary of atoms — type tests, comparisons, predicate calls, negation, aggregates — and a few advanced shapes for cases that need them. Head parameters bind bare names; ? prefixes are reserved for body-fresh variables. The reasoner is a three-engine pipeline; the tier ladder makes decidability a graded property; --reason opts in at compile time, and --explain shows why-trees at runtime. The lease tutorial now has rules, asserts, and queries. Next we add operations.

Computations and Mutations

derive and query give you reasoning. Most real ontologies need two more things: pure functions over the data (a lease’s days-until-expiry, the total rent owed) and operations that change the world (signing the lease, expiring it). Argon has dedicated item kinds for both.

compute is the function form: input → output, no side effects, fully evaluable as an expression. mutation is the state-changing form: imperative body, audit-trailed events, with bitemporal valid-time and transaction-time semantics modeled at the language surface and at the kernel API level. (ox mutate accepts --principal, --standpoint, --valid-at, and --idempotency-key; the in-process runtime applies them against the current knowledge store, while a fully durable bitemporal log lives in the kernel API tier — see Part 4.)

This chapter teaches both. The lease-tutorial examples below model parties as UFO kind / role concepts — those metatypes are user-declared via the substrate of Chapter 2.1, not built into the language; computations and mutations themselves are vocabulary-neutral.

compute — pure functions

The simplest compute is one expression:

pub compute annual_rent(l: Lease) -> Money =
    l.monthly_rent * 12

Read in English: “the function annual_rent, given a Lease, returns twelve times its monthly rent.”

A few mechanics:

• compute is a hard-reserved keyword. Like derive and mutation, the name introduces a kind of item, not a type.
• -> Money is the return type. Argon will not infer it; computes always declare their return type explicitly. This is intentional — the return type is part of the function’s contract.
• = expr is the body. A single expression. No statements, no early returns, no side effects.

The body uses ordinary arithmetic over the primitive types (Int, Decimal, Money) and the operators in Appendix B. Date arithmetic — durations between dates, .days-style accessors, calendar-aware arithmetic — lives in domain packages today; the language core ships only the primitive types.

Three forms

compute admits three body shapes, each useful in different situations.

Form 1 — single expression

pub compute total_rent(l: Lease) -> Money =
    l.monthly_rent * months_between(l.start_date, l.end_date)

The most common form. Reads like a definition; lifts trivially into rule bodies; participates in the meta-property calculus and the tier classifier.

Form 2 — block with a body expression

When the computation needs intermediate bindings:

pub compute deposit_after_deductions(d: SecurityDeposit) -> Money {
    body {
        let allowed = sum(x.amount for x in d.deductions where x.is_allowed)
        let disallowed = sum(x.amount for x in d.deductions where not x.is_allowed)
        d.held_amount - allowed
    }
}

The body { let ... ; let ... ; <expr> } block carries let-statements (intermediate bindings, never side-effects) followed by a trailing expression that is the computed value. Form 2 looks imperative but evaluates as a pure expression — the engine inlines the lets and reads the trailing expression as the result.

Use Form 2 when an intermediate name makes the computation readable. When you find yourself writing five lets in a row, think about whether the intermediate values deserve to be their own computes — small composable functions read better than big block bodies.

Form 3 — Rust FFI

Some functions cannot be expressed in Argon — cryptographic primitives, regex matching, OS clock access. For those:

pub compute hash_id(input: String) -> String {
    impl rust("crypto_helpers::sha256_hex")
}

The impl rust("path::to::function") clause delegates to a Rust function bundled with your toolchain. Form-3 computes are opaque to the reasoner — the type-checker still validates the signature, but the body is dispatched through the runtime’s FFI surface. Use them sparingly; every Form-3 binding is a place the reasoner cannot see.

Tip: if a Form-3 compute crops up in a hot rule body, look for a way to refactor: either lift the rust call to a precomputed field (an asserted fact rather than a derived one), or rewrite the rule to keep the FFI off the inner loop.

Compositional bodies

Compute bodies admit the full expression vocabulary: arithmetic, if/else, match, aggregates, list literals, function calls. Tier-classification composes by taking the maximum tier across components, so if and match do not introduce new tiers — they propagate the tier of their branches.

Status note: if-condition type rule. The type rule for if-conditions (that they must be Bool-typed) is part of the upcoming Appendix B operator audit. Today’s elaborator accepts non-Bool conditions like if s.rank { … } where s.rank: Nat; tracked at sharpe-dev/orca-mvp#412.

pub compute lease_status(l: Lease) -> String =
    if l.end_date <= today() {
        "expired"
    } else if l.start_date > today() {
        "pending"
    } else {
        "active"
    }

pub compute lease_summary(l: Lease) -> String =
    match l {
        ResidentialLease(r) => "Residential lease, " + r.bedrooms + " bedroom",
        CommercialLease(c) => "Commercial lease, use: " + c.permitted_use,
        _ => "General lease",
    }

Aggregates lift naturally:

pub compute total_collected(l: Lease) -> Money =
    sum(p.amount for p in l.payments where p.cleared)

The for var in path where atom clause filters the iteration. The filter atom is the same predicate vocabulary as rule bodies.

mutation — operations that change the world

Where compute produces a value, mutation changes the model. A mutation can update fields, retract derived facts, emit typed events into the bitemporal log, and return a value.

pub mutation sign_lease(l: Lease, signed_at: Date) -> Lease {
    require {
        l.start_date < l.end_date
    }
    do { }
    emit LeaseSigned(l, signed_at)
    return l
}

Five clauses, all but do optional:

The recommended ordering is the table above. The parser is order-permissive — you can write emit before do — but the convention reads better in order.

A worked example using all five clauses. The retract clause removes facts from the knowledge base before the new state asserts; emit publishes the supersession event into the bitemporal log:

pub mutation correct_rent(l: Lease, new_rent: Money) -> Lease {
    require {
        new_rent > 0,
        l.monthly_rent != new_rent
    }
    retract {
        MonthlyRent(l, l.monthly_rent)
    }
    do {
        l.monthly_rent = new_rent
    }
    emit RentCorrected(l, new_rent, today())
    return l
}

Variants: _catalog/mutation-retract-clause/{minimal,composition,bitemporal,idiom}/. The catalog’s idiom/ variant pairs retract with a follow-up emit of a supersession axiom — the canonical pattern for keeping the bitemporal log audit-honest when a value is corrected.

Migration note: the team is exploring removing the do keyword: a mutation body would just be raw statements, with lets and field updates appearing directly. The emit clauses stay where they are. Today’s do { } block continues to compile; the migration will land additively. See Appendix D.

Field updates

The do { } block is where state actually changes:

pub mutation pay_rent(l: Lease, amount: Money) {
    require {
        amount > 0,
        amount <= l.monthly_rent
    }
    do {
        let new_balance = l.balance + amount
        l.balance = new_balance
    }
    emit PaymentReceived(l, amount, today())
}

Two statement forms inside do { }:

• let name [: Type] = expr — bind an intermediate value (not a state change).
• <field-path> = expr — set a field value (state change).

There is no compound assignment (+= or similar) yet. The Phase-B agenda has compound-assignment as an open ergonomics item; for now, write the equivalent: l.balance = l.balance + amount.

Events

emit Expr publishes the value of Expr into the bitemporal axiom-event log. The engine wraps the emission with three pieces of metadata: a valid time (when the event becomes true in the world), a transaction time (when the system learned of it), and a principal (which agent caused the emission, supplied via the --principal flag on ox mutate).

Events are first-class typed values. A user-defined event:

pub kind PaymentReceived {
    lease: Lease,
    amount: Money,
    received_at: Date,
}

Then emit PaymentReceived(l, amount, today()) constructs an instance and publishes it. The runtime’s bitemporal storage treats it as an append-only fact.

Migration note: events are moving toward being a first-class language primitive — a dedicated event item kind that ties consequences in rules and mutations through the same declared event types. Today, declare the event as a kind with the relevant fields; the migration will introduce event declarations as a richer alternative. See Appendix D.

Bitemporal axes — what the runtime gives you

Every event in the log carries two times. Concretely:

• Valid time — the time at which the event is true in the world. By default, today() at the moment of emission, but you can override with ox mutate --valid-at #2026-01-01#.
• Transaction time — the time at which the system learned of the event. Always the wall clock at emission; never overridable.

Queries can dial in either axis:

$ ox query active_leases --as-of-valid #2026-04-01#
   What was active on April 1?

$ ox query active_leases --as-of-tx #2026-04-15#
   What did we know was active, as of the database state on April 15?

--as-of-valid is “go back in time in the world.” --as-of-tx is “go back in time in the database.” They are independent: you can ask “as of April 15 in the database, what was active on April 1 in the world?” by combining them.

This is built in. You do not write any of it.

Forks

Sometimes you want to reason in a what-if world without mutating the canonical one. Argon’s runtime gives you forks:

$ ox mutate sign_lease --fork experimental --principal user-1 --arg l=lease-001
   Mutation applied to fork=experimental.

$ ox query active_leases --fork experimental
   ...sees the signed lease in the experimental fork only.

A fork is a structural-shared branch of the world. Mutations against a fork do not flow back to MAIN unless you explicitly promote them. We will see more of this in Chapter 5.4; here the point is just that mutations are fork-aware.

Reading the consequences

ox mutate --explain shows the mutation’s effects:

$ ox mutate sign_lease --principal user-1 --arg l=lease-001 --arg signed_at=#2026-01-15# --explain
   Preconditions:
     ✓ l.start_date < l.end_date

   Field updates:
     (none)

   Events emitted:
     LeaseSigned(lease-001, #2026-01-15#)
       valid_time = #2026-01-15#
       tx_time    = #2026-04-24T10:32:11Z#
       principal  = user-1

   Returned: lease-001

--dry-run runs the mutation without committing it — useful for testing whether preconditions hold and what events would land.

Edge cases worth knowing

• compute Form-2 cannot emit events. That is the line between compute and mutation: computes are referentially transparent.
• require is a precondition, not a guard. If require’s body does not hold, the mutation does not fire and an error is reported. It is not “skip silently.”
• mutation items must be pub to be runtime-dispatchable. The CLI dispatches by qualified name; non-pub mutations are file-scoped and unreachable from outside.
• --principal is mandatory on ox mutate. The runtime refuses to apply a mutation without an attribution. Set it; pass it; track it. The audit trail is the point.
• Event types should be declared as concepts. Inline emit of an ad-hoc tuple loses you typed-querying later. Declare a kind for every event you emit; it pays back the keystrokes immediately.

Putting it in the running example

Add src/computes.ar:

use lease::*

pub compute annual_rent(l: Lease) -> Money =
    l.monthly_rent * 12

Add src/mutations.ar:

use lease::*

pub kind LeaseSigned {
    lease: Lease,
    signed_at: Date,
}

pub kind LeaseExpired {
    lease: Lease,
    effective_at: Date,
}

pub mutation sign_lease(l: Lease, signed_at: Date) -> Lease {
    require {
        l.start_date < l.end_date
    }
    do { }
    emit LeaseSigned(l, signed_at)
    return l
}

pub mutation expire_lease(l: Lease, effective_at: Date) -> Lease {
    do { }
    emit LeaseExpired(l, effective_at)
    return l
}

Update prelude.ar:

pub use metatypes::*
pub use party::*
pub use lease::*
pub use rules::*
pub use queries::*
pub use computes::*
pub use mutations::*

Then:

$ ox check
   Checking lease-tutorial v0.1.0
    Finished in 0.12s

The model now derives, queries, computes, and mutates. We have all three computational modes wired up.

Summary

compute is for pure functions; mutation is for state changes. compute has three body forms — single expression, block, and Rust FFI — picked by what the function does. mutation has five clauses — require, retract, do, emit, return — and operates against a bitemporal, fork-aware, audit-trailed runtime. The lease tutorial now signs and expires leases. Next we tighten the type system around the model.

The Type System

Argon’s type system is unusual on three dimensions. It is ontology-aware: the metatype calculus runs alongside type-checking, so the compiler tracks not just whether a value is a Lease but whether Lease is a rigid sortal relator. It is refinement-equipped: types can be sharpened by predicate sub-types, and the compiler proves the refinement fragment decidable. It is tier-classified: the type-checker knows which decidability tier each rule sits in and refuses to sit you above the package’s cap.

The metatype machinery the type-checker reads is itself user-declarable. UFO’s metatypes — kind, subkind, role, phase, relator — are built from the substrate forms covered in Chapter 2.1; the type-checker has no special-case knowledge of them.

Most readers will get value from the surface — primitives, concept types, generics, refinements, subtype reasoning, and the ⊤ type — without reaching for the calculus underneath. This chapter sticks to the surface.

Primitive types

Ten primitives live in std::math and reach a module via explicit use:

Primitives appear as field types, parameter types, return types, and atom positions inside expressions:

use std::math::{Nat, Int, Real, String, Bool, Date, Money};

pub kind Person {
    id: String,
    age: Nat,
    height_cm: Real,
    is_active: Bool,
    born_on: Date,
}

pub compute total_owed(principal: Money, monthly_payment: Money, months: Nat) -> Money =
    principal - (monthly_payment * months)

There is no implicit prelude. A bare primitive name without a corresponding use produces OE0101 UnresolvedIdentifier with a hint pointing at the right use path.

Literals are written naturally: 42 is a Nat (or promotes to Int / Real per context), 3.14 is a Real, "hello" is a String, true and false are Bool, #2026-01-15# is a Date. Numeric promotion follows the chain Nat → Int → Real. Money literals are written as plain numerics; the compiler dispatches to the Money type when the context demands.

Concept types

Every pub kind X { … } (or pub subkind, pub role, pub relator, …) declaration introduces both a concept and a type. You can write a Lease-typed parameter, a Tenant-typed field, a [ResidentialLease]-typed return value.

pub compute primary_tenant(l: Lease) -> Tenant =
    l.tenant

The subtype graph the metatype declarations + concept hierarchy define is exactly the subtype graph the type-checker uses. So you can pass a ResidentialLease where a Lease is expected, but not the other way around without an explicit narrowing.

Collection types

Multi-valued field types we met in Chapter 2.3:

[Tenant]                 // any number, including zero
[Tenant; >= 1]           // at least one
[Field; == 4]            // exactly four
[Modifier; <= 3]         // at most three

The cardinality clause is a structural constraint on the collection’s count, not a value-comparison. The same operators (>=, ==, <=) appear elsewhere with value-comparison semantics; the type-checker keeps the two uses separated.

The Top type

When a value is genuinely heterogeneous — a comment annotation that can apply to anything, a metadata blob — type it as ⊤:

pub kind Annotation {
    target: ⊤,
    note: String,
}

The Unicode ⊤ is the canonical spelling; ASCII Top parses as an alias.

A value of type ⊤ accepts anything, but the compiler knows nothing about it: dispatch, refinement, and field-access on ⊤-typed values is restricted because there is no static structure to reach into. Use ⊤ sparingly; it is genuinely the right tool only for heterogeneous metadata.

Refinement types

A refinement type is a sub-type of an existing type whose instances satisfy a predicate over the metatype calculus. The dedicated item:

pub subkind RigidLease : Lease where {
    A.rigidity == rigid
}

Read in English: “RigidLease is the subtype of Lease whose metatype profile carries rigidity == rigid.” Because Lease is declared as a relator and relator carries { rigid, sortal } in its profile, every Lease is a RigidLease — the refinement is near-tautological for this base. The pattern becomes useful when the base type’s metatype profile is not pinned by the declaration alone.

The where { … } block is a comma-separated conjunction of refinement predicates. Today’s surface admits predicates over the meta-property calculus only — atoms of the form A.<axis> == <value>, with not available for negation:

$$predicate::=A.axis==value\mid \mathsf{not}A.axis==value$$

$$refinement::=\mathsf{pub}metatypeT:U\mathsf{where}\{{predicate}^{\ast }\}$$

Refinement bodies do not admit instance-level field comparisons (e.g., start_date < end_date) or arbitrary expressions. Instance-level invariants — “this lease’s start date precedes its end date” — ride on the assert items in Chapter 2.4, not on refinement types. The two mechanisms compose: a refinement narrows by metatype (A.rigidity == rigid); an assert narrows by instance value.

Three things make refinements useful:

1. The refinement fragment is decidable in PTIME. With respect to the size of the concept hierarchy and axis count, deciding membership in a refinement subtype is a polynomial-time procedure. ox check mechanically determines TBox-level refinement membership — given a concept declared pub subkind T : U where { … }, the compiler decides whether the refined type is satisfiable and how it sits in the subtype lattice — without invoking the reasoner.

   Status note: ABox-level refinement classification. Determining whether a specific individual (let l: Lease = { … }) actually inhabits a refinement subkind at evaluation time — i.e. assert l: ValidLease or assert ValidLease(l) against an l declared at the base type — is on the roadmap. Today the runtime classifies individuals by their declared concept and the saturation graph, but it does not yet evaluate refinement-predicate membership against an asserted individual; expect refinement-membership tests to mark #[unproven] until the classifier extends to ABox.

2. You can layer refinements. A refinement of a refinement composes by conjunction of axis-predicates.

3. Three-valued semantics ($K3$). Membership uses Kleene’s strong three-valued logic ($K3$, Kleene 1952) under the open-world assumption with the Pietz-Rivieccio “Exactly True” designation (Pietz & Rivieccio 2013): only $\mathsf{IS}$ on every conjunct admits membership; $\mathsf{CAN}$ leaves membership indeterminate; $\mathsf{NOT}$ rejects. The “Exactly True” framing — only $\mathsf{IS}$ counts as success — is the formal anchor for the fail-closed convention. Under closed-world assumption, $\mathsf{CAN}$ collapses to $\mathsf{NOT}$. That $\mathsf{CAN}$ at fixpoint completion really is genuine indeterminacy (no monotone extension of the input pins it to $\mathsf{IS}$ or $\mathsf{NOT}$) is one of the principal results stated in Chapter 5.1. Cross-standpoint federated queries lift to the four-valued $\mathsf{FDE}$ extension (Belnap 1977 / Dunn 1976) where source-level disagreement surfaces as $\mathsf{BOTH}$; per-standpoint refinement membership stays in $K3$. The full algebraic substrate is Approximation Fixpoint Theory (Denecker-Marek-Truszczynski 2000).

Variants: _catalog/concept-where-clause/{minimal,composition-with-derive,boolean-conjunction,tier-aware,negative-unsatisfiable}/. The boolean-conjunction/ workspace shows the multi-axis conjunction shape (A.rigidity == rigid, A.sortality == sortal); the tier-aware/ workspace caps the refinement to tier:closure via max_tier; the negative-unsatisfiable/ workspace declares a refinement whose body conjoins mutually-exclusive axis values — a tripwire for the post-elaboration refinement pass once the ABox classifier lands (Status note above).

A worked excerpt from _catalog/concept-where-clause/boolean-conjunction/src/prelude.ar:

// A rigid, sortal concept that also provides its own identity.
// The refinement reads three axes from the meta-property calculus
// and demands IS for each.
pub subkind IdentityProvider <: Concept where {
    A.rigidity == rigid,
    A.sortality == sortal,
    A.identity_provision == provides
}

// A field typed by this refinement only admits instances whose
// elaborated meta-property profile satisfies all three axes.
pub kind Registry {
    primary: IdentityProvider,
    aliases: [IdentityProvider; >= 0],
}

The body is a conjunction over the meta-property calculus axes from Chapter 5.1, not over instance fields. The compiler proves the fragment decidable in PTIME with respect to the concept hierarchy and axis count; the tier-aware/ variant tightens this further with max_tier: closure.

Layered refinements

pub subkind SortalLease : Lease where { A.sortality == sortal }
pub subkind RigidSortalLease : SortalLease where { A.rigidity == rigid }

RigidSortalLease is a refinement of a refinement. The compiler composes the predicates: a RigidSortalLease is a Lease whose meta-property profile satisfies both axis predicates.

Why metatype-axis-only

A refinement-type body that admitted arbitrary expressions over instance fields would be undecidable in general — equality on String and inequality on Decimal quickly take you out of any tractable fragment. Argon admits only the meta-property calculus’s three-valued state in the body precisely so the decidability proof goes through. Future cuts of the language may extend the fragment with carefully-chosen value predicates (A.rigidity == rigid plus f.size < 100, where f is a finite-domain field) — see Appendix D for the trajectory.

Narrowing and occurrence typing

Once a value is narrowed to a refinement type, subsequent uses see the narrower type. Argon’s occurrence typing is sound: a narrowing introduced at one point in a rule body remains valid for the rest of the body, and the narrowing survives composition with monotone rule application.

The CWA/OWA interaction is well-behaved as well: a narrowing established in a CWA context survives transition into an OWA context, because the narrowing is monotone in the information ordering, so adding open-world facts only strengthens it.

Subtype reasoning

The compiler’s subtype lattice is the closure of the supertype declarations across all visible packages. A few mechanics:

• A : B makes A a direct subtype of B. All of B’s fields are inherited; subtype-typed values are usable wherever B-typed values are expected.
• Multiple supertypes are admitted. A : B, C makes A a direct subtype of both. The compiler enforces field-name uniqueness across the closure and reports a diagnostic if B and C share a field name with different types.
• Refinements participate. pub subkind A : B where { p } makes A a refinement subtype of B; an A value can be used where a B is expected, but the reverse requires a refinement check.

The subtype operator is a primitive relation in the language core. The notation <: is the primary form; specializes is its keyword spelling; ⊑ is accepted as a typeset alternate:

pub derive AnyLease(l: ⊤) :-
    l <: Lease

: (instantiates) and <: (specializes) are first-class atoms in rule bodies, queries, and assertions. They are not user-declared pub rels — the type system builds on them.

Type-checking the running example

The lease tutorial accumulates refinement at this point. Add src/types.ar:

Refinements narrow by metatype, not by instance value — that constraint is what makes the membership decision tractable. Instance-level invariants (“this lease’s start date precedes its end date”) ride on assert items per Chapter 2.4. Here we use both: a refinement type that narrows by a meta-property axis, and an assert that gates instance-level admission.

use lease::*

// Refinement narrows by axis-predicate. The compiler composes the
// `where {...}` body against each candidate type's meta-property
// profile and decides membership without invoking the reasoner.
pub subkind RigidLease : Lease where { A.rigidity == rigid }

// `ValidLease` narrows by metatype as well — it's a `RigidLease` (so
// rigid) that's additionally sortal. Both predicates compose by
// conjunction over the axes declared in `metatypes.ar`.
pub subkind ValidLease : RigidLease where { A.sortality == sortal }

// Instance-level invariants live on `assert`, not on refinement bodies.
// The gate that checks `start_date < end_date` for each instance is an
// `assert` rule, decoupled from the type-system narrowing above.
assert valid_lease_dates(l: ValidLease) :- l.start_date < l.end_date
assert valid_lease_rent(l: ValidLease) :- l.monthly_rent > 0

And update prelude.ar:

pub use metatypes::*
pub use party::*
pub use lease::*
pub use rules::*
pub use queries::*
pub use computes::*
pub use mutations::*
pub use types::*

Then:

$ ox check
   Checking lease-tutorial v0.1.0
    Finished in 0.13s

ValidLease is now a type other items can reach for. A query that returns ValidLeases is well-typed:

pub query valid_active_leases() -> [ValidLease] :-
    ?l: ValidLease,
    ActiveLease(?l)
    => ?l

The compiler verifies at type-check time that every result row satisfies the ValidLease predicate. Bad data does not survive ox check.

Typed-domain metaxis values

A metaxis declaration may bind to a typed value space rather than a finite enum:

pub metaxis order : Nat for type
pub metaxis weight : Real for type where { _ > 0 }

metaxis <Name> : <Type> for <kind> admits values of the named primitive type. The optional where { _ <pred> } clause refines the admitted value-domain; the underscore _ is the candidate-value placeholder. A literal that fails type-check against the axis’s declared value_type emits OE0603 MetaxisValueTypeMismatch; a literal that satisfies the type but fails the refinement predicate emits OE0606 MetaxisRefinementViolation.

Typed-axis values flow into metatype declarations:

pub metatype kind = { rigid, sortal, provides, order = 1 }
pub metatype higher_order_type = { rigid, sortal, provides, order = 2 }

This is the foundation for multi-level theory: kind Person carries order = 1; higher_order_type Species carries order = 2; vocabulary-defined constraint rules over order enforce MLT axioms (specialization preserves order; instantiation crosses order by exactly one).

Reflection: meta() and std::meta

The compiler exposes two reflection surfaces over the type lattice. Both are usable in any rule body, query, assertion, or constraint. Both are pure: they evaluate at elaboration time against the resolved concept graph, no kernel call required.

The meta() intrinsic

meta(X) returns X’s metatype as a value. It is a compiler intrinsic, not a std::meta predicate. The argument is either a concept name or a bound variable.

pub kind Person {}
pub kind Employee : Person {}

// Test against a known metatype keyword
pub derive is_a_kind(c: Person) :- meta(c) == kind

// Explicit subject — the concept name itself
pub derive person_is_kind() :- meta(Person) == kind

meta() is part of the language substrate; no use declaration is required to call it. (use std::meta::* is for the seven reflection predicates covered below — a separate surface.)

The argument must be ground at rule-evaluation time. A free variable that no preceding atom binds emits OE0212 MetaArgumentNotGround:

// Compile error: ?z is unbound when meta() runs.
pub derive r(c: Person) :- meta(?z) == kind

Negation composes: not meta(c) == role is well-formed. The :: sugar form (Person :: kind to test meta(Person) == kind) lowers to the same atom. Tests Chapter 3.3 covers the testing-time idioms.

std::meta — universal reflection predicates

std::meta::* exposes seven typed-domain reflection predicates over the concept graph. They are universal: ontology-neutral, available without importing any vocabulary package, and structurally classified at tier:structural so they cost nothing in the decidability budget.

use std::meta::*

Examples that compile against std::meta::* alone:

use std::meta::*
use std::math::*

pub kind Person { name: String, age: Nat }
pub kind Employee : Person {}
pub kind Manager : Employee {}

// Walk the supertype lattice.
pub derive direct_super(c: Person, s: Person) :- supers(c, s)
pub derive any_ancestor(c: Person, a: Person) :- ancestors(c, a)

// Surface field names and the owning module.
pub derive has_field(c: Person, f: String) :- fields(c, f)
pub derive in_module(c: Person, m: String) :- module(c, m)

// Bind the metatype keyword as a string.
pub derive metatype_of(c: Person, m: String) :- metatype(c, m)

When to use which

meta() is for asking “what metatype is this?” — a single test against a keyword. std::meta::* is for walking the structure: every supertype, every field, every ancestor of every concept. Both compose with the rest of the rule grammar; neither carries foundational-ontology opinions. Vocabulary packages layer their own classifications on top — is_kind, is_rigid, is_relator — by composing these primitives.

std::meta and multi-level theory

std::meta::ancestors plus the order : Nat for type typed-axis from the previous section give you the substrate for multi-level theory enforcement:

pub metaxis order : Nat for type
pub metatype kind = { rigid, sortal, provides, order = 1 }
pub metatype higher_order_type = { rigid, sortal, provides, order = 2 }

// MLT axiom (one form): specialization preserves order.
// A vocabulary package writes the structural rule against std::meta:
//   ancestors(X, A), meta(X) == M_X, meta(A) == M_A
//   => order(M_X) == order(M_A)

The compiler does not bake this rule in; it is a vocabulary-level constraint that consumes the universal reflection surface. That is the design intent — Argon ships the substrate, vocabulary packages contribute the discipline.

Decorators and the recognizer

Decorators are user-defined annotations whose semantics lower to logical formulas. A vocabulary declares a decorator with an explicit body:

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

The compiler pattern-matches lowered decorator bodies against a closed set of recognized shapes (Transitive, Symmetric, Asymmetric, Reflexive, Irreflexive, Functional, InverseFunctional, QualifiedCardinality, DisjointClasses, CoveringClasses). A recognized rule gets fast-path treatment in the reasoner — enable_transitive_closure_for(r) for Transitive, and so on — and inhabits the structural tier even when the body’s syntactic form is FOL. Six normalization passes (alpha-rename, flatten-associative, push-negations-inward, implications-to-disjunctions, canonicalize-equality, sort-conjuncts) ensure equivalent formulas with different syntactic surfaces match the same canonical shape.

Decorator authors may pre-tag a body with lowers_to: <shape> for explicit fast-path declaration; the recognizer verifies the body matches the named shape and emits OE0232 RecognizedShapeMismatch on divergence. Bodies that don’t match any recognized shape fall through to generic Datalog evaluation — this is a normal outcome, not an error.

Tier classification (a brief look)

Every type-related construct is also classified at one of seven decidability tiers, the same ladder we met in Chapter 2.4. Refinement predicates that compose tier:structural atoms classify at tier:structural; refinements that include aggregates classify higher. A #dec(<tier>) directive at module / block / declaration scope binds an ambient ceiling; a refinement whose effective tier exceeds the ceiling produces OE0604 TierViolation.

A rule’s effective tier is min(syntactic_tier, recognized_tier). A forall x y z. r(x,y) ∧ r(y,z) → r(x,z) body is syntactically tier:fol, but the recognizer matches it as Transitive and the effective tier collapses to tier:closure — the rule passes a stricter ceiling that a non-recognized FOL body would not.

You will rarely see the tier classification surface unless you reach above tier:recursive. When you do, the compiler tells you, by name, which atom pushed the classification up. The InfoView panel in the editor extension (Chapter 4.3) shows the tier of any symbol on hover.

Edge cases worth knowing

• Refinements cannot be cyclic. pub subkind A : B where { p }, pub subkind B : A where { q } — the compiler rejects this at elaboration.
• ⊤ does not absorb subtypes. Lease is a subtype of ⊤, but a ⊤-typed binding does not implicitly narrow to Lease when used; you need an explicit type test.
• Primitive types are not concept types. You cannot declare pub kind Customer : Int { ... }. Concepts subtype other concepts; primitives are leaves of the type lattice.
• Generics have a future. Argon has the syntactic surface for generic parameters (<T: ordered>), but most of the running example does not need them. They land in detail in Part 5.

Putting it together

The type system gives you:

• A small set of primitives.
• A subtype lattice generated from concept declarations, refined per-package by visibility.
• Cardinality-constrained collection types.
• Predicate-subtypes via refinement, with mechanical decidability.
• A graded decidability classification that applies uniformly to types and rules.

The lease tutorial uses primitives, concept types, refinement types, and subtype reasoning. It does not yet use generics or modal-typed bindings; those wait for Part 5.

Summary

Primitives, concept types, collections, refinements, the Top type, and subtype reasoning. The refinement fragment is decidable; the subtype lattice is the closure of declarations; tier classification runs alongside type-checking. The lease tutorial now has refinement types that catch bad data at ox check time. Part 2 is complete.

Enums

An enum declaration introduces a type whose values are a finite, named set of tags. Use it when you need a type-level enumeration of mutually-exclusive cases — a status, a mode, a severity, a response category — that are not themselves concepts in your ontology and don’t carry their own data.

Enums sit alongside the other type-introducing forms in Chapter 2.6: like primitives and concepts, an enum is a thing a field can hold. Unlike concepts, enums do not participate in the metatype calculus, do not specialise other types, and do not anchor relations. They are deliberately small.

Declaring an enum

Top-level form:

enum Severity {
    Info,
    Warning,
    Error,
}

Variants are bare identifiers separated by commas. A trailing comma is permitted. A pub keyword exports the enum from its module:

pub enum LeaseStatus {
    Pending,
    Active,
    Terminated,
}

Variants may carry nested sub-variants using a brace-enclosed body. Nesting expresses a tagged hierarchy on top of the outer enumeration:

pub enum HttpResponse {
    Ok,
    Error {
        NotFound,
        ServerError,
        Timeout,
    },
}

Argon enums do not carry payload data on their variants. A variant is a name; if you need a name plus associated structure, the right form is a concept hierarchy (covered below).

Doc comments attach to the enum and to each variant:

/// The lifecycle of a residential lease.
pub enum LeaseStatus {
    /// The contract has been signed but the term has not begun.
    Pending,
    /// The term is in effect.
    Active,
    /// The term has ended; deposits and reconciliations remain.
    Terminated,
}

Using an enum value

An enum is a type. It can appear anywhere a type can — as a field type on a concept, as a parameter type on a compute, as a filler in a relation’s range:

use std::math::String

pub enum LeaseStatus { Pending, Active, Terminated }

pub kind Lease {
    id: String,
    state: LeaseStatus,
}

Variants are referenced by name. When the enum is unambiguously in scope, the bare name resolves:

test "newly-signed lease starts pending" {
    let l: Lease = {
        id: "lease-001",
        state: Pending,
    }
}

When two enums in scope expose a same-named variant, qualify with the enum’s name and a dot:

use std::math::String

pub enum LeaseStatus { Active, Inactive }
pub enum AccountStatus { Active, Frozen }

pub kind Account {
    id: String,
    lease_state: LeaseStatus,
    acct_state: AccountStatus,
}

test "fully qualified variants" {
    let a: Account = {
        id: "a-001",
        lease_state: LeaseStatus.Active,
        acct_state: AccountStatus.Active,
    }
}

The qualified form is <EnumName>.<VariantName>. Nested variants extend the path: a HttpResponse.Error.NotFound expression names the deepest tag.

When to reach for an enum

Argon offers three forms that all enumerate something. They serve distinct purposes; mixing them up produces models that are harder to reason about than they need to be.

A useful test: can a variant own a relation? If yes, it’s a concept and you want a hierarchy of subtypes. If no, it’s a tag and you want an enum.

// Tag: the response category doesn't have its own structure.
pub enum HttpStatus { Ok, Created, NotFound, ServerError }

// Concept: each lease phase carries its own roles, rules,
// and may refine further — each phase is a concept in the lattice.
pub kind Lease {}
pub phase SignedPending : Lease {}
pub phase Active : Lease {}
pub phase Terminating : Lease {}
pub phase Settled : Lease {}

Edge cases worth knowing

Empty enums are accepted. pub enum Marker {} elaborates today. There is no diagnostic for it. Empty enums are rarely useful and a future cut may flag them; don’t rely on the silence as endorsement.

Variant-validity at assignment time is not yet checked. A field declared as state: LeaseStatus will currently accept any identifier in its position — including identifiers that aren’t variants of LeaseStatus. The check is queued for a future cut; today the elaborator records the variant reference but does not yet emit a diagnostic when the reference doesn’t resolve to one of the enum’s declared variants. Treat the type annotation as documentation until the check lands.

Duplicate variant names within one enum elaborate today. A future cut will reject them; in the meantime keep variants unique by hand.

Cross-package referencing. A pub enum in package A is reachable from package B via the standard use path:

use lease_legal::LeaseStatus

Bare-name resolution applies once the use is in scope; otherwise qualify with the package-prefixed path.

Enums and the metatype calculus. Enum types are not metatypes. They cannot appear in metaxis declarations as the carrier of an axis (use a typed metaxis : <Primitive> for that), and they do not specialise via <:. They are leaves in the type system, not nodes in the lattice.

Putting it in the running example

The running lease model in Chapter 2.2 treats each lifecycle phase — SignedPending, Active, Terminating, Settled — as a concept in its own right, declared as phase subtypes of Lease. That is the right call when each phase carries its own roles, refinements, and per-phase rules. Phases are concepts.

A small enum sits alongside the phase hierarchy for an orthogonal concern — the disposition of an emitted notice:

use std::math::String

pub enum NoticeDisposition {
    Pending,
    Acknowledged,
    Disputed,
}

pub kind RentNotice {
    notice_id: String,
    disposition: NoticeDisposition,
}

The disposition is a tag attached to the notice. It doesn’t itself anchor roles or rules — those live on RentNotice — and a Disputed notice doesn’t structurally specialise into a sub-concept the lattice cares about. Enum is the lighter form, and it’s the right one here.

Worked examples in the codebase

Two of the foundational example workspaces use enums idiomatically:

• argon/examples/pizza/src/prelude.ar declares pub enum Spiciness { Hot, Medium, Mild } and attaches it to PizzaTopping via hasSpiciness: PizzaTopping -> Spiciness. The variants are tags — a Hot topping does not own its own relations, fields, or further sub-spicinesses; the enum is the right form.
• argon/examples/time/src/prelude.ar declares pub enum DayOfWeek { Monday, Tuesday, Wednesday, Thursday, Friday, Saturday, Sunday } and pub enum MonthOfYear { January, …, December }. These are textbook enums: the values are bare tags drawn from a finite, ordered set, and OWL-Time uses them in dayOfWeek and monthOfYear datatype properties without anchoring relations on the variants.

If you want a contrast — a case where what looks like an enum should actually be a concept hierarchy — read argon/examples/pizza/src/prelude.ar’s PizzaTopping lattice. There are 30+ tagged topping concepts (Mozzarella, Pepperoni, JalapenoPepperTopping, …), each capable of further specialisation, each anchoring hasSpiciness and hasCountryOfOrigin relations. Concept hierarchy is right; enum would be wrong.

Summary

• [pub] enum Name { Variant, ... } introduces a type whose values are a finite set of named tags.
• Variants are bare identifiers; nested variants extend the path (Outer.Inner.Leaf).
• Doc comments attach to the enum and to each variant.
• An enum is a type — fields and parameters can hold its values; variants are referenced bare or EnumName.Variant.
• Reach for enum when the cases are tags. Reach for a concept hierarchy when the cases are themselves ontology objects with structure. Reach for a typed metaxis when the values drive the metatype calculus.

Collections

Most real models eventually need to talk about many things at once. A building has units; a unit has tenants; a lease has parents on the title; a tax filing has dependents. Argon’s collection surface — sets, lists, maps, optionals, and ranges — gives you the shapes you reach for, the operations that go with them, and an expression-level surface (method calls, indexing, slicing, comprehensions, membership tests) that reads like the languages you already know.

This chapter sticks to the collection substrate that ships with the language. Everything in it lives under std::collection (with Range under std::math); none of it is a user-declarable concept, and none of it comes from a foundational-ontology package. The reason that matters is the next section.

Why collections live in the substrate

Argon does not admit user-declared parametric concepts. A modeler cannot write pub kind Container<T> and have the type-checker treat Container[Person] as a distinct type from Container[Organization]. That position is deliberate: parametric concepts would commit the language to a particular reading of how foundational ontologies handle type families, which would couple Argon to a specific foundation. Argon stays foundation-neutral on that question; user code consumes a small closed set of parametric type constructors, and the substrate ships them.

The collection surface is therefore a fixed inventory:

Range lives under std::math, not std::collection, because it is parametric over any orderable primitive (a numeric range, a date range, a money range) rather than collection-shaped. The four under std::collection carry an operation surface that the language treats uniformly; Range carries a small operation surface of its own.

The substrate cannot ship a new constructor without a compiler change. That is the cost of foundation-neutrality on this point: the door to user-declared parametric concepts stays shut, and the closed inventory is the consolation. The everyday modeling cases fit.

The five type constructors

A collection-typed field, parameter, or return looks like any other type position:

use std::math::{Nat, Text, Money, Date}
use std::collection::{Set, List, Map, Optional}
use std::math::Range

pub kind Building {
    id: Text,
    units: List[Unit],
    tenants: Set[Person],
    primary_contact: Optional[Person],
    rent_band: Optional[Range[Money]],
}

pub kind Unit {
    number: Text,
    occupants: Map[Date, Person],
}

The brackets Set[T] are mandatory. Argon’s expression grammar reserves < and > for comparison; angle-bracket generic syntax would fight with a < b and force lookahead. Brackets make the grammar unambiguous.

T? is sugar for Optional[T]. The two spellings lower to the same type at elaboration, and either is well-typed:

pub kind Lease {
    cosigner:           Optional[Person],
    promo_code:         Text?,
}

T? is the idiomatic surface for the common 0-or-1 case. Reach for the unsugared Optional[T] when you want the optionality to read prominently in the field shape — typically when the inner type itself is a collection (Optional[List[Person]] reads more clearly than List[Person]?).

A Map[K, V] requires K to be orderable. Concept-typed keys are admitted because every kernel id orders; primitive keys order naturally. The map is built on the same deterministic ordering the kernel uses elsewhere — never insertion order.

A Range[T] is parametric over any orderable primitive. The most common instances are Range[Nat], Range[Money], and Range[Date].

For Agents: every collection type constructor uses brackets, not angle brackets. Writing Set<T> is a parse error today. The token < always means “less than” in this grammar.

Field cardinality vs List[T]

Concept declarations have used multi-valued field syntax since Chapter 2.3:

[Tenant]                 // any number, including zero
[Tenant; >= 1]           // at least one
[Modifier; <= 3]         // at most three
[Field; == 4]            // exactly four

That form is for relation-shaped fields: the cardinality bound is a structural constraint on the underlying binary relation, not a collection object. It lowers to Set[T] semantics by default. The cardinality clause survives elaboration as a constraint over the relation’s count.

List[T], Set[T], Map[K, V], and Optional[T] are collection-typed fields: the field’s value is a single collection object that carries its members. Cardinality on these is expressed by predicates over .size() in a where clause, not by an inline bound.

When do you reach for which?

• The field is conceptually a relation between the owning concept and others (a building’s tenants; an organisation’s employees): write [T; <bound>]. Order does not matter; duplicates are not meaningful.
• The field’s value is conceptually a collection object the modeler reaches into with methods, comprehensions, or indices: write Set[T] / List[T] / Map[K, V] / Optional[T].
• The field is ordered: write List[T], or (if you want to keep the cardinality-bound surface) [T; <bound>, ordered].

The two forms share storage shape — both lower to a collection value at the data layer — but the expression-level operations differ. Method calls (xs.size(), xs.append(x)) are available on the collection-typed forms; relation-shaped fields participate in rule bodies through the relation’s atoms.

One special case carries a quickfix hint:

pub kind Lease {
    cosigner: [Person; <= 1],   // OW2402 fires here
}

[T; <= 1] is a singleton-bounded set. The semantics are identical to Optional[T], but the reading is different: a <= 1 cardinality reads like “at most one tenant”, which is fine; Optional[T] (T?) reads like “a value that may or may not be present”, which is what the surface usually means. The compiler emits OW2402 suggesting the rewrite. Take the suggestion when the intent is “value that may be absent”; keep [T; <= 1] when the intent is “this relation, capped at one”.

Method-call surface

Every collection operation is invocable by method-call syntax against a typed receiver:

pub compute count_units(b: Building) -> Nat = b.units.size()
pub compute knows_tenant(b: Building, p: Person) -> Bool = b.tenants.contains(p)

The xs.m(a, b) form desugars at elaboration time to <TypeOf(xs)>::m(xs, a, b) — a qualified call into the receiver’s submodule. There are no traits; there is no runtime method-resolution table; the receiver’s type at the call site determines the submodule, and the submodule lookup succeeds or fails at elaboration.

b.units.size()
// elaborates to
std::collection::List::size(b.units)

The desugar is mechanical and total. Unknown method names produce OE2402 UnknownCollectionMethod with a “did you mean” hint listing the valid methods on the receiver’s submodule. Wrong-typed receivers — calling .size() on something that isn’t a collection — produce OE0101 UnresolvedIdentifier at the method position.

Chained calls compose left-to-right:

pub compute active_unit_count(b: Building) -> Nat =
    b.units.filter(unit_is_active).size()

The chain is read as (b.units).filter(unit_is_active).size() and elaborates two qualified calls. Each intermediate value carries its own type; the chain is well-formed exactly when each step’s receiver matches the next step’s expected receiver.

Higher-order arguments accept two forms:

• Compute references — the bare name of a pub compute in an argument position passes that compute as a callable value. The elaborator validates the compute’s signature against the operation’s expected closure shape; mismatches fire OE2407.
• Comprehensions — inline transformations that don’t need a named function. See the comprehensions section below.

First-class lambdas (|x| x + 1) and explicit function-type syntax (T -> U) are deferred. The two forms above cover the common cases without committing the language to a function-type vocabulary.

Comprehensions

A comprehension produces a List[U] (or, when the source is a Set, a Set[U]) by walking a source collection, optionally filtering, and projecting each surviving element:

pub compute active_unit_numbers(b: Building) -> List[Text] =
    [u.number for u in b.units where unit_is_active(u)]

The shape is [<projection> for <binder> in <source> where <predicate>]. The where clause is optional. The binder is a fresh name local to the comprehension body; the projection and the predicate both see it.

Comprehensions reuse the same binding subgrammar that aggregates use in rule bodies — sum(r for s in path where pred). The semantics are the same: walk the source, retain elements satisfying the predicate, project the surviving expression.

Multiple binders are not yet admitted in the v1 surface — one source, one binder, optional where. Multi-source comprehensions, when they land, will read as [expr for x in xs, y in ys where pred] and desugar to nested filter-maps.

A comprehension desugars to a filter-map chain:

[u.number for u in b.units where unit_is_active(u)]
// elaborates to
b.units.filter(unit_is_active).map(<closure projecting u.number>)

The projection’s closure has the same elaboration discipline as a named compute: the binder is in scope, and the body must type-check against the operation’s expected closure shape.

Shadow-with-warning. If the comprehension’s binder name collides with an in-scope let binding or parameter, the comprehension shadows the outer binding within its body and the compiler emits OW2403 ComprehensionBinderShadowsOuter. The warning matches what Datalog rule-body conventions already do — fresh binders per rule body — and keeps modelers from accidentally believing the outer name is in scope. Rename the binder to silence the warning.

pub compute weird(units: List[Unit], unit: Unit) -> List[Text] =
    [unit.number for unit in units]   // OW2403 — `unit` shadowed

Indexing, slicing, membership

Three postfix forms extend the method-call surface:

Indexing. xs[i] desugars to <TypeOf(xs)>::at(xs, i) returning Optional[T]. The index type must be Nat for a List; for a Map, the index must match the declared key type and the operation desugars to Map::get. Set[T] rejects indexing with OE2406 — set elements have no positional identity, so s[0] has no meaning.

pub compute first_unit(b: Building) -> Optional[Unit] = b.units[0]
pub compute tenant_at(b: Building, d: Date) -> Optional[Person] =
    b.units[0].occupants[d]

Slicing. xs[i..j] desugars to <TypeOf(xs)>::slice(xs, Range::new(i, j)), returning List[T]. Half-open i..j, open-ended i.. and ..j are admitted. Slice bounds are checked at elaboration time when both bounds are literals (xs[5..2] fires OE2405); dynamic bounds defer the check to runtime.

pub compute first_three(b: Building) -> List[Unit] = b.units[0..3]
pub compute tail(b: Building) -> List[Unit] = b.units[3..]

Range literals. i..j constructs a half-open Range[T]; i..=j constructs an inclusive range. The range never materializes its element sequence in the v1 surface; Range::contains(r, x) answers the membership question without iterating.

pub compute rent_in_band(l: Lease, lo: Money, hi: Money) -> Bool =
    Range::new(lo, hi).contains(l.monthly_rent)

Membership. x in xs desugars to <TypeOf(xs)>::contains(xs, x). x not in xs desugars to the negation. The form is admitted at expression position and at rule-atom position:

pub derive premium_unit(U) :-
    Unit(U),
    monthly_rent(U, R),
    R in Range::new(2500, 5000)

pub compute is_listed(b: Building, p: Person) -> Bool = p in b.tenants

Operation catalog

The v1 surface ships a fixed set of operations per type constructor. The table records the operation’s signature, its return shape, its decidability tier (the per-context admission cell uses this — see the next section), and a one-line example.

The signature notation reads op(receiver, args...) -> Return. Where the return depends on the receiver’s element type or on a closure argument’s return type, that is called out.

Set[T]

List[T]

Map[K, V]

Optional[T]

Range[T]

The v1 surface is intentionally narrow. Set algebra (intersection, difference, symmetric difference), additional list ops (prepend, insert_at, sort, take_while, …), additional optional ops (flat_map, and, or), and Range::collect (which would materialize a range’s elements) are tracked as follow-up work. Until they land, modelers compose the v1 ops via comprehensions and fold.

Tier dispatch matrix

Every operation carries a decidability tier (the rightmost column of each table above). The tier interacts with the surrounding evaluation context: different bodies admit different sets of operations.

The reading is:

• pub compute / pub mutation / test admit the full operation surface. These contexts are where transformations live; they are tier-tolerant by design.
• pub derive / query admit only closure-tier operations. Rule bodies in these contexts feed the kernel’s saturation; higher-tier operations risk pushing the rule above the closure ceiling that derivation depends on for tractable evaluation.
• Refinement where { } rejects every collection operation. Refinement bodies admit predicates over the metatype calculus only — see Chapter 2.6 — and collection ops are out of fragment.

The closure-tier operations (size, contains, union, at, append, slice, get, Some, None, is_some, is_none, unwrap_or, Range::new, Range::contains) are the ones a rule body or query body can call freely. The expressive- and recursive-tier ops (map, filter, fold) move to a pub compute body if you need them inside a rule’s logic.

A rule-body violation produces OE2408 with a hint suggesting the move:

error[OE2408]: higher-tier collection op in restricted context
  --> rules.ar:14:18
   |
14 |     adult_count = b.tenants.filter(is_adult).size(),
   |                            ^^^^^^^ filter is `tier:expressive`
   |
   = note: `pub derive` bodies admit only `tier:closure` ops
   = help: lift the transformation into a `pub compute` and call it
           from the rule body

Functional semantics and the rebuild-and-assign idiom

Every collection operation is pure: it returns a new collection and leaves the receiver unchanged. xs.append(x) does not modify xs; it returns a new List[T] whose elements are xs’s followed by x.

In a pub mutation do { } body, the idiomatic way to “modify” a collection-valued field is to rebuild it and assign:

pub mutation add_parent(l: Lease, p: Person) {
    do {
        l.parents = l.parents.append(p);
    }
    return l;
}

The right-hand side computes a new List[Person]; the assignment rebinds the field. The kernel records the change as a new GroundAssertion in the append-only event log — every collection-valued property change is a single event, not a partial-update event. The discipline matches the storage model byte for byte.

In-place mutators (l.parents.insert!(p), l.parents.push!(p)) are deferred. The rebuild-and-assign form is the only mutation idiom in v1.

For optional fields, the same pattern applies:

pub mutation set_primary(b: Building, p: Person) {
    do {
        b.primary_contact = Some(p);
    }
    return b;
}

pub mutation clear_primary(b: Building) {
    do {
        b.primary_contact = None();
    }
    return b;
}

Optional under the open-world assumption

Optional[T] interacts with Argon’s open-world semantics in a way that matters for two ops: is_some and unwrap_or.

is_some(o) is classical on presence. If o is Some(_) it returns true; if o is None() it returns false. The truth value of the inner element does not enter the determination — is_some(Some(undefined)) returns true because the option has a value, even if that value’s truth status is itself Undefined.

unwrap_or(o, default) returns the inner value when o is Some(_), returning default only when o is None(). Critically, unwrap_or(Some(Undefined), default) returns Undefined, not default. The fallback applies to absence, not to the inner element’s truth status.

The reason: K3 (the three-valued logic the language uses for refinement under OWA — see Chapter 2.6) distinguishes “no value here” (a structural absence) from “value present but its truth is unknown” (an epistemic gap on the value itself). unwrap_or collapsing both cases would lose the distinction; the truth-value semantics rely on the distinction surviving.

When the intent is “if the inner value is undefined, substitute a default,” chain a separate operation that operates on the inner value:

pub compute rent_or_zero(l: Lease) -> Money =
    l.monthly_rent.unwrap_or(0)

// If `l.monthly_rent` is `Some(undefined)`, the result is undefined.
// To force a fallback on undefined values, use a refinement
// or `match` over the truth state of the inner value.

The Argon truth-value substrate (RFD-0037) covers the bilattice mechanics. Optional[T]’s semantics are downstream of that substrate: presence is classical; truth-of-the-inner-value follows whichever lattice context the surrounding standpoint declares.

Worked example

A small but real exercise. A residential building owns units; each unit has occupants over time; each occupant has a contact; the building reports a roster.

use std::math::{Nat, Text, Money, Date}
use std::collection::{Set, List, Map, Optional}
use std::math::Range

pub kind Person {
    id: Text,
    full_name: Text,
    contact_email: Optional[Text],
}

pub kind Unit {
    number: Text,
    occupants: List[Person],
    rent: Money,
}

pub kind Building {
    id: Text,
    units: List[Unit],
    rent_band: Optional[Range[Money]],
}

// Closure-tier predicates — usable in rule bodies, query bodies,
// compute bodies, mutation bodies.
pub compute has_occupants(u: Unit) -> Bool = u.occupants.size() > 0

pub compute rent_in_band(u: Unit, band: Range[Money]) -> Bool =
    band.contains(u.rent)

// Expressive-tier transformations — compute / mutation / test only.
pub compute occupied_units(b: Building) -> List[Unit] =
    b.units.filter(has_occupants)

pub compute unit_numbers(b: Building) -> List[Text] =
    [u.number for u in b.units]

pub compute roster(b: Building) -> List[Text] =
    [p.full_name for u in b.units where has_occupants(u)
                 for p in u.occupants]
    // Multi-source comprehensions are deferred; today this would
    // chain two computes or compose two filter-map calls. Shown
    // here as the form the v2 surface will admit.

// Optional unwrap with a fallback.
pub compute contact_or_placeholder(p: Person) -> Text =
    p.contact_email.unwrap_or("(no contact)")

// Membership at rule-atom position — closure-tier, admitted in
// derive bodies.
pub derive premium_unit(U) :-
    Unit(U),
    rent(U, R),
    R in Range::new(2500, 5000)

// Mutation — rebuild and assign.
pub mutation add_occupant(u: Unit, p: Person) {
    do {
        u.occupants = u.occupants.append(p);
    }
    return u;
}

// Setting an optional field.
pub mutation set_rent_band(b: Building, lo: Money, hi: Money) {
    do {
        b.rent_band = Some(Range::new(lo, hi));
    }
    return b;
}

Running ox check against this module exercises every operator the chapter introduced: bracket type construction, the ? sugar at none of the field sites (intentional — every optional field here uses the unsugared Optional[T] so the optionality reads loud), method-call dispatch, comprehension, indexing through at, range construction and membership, the in operator at rule-atom position, and the rebuild-and-assign mutation idiom.

The compute roster references multi-source comprehensions; the v1 elaborator does not yet admit them (OE2402 fires today with a hint pointing at the tracking issue). The single-source forms are shipping; the multi-source form lands with the v2 surface.

For Agents

Four idioms cover the bulk of collection work:

• Comprehension over method chain. Prefer [u.number for u in b.units where unit_is_active(u)] over b.units.filter(unit_is_active).map(unit_to_number) when the projection is a small expression. The comprehension reads closer to the intent. Reach for the chain when each step has a name worth preserving.
• Optional unwrap with fallback. o.unwrap_or(default) covers presence-based defaulting. Remember that the fallback applies to absence only; if the inner value is Undefined, the result is Undefined. When you want “either way, substitute a default”, chain a separate operation that operates on the inner value’s truth state.
• Rebuild-and-assign for mutation. do { l.parents = l.parents.append(p) } is the only way to “modify” a collection field in v1. The functional semantics are deliberate; the kernel’s event log depends on every collection-valued property change being a single GroundAssertion.
• [T; <=1] should become T?. The compiler emits OW2402 on the singleton-bounded form. Take the suggestion when the field’s intent is “value that may be absent”; the Optional form unlocks the full optional op surface (is_some, unwrap_or, map). Keep [T; <= 1] only when the field genuinely reads as “this relation, capped at one occurrence”.

A fifth, less frequent: the tier matrix is the gate. A map / filter / fold call in a derive rule body fires OE2408; lift the transformation into a pub compute and call the compute from the rule. The tier ceiling is what keeps rule-body evaluation tractable.

Summary

• Set[T], List[T], Map[K, V], Optional[T] live in std::collection. Range[T] lives in std::math. Brackets are mandatory; T? is sugar for Optional[T].
• Field cardinality [T; bound] is relation-shaped; List[T] / Set[T] are collection-typed; [T; <= 1] triggers a rewrite hint to T?.
• Method-call syntax desugars to a qualified UFCS call at elaboration time. No traits; no runtime dispatch.
• Comprehensions reuse the aggregate-binding grammar; binders shadow with a warning.
• xs[i] / xs[i..j] / x in xs desugar through the catalog. Sets reject indexing.
• The operation catalog is the closed v1 surface. Each op carries a tier; the tier-dispatch matrix decides admission per context.
• Mutation is rebuild-and-assign. Functional semantics align with the kernel’s append-only event log.
• Optional under OWA: is_some is classical on presence; unwrap_or applies only to absence and preserves inner-value truth status.

Composition

Part 2 taught the atoms — concepts, properties, rules, computations, mutations, the type system. This part teaches what to do with them.

• 3.1 Patterns and Pattern-Matching — match over data and over reasoning outcomes.
• 3.2 State Machines — modeling lifecycle via the lifecycle { … } block.
• 3.3 Tests and Verification — test blocks and @[theorem].
• 3.4 Diagrams — turning the model into pictures.

Two threads run through this part. The first is composition in the obvious sense: putting the atoms together to model real lifecycles, real rules, real interactions. The second is verification: pinning the meaning of the model down with tests and diagrams that double as living documentation.

By the end of Part 3 the lease tutorial has a state machine for Lease, a test suite that exercises it, and a set of diagrams you can hand to a non-technical stakeholder.

Patterns and Pattern-Matching

A match expression dispatches on a value’s shape. In Argon you reach for it in two settings: when destructuring data (a lease that might be residential, commercial, or general), and when handling reasoning outcomes (a query that might be unknown, ambiguous, or have timed out).

This chapter teaches both.

A first match

pub compute lease_summary(l: Lease) -> String =
    match l {
        ResidentialLease(r) => "Residential, " + r.bedrooms + " bedrooms",
        CommercialLease(c) => "Commercial: " + c.permitted_use,
        _ => "General lease",
    }

Three things to notice.

The scrutinee is the expression being matched. Here, l. Match arms are tried in source order; the first matching pattern fires.

Each arm is pattern => body. The body is any expression — a string, a method call, another match. The arrow => is the same => used elsewhere in the language; the parser disambiguates by context.

Trailing comma is allowed. Use it; rebasing match arms is friendlier when the last arm has a comma too.

Six pattern forms

The first three are the bread-and-butter. The last three are situational.

Wildcard

match status {
    "active" => 1,
    "pending" => 0,
    _ => -1,
}

_ matches anything that did not match earlier arms. It is the conventional default.

Literal

match phase_name {
    "Pending" => initial_state(),
    "Active" => active_state(),
    _ => unknown_state(),
}

Literal patterns match the exact value. Int, Decimal, String, Bool, and Date literals are all admitted.

Variant

When the scrutinee’s static type is a parent concept and you want to dispatch on which subtype it actually is:

pub compute permitted_use_or_bedrooms(l: Lease) -> String =
    match l {
        ResidentialLease(r) => r.bedrooms.to_string(),
        CommercialLease(c) => c.permitted_use,
        _ => "unspecified",
    }

ResidentialLease(r) reads “if l is a ResidentialLease, bind it to r and use that binding in the body.” The variable r is typed as ResidentialLease inside the arm body.

Type test

match v {
    p: Person => p.name,
    o: Organization => o.legal_name,
    _ => "unknown",
}

p: Person is shorthand for the variant pattern when you want the binding’s type to drive the matching. The semantics are the same; the spelling is the one most programmers reach for first.

Named-with-guard

A pattern can carry an inline filter:

match lease {
    l: ResidentialLease where l.bedrooms > 4 => "large residential",
    l: ResidentialLease => "residential",
    l: CommercialLease => "commercial",
    _ => "other",
}

The where clause is a single rule-atom — comparisons, type tests, predicate calls. Use guards when the same type maps to multiple semantic categories.

Reasoning outcomes

Argon’s reasoner returns three-valued results. A query under the open-world assumption can return:

• A concrete result.
• unknown — the reasoner cannot decide.
• ambiguous(x) — multiple inconsistent derivations.
• timeout(x) — the reasoner gave up before deciding.

A match over a query result handles each:

match ActiveLease(l) {
    is unknown => Pending,
    is ambiguous(_) => undecided_state(),
    is timeout(_) => undecided_state(),
    _ => Active,
}

This is the surface for handling reasoning-outcome cases inside compute bodies. We use it sparingly in the running tutorial; most rules sit at tier 0–3 where outcomes are decided.

Each of the six pattern forms ships with a runnable workspace under argon/examples/_catalog/match-pattern-{literal,variant,wildcard,guard}/ and _catalog/match-expression/. The match-expression directory in particular has variants for each match-in-context shape: against-literal/, against-variant/, with-wildcard/, with-guard/, composition-rule-body/. Each is a self-contained workspace — cd and ox check.

A worked example from _catalog/match-pattern-guard/with-cross-axis-guard/src/prelude.ar — a pattern arm with a multi-axis guard:

pub compute classify_payment_state(l: Lease) -> PaymentState =
    match l {
        ActiveLease(a) if a.is_current and a.balance == zero => Current,
        ActiveLease(a) if a.balance > zero => InArrears,
        ActiveLease(_) => Active,
        TerminatedLease(_) => Settled,
        _ => Unknown,
    }

The guard’s body uses the rule-body sublanguage from Chapter 2.4; it can reference fields, call computes, and probe the metatype calculus. The compiler enforces exhaustiveness after guard analysis, so an unreached arm produces OE0203 not silent fallthrough.

Exhaustiveness

The compiler checks that every match has a way of reaching a body. If a match has no wildcard and no guardless variant covering every possible subtype, the compiler reports OE0203 — non-exhaustive match:

match l {
    ResidentialLease(r) => r.bedrooms.to_string(),
    CommercialLease(c) => c.permitted_use,
    // OE0203 — what about a bare `Lease`?
}

Adding _ => "general" as the last arm fixes this. Adding l: Lease => "general" (a guardless type test for the parent type) also fixes it.

The exhaustiveness check is static — it runs at ox check. You do not pay for it at runtime.

match in different contexts

match is a single expression form, but it shows up in three places:

Compute bodies

The most common — a single-expression compute returns the result of a match:

pub compute lease_summary(l: Lease) -> String =
    match l { ... }

Mutation bodies

Inside a do { } block, a let can bind the result of a match:

do {
    let category = match l {
        r: ResidentialLease => "residential",
        c: CommercialLease => "commercial",
        _ => "general",
    }
    l.category_label = category
}

Rule bodies

A whole rule body can be a single match expression — useful when the body splits cleanly along subtype lines:

pub derive lease_category(l: Lease, cat: String) :-
    match l {
        r: ResidentialLease => cat = "residential",
        c: CommercialLease => cat = "commercial",
        _ => cat = "general",
    }

The match is desugared into a disjunction of derive rules with subtype guards.

Edge cases worth knowing

• Match arms are tried in source order. A more general pattern earlier in the list will short-circuit later, more specific arms.
• Bindings are scoped to the arm body. r in ResidentialLease(r) => is not visible after the arrow leaves.
• Type tests narrow. Inside r: ResidentialLease =>, r.bedrooms is well-typed because the compiler knows r is a ResidentialLease. This is occurrence typing (occurrence narrowing); the compiler tracks per-arm refinements automatically.
• is unknown and friends are different from _ where outcome == unknown. The is-family is a dedicated pattern shape because reasoning outcomes are not ordinary values; they live in a sum-type at the engine level that the regular comparison operators do not reach into.

Putting it in the running example

We do not add a dedicated patterns file — match shows up where it fits. Our running tutorial threads match into existing computes and mutations. For example, computes.ar could grow:

use lease::*

pub compute annual_rent(l: Lease) -> Money =
    l.monthly_rent * 12

pub compute lease_summary(l: Lease) -> String =
    match l {
        r: ResidentialLease => "Residential, " + r.bedrooms + " bedrooms",
        c: CommercialLease => "Commercial, use: " + c.permitted_use,
        _ => "General lease",
    }

$ ox check
   Checking lease-tutorial v0.1.0
    Finished in 0.13s

Summary

match dispatches on a value’s shape. Six pattern forms cover the everyday cases — wildcard, literal, variant, type test, named-with-guard, and reasoning outcome. The compiler enforces exhaustiveness at ox check; occurrence typing narrows bindings inside arms. match shows up in compute bodies, mutation bodies, and rule bodies; the surface is the same in all three.

State Machines

A great many domain concepts have a lifecycle: a Lease is Pending, then Active, then Expired or Terminated. An Order moves through Placed, Paid, Shipped, Delivered. A Patient cycles through Admitted, InTreatment, Discharged.

Argon has a dedicated construct for these — a lifecycle { … } block inside a concept body — that turns “this concept moves through phases” into a first-class part of the type system. The phases become subtypes of the parent concept. The transitions become rules. The reasoner can answer “what phase is this lease in right now” and “could this lease ever reach Terminated from where it is.”

This chapter teaches today’s lifecycle surface and shows where it is going.

A first lifecycle

Inside the Lease declaration:

pub relator Lease {
    id: String,
    tenant: Tenant,
    landlord: Landlord,
    property: Property,
    start_date: Date,
    end_date: Date,
    monthly_rent: Money,

    lifecycle {
        initial Pending,
        Active,
        Expired,
        terminal Terminated,

        Pending -> Active { on: signed }
        Active -> Expired { on: term_end }
        Active -> Terminated { on: termination_notice }
        Expired -> Terminated { on: settled }
    }
}

Five things happen here.

Phases

Inside lifecycle { }, the first members are phases. Each phase is a subtype of the parent concept (Lease) — Pending, Active, Expired, and Terminated are all subtypes of Lease, picked out by which lifecycle phase a particular lease is in at a given valid time.

A phase can be marked initial (the entry state) or terminal (an exit state with no outgoing transitions). A phase can carry its own fields — Active { occupied_since: Date } says any active lease has an occupied_since field that the others do not.

The phase metatype (declared in our package’s metatypes.ar) carries the semantic weight: phase is anti-rigid (instances move through phases) and sortal. The compiler treats sibling phases as disjoint — a lease cannot be both Active and Expired at the same valid time.

Transitions

After phases come transitions: Source -> Target { clauses }. Each transition declares one allowed move from one phase to another.

A transition admits three inner clauses, of which only one — on: — is fully wired today:

The lease’s Pending -> Active { on: signed } reads: when the signed event arrives, transition to Active. The compiler turns this into a derive rule plus an event consequence.

Migration note (the big one for this chapter): the team is exploring a redesign that collapses lifecycle { … } into a top-level statemachine sugar, desugaring to an enum, a set of derive rules, and Transition events. The current lifecycle keyword stays through a migration window; the new shape sits next to it. The two forms are close enough that switching is mechanical:

Today:

pub relator Lease {
    ...
    lifecycle {
        initial Pending,
        Active,
        terminal Terminated,

        Pending -> Active { on: signed }
    }
}

Trajectory:

pub statemachine LeaseState {
    states { Pending, Active, Terminated }
    initial Pending
    terminal Terminated

    transitions {
        Pending -> Active :- signed(self), self.start_date <= today()
    }
}

The redesign’s body shape (:- pred-body => Transition(Pending, Active)) is more uniform with the rest of the language; today’s form is a curried sugar. Both produce the same runtime behavior. Do not rewrite working code today; expect the new form to be alias-accepted when it lands. See Appendix D.

What the lifecycle gives you

A lifecycle block is not just notation. The compiler does several things with it.

Disjointness for free

A Lease is in exactly one phase at a given valid time. The phase metatype encodes the disjointness; the compiler enforces it. You do not write a partition axiom over the phases. (This is one of the places the redesign tightens — see Appendix D.)

Phases as subtypes

pub query active_leases() -> [Active] :-
    ?l: Active
    => ?l

Active is a type. You can return phase-typed values; you can pattern-match on phases; you can dispatch behavior based on phase. The compiler tracks the subtype relationship so that an Active is also a Lease for any context that expects one.

Reachability checks

The compiler computes reachability from initial phases to terminal phases. If you declare a phase that is not reachable from any initial phase — say, you forget the transition into it — the compiler tells you. If you declare a terminal phase that has outgoing transitions, you get an error.

Bitemporal tracking

The runtime treats phase changes as events on the bitemporal log. A query against --as-of-valid #2026-04-15# answers “what phase was the lease in on April 15?” The phase history is queryable.

A worked time-travel pattern: the bitemporal/ variant in _catalog/lifecycle-block/ shows a lease declaring its lifecycle, transitioning through Pending → Active, and a query filtered by valid time:

pub relator Lease {
    id: String,
    start_date: Date,
    end_date: Date,

    lifecycle {
        initial Pending,
        Active,
        terminal Terminated,

        Pending -> Active { on: signed }
        Active -> Terminated { on: term_end }
    }
}

pub derive ActiveLease(l: Lease) :-
    l: Lease, Active(l)

// At the runtime, `ox query ActiveLease --as-of-valid #2026-04-15#`
// returns the leases that were in the Active phase on April 15,
// even if they have since transitioned to Terminated.

Variants: _catalog/lifecycle-{block,phase,transition}/{minimal,bitemporal,composition-with-derive,multi-transition}/.

Variations

A few common shapes worth recognizing.

Phase with fields

A phase can carry its own data:

Active { occupied_since: Date, last_payment: Date },

The intent: occupied_since exists on Active-typed values but not on Pending or Expired. Phase fields are reserved for data that only makes sense within a phase.

Note: today’s compiler accepts the syntax but emits OW1808 (“lifecycle phase data fields not yet elaborated”) because phase-field resolution is incomplete. Until that lands, keep phases bare names — Active, rather than Active { occupied_since: Date }, — and put per-phase data on the parent concept or on a related kind keyed by phase.

Guards and effects today

Until the unified consequence syntax lands, gate a transition by putting the precondition on the mutation that fires its trigger event, and emit downstream events from the same mutation. For the lease tutorial, the sign_lease mutation precondition checks the start date is valid, then emits signed; the lifecycle’s Pending -> Active { on: signed } does the rest.

pub mutation sign_lease(l: Lease, signed_at: Date) -> Lease {
    require {
        l.start_date < l.end_date
    }
    do { }
    emit LeaseSigned(l, signed_at)
    return l
}

The runtime publishes LeaseSigned into the bitemporal log; the lifecycle’s transition fires; the phase moves from Pending to Active. The event is queryable, audit-trailable, and contributes to provenance.

Migration note: when { … } and brings_about { … } clauses inside transitions become first-class once the unified consequence syntax lands — the redesign reads transitions as Pending -> Active :- signed(self), self.start_date <= today() => Transition(Pending, Active) and LeaseSigned(self). Same semantics; the rule-body grammar replaces the constraint sublanguage. See Appendix D.

Multi-source transitions

Two transitions can share a target:

Active -> Terminated { on: termination_notice }
Expired -> Terminated { on: settled }

The Datalog the compiler produces fans these out as separate rules with the same head; the disjunction is automatic.

Standalone state-machines

Sometimes the state machine is the whole point and the parent concept is just a peg to hang it on. Declare a minimal kind whose only purpose is to host the lifecycle:

pub kind ApplicationStatus {
    application_id: String,

    lifecycle {
        initial Submitted,
        UnderReview,
        Approved,
        terminal Rejected,

        Submitted -> UnderReview { on: review_started }
        UnderReview -> Approved { on: approved }
        UnderReview -> Rejected { on: rejected }
    }
}

Once the redesign lands, this becomes a top-level statemachine ApplicationStatus { … } declaration without the parent kind, but the semantics are the same.

Edge cases worth knowing

• lifecycle is inside a concept body, not an item-start construct. You cannot write lifecycle X { … } at module level today.
• Phases cannot be pub independently of their parent. Visibility flows from the host concept.
• A concept can have at most one lifecycle. If you find yourself wanting two state machines on the same concept, either model the second as a separate concept or use a phase-of-phase nesting (which the parser does not directly support today; see Phase-B’s open thread on hierarchical state machines).
• Phase names cannot collide with the host’s field names. The compiler reports a collision error.
• initial and terminal are contextual modifiers, not keywords. They lex as IDENTs and the parser dispatches on context.

Putting it in the running example

Update src/lease.ar to add the lifecycle:

use metatypes::*
use party::*

pub kind Property {
    id: String,
    address: String,
}

pub relator Lease {
    id: String,
    tenant: Tenant,
    landlord: Landlord,
    property: Property,
    start_date: Date,
    end_date: Date,
    monthly_rent: Money,

    lifecycle {
        initial Pending,
        Active,
        Expired,
        terminal Terminated,

        Pending -> Active { on: signed }
        Active -> Expired { on: term_end }
        Active -> Terminated { on: termination_notice }
        Expired -> Terminated { on: settled }
    }
}

pub subkind ResidentialLease : Lease {
    bedrooms: Int,
}

pub subkind CommercialLease : Lease {
    permitted_use: String,
}

Then:

$ ox check
   Checking lease-tutorial v0.1.0
    Finished in 0.13s

The lease now has a lifecycle. We can ask ox query active_leases and the runtime knows how to filter by phase. We can mutate from Pending to Active via the existing sign_lease mutation, and the event flows through the lifecycle’s transition guard.

Summary

A lifecycle { … } block declares phases as subtypes and transitions as rule-events between them. The compiler gives you sibling-disjointness, subtype-typed phases, reachability checks, and bitemporal phase tracking. The lease tutorial now has a complete lifecycle. The redesign trajectory collapses the surface into statemachine sugar; today’s syntax stays through the migration. Next we test the model.

Tests and Verification

A test is a small named world the runtime sets up, makes claims about, and tears down. Argon has a dedicated test item kind, plus @[theorem]-tagged rules that the compiler preserves as theorem markers for a future mechanical-verification pipeline.

This chapter covers both.

A first test

test "a freshly-signed residential lease is active" {
    let alice: Tenant = {
        id: "alice-001",
        name: "Alice",
        contact_email: "alice@example.com",
    }
    let bob: Landlord = {
        id: "bob-001",
        name: "Bob",
        payout_account: "acct-bob",
    }
    let house: Property = {
        id: "p-1",
        address: "1200 University Ave",
    }
    let lease: ResidentialLease = {
        id: "lease-1",
        tenant: alice,
        landlord: bob,
        property: house,
        start_date: #2026-01-01#,
        end_date: #2027-01-01#,
        monthly_rent: 9500,
        bedrooms: 3,
    }

    assert ResidentialLease(lease)
    assert ActiveLease(lease)
}

Run it:

$ ox test
   Compiling lease-tutorial v0.1.0
   Running 1 test
test scene "a freshly-signed residential lease is active" ... ok

test result: ok. 1 passed; 0 failed; 0 unproven; 0 assumed; 0 ignored

Three things to notice.

test "string" not test name

Tests are named with string literals — they are descriptive narratives, not identifiers. This is intentional: a test description is what shows up in ox test output, in CI logs, and in failure reports. Make it readable. “a freshly-signed residential lease is active” beats signed_lease_active.

let for setup

The body’s let name : Type = { fields } form constructs an instance directly. Field-block syntax lets you supply each field by name; the compiler validates against the declared type. The instance is bound to the local name; you can refer to it in assert statements.

This is a different let from the one inside compute Form-2 bodies: that let binds an intermediate value during evaluation; this let constructs a concept instance for the test’s local world.

assert <atom> for claims

Inside a test, assert introduces a single rule-atom claim — a type test, a derive-head call, a comparison, an aggregate inequality, or any other shape the rule-body grammar admits. The runtime evaluates the atom against the test’s world; if it does not hold, the test fails.

assert here is post-reasoning: the runtime saturates the model first (running all asserts and derives), then checks each test claim against the saturated knowledge base. So assert ActiveLease(lease) works because the ActiveLease derive rule has fired during reasoning.

You can also write assert not <atom>:

test "a lease with start >= end is rejected by the validity refinement" {
    let bad: Lease = {
        id: "lease-bad",
        ...
        start_date: #2027-01-01#,
        end_date: #2026-01-01#,
        ...
    }

    assert not bad: ValidLease
}

not negates the atom — the test passes when the atom fails. Useful for exclusion claims like “this bad input does not pass our refinement.”

Status note: instantiates-form assertions in tests. The runtime’s assertion evaluator currently supports concept-as-predicate atoms (assert ResidentialLease(lease), assert ActiveLease(lease)) but does not yet evaluate the instantiates-form assert <ind>: <Concept> (and its negation) — running such a test reports atom shape not yet supported: Instantiates. The shape is parsed and elaborated and passes ox check / ox build; it just isn’t dispatched by ox test yet. Until that lands, prefer assert <Concept>(<ind>) for membership claims; refinement-membership tests will roll in alongside the runtime extension.

Sequenced statements: mutate and cleanup

Tests aren’t only declarative. A test can also exercise a pub mutation against the test ABox, observe its effects, and run ordered teardown. The test body admits four statement kinds in source order: let, assert, mutate, and cleanup.

test "rent payment passes timeliness check" {
    let p: RentPayment = {
        paid_on: 2025-03-03,
        amount: 9500,
        period_label: "2025-03",
        is_timely: true,
    }

    mutate record_rent_payment(p)

    assert RentPayment(p)
    assert tenant_balance(p.tenant) == 0

    cleanup {
        mutate retract_test_payment(p)
        assert not RentPayment(p)
    }
}

mutate <name>(<args>) invokes a pub mutation. The runner:

1. Resolves the mutation by name through the same import surface as any other cross-package symbol.
2. Evaluates each require { } precondition against the current post-saturation ABox. On the first false, the runner records a structured MutationPreconditionFailure and skips the mutation’s do / retract / emit clauses; subsequent statements continue against the unchanged ABox so you see all assertion drift in one run.
3. Otherwise applies retract, do (field updates and locally-bound let individuals), and emit (events become individuals visible to subsequent saturation).
4. Re-saturates. The next assert evaluates against the post-mutation state.

cleanup { stmts } is a single, trailing teardown block. Cleanup admits the same four statement kinds and runs regardless of whether main-body assertions failed. Failures inside cleanup are tagged with a cleanup: true flag on the runner output so you can distinguish “the operation failed” from “the teardown failed.”

Well-formedness rules:

• A test admits at most one cleanup block (OE0240 MultipleCleanupBlocks if more).
• cleanup must be the last statement (OE0241 CleanupNotAtEnd if anything follows it).
• Cleanup blocks don’t nest (OE0242 NestedCleanup).

What v1 catches

Before this surface existed, the only way to “test” a mutation was the scene-shape convention: let-bind the mutation’s emitted events as if it had run, then assert the post-state shape. That convention proved input shapes were constructible but never evaluated require, never exercised do, never verified that emit clauses fired.

mutate <name>(<args>) closes those gaps for the clauses v1 fully evaluates:

• Existing-precondition violations. A test that hands record_rent_payment an is_timely: false payment fails with MutationPreconditionFailure rather than silently passing.
• emit clauses (constructor case). emit Event { ... } evaluates the expression and mints a fresh event individual with the literal field values. An assert Event(...) after the mutate statement is meaningful coverage of the emit clause.
• Multi-mutation flows. mutate A(...); mutate B(...); assert <post-state> proves the chained effect with re-saturation between steps so B’s require sees A’s derived facts.
• Cleanup ordering. A cleanup { } block runs regardless of mid-test assertion failures, so a teardown mutation’s post-state assertion is exercised even when an earlier assertion drifted.

What v1 does NOT catch

The runner is honest about which clauses it does not yet evaluate against the test ABox — those clauses surface as MutationUnsupported test failures so the modeler sees the gap rather than a silent pass:

• do { x.field = expr } field-updates. v1 emits a MutationUnsupported failure per field-update. A test like mutate update_balance(acct, 100); assert acct.balance == 100 will see the runner flag the gap explicitly. v2 scope.
• retract { } clauses. v1 emits a MutationUnsupported failure per retract. mutate teardown(x); assert not Concept(x) reports the unsupported flag rather than silently passing or failing the assertion. v2 scope.
• do { let } value-expression bindings. The let’s type assertion lands and the binding is visible to subsequent statements as a typed individual, but the field assignments inside the let’s value expression do not yet bind. v2 scope.
• emit p path-reference (no-op). When the elaborator lowers emit p (where p is a do { let }-bound name) the resulting CoreEmit carries empty args. v1 treats this as a no-op since p is already in the ABox via the let. Constructor-form emits are the meaningful coverage path; path-reference assertions test the let-binding shape, not the emit clause itself.
• Dropped preconditions. A record_rent_payment whose require { p.is_timely } line was deleted from source still appears to pass — there’s no atom left to evaluate, so no MutationPreconditionFailure ever fires. Detecting “this mutation should have a precondition but doesn’t” requires a separate mutate_fails <name>(<args>) form that proves a precondition fails. v1 catches violations of preconditions the modeler kept; v2 will catch dropped-precondition regressions.

Multi-mutate failure propagation

When mutation A’s require fails, A’s do / retract / emit are skipped and the ABox stays unchanged. The runner does not halt the statement loop — it continues to the next statement. A subsequent mutate B(...) runs with B’s require evaluating against the pre-A state; if B’s preconditions hold against that state, B applies normally.

This means a chained-mutation test where B depends on A’s effects will see B fail or behave unexpectedly when A is skipped — but the source ordering of failures (A first, then B’s drift) makes the dependency obvious. The alternative — halting after A’s failure — would hide downstream drift.

Ordering

Tests with only let and assert statements observe today’s behavior unchanged: lets materialize, the ABox saturates, assertions evaluate. Tests that introduce mutate get per-statement saturation — re-saturation runs between mutate statements so each mutation’s require sees the previous mutation’s derived facts. A test author who introduces a mutate and observes that an assertion that previously passed now fails should investigate whether the mutation legitimately changes the asserted state — the change is signal, not noise.

Failed assertions don’t halt the loop. The runner records every assertion’s outcome and continues, so you see all failures in one run.

Compute equality

A specifically-supported test-only form: assert that a compute call equals an expected value.

test "deposit return arithmetic" {
    let r: DepositReturn = {
        deposit_held_amount: 9500,
        allowed_deduction_total: 1400,
    }

    assert deposit_after_deductions(r) == 8100
}

The compute is called against the test’s world; the result is compared with the expected value. This is how you validate that arithmetic-heavy computes do what you mean.

Multiple tests in a module

A test block is an item, like any other. Several can live in the same file:

use lease::*
use party::*
use rules::*
use types::*

test "active lease is queryable" { ... }
test "expired lease is queryable" { ... }
test "validity refinement catches bad dates" { ... }
test "validity refinement catches non-positive rent" { ... }

Convention: put tests in their own module — typically src/tests.ar for a small package. The book’s running tutorial follows this convention.

Frames and fixtures

When several tests share setup — the same Tenant, the same Property, the same baseline rules — pull that setup into a frame. A frame is a named, composable bundle of TBox + rules + ABox that any test can opt into.

frame canonical_party {
    let alice: Tenant = {
        id: "alice-001",
        name: "Alice",
        contact_email: "alice@example.com",
    }
    let bob: Landlord = {
        id: "bob-001",
        name: "Bob",
        payout_account: "acct-bob",
    }
    let house: Property = {
        id: "p-1",
        address: "1200 University Ave",
    }
}

A frame’s body admits any top-level item form — concept declarations, rules, asserts, lets. pub frame exports across packages; bare frame is package-local.

Tests compose frames with using:

test "a freshly-signed lease over the canonical party is active" using canonical_party {
    let lease: ResidentialLease = {
        id: "lease-1",
        tenant: alice,
        landlord: bob,
        property: house,
        start_date: #2026-01-01#,
        end_date: #2027-01-01#,
        monthly_rent: 9500,
        bedrooms: 3,
    }

    assert ResidentialLease(lease)
    assert ActiveLease(lease)
}

using pulls every binding, rule, and assertion the frame defines into the test’s world. Multiple frames compose: using canonical_party, baseline_rules brings both. The same name declared in two composed frames is a conflict (OE0215); a using reference that does not resolve to a known frame is OE0214; an inline fixture that redeclares a frame member is OE0216; circular frame includes are OE0218.

A worked multi-frame example:

frame canonical_party {
    let alice: Tenant = { id: "alice-001", name: "Alice", contact_email: "alice@example.com" }
    let house: Property = { id: "p-1", address: "1200 University Ave" }
}

frame baseline_rates {
    let standard_rent: Money = 9500
    let standard_deposit: Money = 19000
}

test "standard-rate lease matches baseline" using canonical_party, baseline_rates {
    let lease: ResidentialLease = {
        id: "lease-1",
        tenant: alice,
        property: house,
        monthly_rent: standard_rent,
        start_date: #2026-01-01#,
        end_date: #2027-01-01#,
        bedrooms: 3,
    }

    assert lease.monthly_rent == standard_rent
}

Variants: _catalog/test-frame-declaration/{minimal,multi-frame,frame-with-fixtures}/ and _catalog/test-using-clause/{multi-using,composition-with-expect}/.

Status note: OE0216 not yet emitted. OE0216 is registered in the diagnostic catalog and committed by the rule above, but the emit-site at the inline-fixture-vs-frame-composition junction is not yet wired in the elaborator. Tests that exercise the collision (an inline fixture redeclaring a name a using-pulled frame already contributes) currently compile clean. Sibling diagnostics OE0214 / OE0215 / OE0218 are wired. Tracked at sharpe-dev/orca-mvp#411.

Inside a test, fixture { … } declares a test-local mini-module — items declared in the fixture are visible in the surrounding test but never escape to the parent module:

test "deposit return arithmetic with a custom property" {
    fixture {
        let custom: Property = {
            id: "custom-1",
            address: "42 Galaxy Way",
        }
    }

    let r: DepositReturn = {
        deposit_held_amount: 9500,
        allowed_deduction_total: 1400,
    }

    assert deposit_after_deductions(r) == 8100
}

Diagnostics that arise inside a fixture block are captured — they are visible to the test’s expect block (below) but never propagate to the parent module’s diagnostic stream. This lets a test deliberately exercise a malformed fixture and assert the right error fires, without the malformation breaking unrelated tests in the same package.

Diagnostic expectations

Tests can verify the compiler’s diagnostics, not just post-saturation fact-claims. The mechanism is the expect { … } block paired with //~ <label> source markers:

test "a sortal without a Kind ancestor is flagged" {
    fixture {
        pub kind Person { name: String }
        //~ orphan_role
        pub role Orphan { }
    }

    expect {
        diagnostic OW0207 at orphan_role
    }
}

//~ <label> anchors a labelled marker to the next source line — the convention follows Rust’s compiletest. Inside expect { … }, the bare form diagnostic <code> requires that exactly one diagnostic with that code fires somewhere in the test’s scope; at <marker> constrains the match to the labelled span; severity:<level> (one of error, warning, info) further constrains. Severity defaults to error when omitted.

expect {
    diagnostic OE0211 at line_a
    diagnostic OE0212 severity:warning
    diagnostic OE0605
}

The test passes when every claim in the expect block matches. An unmatched claim, an unexpected diagnostic above the configured severity floor, or a diagnostic anchored at the wrong span is a test failure; the runner surfaces the diff between expected and actual.

expect { … } and assert <atom> compose. A single test can verify both that a fixture produces the right diagnostic and that the rest of the model still satisfies its post-saturation claims.

test "bad lease shape flags + good lease still classifies" {
    fixture {
        //~ bad_lease
        let bad: Lease = { id: "x", start_date: #2027-01-01#, end_date: #2026-01-01# }
    }

    let good: Lease = {
        id: "y",
        start_date: #2026-01-01#,
        end_date: #2027-01-01#,
        monthly_rent: 9500,
    }

    expect {
        diagnostic OE0606 at bad_lease    // refinement violation on bad
    }

    assert ValidLease(good)               // good still satisfies the refinement
}

Variants: _catalog/test-expect-block/{minimal-expect,multi-arm-expect,with-fixture,expect-with-query}/.

meta() reflection and :: classification

Two related forms surface the metatype of a concept inside a rule body, query, or assertion. meta(X) returns X’s metatype as a value:

pub derive is_kind(x) :- meta(x) == kind

Person :: Kind is sugar for the same query — read “Person is a Kind”. The two lower to the same internal atom; pick whichever reads more naturally in context.

pub derive equiv(x) :- x :: Kind

meta() and :: classify types, not instances. A bound variable or named concept fits. A free unbound variable does not — meta(?z) with no binding fires OE0212 MetaArgumentNotGround at elaboration. Negation composes: not meta(x) == role is well-formed.

Tests use these forms to assert metatype-shape directly:

test "Tenant is a role" {
    assert Tenant :: Role
}

@[theorem] — mechanical verification

Some claims are not test-shaped. They are statements about the rule system itself: “this property holds for every possible lease, not just the three I happen to construct in a test.” For those, mark a derive rule with @[theorem]:

@[theorem]
pub derive transitive_subtype(x: ⊤, y: ⊤, z: ⊤) :-
    x specializes y,
    y specializes z
    => x specializes z

@[theorem] marks the rule as a theorem claim. At the current cut, the marker is preserved through compilation and surfaces in the kernel’s runtime so a future verification pipeline can target it; the compile-time mechanical-verification pass (the saturator + meta-property calculus attempting to prove that the rule’s body always implies its head) is not yet active. Today the value is signalling intent — the body of @[theorem]-tagged rules is the inventory the verification pass will close over when it lands.

@[theorem] is restricted to derive items. Placing it on a compute, mutation, query, or anything else yields OW0821 (“@[theorem] applied to a non-derive item”); declaring it twice on the same derive yields OW0822.

Two related attributes come from the same family:

• #[unproven] — applied to a test block. Marks a theorem-shaped claim that the test asserts as true without mechanical verification. The test runs as usual; the runner reports it under its own status category so the build’s body of unproven claims is visible at a glance.
• #[assumed] — applied to a test block. The body’s claim is injected as a postulate within the test’s scope. Used when a real-world axiom (e.g., “every SSN is unique”) is needed for downstream reasoning but cannot be derived from the model. Reported under its own status category for the same reason.

#[unproven]
test "subtyping is transitive across the entire lattice" {
    /* claim — not yet mechanically verified */
}

#[assumed]
test "every SSN is unique" {
    assert forall ?p1, ?p2: Person where ?p1.ssn == ?p2.ssn => ?p1 == ?p2
}

@[…] AttrList and @<ident> / #<ident> Decorator forms are accepted as alternates to #[…] for both attributes. Pick the form that matches the package’s prevailing style.

What ox test runs

ox test runs every test block in the project. @[theorem] markers are surfaced at ox check / ox build time (today as preserved markers; the verification pass is forthcoming), not under ox test — so a (future) verified theorem will be a property of the build, not of an individual test invocation.

The runner reports five status categories: Pass (every claim held), Fail (a claim did not hold), Unproven (a claim marked #[unproven] ran without proof), Assumed (a claim marked #[assumed] was injected as a postulate), Ignored (the test was excluded from the run). The categories are surfaced as separate counts in the test result: line so a build’s body of unproven and assumed claims stays visible.

$ ox test
   Compiling lease-tutorial v0.1.0
   Running 5 tests

test result: ok. 3 passed; 0 failed; 1 unproven; 1 assumed; 0 ignored

Pass -p <package> to scope to a single package within a workspace. Pass --filter <pattern> to run only tests whose names match. Pass -v / --verbose to show every assertion, not just failures.

Edge cases worth knowing

• let : Type = { fields } is the canonical creation form inside tests. It runs the same field-validation the type-checker runs on parameter passing; bad field types fail at ox check, not at ox test.
• Tests run with full reasoning. Unlike the default ox check, tests trigger the reasoner so that derives and asserts have fired before tests’ assert claims are evaluated.
• Assertions in tests are not the same as assert items at module scope. A module-scope assert declares an invariant over the package; a test’s assert is a single rule-atom check inside the test’s world.

Putting it in the running example

Add src/tests.ar. Bundle the shared party-and-property setup into a frame so each test’s body stays focused on what it actually exercises:

use lease::*
use party::*
use rules::*
use types::*

frame canonical_party {
    let alice: Tenant = {
        id: "alice-001",
        name: "Alice",
        contact_email: "alice@example.com",
    }
    let bob: Landlord = {
        id: "bob-001",
        name: "Bob",
        payout_account: "acct-bob",
    }
    let house: Property = {
        id: "p-1",
        address: "1200 University Ave",
    }
}

test "a freshly-signed residential lease is active" using canonical_party {
    let lease: ResidentialLease = {
        id: "lease-1",
        tenant: alice,
        landlord: bob,
        property: house,
        start_date: #2026-01-01#,
        end_date: #2027-01-01#,
        monthly_rent: 9500,
        bedrooms: 3,
    }

    assert ResidentialLease(lease)
    assert ActiveLease(lease)
    assert lease: ValidLease
}

test "a lease with start >= end is rejected by the validity refinement" using canonical_party {
    let bad: Lease = {
        id: "lease-bad",
        tenant: alice,
        landlord: bob,
        property: house,
        start_date: #2027-01-01#,
        end_date: #2026-01-01#,
        monthly_rent: 9500,
    }

    assert not bad: ValidLease
}

Then:

$ ox test
   Compiling lease-tutorial v0.1.0
   Running 2 tests
test "a freshly-signed residential lease is active" ... ok
test "a lease with start >= end is rejected by the validity refinement" ... ok

test result: ok. 2 passed; 0 failed; 0 unproven; 0 assumed; 0 ignored

The model is now self-validating. Bad inputs do not survive the test pass.

Summary

Tests are first-class — test "string-name" { let setup; assert claims }. Frames bundle setup so tests share it via using. Fixtures scope test-local items and capture their diagnostics. expect { diagnostic … } blocks paired with //~ <label> markers verify the compiler’s output, not just post-saturation facts. meta() and :: surface metatype-shape directly. @[theorem], #[unproven], and #[assumed] provide a graded set of verification claims, from informally-tested through mechanically-verified through axiomatic, and the runner reports them as five distinct status categories. The lease tutorial now has tests covering the happy path and the failure modes that the refinement type catches. Next we render the model.

Diagrams

In Argon, the source is the truth and visuals are lenses onto it. A diagram is not a separate document you maintain alongside the model; it is a block of source code in the same file as the rest of the model, evaluated by the compiler, rendered to SVG or OntoUML JSON by ox diagram. (PNG / PDF are produced by passing the SVG through an external rasterizer such as rsvg-convert or cairosvg.)

When the model changes, the diagram changes with it. When you want to look at a different facet of the same model, you write a different diagram block — not a different ontology.

This chapter teaches the diagram surface and ends the running example with a set of pictures of the lease model.

A first diagram

diagram "lease participants" {
    include {
        Property,
        Person,
        Tenant,
        Landlord,
        Lease,
        ResidentialLease,
        CommercialLease,
    }
}

Render it:

$ ox diagram "lease participants"

ox diagram writes one SVG per diagram into the output directory (diagrams/ by default; override with -o <dir>). The file for the example above lands at diagrams/lease participants.svg — an SVG showing the seven concepts and the supertype + role + relator edges between them. No layout work, no manual node placement — the renderer’s layout engine handles that.

Anatomy of a diagram block

Three slots:

diagram "<name>" [from "<base>"] {
    <statements>
}

• "<name>" is a string literal — diagram names admit spaces and Unicode so they read well in figure captions.
• from "<base>" is optional inheritance: a diagram can derive from another by adding/removing/overriding statements. We use it sparingly; it is occasionally useful when you have a base diagram for an audience and want a tightened version for a different one.
• <statements> are the eight families of diagram statements — include/exclude, set/show, color/label/highlight, group/layer/collapse, layout/direction/align, ensure/encourage, title/description, format/size.

Most diagrams need only a couple of statement families. We will mostly use include/exclude.

Source forms

The include statement takes a source. Argon admits seven source forms:

The same forms work for exclude (which removes concepts from the diagram). exclude runs after include, so the typical pattern is “include broad, exclude narrow.”

Pipe chains

A trailing pipe-chain refines the source via predicate filters:

include * | where metatype == kind | where rigidity == rigid

Each | where ... filters the running selection. The grammar inside where is the same predicate vocabulary you use in rule-atom positions: comparisons, type tests, and the ontology-aware predicates that come from the metatype calculus (metatype, rigidity, sortality, …).

Use pipes when you want to show a facet of the model rather than every concept — “all rigid kinds,” “every concept with a non-empty lifecycle,” and so on.

Styling and layout

A handful of statement families let you reach into the visual:

diagram "lease participants" {
    include { Person, Tenant, Landlord, Property, Lease }

    color by metatype {
        kind: blue,
        role: green,
        relator: orange,
    }

    layout sugiyama(spread: 1.5)
    direction left-to-right
    format svg, png
}

• color by metatype { ... } — colour-code nodes by metatype. Other axes (color by rigidity, color by sortality) work too.
• layout <algo>(...) — pick a layout algorithm. sugiyama is the default; alternatives include force, tree, circular. The (...) arguments are layout-specific.
• direction — left-to-right, right-to-left, top-to-bottom, bottom-to-top.
• format svg, pdf, png — declare output formats at the diagram level. The CLI flag --format overrides.

You can usually leave layout alone for small diagrams; the defaults work well up to about 30 nodes.

OntoUML round-trip

For audiences who use OntoUML tooling — Visual Paradigm, Menthor Editor, the ontouml-vp-plugin — Argon can emit an OntoUML JSON document instead of (or in addition to) a visual format:

$ ox diagram "lease participants" --format ontouml

The OntoUML format writes a single <package-name>.ontouml.json whose diagrams array carries every (filtered) diagram as an OntoUML 2.0 diagram-section entry — landing in the same output directory (diagrams/ by default; override with -o <dir>).

Round-trip is layout-stable: the visual layout decisions an OntoUML editor adds when a human curates the model can be preserved through a @[layout] attribute and round-tripped on re-export. The mechanism is in flight; treat it as the way to keep visual edits when collaborating with OntoUML-native colleagues.

Inheriting a diagram

Use from "<base>" to extend a base diagram with refinements:

diagram "lease participants" {
    include { Person, Tenant, Landlord, Property, Lease }
}

diagram "lease lifecycle" from "lease participants" {
    include connected_by lifecycle to Lease
        | where metatype == phase

    color by phase {
        Pending: gray,
        Active: green,
        Expired: yellow,
        Terminated: red,
    }
}

"lease lifecycle" carries everything from "lease participants" and adds the lifecycle phases plus a colour scheme. Inheritance composes — you can derive again, and again — though in practice two layers is plenty.

Status note: lifecycle-as-relation projection. Today’s diagram parser does not yet recognise a lifecycle { … } block as a binary-relation source for connected_by, so the connected_by lifecycle form above currently produces OE1102 unknown relation 'lifecycle'. The form shown is the trajectory; the tutorial therefore ships its participants and ontology-overview diagrams and defers the lifecycle projection to a follow-up. If you need a phase view in the meantime, render the lifecycle states by including the phase concepts directly: include { Pending, Active, Expired, Terminated }.

Variations

A handful of common diagram shapes worth remembering.

Module map

The shape of a package’s vocabulary, seen at one glance:

diagram "lease-tutorial overview" {
    include mod lease_tutorial::*
    color by metatype {
        kind: blue,
        role: green,
        relator: orange,
        phase: gray,
    }
}

Neighborhood around a focal concept

What does Lease connect to, two hops out?

diagram "lease neighborhood" {
    include 2 from Lease
}

Filtered facet

Just the rigid sortals — the things with their own permanent identity:

diagram "rigid sortals" {
    include * | where metatype == kind
}

Relator and its mediates

The lease and only the concepts it mediates:

diagram "lease-mediated" {
    include { Lease }
    include connected_by mediates to Lease
}

Edge cases worth knowing

• Diagrams are evaluated, not stored. ox diagram re-renders from source every time. There is no cached SVG that drifts from the model.
• include accumulates; exclude subtracts. Order between an include and a later exclude matters; order between two includes does not.
• Anchor concepts must exist. include 2 from Lease fails to compile if Lease is not in scope.
• Diagram names are visible in ox show. ox show diagrams enumerates every diagram in the package.

Putting it in the running example

Add src/diagrams.ar:

use lease::*

diagram "lease participants" {
    include {
        Property,
        Person,
        Tenant,
        Landlord,
        Lease,
        ResidentialLease,
        CommercialLease,
    }
}

diagram "lease ontology overview" {
    include 2 from Lease
}

(The "lease lifecycle" projection shown earlier in this chapter is on the roadmap — see the Status note above. The tutorial ships the two diagrams that compile cleanly today and will pick up the lifecycle projection when the diagram parser learns to treat lifecycle as a structural source.)

We do not need to re-export diagrams through prelude.ar; they are runtime artifacts, not items consumers use.

Render them:

$ ox diagram --all
   Rendering lease-participants.svg
   Rendering lease-ontology-overview.svg
✓ 2 diagrams.

You now have two SVGs of the model. The first shows the structural skeleton around the lease’s participants; the second gives a two-hop overview around Lease.

Diagrams in the example workspaces

Two example packages ship diagrams in source form:

• argon/examples/pizza/src/diagrams.ar (when present) renders the Manchester pizza ontology’s class lattice with color by metatype to distinguish kind (the abstract Food, Pizza) from subkind (specific pizza varieties) from concrete phase examples. The diagram is the same data as the source — change the supertypes in prelude.ar, re-render, the picture updates.
• argon/examples/ontology-tour/ is itself a “diagram-driven tour”: the package re-exports concepts from pizza, foaf, and wine, and the tour diagram uses include 2 from tour_role (a pub metaxis tour_role for type { event, venue }) to show the cross-package connections.

Both packages render with ox diagram --all from inside the workspace; the SVGs land in diagrams/.

Summary

A diagram block is source code that compiles to a picture. The body uses include/exclude statements with seven source forms and pipe-chain filters; styling and layout are first-class statements; from "<base>" lets diagrams inherit from one another. ox diagram renders to SVG or OntoUML JSON; raster formats (PNG / PDF) are produced by piping the SVG through an external rasterizer. The lease tutorial ships two diagrams today (structural participants + ontology overview), generated from the same model the rest of the book has been building; the lifecycle projection lands when the diagram parser picks up lifecycle-as-source. When the model changes, the diagrams catch up automatically.

Packages and Tooling

The model is built. This last part covers what it takes to ship it: how packages are organized, how dependencies and workspaces work, and what the compiler and LSP do for you in daily editing.

• 4.1 Modules and Packages — mod, use, the prelude pattern, two-tier visibility.
• 4.2 Workspaces and Dependencies — multi-package workspaces, the lockfile, the registry.
• 4.3 The Compiler and LSP — ox check, diagnostic codes, the InfoView panel.

This part is shorter than the others. The ergonomics are largely Cargo-shaped, and most readers will find the surface familiar. We cover what is the same so you can rely on intuition, and what is different so you do not get caught.

Modules and Packages

We have used mod, use, pub, and prelude.ar informally throughout the book. This chapter pulls them together: how a package is laid out, what the visibility tiers actually mean, and how the conventions compose.

Files are modules

Every .ar file under src/ is a module. The file path under src/, with / replaced by ::, is the module’s qualified path:

src/prelude.ar              →  lease_tutorial::prelude
src/party.ar                →  lease_tutorial::party
src/lease.ar                →  lease_tutorial::lease
src/legal/california.ar     →  lease_tutorial::legal::california
src/legal/mod.ar            →  lease_tutorial::legal

Two file-name conventions carry weight:

• prelude.ar is the package’s library entry. It is also aliased as pkg::prelude, so consumers use lease_tutorial::prelude::* to bring in the whole curated surface in one line.
• mod.ar is a directory module’s primary file. When you have src/legal/california.ar and want to add additional content to the legal module itself (rather than legal::california), put it in src/legal/mod.ar. Without mod.ar, src/legal/ is a namespace only — you can use lease_tutorial::legal::california but lease_tutorial::legal itself has no items.

A third file role: root.ar is the project entry — declared in [project] entry, it is the file the toolchain starts module discovery from. Both library packages (which expose a curated surface through prelude.ar) and application packages have a root.ar; the file’s job is to use foo::* every internal submodule so the project’s full module graph is reachable from one anchor.

Inline mod

A module can also be declared inline:

mod legal {
    pub kind Statute { ... }

    mod federal {
        pub kind FederalLaw : Statute { ... }
    }
}

Inline modules nest. The path for FederalLaw is lease_tutorial::legal::federal::FederalLaw. Use inline mod when the sub-module is small enough that splitting into its own file would be overkill. Use a separate file when the sub-module has substantial content.

Variants: _catalog/mod-inline/{minimal,nested-mod,mod-with-pub-items,cross-package,negative-bad-shape}/ — the cross-package/ variant exercises inline-mod items re-exported across a workspace boundary; the nested-mod/ variant demonstrates the qualified-path resolution shown above.

A worked excerpt from _catalog/mod-inline/nested-mod/src/prelude.ar:

use metatypes::*

mod jurisdiction {
    pub kind Statute {
        cite: String,
        text: String,
    }

    mod federal {
        pub kind FederalLaw <: Statute {
            uscode_section: String,
        }
    }

    mod state {
        pub kind StateLaw <: Statute {
            state_code: String,
        }
    }
}

// Qualified-path resolution works across inline mods:
use jurisdiction::federal::FederalLaw
use jurisdiction::state::StateLaw

Inline modules nest as a tree; each level adds one segment to the qualified path. The compiler treats jurisdiction::federal exactly as it would a src/jurisdiction/federal.ar file.

use

Three import shapes:

use ufo::prelude::*                          // glob — every exported item from the path
use ufo::a::endurants::{Object, Person}      // named — specific items
use ufo::a::endurants::{Object as Thing}     // named with rename
use lease                                    // module — the module itself, not its items

The as rename form is the canonical fix when two upstream packages export the same name and you need both in scope. Variants: _catalog/use-rename/{minimal,cross-package-rename,composition-with-re-export,negative-name-collision,idiom}/.

// continuing the import patterns above
use produce::Apple
use tech::{Apple as Computer}   // disambiguates the collision

Choose by intent. Glob imports are convenient for prelude-style modules whose items you almost always want; named imports are explicit about what you depend on; module imports let you write lease::Lease when you want the qualifying segment to appear at the call site.

pub use re-exports

pub use is the canonical pattern for curating a public surface:

// in src/prelude.ar
pub use metatypes::*
pub use party::*
pub use lease::*

Each pub use ::* brings the named module’s exported items into prelude and re-exports them. A consumer who writes use lease_tutorial::prelude::* sees everything, without knowing or caring which internal module declared what.

The pattern decouples your public API from your internal organization. You can split lease.ar into three files later — core.ar, subtypes.ar, lifecycle.ar — and update prelude.ar to re-export from them; no consumer code changes.

Two-tier visibility

There are exactly two visibility levels:

There is no third tier. There is no per-package or per-workspace pub(crate) equivalent. The two-tier discipline is the design choice — when you want a wider surface, re-export through prelude.ar; when you want a narrower one, leave items unmarked.

The default direction matters: an Argon item is file-scoped until you export it. This is the reverse of OOP-conventional public-by-default. Opting into export is explicit.

The direct-dependencies rule

A package can use only items reachable through its own [dependencies], not items reachable transitively through some dependency’s dependencies.

If your package imports cofris and cofris itself imports coex, your package cannot use coex::Foo unless you also list coex in your own [dependencies]. The compiler rejects the transitive import; the rule is not a warning.

The intent is clarity: a package’s manifest is a contract over what it depends on. Transitive use creates accidental coupling — when an upstream removes a dep, downstreams break unexpectedly. The direct-dependencies rule eliminates the surprise.

Putting the conventions together

A typical small package:

my-domain/
├── ox.toml                # package manifest
├── ox.lock                # lockfile (generated)
└── src/
    ├── prelude.ar         # pub use re-exports — the curated surface
    ├── core.ar            # central concept declarations
    ├── rules.ar           # derives + asserts
    ├── queries.ar         # named queries
    ├── computes.ar        # pure functions
    ├── mutations.ar       # state-changing operations
    └── tests.ar           # test blocks

prelude.ar re-exports from each file. Internal modules stay private-by-default; only items they pub slip through prelude’s globs.

A larger package adds directories:

my-large-domain/
├── ox.toml
├── ox.lock
└── src/
    ├── prelude.ar
    ├── party/
    │   ├── mod.ar
    │   ├── person.ar
    │   ├── org.ar
    │   └── relationship.ar
    └── lease/
        ├── mod.ar
        ├── lease.ar
        ├── lifecycle.ar
        └── subtypes.ar

Each directory’s mod.ar re-exports from its siblings. The package’s prelude.ar re-exports from each top-level directory. Consumers use my_large_domain::prelude::* and the whole curated surface lands.

Edge cases worth knowing

• Module names canonicalize. my-package becomes my_package for use paths. Hyphens in package names are friendly for the registry; underscores are the canonical form in code.
• No item renames at the pub use site. You can rename at the use site (use foo::{Bar as Baz}); you cannot at the pub use site. Rename via a wrapper module if you need this.
• Glob re-exports do not propagate beyond direct re-export. If pkg-A’s prelude is pub use pkg-B::* and pkg-B’s prelude is pub use pkg-C::*, then pkg-A’s prelude exposes everything from pkg-B’s prelude including its re-exports of pkg-C. The fixpoint is computed at elaboration; chain re-exports work as expected.
• pub does not mean “registered globally.” Visibility is per-package; the registry is a separate concern.

Summary

Files are modules; mod declares inline modules; use imports; pub opts items into the cross-module surface; pub use re-exports through the prelude. The default visibility is module-internal; the two-tier system is the discipline. The direct-dependencies rule keeps imports honest. The lease tutorial uses these conventions throughout.

Workspaces and Dependencies

A workspace groups several related packages under one root with a shared lockfile and a shared dependency-version pool. Use one when you have packages that need to evolve together — a domain ontology and the test suite that exercises it, for example, or a foundational vocabulary and the domain packages that consume it.

This chapter covers workspaces and the lockfile + registry mechanics that hang off them.

A workspace manifest

The workspace root has its own ox.toml, with a [workspace] section in place of (or alongside) [package]:

[workspace]
members = ["packages/lease-tutorial", "packages/lease-tests"]
resolver = "1"

[workspace.package]
edition = "2025"
license = "CC-BY-4.0"
authors = ["Lease Team <leases@example.com>"]

[workspace.dependencies]
ufo = "0.2.1"
cofris = "0.2.1"

Three sections:

• [workspace] — declares the workspace and lists members. members is a list of relative paths to package directories (glob patterns allowed); each must contain its own ox.toml.
• [workspace.package] — defaults that members can inherit. Common fields: edition, license, authors, repository, description.
• [workspace.dependencies] — version pinnings that members can inherit via <dep>.workspace = true.

Each member’s ox.toml carries both the [project] perspectival-composition layer and the [package] registry layer (see Chapter 1.3 for why both):

[project]
name = "lease-tutorial"
version = "0.1.0"
edition = "2025"
entry = "root.ar"

[schema]
root = "src"

[package]
name = "lease-tutorial"
version = "0.1.0"
edition.workspace = true
license.workspace = true

[dependencies]
ufo.workspace = true
cofris.workspace = true

workspace = true says “use the workspace root’s value.” This keeps version pins consistent across members without the rote of repeating them per file.

How resolution works

When you run ox install at the workspace root:

1. The compiler walks each member’s [dependencies], expanding workspace = true to the workspace root’s pin.
2. It builds the unified dependency graph across all members.
3. External deps that appear in multiple members resolve to the same version — Cargo’s pattern. If two members declare ufo with incompatible version constraints, the resolution fails up front.
4. Workspace members always resolve to the local sibling, never to a registry version. So if lease-tests depends on lease-tutorial and lease-tutorial is a workspace member, lease-tests sees the local source, not a published version.
5. The lockfile lands at the workspace root (ox.lock) and is shared across members.

The lockfile

ox.lock records the exact resolution. It is bivalent: each entry carries two identifiers:

• A content hash — the byte hash of the package’s tarball as published. Reproducible-byte verification at install.
• A Merkle root over construct signatures — a hash over the package’s exported items’ shapes (concept names, field types, rule signatures). Semantic identity: two packages with the same Merkle root expose the same surface, even if their byte hashes differ.

The bivalence matters because Argon packages can be republished with cosmetic changes (a comment fix, a doc-string rewrite) that change the content hash but not the Merkle root. Tooling that wants “did the API change” looks at the Merkle root; tooling that wants “did the artifact change” looks at the content hash.

The lockfile is checked into version control — it is the source of truth for “what versions did this build use.” Re-running ox install against an existing lockfile is deterministic.

Updating dependencies

Two commands:

$ ox update                       # update all packages within their semver constraints
$ ox update <package>             # update a specific package

Both write a new ox.lock. Both report a compatibility diff: which package versions changed, and (via the Merkle root) which API surfaces changed. A surface-changing update is a yellow flag worth reviewing before committing.

The registry

ox publish ships a package to the registry:

$ ox publish
   Building canonical tarball
   Computing content hash + Merkle root
   Authenticating against registry
   Uploading tarball
✓ Published lease-tutorial v0.1.0

The registry’s URL and authentication are configured in ~/.argon/settings.toml; for the Sharpe-internal argon-packages registry, authentication uses GitHub tokens.

ox audit re-verifies the lockfile’s hashes against the cached packages:

$ ox audit
   ✓ All package content hashes match the lockfile.
   ✓ All Merkle roots match the lockfile.

The verification surfaces tampering or registry corruption. Run it in CI if you need a strong guarantee that the build’s inputs have not been substituted.

Local-path dependencies

For dependencies under active development, point at a local directory:

[dependencies]
local-pkg = { path = "../local-pkg" }

The compiler treats local-path deps as workspace members for resolution — they resolve to the source on disk, not a registry version. Use this during development; switch to a version pin before release.

Edge cases worth knowing

• Single-package workspace is fine. A package with [package] only is a workspace of one. You do not need a separate [workspace] table to use a workspace pattern; many small packages live this way.
• Members cannot have [workspace]. A member’s ox.toml carries [project] + [package] (and optionally [dependencies]); the workspace declaration belongs at the root.
• The lockfile lives at the workspace root, not per member. Members do not have their own ox.lock.
• target/ is per-workspace. Build artifacts and test caches share a directory at the workspace root, so members do not duplicate work.
• Git deps are policy-controlled. The Sharpe-internal default disallows git-source dependencies (only registry + path are admitted). The mechanism exists in the manifest grammar for future use.

Putting it in the running example

We have built lease-tutorial as a single-package workspace so far. To grow into a multi-member layout, restructure:

lease-workspace/
├── ox.toml
├── ox.lock
└── packages/
    ├── lease-tutorial/
    │   ├── ox.toml
    │   └── src/
    │       ├── root.ar
    │       ├── prelude.ar
    │       ├── metatypes.ar
    │       └── ...
    └── lease-extras/
        ├── ox.toml
        └── src/
            └── ...

Workspace ox.toml:

[workspace]
members = ["packages/lease-tutorial", "packages/lease-extras"]

[workspace.package]
edition = "2025"
license = "CC-BY-4.0"

[workspace.dependencies]
# none yet

Each member’s ox.toml:

[project]
name = "lease-tutorial"
version = "0.1.0"
edition = "2025"
entry = "root.ar"

[schema]
root = "src"

[package]
name = "lease-tutorial"
version = "0.1.0"
edition.workspace = true
license.workspace = true

[dependencies]

Type-check from the workspace root:

$ ox check
ox lease-tutorial v0.1.0 (./packages/lease-tutorial/ox.toml)
ox lease-extras v0.1.0 (./packages/lease-extras/ox.toml)
check passed

The workspace pattern scales — a real ontology project may have ten or twenty members, with foundational packages (UFO, BFO), domain packages (lease, payments, regulatory), and a test workspace member coordinating them.

Manifest patterns in the catalog

The _catalog/manifest-*/ workspace family exercises each manifest section in isolation:

• _catalog/manifest-catalog/{minimal,multi-version,registry-override,negative-missing-dep,idiom}/ — [catalog] declarations across single- and multi-version slot configurations, plus a registry-override variant that points one dep at a private registry.
• _catalog/manifest-tree-shaking/{minimal,with-conditional-exports,with-feature-flags,cross-package,negative-orphan-import}/ — the [tree-shaking] directives that prune unused items at canonicalization time.
• _catalog/manifest-defeat/{minimal,prioritized-ordering,plugin-strategy,cross-package,negative-missing-strategy}/ — [defeat] section configurations driving the defeasible-rule ordering (foundation: Chapter 5.2).
• _catalog/manifest-modules/{minimal,nested-lattice,cross-package,mixed-world,negative-cycle}/ — the [modules] + [standpoints] machinery covered in Chapter 5.4.

Each variant ships a runnable ox check (and, for negative variants, the expected diagnostic code). Read them as a reference when wiring up a new workspace.

Summary

A workspace groups packages under one root with a shared lockfile and shared version pool. Members inherit defaults from [workspace.package]; they pin versions through [workspace.dependencies]. The lockfile is bivalent — content hash plus Merkle root — so tooling can distinguish byte and semantic identity. The registry handles publish/fetch/audit. Local-path deps support development. Single-package workspaces are fine; the pattern scales when you need it.

The Compiler and LSP

A working day with Argon spends most of its time in two surfaces: the ox CLI in a terminal and the language server in your editor. This chapter is a tour of both — what they do, what flags matter, and what to reach for when something is wrong.

The ox CLI in one page

Eight subcommand families. Most are familiar.

A few habits that pay off:

ox check for the editor loop, ox check --reason before commits. The reasoning step is slower; not every save needs it. Save reasoning for moments where you want the invariants verified.

--explain whenever a query result surprises you. It produces a why-tree showing every rule firing that contributed to the result. Most “why is this happening” questions evaporate after one --explain.

--dry-run for any mutation you have not seen run before. It exercises the preconditions and shows you which events would be emitted, without committing. Combine with --explain to see the reasoning chain.

Diagnostic codes

Argon’s diagnostics use a structured naming scheme. Every diagnostic has a code of the form OE/OW/OI + four digits:

• OE — Errors. The build fails.
• OW — Warnings. The build proceeds; the issue is flagged.
• OI — Info. Hints; nothing is wrong.

A few codes you will see often:

Run ox explain <code> for a longer explanation:

$ ox explain OE0203
   OE0203 — Non-exhaustive match expression.

   A match has no wildcard arm and no guardless arm covering every
   possible subtype of the scrutinee. Every input must reach a body.

   Fix: add a `_ => …` wildcard arm, or add an arm that covers the
   missing subtypes.

The codes are designed to be lookuppable: knowing the code is enough to reach the explanation, the relevant chapter, and (eventually) the relevant decision rationale.

Note: an ox doc command — Argon’s analogue of cargo doc — is on the roadmap. Until it lands, ox explain <code> is the canonical surface for diagnostic-code lookup.

The LSP and editor extension

The language server (ox-lsp) and the VS Code / Cursor extension together provide the editor surface. Open an .ar file in your editor; the extension launches ox-lsp automatically.

Capabilities you will lean on:

• Hover — type, decidability tier, governing decision, links to documentation. Hover over any identifier to see its full classification.
• Inlay hints — inferred types, computed metatype values, implicit consequences on rules. Useful for reading rule code; the implicit => FactDerived(H) shows up as a ghosted suffix.
• Go-to definition / Find references — works across packages.
• Rename — refactor across the workspace.
• Code actions — quick fixes for the common diagnostics. OE0203 (non-exhaustive match) inserts a wildcard arm; OE0101 (unresolved name) suggests an use import; OW0813 (deprecated .ol extension) suggests the .ar rename.
• Diagnostics in real time — OE/OW/OI surfacing as you type; the editor shows them in the gutter and the problems panel.
• Semantic tokens — kind / subkind / role / phase tagged distinctly so syntax highlighting is metatype-aware.
• Palette commands — Argon: Run query, Argon: Run mutation, Argon: Render diagram, Argon: Run tests. The full ox surface, accessible without leaving the editor.

The InfoView panel

A live-updating side panel that surfaces what the compiler knows about the file under the cursor. Open it from the palette (Argon: Open InfoView) and dock it next to your editor.

Three modes:

• Module Dashboard — a bird’s-eye view of the active file: every concept, every rule, every test, with their decidability tiers and meta-property classifications. A good starting place when reading an unfamiliar package.
• Symbol — focuses on whatever symbol your cursor is on. Shows the type, the metatype, the subtype lineage, the rules that mention it, and the tests that exercise it.
• Metatype — shows the meta-property calculus result for a given metatype. Which axes? Which axiom obligations? Which axes are settled, which are open?

You will find yourself in the Module Dashboard when you arrive in a new file, then drill into Symbol when something specific puzzles you, then jump to Metatype when you want to understand why an item classifies the way it does.

Salsa-incremental everything

Behind the scenes, the compiler is built on Salsa — an incremental computation framework. When you change a file, only the things that depend on what changed are recomputed. In practice this means:

• The editor loop is fast. Most ox check invocations through the LSP are sub-100ms.
• ox check --reason reasons over only the rules whose dependencies changed; previously-saturated rules cache.
• The InfoView updates incrementally. Hover after a change shows the new classification.

You do not configure any of this. It is the default mode of the compiler.

When something is wrong

A small triage tree:

The editor reports a diagnostic you do not understand. ox explain <code>. If the explanation does not name the issue, the diagnostic might be missing — file an issue against the project tracker.

ox check is slow. Run with OX_LOG=trace to see what stages take the time. Most slowdowns are reasoning-heavy rules; consider whether @[budget(N)] on the offending rule helps.

A mutation does not fire. --dry-run --explain. The output shows preconditions and event sequencing; one of them will be off.

A query returns wrong results. --explain. The why-tree shows the rules that fired (and the rules that did not fire when you expected them to).

The LSP stops responding. The output channel under Argon in the editor’s output view shows the LSP’s logs. A restart from the palette (Argon: Restart LSP) usually works.

Exercising the CLI in isolation

The _catalog/cli-ox-*/ workspace family ships one minimal workspace per CLI subcommand, so you can run a single command against a focused fixture and watch the output:

• cli-ox-check/{passes,fails-OE0101,fails-OE0203,fails-OE0207,fails-OE0805}/ — pinned regressions for the four most common type-check errors.
• cli-ox-test/{passes,test-with-expect,test-with-assert,multi-frame,negative-no-tests}/ — runs ox test with each test surface in isolation.
• cli-ox-query/{simple,with-explain,with-standpoint,with-as-of-valid,with-fork}/ — exercises each query flag against a small fixture.
• cli-ox-mutate/{simple,with-explain,with-dry-run,with-principal,with-idempotency-key}/ — same for mutations.
• cli-ox-diagram/{single,all,format-ontouml,with-from,negative-bad-source}/ — diagram render paths.

For the LSP surface, _catalog/lsp-{hover,inlay,goto-def,find-refs,rename,code-action}/{minimal,…}/ workspaces ship reproducer source under src/prelude.ar and an EXPECTED.md describing the LSP response the user should see when the file is opened in an ox-lsp-aware editor.

Summary

The CLI is the compile/run surface; the LSP is the editing surface; the InfoView panel is the inspection surface. Diagnostic codes are structured (OE/OW/OI + four digits) and ox explain produces longer explanations. Salsa makes the editor loop incremental. The book’s discipline — ox check in the loop, ox check --reason before commits, --explain whenever something surprises you — produces a fast, debuggable workflow.

A Tooling Cookbook

ox check, ox build, ox install, and ox test are the day-to-day commands the previous chapters lean on. The toolchain has more — for moving models between Argon and OWL/OntoUML, for pulling concepts out of curated catalogs, for inspecting the dependency graph, and for browsing what a package actually exports. This chapter is the reference for those.

Each section is a short recipe: what the command does, what it expects, what it emits, and a 1–2-line example you can run against the lease tutorial (or, where the recipe needs a fixture from outside the tutorial, an explicit fixture path).

ox import — bringing a foreign model in

Argon does not assume your starting point is a green-field package. ox import ingests an OntoUML JSON (or OWL-family) artifact and emits a new Argon package with the corresponding concepts, relations, and rules already wired:

$ ox import model.ontouml.json --into ./my_package

The format is auto-detected from the extension and a content-sniff; pass --from ontouml to force it. The emitted directory contains:

• ox.toml — dual-shape manifest (legacy [project] for ox check / ox test, modern [package] for ox install).
• README.md — generic scaffold describing layout / build / round-trip, with attribution to the source project’s name.
• src/main.ar — root-level declarations plus use ufo::* (and any other foundation packages auto-detected against the registry).
• src/<slug>/mod.ar — one module per OntoUML source package, when the source has nested packages. Each module declares its own classes/relations/generalization-set blocks and use-imports peer modules so cross-module references resolve without fully-qualified paths.

Round-trip identity is preserved via @ontouml-id: doc-comment markers on every emitted declaration and @ontouml-package-id: markers on each mod.ar; no sidecar file is needed.

Two flags are useful in practice:

• --into <DIR> — target directory. Defaults to a sibling directory named after the foreign artifact’s project name (slugified).
• --package-name <NAME> — override the emitted package name when the foreign metadata isn’t what you want. Names must match ^[a-z][a-z0-9_-]*$.

The importer prints a one-line summary at the end (wrote package "X" to <dir> (N files, M warnings)) plus a per-code breakdown of any non-fatal XW084x warnings — unmapped stereotypes, name disambiguations, restrictedTo natures preserved as metadata, generalization-set lattice points lowered to partition / disjoint / complete, and so on. ox explain XW0841 (or any code) gives the full reasoning.

Foundation-package detection

If the OntoUML source references packages that the Argon registry already publishes (UFO, COFRIS, CCF, COEX), ox import resolves matching classes against the registry instead of inlining them. The mapping is built-in (UFO → ufo, COFRIS → cofris, etc.); the bridge introspects the local cache (~/.argon/packages/) for each mapped package, drops local declarations whose names appear in the registry’s public surface, and threads use <pkg>::* plus a [dependencies] entry through the emitted package. Cache-miss is a hard error — run ox install <pkg>@<version> first, or pass --no-registry-detect to opt out and inline everything.

Note: OntoUML JSON is the production-tested format today. OWL-family formats (Turtle, RDF/XML, JSON-LD) ride the same translation pipeline (ox-translate) and will be enabled as the surface stabilizes; until then, convert via OntoUML or hand-translate the parts you care about. The Argon roadmap treats round-trippable OWL as a first-class deliverable.

ox export — emitting a foreign model out

The dual of ox import. Run it inside a project directory to translate the project to a foreign format:

$ ox export --format ontouml -o my-model.ontouml.json

--format defaults to ontouml; --output defaults to <package-name>.ontouml.json next to the manifest.

Alongside the emitted file, ox export writes a .drop.toml sidecar listing constructs that have no analog in the target format — refinement types, defeasible rules, standpoints, the bitemporal axes — so a downstream tool that consumes the export can decide whether the loss is acceptable. A round-trip through ox import → ox export preserves structural identity (class / relation / generalization-set ids on every emitted declaration round-trip via @ontouml-id: markers); whitespace and key order in the emitted JSON may differ from the source, and constructs listed in .drop.toml are dropped by definition.

ox migrate — .ol → .ar

The legacy .ol source extension is being retired (OW0813 warns at every .ol it parses). ox migrate walks the project tree, renames files, edits the manifest, and rewrites .gitignore / .gitattributes patterns:

$ ox migrate --from ol --dry-run     # preview the plan, mutate nothing
$ ox migrate --from ol               # apply the rename
$ ox migrate --from ol --rewrite-docs  # also rewrite `.ol` mentions inside doc comments

The migration is git-aware: inside a git working tree it uses git mv so history follows the rename; outside, it falls back to std::fs::rename. It is atomic — if any step fails, no files are renamed. It is idempotent — running it on an already-migrated tree prints “nothing to migrate” and exits.

Exit codes are stable: 0 success, 1 I/O / manifest / git error, 2 conflict (a .ar file would clobber an existing .ar). CI scripts can branch on the code without parsing the human output.

ox catalog — pinned ontology catalogs

A catalog is a curated collection of ontology entries — pins of UFO, BFO, OntoUML libraries, internal vocabulary packages — that downstream projects can browse and selectively pull from. The pin lives in ox.toml under [catalog]:

[catalog]
url = "git@github.com:sharpe-dev/argon-catalog.git"
sha = "a8f3e2c1b4..."

The pinned SHA is authoritative; every catalog operation reads from it. ox catalog exposes four subcommands:

$ ox catalog list                    # every entry in the catalog
$ ox catalog show <entry>            # full manifest of one entry
$ ox catalog update                  # fetch catalog HEAD; rewrite [catalog].sha
$ ox catalog sources                 # print the pinned URL + SHA

--format human (the default) prints box-drawing tables; --format json emits machine-readable output for scripts.

Exit codes for ox catalog: 0 success, 2 entry not found, 3 version mismatch, 4 dependency cycle, 5 source-parse error, 6 auth failed, 7 lock mismatch.

ox yank — pulling concepts from a catalog into your source

Catalogs store complete ontologies. Often you want one piece — Contract from legal-kb, the Person shape from ufo. ox yank materializes named concepts into src/yanked/:

$ ox yank legal-kb::Contract                          # one concept + its parents
$ ox yank legal-kb::{Contract, Party, Obligation}     # several at once
$ ox yank legal-kb::Contract --no-deps                # just the concept; supply parents yourself
$ ox yank legal-kb::Contract --include-all            # the entry's entire translation
$ ox yank --verify                                    # re-yank everything and diff against disk

The yanked source lands at src/yanked/<entry>_<ConceptName>.ar (or a multi-concept variant). Each yank also appends a row to ox.yank.toml — the yank ledger — recording the catalog URL, SHA, entry, version, source IRIs, timestamp, and a Blake3 content hash. The ledger is what makes yanks reproducible.

--verify re-runs every recorded yank against the pinned SHA and reports any divergence. Run it in CI to catch upstream drift you have not yet pulled.

The default mode includes the transitive parent closure: if you yank Contract, you also get every concept Contract : ParentX : ParentY : ... references along its supertype chain. --no-deps opts out — useful when those parents already live in your project. --include-all opts way in — useful when you want a faithful copy of the upstream entry.

ox tree and ox why — inspecting the dependency graph

Cargo-shaped twin commands for understanding what your project depends on, and why.

$ ox tree
lease-tutorial v0.1.0 (./)

$ ox tree --depth 2
lease-tutorial v0.1.0 (./)
├── ufo v0.2.1
│   └── coex v0.2.1
└── cofris v0.2.1
    └── ccf v0.2.1

ox tree reads ox.lock (no network) and prints a DFS box-tree of transitive dependencies. --depth N truncates; --depth 0 is just the root.

ox why answers “why is this package in my graph?”:

$ ox why coex
coex v0.2.1
  ← ufo v0.2.1
  ← lease-tutorial v0.1.0 (./)

It walks reverse edges from the named package back to the project root, printing every distinct path. If the package is orphaned (lockfile stale; cleaned up by ox install), the output says so.

Both commands are read-only. They will not refresh the lockfile, fetch from the registry, or hit the network.

ox show — schema introspection

ox show prints the schema contents the elaborator built up. Useful for confirming what a package actually exports, or for piping into a script:

$ ox show concepts                                   # every concept the package elaborates
$ ox show concepts --filter rigidity=rigid           # filter by metatype-axis values
$ ox show concepts --filter qname=lease --limit 10   # substring match + cap rows
$ ox show standpoints --lattice                      # standpoint DAG, not the table
$ ox show queries --format json                      # machine-readable

Eight kinds are valid: concepts, relations, properties, standpoints, queries, mutations, computes. --filter KEY=VALUE is repeatable (multiple filters are AND’d; substring match on the column). --sort COL lexicographically sorts ASC by the named column. --limit N truncates after filtering.

--lattice is special: with standpoints, it emits the parent-child DAG instead of the table. With any other kind, it errors.

Both human (default) and json output formats are supported; the JSON shape is stable across patch releases.

ox stats — what’s in the project

A one-shot summary, useful for post-elaboration diffs and for talking-points in design reviews:

$ ox stats
project: lease-tutorial
modules: 11
total lines: 287
concepts: 6
roles: 2
properties: 19
rules: 2
constraints: 2
enums: 0
individuals: 0
queries: 3
computations: 1
standpoints:
  default

Output goes to stderr (so it composes with redirects); the format is intentionally human-shaped — there is no --format json because ox show already covers the machine-readable case.

A typical session

Pulling these together, a realistic UFO-team workflow:

# import the OntoUML model the team has been editing
$ ox import lease-domain.ontouml.json --into ./lease

$ cd lease
$ ox check
$ ox stats
$ ox show concepts --filter rigidity=rigid

# pull supplementary concepts from the curated catalog
$ ox catalog list
$ ox yank ufo::Relator
$ ox yank legal-kb::{Contract, Obligation}
$ ox check

# write a derive rule, run a query, mutate
$ ox query active_leases
$ ox mutate sign_lease --principal alice-001

# emit a snapshot for a downstream tool
$ ox export --format ontouml -o lease-derived.ontouml.json

# inspect the dependency graph before publishing
$ ox tree
$ ox why coex

Every command in that session is read-only against the model, except mutate (which appends to the bitemporal log) and import/yank (which write to the source tree).

Reference workspaces in the catalog

Each ox subcommand in this chapter has a dedicated workspace family in _catalog/:

• _catalog/cli-ox-import/{ontouml-json,ontouml-with-package-name,xw0841,xw0843,negative-missing-file}/ — the ox import recipes plus the two most common XW084x warnings.
• _catalog/cli-ox-export/{ontouml,with-drop-sidecar,format-json,negative-no-package,round-trip-stable}/ — ox export including the round-trip-stability variant exercising structural-identity preservation.
• _catalog/cli-ox-migrate/{dot-ol,dot-ol-dry-run,with-rewrite-docs,already-migrated,exit-code-2}/ — ox migrate across the relevant exit-code branches.
• _catalog/cli-ox-catalog/{list,show,update,sources,negative-missing-sha}/ — ox catalog subcommands.
• _catalog/cli-ox-yank/{single,multi,no-deps,include-all,verify-drift}/ — ox yank recipes plus the CI-friendly --verify mode.
• _catalog/cli-ox-tree/{minimal,depth-2,negative-stale-lock,via-workspace,via-publish-graph}/ and cli-ox-why/{direct,transitive,orphan,negative-not-installed,via-workspace}/.
• _catalog/cli-ox-show/{concepts,relations,standpoints-lattice,with-filter,with-limit}/.
• _catalog/cli-ox-stats/{minimal,multi-module,with-tests,with-mutations,via-workspace}/.

Read these as worked test fixtures — every command in this chapter has a reproducer in version control.

What’s elsewhere

Chapter 4.3 covers ox check, ox build, ox explain, the LSP, and the editor extension — the day-to-day surface. Chapter 4.2 covers ox install, ox update, ox audit, and ox publish — the lockfile and registry side. The commands in this chapter sit alongside both: model-shaped operations that don’t fit cleanly in either bucket but that you’ll use as the project grows.

Beyond — Advanced

This part covers the parts of Argon a working programmer can use without studying the calculus underneath, but that ontology engineers, language designers, and verification-minded readers will want the formal grounding for.

The four chapters in this part:

• 5.1 The Metatype Calculus — the substrate’s calculus in detail: the IS / CAN / NOT three-valued state, the axis dependency DAG, the three-stratum fixpoint, cross-package composition, recognizer dispatch over canonical FOL shapes, and sibling-axiom propagation through user-declared structural rules. The chapter states the principal termination, uniqueness, and composition results.
• 5.2 Defeasibility and Multi-Stratum Reasoning — the @[default] / @[override] / @[defeat] decorators, Governatori three-stratum compilation, NaF stratification, rule-conflict resolution. Builds on the foundational defeasibility-logic work of Reiter, García & Simari, and Governatori et al.
• 5.3 Decidability Tiers — the seven-tier ladder in detail (tier:structural through tier:mlt), tier-cap enforcement at the module level, classification as a structural recursion, @[theorem] for compile-time mechanical verification, unsafe logic { ... } blocks, #[unproven] / #[assumed] test markers.
• 5.4 Standpoints and Bitemporal Reasoning — standpoint declarations and the standpoint lattice, standpoint-discriminated queries, bitemporal axes (valid-time × tx-time) deep-dive, time-travel queries (--as-of-valid, --as-of-tx), forks and structural sharing.

Mathematical preliminaries

A few notational conventions this part uses, drawn from the foundational-ontology and formal-methods literature.

Three-valued state ($K3$). Every (concept, axis, value) triple in the meta-property calculus carries one of three values: $\mathsf{IS}$ (positively held), $\mathsf{NOT}$ (positively excluded), $\mathsf{CAN}$ (genuinely indeterminate). The information ordering is $\mathsf{CAN}⊑\mathsf{IS}$ and $\mathsf{CAN}⊑\mathsf{NOT}$, with $\mathsf{IS}$ and $\mathsf{NOT}$ incomparable. This is canonical $K3$ — Kleene’s strong three-valued logic (Kleene, Introduction to Metamathematics, 1952), realized as the consistent fragment of the four-valued $\mathsf{FDE}$ bilattice (Belnap 1977 / Dunn 1976) under the Pietz-Rivieccio “Exactly True” designation. The $\mathsf{CAN}$ / $\mathsf{IS}$ / $\mathsf{NOT}$ naming follows the engine’s internal vocabulary.

Stratified evaluation. A stratum is an evaluation phase that reads only from earlier strata’s completed states. Stratified semantics for negation goes back to Apt, Blair & Walker (Towards a Theory of Declarative Knowledge, 1988); Argon uses stratification both for negation-as-failure inside rule bodies and for the three-stratum meta-property calculus.

Decidability tiers. Each rule lands at a tier $t\in \{0,1,2,3,4,5,6\}$ classified by the compiler. Tiers 0–3 are executable (the saturator produces results); tiers 4–6 are syntax-only (parsed and type-checked but not evaluated by today’s runtime). The classification is a structural recursion over the rule body, taking the maximum of intrinsic-tier per atom.

Bitemporal axes. Every fact is timestamped with a valid-time $t_v$ (when the fact is true in the world) and a transaction-time $t_x$ (when the system learned it). A query against the log filters by both. Retraction is a new event with later $t_x$; the original fact is preserved. The model follows Snodgrass & Ahn (Temporal Databases, 1986) and Jensen, Soo & Snodgrass (Unifying temporal data models via a conceptual model, 1994).

Standpoints. A standpoint is a named position in a partial-order lattice; facts and rules are tagged with their standpoint and queries can be discriminated to a particular vantage. Standpoints discriminate, they do not partition — a fact in default is also visible in any descendant unless explicitly retracted.

Principal results

Each chapter in this part states the math the implementation rides on. Three results carry the substrate:

• Meta-property fixpoint — termination and uniqueness of the stratified fixpoint over an acyclic axis-dependency graph; package composition (disjoint non-interference, shared-axis confluence); $\mathsf{CAN}$ at completion is genuine indeterminacy. Covered in Chapter 5.1.
• Flow-typing soundness — occurrence-typing narrowing persists across body atoms and survives monotone rule composition; CWA→OWA narrowing preservation. Covered in Chapter 5.1’s stratification discussion and applied throughout Chapter 2.
• Refinement-fragment decidability — the refinement type-checking fragment is decidable in PTIME, with staging correctness for the multi-package case. Covered in Chapter 2.6 and Chapter 5.3.

Reading order

If you have read Parts 1–4, the chapters below can be read in any order. A natural sequence:

1. Ch5.1 Metatypes — explains the calculus that powers Tier 0 reasoning across the language.
2. Ch5.3 Decidability Tiers — shows the ladder the compiler classifies every rule against.
3. Ch5.2 Defeasibility — the layer that runs on top of the tier ladder, organising rule conflicts.
4. Ch5.4 Standpoints + Bitemporal — the runtime story, orthogonal to (and composing with) all of the above.

Or skip directly to the chapter that answers a specific question. Each is self-contained.

The Metatype Calculus

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

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

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

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

The four foundational axes (UFO as worked example)

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

Rigidity

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

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

Sortality

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

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

Identity-provision

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

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

Provides-mediation

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

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

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

The axis dependency DAG

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

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

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

Two constraints follow:

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

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

The three strata

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

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

Stratum 0 — IS propagation

Stratum 0 is a set of monotone rules of the form

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

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

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

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

Stratum 1 — NaF (negation-as-failure)

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

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

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

Stratum 2 — constraint checks

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

The three-valued state

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

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

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

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

Sibling-axiom propagation and structural rules

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

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

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

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

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

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

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

Recognizer dispatch — fast-path for canonical shapes

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

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

The ten shapes:

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

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

A user decorator can pre-tag its expected shape:

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

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

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

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

Cross-package metatype composition

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

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

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

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

Three composition results matter here:

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

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

Bidirectional reasoning

The engine exposes three operations:

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

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

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

Termination, uniqueness, and the indeterminacy guarantee

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

Four results carry the calculus.

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

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

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

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

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

When a metatype declaration goes wrong

Six classes of error worth knowing:

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

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

A worked verification

Take the lease tutorial’s metatypes:

use ufo::prelude::*;

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

The engine, given this input:

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

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

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

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

Why this matters

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

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

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

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

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

What’s next

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

Defeasibility and Multi-Stratum Reasoning

A defeasible rule is one that can be overridden. The classical example, going back to Reiter’s A Logic for Default Reasoning (1980): birds fly; penguins are birds; penguins do not fly. The rule “birds fly” is not wrong — it is defeasible, defeated by the more-specific rule “penguins do not fly.” A reasoning system that cannot represent this kind of layered exception either over-asserts or under-asserts, and either failure mode shows up as soon as a real-world domain enters the picture.

Argon supports defeasibility natively, following Governatori et al.’s formalization in Defeasible Logic: Agency, Intention and Obligation (DEON 2004) and the broader Defeasible Logic Programming tradition (García & Simari, Defeasible logic programming, TPLP 2004). The three layers — strict rules, defeasible rules with a superiority relation, and the resulting stratified evaluation — give unambiguous semantics independent of evaluation order.

This chapter covers the three decorators that mark and order defeasible rules, the Governatori three-stratum compilation that gives them their semantics, and the diagnostics that surface when the defeasibility graph contradicts itself.

The mechanism lives in oxc::stratify. Defeasibility composes with the three-engine derive pipeline (Chapter 2.4), the project-level [defeat] configuration (later in this chapter), and the multi-head disjunction stratification covered below.

Strict versus defeasible

A rule with no decorator is strict: when the body fires, the head holds, full stop. No other rule can defeat it.

pub derive ResidentialLeaseHasOneTenant(l: ResidentialLease) :-
    l: ResidentialLease,
    count(t for t in l.tenant) == 1

A rule marked @[default] is defeasible: it fires when nothing more specific overrides it.

@[default]
pub derive standard_security_deposit_applies(l: Lease) :-
    l: Lease

The default says: every lease falls under the standard security-deposit regime. Unless something more specific says otherwise. (The actual deposit value is computed by a compute keyed off whichever regime the lease classifies under.)

@[override(rule)] — pointing at a specific defeater

Mark a rule as overriding another by name:

@[override(standard_security_deposit_applies)]
pub derive rent_controlled_security_deposit_applies(l: Lease) :-
    l: Lease,
    rent_controlled(l)

When the body of rent_controlled_security_deposit_applies fires, it defeats standard_security_deposit_applies for that lease. The engine treats the two rules as in a superiority relation: the override is more specific.

@[override(rule)] is the most-explicit form of defeasibility. The override target is named explicitly; the dependency is local; the resolver can build the superiority graph statically at compile time.

@[defeat(rule)] — defeasibility as an effect of the body

A different shape: a rule whose body asserts the defeat of another rule, without contributing a positive head of its own.

@[defeat(standard_security_deposit_applies)]
pub derive prohibit_standard_deposit_regime(l: Lease) :-
    l: Lease,
    deposit_prohibited_jurisdiction(l)

@[defeat(rule)] is for the cases where the body’s effect is “this other rule does not apply” rather than a positive consequence. The body fires; the named rule is defeated for the bindings that satisfied the body. The defeat is the rule’s contribution to reasoning.

A companion decorator @[chain(rule)] declares that a defeasible rule chains through another — the chain link’s body assumes the chained rule’s head and the resulting derivation carries both rules’ provenance into the why-tree. This is the canonical pattern for layered regulatory reasoning where one rule’s conclusion is another rule’s premise:

@[default]
pub derive eligible_for_subsidy(t: Tenant) :-
    t: Tenant,
    t.household_income < poverty_line

@[chain(eligible_for_subsidy)]
pub derive senior_subsidy_amount(t: Tenant) -> Money :-
    t: Tenant,
    t.age >= 65
    => t.household_income * 0.4

Variants: _catalog/decorator-chain/{minimal,composition-with-defeasibility,multi-chain-link,idiom}/ and _catalog/decorator-defeat/{minimal,composition-with-default,negative-bad-args}/. The manifest-defeat/cross-package/ workspace shows the project-level [defeat] order strategy resolving conflicts across packages.

Governatori three-stratum compilation

The semantics of a defeasible-rule program is given by a three-stratum compilation, after Governatori (and the broader defeasible-logic-programming tradition).

Formally, let $\mathcal{R}={\mathcal{R}}_s\cup {\mathcal{R}}_d$ partition the rule set into strict rules ${\mathcal{R}}_s$ and defeasible rules ${\mathcal{R}}_d$, and let $>\subseteq {\mathcal{R}}_d\times {\mathcal{R}}_d$ be the superiority relation induced by the @[override] and @[defeat] annotations plus the configured [defeat] order strategies. The semantics of $(\mathcal{R},>)$ is the fixed-point of the three strata:

1. Stratum 1 — strict closure. ${\Delta }_1=T_{{\mathcal{R}}_s}^{\omega }(\varnothing )$, where $T_{{\mathcal{R}}_s}$ is the immediate-consequence operator over strict rules. These derivations are unconditional. Strict rules cannot be defeated; if a strict rule and a defeasible rule disagree on the same head, the strict rule wins by construction.
2. Stratum 2 — defeasible closure with superiority resolution. Starting from ${\Delta }_1$, add a defeasible derivation $r\in {\mathcal{R}}_d$ producing $\varphi$ from facts in ${\Delta }_1$ if and only if no rule $r^{\prime }>r$ produces $\neg \varphi$ from the same facts. Repeat to fixpoint ${\Delta }_2$. When two rules at incomparable priority disagree, the conflict is ambiguous (OE0401).
3. Stratum 3 — multi-head disjunction stratification. Multiple same-named defeasible rules form a Datalog disjunction: a fact holds if any of the rules fires. The disjunction’s contribution to the negation-as-failure layer is resolved by stratification, giving the final closure ${\Delta }_3$.

Each stratum reads from the completed state of the previous one. Stratum 2 cannot read its own in-progress state; that is what makes the compilation deterministic and the result independent of evaluation order.

The output is a triple $({\Delta }_1,{\Delta }_2,{\Delta }_3)$ together with, for each defeasible-rule application in ${\Delta }_2$, a record of which superiority-graph edge made the application win. Why-provenance traces back through the graph; a regulator can ask “which override produced this result?” and get a precise answer.

The superiority graph

The set of @[override] and @[defeat] annotations across a project induces a superiority graph: an edge A → B means rule A is more specific than rule B. The compiler:

• builds the graph from all annotations, across modules;
• checks for cycles (OE0403) — a cycle is an unrecoverable inconsistency in the modeller’s defeat-ordering;
• topologically sorts the graph to give Stratum 2 its priority order.

Cycle detection is binding. A cycle means two rules each claim to defeat the other; there is no consistent way to compute a fixed-point. The build fails.

OE0402 (“unreachable defeater”) fires when an @[override] or @[defeat] references a rule whose body could never fire under any interpretation — a static check that catches the kind of dead-code defeat-annotation that would otherwise pass silently.

Project-level [defeat] strategies

Some defeasibility orderings are systemic — not per-rule but per-project. Lex specialis (more specific wins), lex posterior (later wins), and lex superior (higher-status source wins) are the three classical orderings. Argon admits them as ordered project-level fallbacks:

[defeat]
order = ["explicit", "lex-specialis", "lex-posterior", "lex-superior"]

explicit is the per-rule annotations (@[override], @[defeat]). When two rules contradict and neither is explicitly annotated relative to the other, the engine consults the next strategy: lex specialis (the rule with the more-specific body wins). Then lex posterior (the rule defined later in source order wins). Then lex superior (the rule from the higher-priority package wins).

The four known strategies are explicit, lex-specialis, lex-posterior, lex-superior. Unknown strategies are OE1002. Empty order is allowed — it means “fall through to ambiguity diagnostics if no @[override] resolves.”

Mixed-strength rules and OE0207

A rule cannot be strict in some applications and defeasible in others. The compiler enforces this with OE0207 (“mixed-strength rules on same head”): if two rules with the same head differ in strength (one strict, one @[default]), the build fails. The fix is to make both defeasible or both strict — the modeller’s intent must be uniform.

This is a less-obvious constraint than it first appears. It catches the typical mistake of “I added an override but forgot to mark the original as defeasible,” which would otherwise silently produce contradictions.

Stratification and circular negation

NaF (negation as failure) interacts with defeasibility because both depend on a stratified evaluation order. A circular dependency through a NaF edge is OE0501 (“circular negation”); a program that cannot be stratified at all is OE0502 (“unstratifiable program”). Both are static checks; both fail the build.

The standard pattern that triggers OE0501:

pub derive A(x) :- not B(x)        // can A even be evaluated?
pub derive B(x) :- not A(x)        // ... we'd need to know B

The two rules cycle through a NaF edge. The compiler refuses to compile until the modeller breaks the cycle, typically by inserting a strict rule that grounds one of the predicates.

Multi-head disjunction

Multiple same-named @[default] derive rules form a disjunction: a fact holds if any of the rules fires. The pattern is canonical for genuine disjunctive reasoning where the head is the same predicate but the supporting bodies are independent:

@[default]
pub derive eligible_for_review(l: Lease) :-
    l: Lease,
    l.monthly_rent >= rent_review_threshold

@[default]
pub derive eligible_for_review(l: Lease) :-
    l: Lease,
    rent_controlled(l)

@[default]
pub derive eligible_for_review(l: Lease) :-
    l: Lease,
    l.tenant.is_senior

A lease is eligible for review if any one of the three conditions holds; the why-provenance tags whichever rule fired so a consumer can ask “which branch matched?” and get a precise answer. Mixing strict and defeasible rules under the same head is OE0207 for the same reason single-head mixed-strength is rejected.

Refinement-type interaction

The refinement-type fragment (Chapter 2.6) interacts with defeasibility through the three-valued semantics. A refinement-type predicate where { ... } is decided per $K3$ (Kleene’s strong three-valued logic) with the Pietz-Rivieccio “Exactly True” designation: only IS admits membership, CAN does not. When a defeasible rule conditions on the refinement-type narrowing, the rule fires only if the narrowing is IS — the narrowing itself can be defeated by an override rule that asserts the converse. The corner cases are rare; the semantics is well-defined when they do come up.

Worked example — regulatory-regime classification

The lease tutorial does not yet exercise defeasibility, but the pattern is straightforward to add. Imagine rules.ar extended with:

@[default]
pub derive lease_governance_standard(l: Lease) :-
    l: Lease

@[override(lease_governance_standard)]
pub derive lease_governance_rent_controlled(l: Lease) :-
    l: Lease,
    rent_controlled(l)

@[override(lease_governance_rent_controlled)]
pub derive lease_governance_senior_rent_controlled(l: Lease) :-
    l: Lease,
    rent_controlled(l),
    l.tenant.is_senior

Three classification rules, each more specific than the last. The superiority graph is a chain: senior_rent_controlled → rent_controlled → standard. For a senior tenant in a rent-controlled lease, all three bodies fire; the engine applies them in topological order; lease_governance_senior_rent_controlled wins; the lease classifies under the senior-rent-controlled regime.

For a non-senior tenant in a rent-controlled lease, only the first two bodies fire; lease_governance_rent_controlled wins; the lease classifies under the rent-controlled regime.

For a market-rate lease, only the first body fires; lease_governance_standard wins; the lease classifies under the standard regime.

A separate compute keyed off the regime predicate produces the actual security-deposit cap, monthly-rent ceiling, or whatever the regime determines. Defeasibility classifies; the compute calculates. The why-provenance for each classification tags which override won, giving the regulator a precise audit trail.

Diagnostics worth knowing

ox explain <code> prints the long-form explanation and the canonical fix.

Why a stratified semantics

A naïve “first-rule-wins” or “most-recent-rule-wins” approach to defeasibility is brittle: rule order in source becomes load-bearing, refactors silently change behavior, and the result depends on evaluation order. The Governatori three-stratum compilation gives unambiguous semantics that is independent of evaluation order — multiple paths through the strata produce the same result, by construction.

This is what makes the defeasibility layer composable. A package can ship rules with their own @[override] annotations; a downstream package can add more rules, more annotations, even override rules from the upstream package; the resulting superiority graph is the union; the semantics stays well-defined; and the compiler tells you when the union has a cycle or an ambiguity.

What’s next

Chapter 5.3 covers the tier ladder; defeasibility’s stratification interacts with tier classification (NaF can lift a rule up the ladder). Chapter 5.4 covers standpoints; defeasibility orderings differ between standpoints, and the same rule pair can have different superiority outcomes depending on which standpoint the query runs against. Chapter 5.1 covers the meta-property calculus that powers Tier-0 reasoning — a substrate the defeasibility layer reads but does not modify.

Decidability Tiers

A rule that the reasoner cannot evaluate is a rule the reasoner cannot use. This is not a complaint — it is a design fact. Description Logic, Datalog, and full first-order logic occupy different points on the tractability/expressiveness curve, and a language that wants to run its rules has to make those points visible to the programmer.

Argon does that with a seven-tier decidability ladder. Every rule is automatically classified at elaboration time. Tiers from tier:structural through tier:recursive execute today. tier:fol admits semi-decidable rules through the unsafe logic { … } escape hatch. tier:modal and tier:mlt are reserved for std::kripke-driven modal reasoning and multi-level types respectively.

This chapter explains the ladder, shows one example per tier, and walks through the three related mechanisms that hang off it: #dec(<tier>) directives that scope ambient ceilings at module / block / declaration granularity, unsafe logic { … } blocks for the FOL escape hatch, and the recognizer table that lets carefully-shaped FOL bodies pass under stricter ceilings via shape-driven tier reduction.

The ladder

The ladder stands on its own — each tier corresponds to a real engine and a real cost model, grounded in the complexity classes those engines target. tier:structural is the polynomial concept-graph saturation regime described in Baader et al., Pushing the EL Envelope (IJCAI 2005); tier:recursive is stratified Datalog as formalized in Abiteboul, Hull & Vianu, Foundations of Databases (1995); tier:fol is unrestricted first-order logic; the four remaining tiers sit between, each with its own engine and acceptance criterion. The names describe what each tier admits and what it costs; they do not align to any other language’s expressivity slices.

Classification is automatic. There is no tier: annotation on a rule; the elaborator walks the body, assigns each atom and operator an intrinsic tier, and takes the maximum:

$$tier(body)=\underset{a\in atoms(body)}{\max }tier(a)$$

where the per-atom function $tier:Atom\to \{0,1,2,3,4,5,6\}$ is a structural recursion:

$$\begin{array}{rcl}tier(\mathsf{MetaPropertyLookup}(c,a,v))& =& 0\\ tier(cspecializes{c}^{\prime })& =& 1\\ tier(count(\dots )\bowtie n)& =& 2\\ tier(e_1\bowtie e_2)& =& 3\text{where }\bowtie \in \{<,\le ,=,\ne ,\ge ,>\}\\ tier(e_{1}op{e}_2)& =& 4\text{where }op\in Allen\\ tier(\exists x:T.\varphi )& =& \{\begin{array}{ll}5& \text{if scope-bounded by }@[scope]\\ 6& \text{otherwise}\end{array}\\ tier(\forall x:T.\varphi )& =& 6\\ tier(op(e_1,\dots ,e_k))& =& \max (tier(op),tier(e_1),\dots ,tier(e_k))\end{array}$$

The recursion is implemented in argon/oxc/src/meta/classify.rs and surfaces through OI0804 at elaboration time. Aggregates compose by max; the binding-form forall is the single construct that can force a rule to tier:fol unilaterally — unless the recognizer (see below) matches the body against a known shape and reduces the effective tier.

The classification surfaces through OI0804 — an info-level diagnostic emitted at elaboration time so you can see what tier each derive rule landed at:

$ ox check
OI0804

  > [OI0804] derive rule `ActiveLease` classified at tier:recursive
    ,-[11:1]
 11 | ,-> pub derive ActiveLease(l: Lease) :-
 12 | |       l: Lease,
 13 | |       l.start_date <= today(),
 14 | |       l.end_date > today()
 15 | |->
    : `---- tier:recursive
    `----
  help: for more information, try `ox explain OI0804`

ox explain OI0804 prints the long-form explanation: which sub-expressions contributed which intrinsic tiers, and how they composed.

One example per tier

The seven tiers, illustrated against the running lease ontology and standard-shape predicates over it.

Tier 0 — MetaPropertyOnly

Pure meta-property lookups. No traversal of the structural graph; no value comparisons; no arithmetic.

pub derive RigidConcept(c: ⊤) :-
    A.rigidity(c) == rigid

The reasoner answers this from the meta-property calculus’s IS-state (Stratum 0). Polynomial in the number of axes × the number of concepts. The classifier rejects nothing here.

Tier 1 — HierarchyTraversal

Subtype reasoning, transitive closure, simple sibling-axiom checks.

pub derive AnyResidentialSibling(l: Lease) :-
    l: Lease,
    l specializes ResidentialLease

The nous saturator handles tier-1 rules by traversing the type hierarchy.

Tier 2 — CountingAndPaths

Bounded-length path queries through the structural graph.

pub derive HasGuarantorWithin2Hops(l: Lease) :-
    l: Lease,
    l connected_by mediates within 2 to Guarantor

within N caps the traversal depth; the connected_by operator becomes a bounded path expression.

Tier 3 — ValuePredicates

Comparisons over value-typed fields plus integer arithmetic. The QF-LIA fragment.

pub derive ActiveLease(l: Lease) :-
    l: Lease,
    l.start_date <= today(),
    l.end_date > today()

Tier 3 is the highest of the executable tiers — the running edge of what the saturator + value-predicate engine produces results for today. Most real domain rules sit at tier 3. OI0804 for any rule in the lease tutorial reports tier 3 because of the date comparisons.

Tier 4 — Temporal

Allen-interval operators (before, after, meets, overlaps, during, contains, …) — DatalogMTL territory.

pub derive OverlapsActive(a: Lease, b: Lease) :-
    a: Lease, b: Lease,
    a overlaps b,
    a end_date > today()

The Allen operator forces tier 4. Today the elaborator parses, type-checks, and emits the rule into the IR; the saturator does not produce derivations from tier-4 rules until the DatalogMTL execution path ships. ox check reports OI0804: Tier 4 (temporal) and the rule’s body becomes design intent rather than a live derivation.

Tier 5 — BoundedFOL

First-order rules with bounded-cardinality scope annotations. Classical Kodkod territory.

@[scope(leases: 100)]
pub derive AtLeastOneLeaseHasNoTenant() :-
    exists l: Lease where not exists t: Tenant where l.tenant == t

The exists introduces a true binding-form quantifier; the @[scope] annotation tells the classifier it is bounded. Tier 5 is syntax-only today; without @[scope] the same rule is tier 6.

Tier 6 — FullFOL

Unbounded forall / exists, full first-order logic. Semi-decidable.

unsafe logic {
    pub derive transitivity_of_specialization(x: ⊤, y: ⊤, z: ⊤) :-
        forall x, y, z: ⊤ where x specializes y, y specializes z
        => x specializes z
}

The forall binding-form forces tier 6. A tier-6 rule outside an unsafe logic { … } block is a hard error — OE0809: Tier 6 rule outside unsafe logic block. Inside the block, the rule parses, elaborates, and lands in the IR with OI0808 (“unsafe logic rule gated”) — the rule is a property of the source, not of any saturation result.

The decision to gate tier 6 behind unsafe logic is deliberate: full FOL is an escape hatch for rare cases (theorem-shaped invariants you intend to mechanically verify but not execute). It is not a programming idiom.

#dec(<tier>) — capping an effective fragment by scope

A mature ontology project usually wants to be conservative: “we only commit to tier:recursive-or-below reasoning in this module; flag anything that creeps higher.” The #dec(<tier>) directive declares an ambient ceiling at module, block, or declaration scope:

#dec(tier:recursive)

mod core_rules {
    pub derive ActiveLease(l: Lease) :-
        l: Lease,
        l.start_date <= today(),
        l.end_date > today()

    #dec(tier:closure)
    pub derive Ancestor(p: Person, c: Person) :-
        p parent_of c
        => p ancestor_of c
}

unsafe logic {
    pub derive transitivity_of_specialization(x: ⊤, y: ⊤, z: ⊤) :-
        forall x, y, z: ⊤ where x specializes y, y specializes z
        => x specializes z
}

The directive scopes:

• Module head. #dec(<tier>) at the top of a .ar file binds the ambient ceiling for every item in the file.
• Per-block. #dec(<tier>) { … } binds an ambient inside a block — handy for a research subsection that uses one stricter-or-looser tier than its surroundings.
• Per-declaration. #dec(<tier>) immediately preceding a pub derive (or any other tier-classified declaration) overrides the enclosing ambient for that declaration only.
• unsafe logic { … }. Injects a whole-block tier:fol ambient, the FOL escape hatch. Every item nested inside — derive rules, nested concept declarations, anything else admitted in block scope — inherits FOL regardless of any outer ceiling.

Stricter wins: the effective ceiling at any point is min over the entire ambient stack. A #dec(tier:closure) declaration nested inside a #dec(tier:recursive) module compares its rules against the stricter closure ceiling, not the looser ambient.

A rule whose effective syntactic tier exceeds the stack’s ceiling fires OE0604 TierViolation. The check runs at elaboration, before any reasoning, so the build fails with a precise pointer at the offending rule.

There is no [reasoning] max_tier manifest field. Per-scope tier concerns live in source directives; package-wide concerns (no-std, edition, dependencies) live in the manifest. The two never mix.

Recognized-shape tier reduction

A rule’s effective tier is min(syntactic_tier, recognized_tier). Carefully-shaped FOL bodies pass under stricter ceilings:

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

#dec(tier:closure)
@[transitive]
pub rel parent_of(p: Person, c: Person)

The decorator’s body is syntactically tier:fol (forall is a binding-form quantifier). But the recognizer matches the body against RecognizedShapeKind::Transitive { rel } — the canonical FOL shape for transitivity — and the effective tier collapses to tier:closure. The parent_of rule passes the #dec(tier:closure) ceiling. The reasoner takes the transitive-closure fast-path.

The recognizer admits ten canonical shapes (Transitive, Symmetric, Asymmetric, Reflexive, Irreflexive, Functional, InverseFunctional, QualifiedCardinality, DisjointClasses, CoveringClasses). Six normalization passes (alpha-rename, flatten-associative, push-negations-inward, implications-to-disjunctions, canonicalize-equality, sort-conjuncts) ensure that semantically-equivalent bodies with different syntactic surfaces match the same canonical form. Bodies that don’t match any shape — the common case for hand-written forall — fall through to generic FOL handling and require unsafe logic { … } to lift the FOL ceiling.