Lex specialis: the specific rule defeats the general

Area: Defeasible reasoning Teaches: resolving a same-strength norm conflict with #[defeats] — lex specialis, where a specific rule beats the general one it names, per-tuple, by an explicit checked edge rather than a pair of magic priority integers. Prerequisites: strict vs default vs defeater. Run: ox build examples/legal_priority_v0 && ox run-scenario examples/legal_priority_v0

Two norms conclude about the same head at the same strength: imported goods owe import duty (general); medical imports are exempt (specific). Without a superiority mechanism this conflict is unresolvable — both fire on a medical import and you get a contradiction. Lex specialis is the legal rule that the specific norm wins; Argon expresses it as one rule defeating another’s labeled clause.

What to read in statute.ar

The general norm is an overridable, labeled default. #[label(general)] is the handle a more specific rule will name:

#[default]
#[label(general)]
pub derive must_pay_duty(g) :- Imported(g);

The specific norm names the general clause and defeats it. The #[defeats] target is qualified by the label — must_pay_duty.general(g) — and resolves per-tuple against the bound g. It defeats the general duty clause for exactly the goods exempt derives, and no others:

#[defeats(must_pay_duty.general(g))]
pub derive exempt(g) :- MedicalGood(g);

This is the whole lex-specialis idea in two lines: the more specific rule (medical imports) defeats the more general one (imported goods), tuple by tuple. A non-medical import is untouched by the defeat and keeps owing duty.

Running it

The scenario declares four goods:

steel    imported=true   medical=false  → owes duty   (general default, unattacked)
insulin  imported=true   medical=true   → exempt      (specific defeats general)
gauze    imported=true   medical=true   → exempt      (specific defeats general)
widget   imported=false  medical=false  → no clause fires

so dutiable (the warranted must_pay_duty) returns 1 row — steel — while exemptions returns 2 rows, insulin and gauze. The two medical imports are dutiable under the general norm and exempt under the specific one; lex specialis subtracts them from the duty extent, leaving the single non-medical import.

This example is compiled and run in CI; the post-defeat must_pay_duty and exempt extents are pinned by a corpus test (oxc-runtime/tests/examples_corpus.rs), so the lex-specialis resolution can’t drift.

Source

The package’s real Argon source, transcluded from the files this corpus compiles — what you read here is exactly what CI builds.

root.ar

//! Lex specialis via `#[defeats]` (RFD 0028, register R-B8).
//!
//! The legal-domain unblock: same-strength norm conflicts
//! (lex specialis / lex posterior) were unresolvable without a
//! superiority mechanism. RFD 0028 makes the specific rule defeating
//! the general clause's label an explicit, resolution-checked edge —
//! not a pair of magic priority integers.

mod statute;

statute.ar

//! A customs statute with a lex-specialis exception.
//!
//! General norm:  imported goods owe import duty (the default).
//! Specific norm: medical imports are exempt — and *lex specialis*
//!                says the specific rule wins.
//!
//! Pre-RFD-0028 this conflict was unresolvable: both rules concluded
//! about the same head at the same strength, and there was no
//! superiority mechanism (`#[priority]` was silently dropped;
//! `#[defeats]` did not exist) — register blocker R-B8. Now the
//! exemption rule names the general clause's label and defeats it,
//! per-tuple, with an explicit edge:
//!
//!   #[defeats(must_pay_duty.general(g))]
//!
//! Reads true at every line: imported goods owe duty by default;
//! medical goods are exempt; the exemption defeats the general duty
//! clause for exactly the exempt goods.
//!
//! Expected `must_pay_duty` extent over the four goods below:
//!   steel    (imported, not medical)  → owes duty   (default, unattacked)
//!   insulin  (imported, MEDICAL)       → exempt      (lex specialis defeats)
//!   gauze    (imported, MEDICAL)       → exempt      (lex specialis defeats)
//!   widget   (NOT imported)            → no clause fires
//!
//!   ⇒ must_pay_duty = { steel }

pub type Good {
    mut imported: Bool,
    mut medical: Bool,
}

pub type Imported <: Good iff { self.imported == true };

pub type MedicalGood <: Good iff { self.medical == true };

// General norm: imported goods owe import duty — but overridable, and
// labeled so a more specific rule can name it.
#[default]
#[label (general)]
pub derive must_pay_duty(g) :- Imported(g);

// Specific norm: medical imports are exempt. Lex specialis — the
// specific rule defeats the general clause for exactly the medical
// goods it derives.
#[defeats (must_pay_duty.general(g))]
pub derive exempt(g) :- MedicalGood(g);

pub mutate declare(g: Good, imported: Bool, medical: Bool) {
    insert iof(g, Good);
    update g: Good set { imported = imported, medical = medical }
}

pub query dutiable() -> must_pay_duty;
pub query exemptions() -> exempt;