Positional faithfulness

A positional faithfulness constraint is a faithfulness constraint restricted to a prominent position, such as the beginning of a word or a root, whose segments it protects. Restricted to deletion, a candidate is the set of input positions it deletes, and the MAX constraint of a set of positions counts the deleted positions in it. The deletion of a single position therefore violates exactly the constraints that protect that position, and two single deletions compete through those sets of constraints: one of them is optimal under some ranking exactly when the constraints protecting the other position are not a proper subset of those protecting its own.

Main definitions

• OptimalityTheory.maxAt: MAX restricted to a set of positions, on deletions.
• OptimalityTheory.positionalMax: a family of such constraints, on candidates that delete positions.

Main results

• OptimalityTheory.maxAt_singleton_eq_maxViolAt: on the deletion of one position from a string, maxAt is MAX restricted to the positions in the sense of Correspondence Theory.
• OptimalityTheory.exists_mem_optimal_positionalMax_iff: of two single deletions, one is optimal under some ranking iff the constraints protecting the other position are not a proper subset of those protecting its own.

References

• [Bec99]
• [McCP95]

MAX restricted to a set of positions

def OptimalityTheory.maxAt (P : ℕ → Prop) [DecidablePred P] : Constraint (Finset ℕ)

maxAt P D counts the positions of the deletion D that lie in P, the violations of MAX restricted to P.

Equations

• OptimalityTheory.maxAt P D = (Finset.filter P D).card

@[simp]

theorem OptimalityTheory.maxAt_empty (P : ℕ → Prop) [DecidablePred P] : maxAt P ∅ = 0

@[simp]

theorem OptimalityTheory.maxAt_singleton (P : ℕ → Prop) [DecidablePred P] (k : ℕ) : maxAt P {k} = if P k then 1 else 0

@[simp]

theorem OptimalityTheory.maxAt_true (D : Finset ℕ) : maxAt (fun (x : ℕ) => True) D = D.card

theorem OptimalityTheory.maxAt_insert (P : ℕ → Prop) [DecidablePred P] {k : ℕ} {D : Finset ℕ} (hk : k ∉ D) : maxAt P (insert k D) = maxAt P D + if P k then 1 else 0

Deleting one more position adds a violation exactly when the position lies in P.

theorem OptimalityTheory.maxAt_singleton_eq_maxViolAt (P : ℕ → Prop) [DecidablePred P] {α : Type u_1} {s : List α} {k : ℕ} (hk : k < s.length) : maxAt P {k} = Correspondence.maxViolAt P (Correspondence.eraseIdx s k) BinaryRole.lhs BinaryRole.rhs

On the deletion of one position from a string, maxAt P counts the input segments in P that have no correspondent in the output.

Families of positional constraints

def OptimalityTheory.positionalMax {ι : Type u_1} {C : Type u_2} (P : ι → ℕ → Prop) [(i : ι) → DecidablePred (P i)] (del : C → Finset ℕ) : ConstraintSet C ι

positionalMax P del is MAX restricted to each set of positions P i, on candidates that delete the positions del c.

Equations

• OptimalityTheory.positionalMax P del i c = OptimalityTheory.maxAt (P i) (del c)

@[simp]

theorem OptimalityTheory.positionalMax_apply {ι : Type u_1} {C : Type u_2} (P : ι → ℕ → Prop) [(i : ι) → DecidablePred (P i)] (del : C → Finset ℕ) (i : ι) (c : C) : positionalMax P del i c = maxAt (P i) (del c)

theorem OptimalityTheory.positionalMax_lt_positionalMax_iff {ι : Type u_1} {C : Type u_2} {P : ι → ℕ → Prop} [(i : ι) → DecidablePred (P i)] {del : C → Finset ℕ} {c d : C} {k k' : ℕ} (hc : del c = {k}) (hd : del d = {k'}) {i : ι} : positionalMax P del i c < positionalMax P del i d ↔ ¬P i k ∧ P i k'

theorem OptimalityTheory.positionalMax_lt_iff {ι : Type u_1} {C : Type u_2} {P : ι → ℕ → Prop} [(i : ι) → DecidablePred (P i)] {del : C → Finset ℕ} {c d : C} {k k' : ℕ} (hc : del c = {k}) (hd : del d = {k'}) : ((fun (x : ι) => positionalMax P del x c) < fun (x : ι) => positionalMax P del x d) ↔ {i : ι | P i k} ⊂ {i : ι | P i k'}

One single deletion is below another on every constraint exactly when the constraints protecting its position are a proper subset of those protecting the other's.

theorem OptimalityTheory.optimal_eq_singleton_positionalMax_iff {ι : Type u_1} {C : Type u_2} {P : ι → ℕ → Prop} [(i : ι) → DecidablePred (P i)] {del : C → Finset ℕ} {c d : C} {k k' : ℕ} [DecidableEq C] {n : ℕ} {cands : List C} {h : cands ≠ []} (hcand : cands.toFinset = {c, d}) (hne : c ≠ d) (hc : del c = {k}) (hd : del d = {k'}) (r : Ranking ι n) : (Tableau.ofPerm (positionalMax P del) r cands h).optimal = {c} ↔ ∃ (i : ι), P i k' ∧ ¬P i k ∧ ∀ (j : ι), P j k → ¬P j k' → r.Dominates i j

Of two single deletions, one is the sole optimum under a ranking exactly when some constraint protecting only the other position outranks every constraint protecting only its own.

theorem OptimalityTheory.exists_mem_optimal_positionalMax_iff {ι : Type u_1} {C : Type u_2} {P : ι → ℕ → Prop} [(i : ι) → DecidablePred (P i)] {del : C → Finset ℕ} {c d : C} {k k' : ℕ} [DecidableEq C] {n : ℕ} {cands : List C} {h : cands ≠ []} [Fintype ι] (hn : Fintype.card ι = n) (hcand : cands.toFinset = {c, d}) (hc : del c = {k}) (hd : del d = {k'}) : (∃ (r : Ranking ι n), c ∈ (Tableau.ofPerm (positionalMax P del) r cands h).optimal) ↔ ¬{i : ι | P i k'} ⊂ {i : ι | P i k}

Of two single deletions, one is optimal under some ranking exactly when the constraints protecting the other position are not a proper subset of those protecting its own.

theorem OptimalityTheory.exists_optimal_eq_singleton_positionalMax_iff {ι : Type u_1} {C : Type u_2} {P : ι → ℕ → Prop} [(i : ι) → DecidablePred (P i)] {del : C → Finset ℕ} {c d : C} {k k' : ℕ} [DecidableEq C] {n : ℕ} {cands : List C} {h : cands ≠ []} [Fintype ι] (hn : Fintype.card ι = n) (hcand : cands.toFinset = {c, d}) (hne : c ≠ d) (hc : del c = {k}) (hd : del d = {k'}) : (∃ (r : Ranking ι n), (Tableau.ofPerm (positionalMax P del) r cands h).optimal = {c}) ↔ ¬{i : ι | P i k'} ⊆ {i : ι | P i k}

Of two single deletions, one is the sole optimum under some ranking exactly when some constraint protects the other position and not its own.