Legal norms: strict vs default vs defeater

Area: Defeasible reasoning Teaches: the three rule strengths of defeasible reasoning on one head — a strict (unattackable) clause, an overridable #[default] clause, and a #[defeats] directive that attacks the default per-tuple. RFD 0028’s “honest heads”: no rule spells the conclusion it denies. Prerequisites: refinement (iff/where), and derive rule bodies (see first-class relations). Run: ox build examples/legal_norms_can_vote && ox run-scenario examples/legal_norms_can_vote

Who can vote? Three norms speak to can_vote, and they conflict. A pre-defeasibility data language forces you to fold the exceptions into the rule body by hand (Adult(p), not Felon(p), not …), which becomes unmaintainable as exceptions accumulate. Argon keeps each norm a separate honest rule and resolves the conflict with directives.

What to read in norms.ar

The strict clause is unmarked — it is unattackable. Special-class members vote regardless of any disenfranchisement edge:

pub derive can_vote(p) :- SpecialClass(p);

The default clause is overridable. Adults vote by default — #[default] marks the clause as defeasible, and #[label(adult)] gives it an identity an attacker can name:

#[default]
#[label(adult)]
pub derive can_vote(p) :- Adult(p);

The exception is its own honest rule, and the attack is a directive. disenfranchised reads true on its own terms — it does not spell not can_vote. The attack lives in #[defeats(can_vote(p))], a meta-level statement about rules that resolves per-tuple against the bound p:

#[defeats(can_vote(p))]
pub derive disenfranchised(p) :- Felon(p);

So for a given person, disenfranchised defeats the default can_vote clause — but the strict clause is not a default, so the attack cannot touch it.

Running it

The scenario registers four people, one per case:

alice  age=25  felon=false  special=false  → can_vote   (default holds, unattacked)
bob    age=12  felon=false  special=false  → not        (not an Adult — no clause fires)
carol  age=30  felon=true   special=false  → not        (default defeated by disenfranchised)
dave   age=45  felon=true   special=true   → can_vote   (strict clause; the attack can't reach it)

so voters returns 2 rows — alice (default survives) and dave (strict overrides the very defeat that blocks carol). The decisive contrast is carol vs dave: both are felons, both are disenfranchised, but dave’s vote comes from the strict clause that #[defeats] cannot attack.

This example is compiled and run in CI; its can_vote extent under the strict/default/defeater interplay is pinned by a corpus test (oxc-runtime/tests/examples_corpus.rs), so the resolution can’t drift from the language.

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

//! Defeasibility (Governatori-style strict / defeasible / defeater).

mod norms;

norms.ar

//! Defeasibility, RFD 0028 honest-head form.
//!
//! The legal-norms use case: special-class members can vote (strict);
//! adults can vote by default; felons are disenfranchised, and that
//! disenfranchisement defeats the adult default.
//!
//! Every rule reads true (RFD 0028 D1 — "honest heads"): no rule
//! spells the head it denies. The exception (`disenfranchised`) lives
//! under its own name, and the attack is a directive (`#[defeats]`),
//! never the rule's syntax.
//!
//! Demonstrates:
//!   * `#[default]` — an overridable clause (the adult default)
//!   * `#[label(adult)]` — the clause's identity
//!   * `#[defeats(can_vote(p))]` — the attack, a meta-level statement
//!     about rules, resolving per-tuple against the bound `p`
//!   * the strict clause (unmarked) is unattackable — special-class
//!     members vote regardless of the disenfranchisement edge
//!
//! Expected runtime behavior:
//!   alice  age=25, felon=false, special=false  → can_vote (default holds)
//!   bob    age=12, felon=false, special=false  → not can_vote (not adult)
//!   carol  age=30, felon=true,  special=false  → not can_vote (defeated)
//!   dave   age=45, felon=true,  special=true   → can_vote (strict; unattackable)

pub type Person {
    mut age: Int,
    mut felon: Bool,
    mut special: Bool,
}

pub type Adult <: Person iff { self.age >= 18 };

pub type Felon <: Person iff { self.felon == true };

pub type SpecialClass <: Person iff { self.special == true };

// strict = unmarked: special-class members vote, period (unattackable)
pub derive can_vote(p) :- SpecialClass(p);

// the overridable default
#[default]
#[label (adult)]
pub derive can_vote(p) :- Adult(p);

// the exception: an honest head, and the attack as a directive
#[defeats (can_vote(p))]
pub derive disenfranchised(p) :- Felon(p);

pub mutate register(p: Person, age: Int, felon: Bool, special: Bool) {
    insert iof(p, Person);
    update p: Person set { age = age, felon = felon, special = special }
}

pub query voters() -> can_vote;