Late merger

Late merger introduces a sub-constituent of a moved phrase countercyclically at a non-base position of its movement chain: adjuncts in [Leb88], the NP restrictor of a determiner in [TH09]'s wholesale late merger, degree clauses in [BP04b]. The flavors differ only in which chain positions admit the merger and share one Condition C profile: late merger bleeds Condition C exactly when an admissible position lies strictly above the pronoun binder. LateMergerBleeds is that profile, polymorphic in the position type and the admissibility predicate, and WLMBleedsCondC its case-licensing instance on ChainPosition, whose admissible positions are those where the resulting DP receives case; [Gon22] shows that reconstruction under scrambling tracks these case positions rather than the A/Ā distinction.

References

• [Leb88]
• [TH09]
• [BP04b]
• [Gon22]

def Minimalist.LateMergerBleeds {α : Type u_1} (admissible : α → Prop) (height : α → ℕ) (chain : List α) (binder : ℕ) : Prop

Late merger bleeds Condition C when an admissible chain position lies strictly above the binder.

Equations

• Minimalist.LateMergerBleeds admissible height chain binder = ∃ (p : α), p ∈ chain ∧ admissible p ∧ binder < height p

@[instance_reducible]

instance Minimalist.instDecidableLateMergerBleedsOfDecidablePred {α : Type u_1} {admissible : α → Prop} {height : α → ℕ} {chain : List α} {binder : ℕ} [DecidablePred admissible] : Decidable (LateMergerBleeds admissible height chain binder)

Equations

• Minimalist.instDecidableLateMergerBleedsOfDecidablePred = Minimalist.instDecidableLateMergerBleedsOfDecidablePred._aux_1

theorem Minimalist.lateMergerBleeds_cons_of {α : Type u_1} {admissible : α → Prop} {height : α → ℕ} {chain : List α} {binder : ℕ} (p : α) (hp : admissible p) (hgt : binder < height p) : LateMergerBleeds admissible height (p :: chain) binder

An admissible position above the binder bleeds Condition C.

theorem Minimalist.LateMergerBleeds.cons {α : Type u_1} {admissible : α → Prop} {height : α → ℕ} {chain : List α} {binder : ℕ} (p : α) (h : LateMergerBleeds admissible height chain binder) : LateMergerBleeds admissible height (p :: chain) binder

Adding a chain position never removes bleeding.

theorem Minimalist.not_lateMergerBleeds_of_le {α : Type u_1} {admissible : α → Prop} {height : α → ℕ} {chain : List α} {binder : ℕ} (h : ∀ (p : α), p ∈ chain → height p ≤ binder) : ¬LateMergerBleeds admissible height chain binder

A chain at or below the binder forces reconstruction, whatever is admissible.

theorem Minimalist.not_lateMergerBleeds_of_none {α : Type u_1} {admissible : α → Prop} {height : α → ℕ} {chain : List α} {binder : ℕ} (h : ∀ (p : α), p ∈ chain → ¬admissible p) : ¬LateMergerBleeds admissible height chain binder

A chain without an admissible position forces reconstruction, whatever the heights.

structure Minimalist.ChainPosition : Type

A position on a movement chain: its height and whether it admits the late merger, for NP restrictors whether the DP receives case there.

• height : ℕ
• admissible : Bool

@[instance_reducible]

instance Minimalist.instDecidableEqChainPosition : DecidableEq ChainPosition

Equations

• Minimalist.instDecidableEqChainPosition = Minimalist.instDecidableEqChainPosition.decEq

def Minimalist.instDecidableEqChainPosition.decEq (x✝ x✝¹ : ChainPosition) : Decidable (x✝ = x✝¹)

Equations

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

def Minimalist.instReprChainPosition.repr : ChainPosition → ℕ → Std.Format

Equations

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

@[instance_reducible]

instance Minimalist.instReprChainPosition : Repr ChainPosition

Equations

• Minimalist.instReprChainPosition = { reprPrec := Minimalist.instReprChainPosition.repr }

def Minimalist.WLMBleedsCondC (chain : List ChainPosition) (binder : ℕ) : Prop

Wholesale late merger of an NP restrictor bleeds Condition C when a case position lies strictly above the binder ([TH09], [Gon22]'s condition (2)).

Equations

• Minimalist.WLMBleedsCondC chain binder = Minimalist.LateMergerBleeds (fun (x : Minimalist.ChainPosition) => x.admissible = true) Minimalist.ChainPosition.height chain binder

@[instance_reducible]

instance Minimalist.instDecidableWLMBleedsCondC (chain : List ChainPosition) (binder : ℕ) : Decidable (WLMBleedsCondC chain binder)

Equations

• Minimalist.instDecidableWLMBleedsCondC chain binder = Minimalist.instDecidableWLMBleedsCondC._aux_1 chain binder

theorem Minimalist.wlmBleedsCondC_cons_of {chain : List ChainPosition} {binder h : ℕ} (hgt : binder < h) : WLMBleedsCondC ({ height := h, admissible := true } :: chain) binder

A case position above the binder bleeds Condition C.

theorem Minimalist.not_wlmBleedsCondC_of_none {chain : List ChainPosition} {binder : ℕ} (h : ∀ (p : ChainPosition), p ∈ chain → p.admissible = false) : ¬WLMBleedsCondC chain binder

A chain without a case position forces reconstruction.