Elsewhere selection

This file proves that selection by a specificity score (selectBy) and selection over the specificity preorder (selectMinimal) produce Elsewhere winners.

Main definitions

• selectBy, realize: the applicable rule of greatest score, and its exponent.
• selectMinimal: the first applicable rule that no applicable rule strictly undercuts.
• selectBy_isElsewhereWinner, selectMinimal_isElsewhereWinner: both selections produce Elsewhere winners.

Score selection

def Morphology.Exponence.applicable {Ctx : Type u_1} {E : Type u_2} {R : Type u_3} [Rule R Ctx E] [DecidableRel Applies] (v : List R) (c : Ctx) : List R

The rules of v applicable at c, in vocabulary order.

Equations

• Morphology.Exponence.applicable v c = List.filter (fun (r : R) => decide (Morphology.Exponence.Applies r c)) v

@[simp]

theorem Morphology.Exponence.mem_applicable {Ctx : Type u_1} {E : Type u_2} {R : Type u_3} [Rule R Ctx E] [DecidableRel Applies] {v : List R} {c : Ctx} {r : R} : r ∈ applicable v c ↔ r ∈ v ∧ Applies r c

def Morphology.Exponence.selectBy {Ctx : Type u_1} {E : Type u_2} {R : Type u_3} [Rule R Ctx E] [DecidableRel Applies] {α : Type u_4} [LinearOrder α] (f : R → α) (v : List R) (c : Ctx) : Option R

The applicable rule of greatest score f, ties broken by vocabulary order; scores to be minimized pass through OrderDual.

Equations

• Morphology.Exponence.selectBy f v c = List.argmax f (Morphology.Exponence.applicable v c)

theorem Morphology.Exponence.selectBy_mem {Ctx : Type u_1} {E : Type u_2} {R : Type u_3} [Rule R Ctx E] [DecidableRel Applies] {v : List R} {c : Ctx} {r : R} {α : Type u_4} [LinearOrder α] {f : R → α} (h : selectBy f v c = some r) : r ∈ v

theorem Morphology.Exponence.selectBy_applies {Ctx : Type u_1} {E : Type u_2} {R : Type u_3} [Rule R Ctx E] [DecidableRel Applies] {v : List R} {c : Ctx} {r : R} {α : Type u_4} [LinearOrder α] {f : R → α} (h : selectBy f v c = some r) : Applies r c

theorem Morphology.Exponence.selectBy_eq_none_iff {Ctx : Type u_1} {E : Type u_2} {R : Type u_3} [Rule R Ctx E] [DecidableRel Applies] {v : List R} {c : Ctx} {α : Type u_4} [LinearOrder α] {f : R → α} : selectBy f v c = none ↔ applicable v c = []

theorem Morphology.Exponence.selectBy_congr {Ctx : Type u_1} {E : Type u_2} {R : Type u_3} [Rule R Ctx E] [DecidableRel Applies] {v : List R} {c c' : Ctx} {α : Type u_4} [LinearOrder α] {f : R → α} (h : applicable v c = applicable v c') : selectBy f v c = selectBy f v c'

Contexts with the same applicable rules select the same rule.

def Morphology.Exponence.realize {Ctx : Type u_1} {E : Type u_2} {R : Type u_3} [Rule R Ctx E] [DecidableRel Applies] {α : Type u_4} [LinearOrder α] (f : R → α) (v : List R) (c : Ctx) : Option E

The exponent of the rule selected by selectBy.

Equations

• Morphology.Exponence.realize f v c = Option.map Morphology.Exponence.exponent (Morphology.Exponence.selectBy f v c)

theorem Morphology.Exponence.realize_eq_none_iff {Ctx : Type u_1} {E : Type u_2} {R : Type u_3} [Rule R Ctx E] [DecidableRel Applies] {v : List R} {c : Ctx} {α : Type u_4} [LinearOrder α] {f : R → α} : realize f v c = none ↔ applicable v c = []

theorem Morphology.Exponence.realize_congr {Ctx : Type u_1} {E : Type u_2} {R : Type u_3} [Rule R Ctx E] [DecidableRel Applies] {v : List R} {c c' : Ctx} {α : Type u_4} [LinearOrder α] {f : R → α} (h : applicable v c = applicable v c') : realize f v c = realize f v c'

Soundness

theorem Morphology.Exponence.selectBy_isElsewhereWinner {Ctx : Type u_1} {E : Type u_2} {R : Type u_3} [Rule R Ctx E] [DecidableRel Applies] {v : List R} {c : Ctx} {r : R} {α : Type u_4} [LinearOrder α] {f : R → α} [Preorder R] (hf : StrictAntiOn f {r : R | r ∈ applicable v c}) (h : selectBy f v c = some r) : IsElsewhereWinner v c r

A score strictly antitone on the applicable rules selects an Elsewhere winner.

theorem Morphology.Exponence.realize_realizes {Ctx : Type u_1} {E : Type u_2} {R : Type u_3} [Rule R Ctx E] [DecidableRel Applies] {v : List R} {c : Ctx} {φ : E} {α : Type u_4} [LinearOrder α] {f : R → α} [Preorder R] (hf : StrictAntiOn f {r : R | r ∈ applicable v c}) (h : realize f v c = some φ) : Realizes v c φ

Realized exponents satisfy Realizes.

Order selection

def Morphology.Exponence.selectMinimal {Ctx : Type u_1} {E : Type u_2} {R : Type u_3} [Rule R Ctx E] [DecidableRel Applies] [Preorder R] [DecidableRel fun (x1 x2 : R) => x1 < x2] (v : List R) (c : Ctx) : Option R

The first applicable rule that no applicable rule strictly undercuts.

Equations

• Morphology.Exponence.selectMinimal v c = List.find? (fun (r : R) => (Morphology.Exponence.applicable v c).all fun (s : R) => decide ¬s < r) (Morphology.Exponence.applicable v c)

theorem Morphology.Exponence.selectMinimal_isElsewhereWinner {Ctx : Type u_1} {E : Type u_2} {R : Type u_3} [Rule R Ctx E] [DecidableRel Applies] {v : List R} {c : Ctx} {r : R} [Preorder R] [DecidableRel fun (x1 x2 : R) => x1 < x2] (h : selectMinimal v c = some r) : IsElsewhereWinner v c r

selectMinimal returns an Elsewhere winner.

theorem Morphology.Exponence.selectMinimal_mem {Ctx : Type u_1} {E : Type u_2} {R : Type u_3} [Rule R Ctx E] [DecidableRel Applies] {v : List R} {c : Ctx} {r : R} [Preorder R] [DecidableRel fun (x1 x2 : R) => x1 < x2] (h : selectMinimal v c = some r) : r ∈ v

theorem Morphology.Exponence.selectMinimal_applies {Ctx : Type u_1} {E : Type u_2} {R : Type u_3} [Rule R Ctx E] [DecidableRel Applies] {v : List R} {c : Ctx} {r : R} [Preorder R] [DecidableRel fun (x1 x2 : R) => x1 < x2] (h : selectMinimal v c = some r) : Applies r c

theorem Morphology.Exponence.selectMinimal_isSome_iff {Ctx : Type u_1} {E : Type u_2} {R : Type u_3} [Rule R Ctx E] [DecidableRel Applies] {v : List R} {c : Ctx} [Preorder R] [DecidableRel fun (x1 x2 : R) => x1 < x2] : (selectMinimal v c).isSome = true ↔ ∃ r ∈ v, Applies r c

selectMinimal succeeds iff some rule applies.

theorem Morphology.Exponence.selectMinimal_eq_none_iff {Ctx : Type u_1} {E : Type u_2} {R : Type u_3} [Rule R Ctx E] [DecidableRel Applies] {v : List R} {c : Ctx} [Preorder R] [DecidableRel fun (x1 x2 : R) => x1 < x2] : selectMinimal v c = none ↔ applicable v c = []