Tier Selection

This page answers: which decidability tier should I use for this rule, and when do I need to escalate?

Argon’s decidability ladder is graduated by evaluation cost. Tiers are independent of OWL profiles (RFD-0004).

The seven tiers

Tier	Admits	Cost profile	Default?
`tier:structural`	Meta-property lookup, simple subsumption, atomic constraints	Polynomial; fast	Yes
`tier:closure`	Transitive closure, counting, classification	Polynomial; saturation cost	No
`tier:expressive`	GNFO (Guarded Negation First-Order)	Polynomial in expressive class; richer than closure	No
`tier:recursive`	Quantifier-free Linear Integer Arithmetic + recursion	Polynomial in QF-LIA; recursion adds bounded cost	No
`tier:fol`	DatalogMTL, bounded FOL via Kodkod (`@[scope]`); `unsafe logic { }` admits unbounded FOL	Decidable per-bound; unbounded FOL is undecidable	No (escape hatch)
`tier:modal`	Modal operators (`box()`, `diamond()`); modal axioms	Decidable for bounded modal logic	No
`tier:mlt`	Multi-Level Theory: a metatype’s instances are themselves types	Reserved for foundational-ontology bootstrapping	No (exotic)

Picking a tier

Is the rule structural — references only ancestors, fields, atomic predicates,
no recursion, no aggregates, no negation?
  → tier:structural (default; no #dec needed)

Need transitive closure (e.g., ancestor-of), counting, or saturation-driven classification?
  → tier:closure

Need negation, disjunction, complex universal/existential quantification (still bounded)?
  → tier:expressive

Need recursion that can't be expressed via transitive closure?
  → tier:recursive

Need full FOL with bounded scopes (Kodkod-class)?
  → #dec(tier:fol) + @[scope] annotations

Need modal reasoning (necessity, possibility)?
  → #dec(tier:modal)

Need full unbounded FOL (proof-theoretic, undecidable)?
  → unsafe logic { ... } block (which carries tier:fol)

Need multi-level types?
  → #dec(tier:mlt) — exotic; usually only foundational-ontology authoring

How to declare a tier

// Module-scope: caps every declaration in this module
#dec(tier:closure)

// Declaration-scope: caps a single declaration
#dec(tier:expressive)
pub derive complex_classification(X) :- ...

// Block-scope: caps a single block
#dec(tier:recursive) {
  pub derive ancestral(P, A) :- parent(P, A)
  pub derive ancestral(P, A) :- parent(P, M), ancestral(M, A)
}

// FOL escape hatch
unsafe logic {
  // full FOL admitted; carries tier:fol
}

The compiler classifies each expression’s natural tier and rejects expressions that exceed the surrounding #dec annotation with OE0604 TierViolation. Recognized shapes (transitive, symmetric, …) inhabit the recognized tier regardless of their syntactic appearance.

Recognized shapes inhabit the recognized tier

A @[transitive] decorator on a relation lowers to a recognized shape with a known polynomial-time fast-path. The expression inhabits the recognized tier (often closure-equivalent) even though its naive interpretation might lift it higher. This is structural and intentional (RFD-0004).

The 10 canonical recognized shapes:

Transitive       Symmetric     Asymmetric    Reflexive    Irreflexive
Functional       InverseFunctional
QualifiedCardinality
DisjointClasses  CoveringClasses

If an expression matches one of these (after the recognizer’s 6 normalization passes), the reasoner dispatches to a fast-path; tier classification reflects that.

Collection operations and per-context admission

The collection substrate (ch02-08) ships each operation with an explicit tier. The tier interacts with the surrounding evaluation context: different bodies admit different operation sets.

Context	`closure`-tier ops	`expressive`-tier ops (`map`, `filter`, `Optional::map`)	`recursive`-tier ops (`fold`)
`pub compute` body	yes	yes	yes
`pub mutation` `do { }`	yes	yes	yes
`pub derive` body	yes	reject (`OE2408`)	reject (`OE2408`)
`query` body	yes	reject (`OE2408`)	reject (`OE2408`)
Refinement `where { }`	reject (`OE2408`)	reject	reject
`test` block	yes	yes	yes

Closure-tier ops (size, contains, at, append, slice, union, get, Some, None, is_some, is_none, unwrap_or, Range::new, Range::contains) are admitted freely in rule bodies and queries. Expressive- and recursive-tier ops (map, filter, fold) belong inside a pub compute body; call the compute from the rule.

Refinement bodies admit the metatype calculus only; every collection op is out of fragment there.

See ch02-08 — tier dispatch matrix, RFD-0039.

Common tier mistakes

Reaching for tier:fol when tier:expressive would do. Most “I need negation” cases fit GNFO. Try the lower tier first.
Recursion in tier:closure. tier:closure admits transitive closure but not arbitrary recursion. If your rule recurses through aggregates or arithmetic, it’s at least tier:recursive.
unsafe logic without an obvious need. The escape hatch is for genuinely unbounded FOL. Most “I need full FOL” turns out to be “I need bounded FOL” and tier:fol with @[scope] annotations is enough.

The Argon Programming Language