Domain rules

This file defines domain rules, rules of exponence that apply exactly at the contexts of a finite domain, ordered by domain inclusion so that the rule with the narrower domain is the more specific. O'Donnell's finitely supported rules, whose domain is the finite set of forms a rule generates, and Stump's rules of paradigm linkage, whose domain is a set of content cells, are domain rules.

Main definitions

• Exponence.DomainRule: a finite domain with an exponent, with its Exponence.Rule instance and the specificity preorder of domain inclusion.

Main results

• DomainRule.le_iff, DomainRule.lt_iff: specificity is domain inclusion.
• DomainRule.factorsThrough_applies_iff: a rule's applicability factors through a map exactly when its domain is a union of the map's fibers.
• DomainRule.isChain_of_nested: rules whose overlapping domains are nested satisfy Pāṇinian Determinism, their Elsewhere winners forming a chain.
• DomainRule.exists_not_isContiguous_realizeMinimal: without Pāṇinian Determinism, minimal selection over upper-set domains realizes ABA even with distinct exponents on distinct rules.

References

• [OD15]
• [Stu06]

structure Morphology.Exponence.DomainRule (Ctx : Type u_1) (E : Type u_2) : Type (max u_1 u_2)

A domain rule carries an exponent and applies exactly at the contexts of a finite domain.

• dom : Finset Ctx

  The domain is the finite set of contexts the rule applies at.

• exponent : E

  The exponent is what the rule assigns.

@[instance_reducible]

instance Morphology.Exponence.instDecidableEqDomainRule {Ctx✝ : Type u_1} {E✝ : Type u_2} [DecidableEq Ctx✝] [DecidableEq E✝] : DecidableEq (DomainRule Ctx✝ E✝)

Equations

• Morphology.Exponence.instDecidableEqDomainRule = Morphology.Exponence.instDecidableEqDomainRule.decEq

def Morphology.Exponence.instDecidableEqDomainRule.decEq {Ctx✝ : Type u_1} {E✝ : Type u_2} [DecidableEq Ctx✝] [DecidableEq E✝] (x✝ x✝¹ : DomainRule Ctx✝ E✝) : Decidable (x✝ = x✝¹)

Equations

• One or more equations did not get rendered due to their size.

@[instance_reducible]

instance Morphology.Exponence.DomainRule.instRule {Ctx : Type u_1} {E : Type u_2} : Rule (DomainRule Ctx E) Ctx E

Equations

• Morphology.Exponence.DomainRule.instRule = { exponent := Morphology.Exponence.DomainRule.exponent, Applies := fun (r : Morphology.Exponence.DomainRule Ctx E) (c : Ctx) => c ∈ r.dom }

@[instance_reducible]

instance Morphology.Exponence.DomainRule.instPreorder {Ctx : Type u_1} {E : Type u_2} : Preorder (DomainRule Ctx E)

Domain rules are ordered by the specificity preorder, so that a rule whose domain is included in another's is the more specific.

Equations

• Morphology.Exponence.DomainRule.instPreorder = Morphology.Exponence.toPreorder

@[simp]

theorem Morphology.Exponence.DomainRule.applies_iff {Ctx : Type u_1} {E : Type u_2} {r : DomainRule Ctx E} {c : Ctx} : Applies r c ↔ c ∈ r.dom

@[simp]

theorem Morphology.Exponence.DomainRule.rule_exponent {Ctx : Type u_1} {E : Type u_2} {r : DomainRule Ctx E} : Exponence.exponent r = r.exponent

theorem Morphology.Exponence.DomainRule.le_iff {Ctx : Type u_1} {E : Type u_2} {r s : DomainRule Ctx E} : r ≤ s ↔ r.dom ⊆ s.dom

theorem Morphology.Exponence.DomainRule.lt_iff {Ctx : Type u_1} {E : Type u_2} {r s : DomainRule Ctx E} : r < s ↔ r.dom ⊂ s.dom

theorem Morphology.Exponence.DomainRule.factorsThrough_applies_iff {Ctx : Type u_1} {E : Type u_2} {r : DomainRule Ctx E} {V : Type u_3} {A : Ctx → V} : Function.FactorsThrough (Applies r) A ↔ ∀ (c c' : Ctx), A c = A c' → (c ∈ r.dom ↔ c' ∈ r.dom)

A domain rule's applicability factors through A exactly when its domain is a union of fibers of A.

theorem Morphology.Exponence.DomainRule.isChain_of_nested {Ctx : Type u_1} {E : Type u_2} {v : RuleSet (DomainRule Ctx E)} (h : ∀ r ∈ v, ∀ s ∈ v, ¬Disjoint r.dom s.dom → r ≤ s ∨ s ≤ r) (c : Ctx) : IsChain (fun (x1 x2 : DomainRule Ctx E) => x1 ≤ x2) {r : DomainRule Ctx E | v.IsElsewhereWinner c r}

Rules whose overlapping domains are nested satisfy Pāṇinian Determinism, their Elsewhere winners at any context forming a chain.

@[instance_reducible]

instance Morphology.Exponence.DomainRule.instDecidableRelApplies {Ctx : Type u_1} {E : Type u_2} [DecidableEq Ctx] : DecidableRel Applies

Equations

• r.instDecidableRelApplies c = Finset.decidableMem c r.dom

@[instance_reducible]

instance Morphology.Exponence.DomainRule.instDecidableRelLt {Ctx : Type u_1} {E : Type u_2} [DecidableEq Ctx] : DecidableRel fun (x1 x2 : DomainRule Ctx E) => x1 < x2

Equations

• r.instDecidableRelLt s = { decide := decide (r.dom ⊆ s.dom) && decide ¬s.dom ⊆ r.dom, reflects_decide := ⋯ }

@[instance_reducible]

instance Morphology.Exponence.DomainRule.instDecidableFactorsThroughAppliesOfFintypeOfDecidableEq {Ctx : Type u_1} {E : Type u_2} [DecidableEq Ctx] [Fintype Ctx] {V : Type u_3} [DecidableEq V] (r : DomainRule Ctx E) (A : Ctx → V) : Decidable (Function.FactorsThrough (Applies r) A)

Equations

• r.instDecidableFactorsThroughAppliesOfFintypeOfDecidableEq A = decidable_of_iff (∀ (c c' : Ctx), A c = A c' → (c ∈ r.dom ↔ c' ∈ r.dom)) ⋯

theorem Morphology.Exponence.DomainRule.exists_not_isContiguous_realizeMinimal : ∃ (v : RuleSet (DomainRule (Finset (Fin 3)) String)), v.Antihomophonous ∧ (∀ r ∈ v, IsUpperSet ↑r.dom) ∧ ¬IsContiguous v.realizeMinimal

Without Pāṇinian Determinism, minimal selection realizes ABA. Over feature bundles ordered by inclusion, a rule S for feature 1, a rule R for feature 0, and a rule T for features 1 and 2 each apply on an upper set, and listed in that order they realize R, S, R on the chain {0} ⊆ {0, 1} ⊆ {0, 1, 2}: at {0, 1} the winners S and R are incomparable, and the list order picks S.