Feeding and bleeding

Kiparsky classifies how one rule bears on another by what applying the first does to the second's conditions: the first feeds the second when it creates them and bleeds it when it destroys them. Over any rules, each with a condition under which it fires and an effect on the state it applies to, the two notions need only a firing predicate and an application map, so they serve phonological rules, postsyntactic impoverishment, and syntactic operations alike. The rules may come from different modules, as when impoverishment of a structure feeds metathesis of its linearization.

Main definitions

• RuleInteraction.Feeds, RuleInteraction.Bleeds: applying one rule creates, or destroys, the conditions under which another fires.

Main results

• RuleInteraction.feeds_iff_bleeds_not: feeding a rule is bleeding the rule that fires where it does not.

References

• [Kip68]

def RuleInteraction.Feeds {R : Type u_1} {R' : Type u_2} {S : Type u_3} (apply : R → S → S) (fires : R' → S → Prop) (a : R) (b : R') (s : S) : Prop

Applying a feeds b at s when b does not fire at s but fires once a has applied.

Equations

• RuleInteraction.Feeds apply fires a b s = (¬fires b s ∧ fires b (apply a s))

def RuleInteraction.Bleeds {R : Type u_1} {R' : Type u_2} {S : Type u_3} (apply : R → S → S) (fires : R' → S → Prop) (a : R) (b : R') (s : S) : Prop

Applying a bleeds b at s when b fires at s but not once a has applied.

Equations

• RuleInteraction.Bleeds apply fires a b s = (fires b s ∧ ¬fires b (apply a s))

@[instance_reducible]

instance RuleInteraction.instDecidableFeeds {R : Type u_1} {R' : Type u_2} {S : Type u_3} {apply : R → S → S} {fires : R' → S → Prop} {a : R} {b : R'} {s : S} [(b : R') → (s : S) → Decidable (fires b s)] : Decidable (Feeds apply fires a b s)

Equations

• RuleInteraction.instDecidableFeeds = { decide := decide ¬fires b s && decide (fires b (apply a s)), reflects_decide := ⋯ }

@[instance_reducible]

instance RuleInteraction.instDecidableBleeds {R : Type u_1} {R' : Type u_2} {S : Type u_3} {apply : R → S → S} {fires : R' → S → Prop} {a : R} {b : R'} {s : S} [(b : R') → (s : S) → Decidable (fires b s)] : Decidable (Bleeds apply fires a b s)

Equations

• RuleInteraction.instDecidableBleeds = { decide := decide (fires b s) && decide ¬fires b (apply a s), reflects_decide := ⋯ }

theorem RuleInteraction.feeds_iff_bleeds_not {R : Type u_1} {R' : Type u_2} {S : Type u_3} {apply : R → S → S} {fires : R' → S → Prop} {a : R} {b : R'} {s : S} : Feeds apply fires a b s ↔ Bleeds apply (fun (b : R') (s : S) => ¬fires b s) a b s