Elsewhere selection

import Linglib.Morphology.Exponence.Select · namespace Morphology.Exponence.RuleSet

This file defines selection by a specificity score (selectBy) and by minimality under a specificity key (selectMinimal), and proves that both produce Elsewhere winners. Selection by a score keeps its choice when the competition shrinks around the winner, so rules applicable on upper sets of ordered contexts realize contiguous patterns. Minimal selection does the same, and agrees with selection by a score, where Stump's Pāṇinian Determinism holds, the Elsewhere winners forming a chain. The exponent of the minimal selection, falling back on a default where no rule applies, is the shape shared by Stump's rules of paradigm linkage over a root and by Bonami and Stump's rules of basic stem choice.

Main definitions

RuleSet.selectBy, RuleSet.realize: the applicable rule of greatest score, and its exponent.
RuleSet.selectMinimal, RuleSet.realizeMinimal: the first applicable rule that no applicable rule strictly undercuts, and its exponent.
RuleSet.realizeMinimalD: the exponent of the minimal selection, or a fallback where no rule applies.
RuleSet.HasMostSpecific: some applicable rule is at least as specific as every other.

Main results

RuleSet.selectBy_eq_some_of_applies: selection by a score is consistent under contraction, so the rule selected in a context stays selected in any context with fewer applicable rules where it still applies.
RuleSet.selectBy_eq_head?_applicable: on a rule set listed by non-increasing score, selection takes the first applicable rule.
RuleSet.selectBy_map: selection commutes with a map of rules preserving applicability and the comparison of scores.
RuleSet.isContiguous_realize_of_monotone, RuleSet.isContiguous_realize_of_antitone: rules applicable on upper sets, or on lower sets, of ordered contexts realize contiguous patterns when distinct rules carry distinct exponents.
RuleSet.selectBy_isElsewhereWinner, RuleSet.selectMinimal_isElsewhereWinner: both selections produce Elsewhere winners.
RuleSet.selectMinimal_append_singleton: a rule appended to a rule set and no more specific than its rules is selected only where none of them applies.
RuleSet.HasMostSpecific.isChain: where some applicable rule is most specific, the Elsewhere winners form a chain, as Pāṇinian Determinism requires.
RuleSet.selectMinimal_eq_some_of_applies, RuleSet.isContiguous_realizeMinimal_of_monotone: under Pāṇinian Determinism minimal selection is consistent under contraction and realizes contiguous patterns.
RuleSet.realizeMinimal_eq_realize: under Pāṇinian Determinism minimal selection realizes what selection on any score strictly reversing specificity realizes.
RuleSet.selectMinimal_factorsThrough, RuleSet.realizeMinimal_factorsThrough, RuleSet.realizeMinimalD_factorsThrough: selection, realization, and realization with a fallback, factor through any map on contexts that every rule's applicability (and the fallback) factors through.
RuleSet.realizeMinimalD_eq_of_isElsewhereWinner: over a coherent rule set under Pāṇinian Determinism, realization with a fallback is the exponent of any Elsewhere winner, whatever the order of the rule set.

References

Bonami & Stump 2016, Paradigm Function Morphology formalized
Stump 2006, Heteroclisis and Paradigm Linkage formalized

Score selection

L77–79

L81–83

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

def selectBy L87–90

{Ctx : Type u_1} {E : Type u_2} {R : Type u_3} [Rule R Ctx E] [DecidableRel Applies] {α : Type u_4} [LinearOrder α] (v : RuleSet R) (f : R → α) (c : Ctx) :

Option R

v.selectBy f c = List.argmax f (v.applicable c)

Built from

Used by selectBy_mem, selectBy_applies, selectBy_eq_none_iff, selectBy_eq_head?_applicable, selectBy_isSome_iff, selectBy_congr, realize, le_of_selectBy_eq_some, selectBy_eq_some_of_applies, selectBy_eq_none_of_applies, selectBy_filter_of_mem, selectBy_map, selectBy_isElsewhereWinner

Used in Morphology/DistributedMorphology/VocabularyInsertion/Basic, Morphology/Exponence/Containment/Contiguity, Morphology/Exponence/Containment/Selection, Morphology/Exponence/Decomposition, Morphology/Nanosyntax/TreeSpellout and 3 more

L92–93

L95–96

L98–99

On a rule set listed by non-increasing score, selection takes the first applicable rule.

theorem selectBy_eq_head?_applicable L101–104

{Ctx : Type u_1} {E : Type u_2} {R : Type u_3} [Rule R Ctx E] [DecidableRel Applies] {v : RuleSet R} {c : Ctx} {α : Type u_4} [LinearOrder α] {f : R → α} (h : List.Pairwise (fun (r s : R) => f s ≤ f r) v) :

v.selectBy f c = (v.applicable c).head?

Built from ,

L106–107

L109–111

The exponent of the rule selected by selectBy.

def realize L113–115

{Ctx : Type u_1} {E : Type u_2} {R : Type u_3} [Rule R Ctx E] [DecidableRel Applies] {α : Type u_4} [LinearOrder α] (v : RuleSet R) (f : R → α) (c : Ctx) :

Option E

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

Built from

Used by realize_eq_none_iff, realize_congr, realize_eq_of_forall_le, realize_eq_of_applies, isContiguous_realize_of_monotone, isContiguous_realize_of_antitone, realize_filter_eq_some, realize_realizes, realizeMinimal_eq_realize

Used in Morphology/DistributedMorphology/VocabularyInsertion/Basic, Morphology/Exponence/Containment/Selection, AckemaNeeleman2018, Bobaljik2012, Hanink2021

Contraction

L140–143

Selection by a score is consistent under contraction. The rule selected at c' is selected at any context whose applicable rules are among those at c', as long as it applies there.

theorem selectBy_eq_some_of_applies L145–150

{Ctx : Type u_1} {E : Type u_2} {R : Type u_3} [Rule R Ctx E] [DecidableRel Applies] {v : RuleSet R} {c c' : Ctx} {r : R} {α : Type u_4} [LinearOrder α] {f : R → α} (h : ∀ s ∈ v, Applies s c → Applies s c') (hr : v.selectBy f c' = some r) (hrc : Applies r c) :

v.selectBy f c = some r

Built from

L152–154

L156–166

Rules applicable on upper sets of contexts realize contiguous patterns.

theorem isContiguous_realize_of_monotone L172–176

{Ctx : Type u_1} {E : Type u_2} {R : Type u_3} [Rule R Ctx E] [DecidableRel Applies] {v : RuleSet R} {α : Type u_4} [LinearOrder α] {f : R → α} [Preorder Ctx] (hv : v.Antihomophonous) (h : ∀ r ∈ v, Monotone (Applies r)) :

IsContiguous (v.realize f)

Built from

Rules applicable on lower sets of contexts realize contiguous patterns.

theorem isContiguous_realize_of_antitone L178–182

IsContiguous (v.realize f)

Built from

Loss of rules

L188–190

L192–195

L197–204

Transport

Selection commutes with a map of rules that preserves applicability and the comparison of scores.

theorem selectBy_map L213–223

{Ctx : Type u_1} {E : Type u_2} {R : Type u_3} [Rule R Ctx E] [DecidableRel Applies] {v : RuleSet R} {c : Ctx} {α : Type u_4} [LinearOrder α] {f : R → α} {R' : Type u_5} {Ctx' : Type u_6} {E' : Type u_7} [Rule R' Ctx' E'] [DecidableRel Applies] {β : Type u_8} [LinearOrder β] {f' : R' → β} {g : R → R'} {c' : Ctx'} (happ : ∀ r ∈ v, Applies (g r) c' ↔ Applies r c) (hf : ∀ r ∈ v, ∀ s ∈ v, f' (g r) ≤ f' (g s) ↔ f r ≤ f s) :

selectBy (List.map g v) f' c' = Option.map g (v.selectBy f c)

Built from

Soundness

A score that strictly reverses specificity on the applicable rules selects an Elsewhere winner.

theorem selectBy_isElsewhereWinner L231–238

{Ctx : Type u_1} {E : Type u_2} {R : Type u_3} [Rule R Ctx E] [DecidableRel Applies] {v : RuleSet R} {c : Ctx} {r : R} {α : Type u_4} [LinearOrder α] {f : R → α} {κ : Type u_5} [Preorder κ] {key : R → κ} (hf : ∀ r ∈ v.applicable c, ∀ s ∈ v.applicable c, key r < key s → f s < f r) (h : v.selectBy f c = some r) :

v.IsElsewhereWinner key c r

Built from ,

L240–244

Pāṇinian Determinism

Some rule of v applicable at c is at least as specific as every rule applicable there, as Stump's Pāṇinian Determinism requires of a rule block at every cell.

def HasMostSpecific L248–251

{Ctx : Type u_1} {E : Type u_2} {R : Type u_3} [Rule R Ctx E] [DecidableRel Applies] {κ : Type u_5} [Preorder κ] (v : RuleSet R) (key : R → κ) (c : Ctx) :

Prop

v.HasMostSpecific key c = ∃ r ∈ v.applicable c, ∀ s ∈ v.applicable c, key r ≤ key s

Built from

Used by instDecidableHasMostSpecificOfDecidableRelLe, HasMostSpecific.isChain

L253–254

Where some applicable rule is most specific, the Elsewhere winners form a chain.

theorem HasMostSpecific.isChain L256–262

{Ctx : Type u_1} {E : Type u_2} {R : Type u_3} [Rule R Ctx E] [DecidableRel Applies] {v : RuleSet R} {c : Ctx} {κ : Type u_5} [Preorder κ] {key : R → κ} (h : v.HasMostSpecific key c) :

IsChain (fun (r s : R) => key r ≤ key s) {s : R | v.IsElsewhereWinner key c s}

Built from

Order selection

The first applicable rule that no applicable rule is strictly more specific than, specificity read through key.

def selectMinimal L268–271

{Ctx : Type u_1} {E : Type u_2} {R : Type u_3} [Rule R Ctx E] [DecidableRel Applies] {κ : Type u_5} [Preorder κ] [DecidableRel fun (x1 x2 : κ) => x1 < x2] (v : RuleSet R) (key : R → κ) (c : Ctx) :

Option R

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

Built from

Used by selectMinimal_eq_find?, selectMinimal_isElsewhereWinner, selectMinimal_mem, selectMinimal_applies, selectMinimal_isSome_iff, selectMinimal_eq_none_iff, selectMinimal_congr, selectMinimal_append_singleton, selectMinimal_factorsThrough, realizeMinimal, selectMinimal_eq_some_of_applies, selectMinimal_eq_none_of_applies, realizeMinimalD_eq_of_selectMinimal_eq_some, realizeMinimalD_eq_fallback_of_selectMinimal_eq_none

Used in Morphology/Paradigm/Function

L273–278

selectMinimal returns an Elsewhere winner.

theorem selectMinimal_isElsewhereWinner L280–286

v.IsElsewhereWinner key c r

Built from

A rule appended to v that applies at c and is no more specific than any rule of v is selected only where no rule of v applies.

theorem selectMinimal_append_singleton L310–323

{Ctx : Type u_1} {E : Type u_2} {R : Type u_3} [Rule R Ctx E] [DecidableRel Applies] {v : RuleSet R} {c : Ctx} {r : R} {κ : Type u_5} [Preorder κ] {key : R → κ} [DecidableRel fun (x1 x2 : κ) => x1 < x2] (hr : Applies r c) (hle : ∀ s ∈ v, key s ≤ key r) :

(v ++ [r]).selectMinimal key c = (v.selectMinimal key c).or (some r)

Built from

A rule system sensitive only to what A sees selects the same rule in contexts that A identifies.

theorem selectMinimal_factorsThrough L325–330

{Ctx : Type u_1} {E : Type u_2} {R : Type u_3} [Rule R Ctx E] [DecidableRel Applies] {v : RuleSet R} {κ : Type u_5} [Preorder κ] {key : R → κ} [DecidableRel fun (x1 x2 : κ) => x1 < x2] {V : Type u_6} {A : Ctx → V} (h : ∀ r ∈ v, ∀ ⦃c c' : Ctx⦄, A c = A c' → (Applies r c ↔ Applies r c')) :

Function.FactorsThrough (v.selectMinimal key) A

Built from

The exponent of the rule selected by selectMinimal, the order-based counterpart of realize.

def realizeMinimal L332–335

Option E

v.realizeMinimal key c = Option.map Morphology.Exponence.exponent (v.selectMinimal key c)

Built from

Used by realizeMinimal_factorsThrough, realizeMinimal_eq_none_iff, realizeMinimal_isSome_iff, realizeMinimal_congr, realizeMinimal_realizes, realizeMinimal_eq_of_isElsewhereWinner, realizeMinimal_eq_realize, realizeMinimal_eq_of_applies, isContiguous_realizeMinimal_of_monotone, isContiguous_realizeMinimal_of_antitone, realizeMinimalD

Used in Morphology/Exponence/Domain, Syntax/Agreement/Paradigm, Brodkin2026

A rule system sensitive only to what A sees realizes the same exponent in contexts that A identifies.

theorem realizeMinimal_factorsThrough L337–342

Function.FactorsThrough (v.realizeMinimal key) A

Built from

Under Pāṇinian Determinism a coherent rule set realizes by minimal selection what it realizes by selection on any score strictly reversing specificity.

theorem realizeMinimal_eq_realize L367–377

{Ctx : Type u_1} {E : Type u_2} {R : Type u_3} [Rule R Ctx E] [DecidableRel Applies] {v : RuleSet R} {c : Ctx} {α : Type u_4} [LinearOrder α] {f : R → α} {κ : Type u_5} [Preorder κ] {key : R → κ} [DecidableRel fun (x1 x2 : κ) => x1 < x2] (hv : v.Coherent key) (hc : IsChain (fun (r s : R) => key r ≤ key s) {s : R | v.IsElsewhereWinner key c s}) (hf : ∀ r ∈ v.applicable c, ∀ s ∈ v.applicable c, key r < key s → f s < f r) :

v.realizeMinimal key c = v.realize f c

Built from , ,

Contraction under Pāṇinian Determinism

Minimal selection is consistent under contraction where the Elsewhere winners of the smaller context form a chain, Stump's Pāṇinian Determinism. The rule selected at c' is then selected at any context whose applicable rules are among those at c', as long as it applies there.

theorem selectMinimal_eq_some_of_applies L381–401

{Ctx : Type u_1} {E : Type u_2} {R : Type u_3} [Rule R Ctx E] [DecidableRel Applies] {v : RuleSet R} {c c' : Ctx} {r : R} {κ : Type u_5} [Preorder κ] {key : R → κ} [DecidableRel fun (x1 x2 : κ) => x1 < x2] (h : ∀ s ∈ v, Applies s c → Applies s c') (hc : IsChain (fun (r s : R) => key r ≤ key s) {s : R | v.IsElsewhereWinner key c s}) (hr : v.selectMinimal key c' = some r) (hrc : Applies r c) :

v.selectMinimal key c = some r

Built from

L403–406

L408–420

Under Pāṇinian Determinism, rules applicable on upper sets of contexts realize contiguous patterns by minimal selection.

theorem isContiguous_realizeMinimal_of_monotone L426–432

{Ctx : Type u_1} {E : Type u_2} {R : Type u_3} [Rule R Ctx E] [DecidableRel Applies] {v : RuleSet R} {κ : Type u_5} [Preorder κ] {key : R → κ} [DecidableRel fun (x1 x2 : κ) => x1 < x2] [Preorder Ctx] (hv : v.Antihomophonous) (hc : ∀ (c : Ctx), IsChain (fun (r s : R) => key r ≤ key s) {s : R | v.IsElsewhereWinner key c s}) (h : ∀ r ∈ v, Monotone (Applies r)) :

IsContiguous (v.realizeMinimal key)

Built from

L434–438

Realization with a fallback

v.realizeMinimalD key fallback c is the exponent of the rule selected by selectMinimal, or fallback c where no rule of v applies at c.

def realizeMinimalD L444–447

{Ctx : Type u_1} {E : Type u_2} {R : Type u_3} [Rule R Ctx E] [DecidableRel Applies] {κ : Type u_5} [Preorder κ] [DecidableRel fun (x1 x2 : κ) => x1 < x2] (v : RuleSet R) (key : R → κ) (fallback : Ctx → E) (c : Ctx) :

v.realizeMinimalD key fallback c = (v.realizeMinimal key c).getD (fallback c)

Built from

Used by realizeMinimalD_nil, realizeMinimalD_eq_of_selectMinimal_eq_some, realizeMinimalD_eq_fallback_of_selectMinimal_eq_none, realizeMinimalD_eq_fallback_or_mem, realizeMinimalD_induction, realizeMinimalD_congr, realizeMinimalD_factorsThrough, realizeMinimalD_eq_of_isElsewhereWinner

Used in Morphology/Paradigm/Linkage, BonamiStump2016, Stump2006

Rules whose applicability factors through A, with a fallback that does too, realize values that factor through A (Stump 2006, §5.5).

theorem realizeMinimalD_factorsThrough L481–488

{Ctx : Type u_1} {E : Type u_2} {R : Type u_3} [Rule R Ctx E] [DecidableRel Applies] {v : RuleSet R} {κ : Type u_5} [Preorder κ] {key : R → κ} [DecidableRel fun (x1 x2 : κ) => x1 < x2] {fallback : Ctx → E} {V : Type u_6} {A : Ctx → V} (hd : Function.FactorsThrough fallback A) (h : ∀ r ∈ v, ∀ ⦃c c' : Ctx⦄, A c = A c' → (Applies r c ↔ Applies r c')) :

Function.FactorsThrough (v.realizeMinimalD key fallback) A

Built from

Over a coherent rule set whose Elsewhere winners form a chain, the realized value is the exponent of any Elsewhere winner, so it does not depend on the order of the rule set.

theorem realizeMinimalD_eq_of_isElsewhereWinner L490–496

{Ctx : Type u_1} {E : Type u_2} {R : Type u_3} [Rule R Ctx E] [DecidableRel Applies] {v : RuleSet R} {c : Ctx} {r : R} {κ : Type u_5} [Preorder κ] {key : R → κ} [DecidableRel fun (x1 x2 : κ) => x1 < x2] {fallback : Ctx → E} (hv : v.Coherent key) (hc : IsChain (fun (r s : R) => key r ≤ key s) {s : R | v.IsElsewhereWinner key c s}) (hr : v.IsElsewhereWinner key c r) :

v.realizeMinimalD key fallback c = exponent r

Built from