Phrasal locality of conditioning

A trigger may condition the Vocabulary Item of a head only if no phrasal boundary separates them. In Bobaljik's formulation no maximal projection may intervene, so suppletion of a head by another is restricted to synthetic formations, in which Merger or head movement has brought the trigger into the target's complex head. Bobaljik and Harley's refinement lets no phrasal projection at all intervene, which renders specifiers non-local, so that a head is local only to the material of its complex head and to its complement. The boundaries crossed going from the target to the trigger are the nodes that dominate the target but not the trigger. The word-internal domains of cycles and pruning are in Locality.lean.

A proform stands for a phrase of its category, so it strands one node from another when a phrase of its category separates them. The refined formulation is the absence of every such phrase: a trigger may condition a head exactly when no proform strands it from the head.

Embedding a phrase in a larger tree leaves the locality of its heads unchanged when the phrase's root is phrasal: everything outside the phrase is separated from its heads by that root, and everything inside is related to them as it was.

Main definitions

• DistributedMorphology.MayCondition, DistributedMorphology.MayCondition': the two formulations of locality.
• DistributedMorphology.Strands: a proform of a category strands one node from another.
• DistributedMorphology.localSet, DistributedMorphology.localLabels: the labels of the terminals that may condition a head under the refined formulation, as a set and as a list.
• DistributedMorphology.x0At: the complex head containing a node.

Main statements

• DistributedMorphology.mayCondition'_iff_forall_not_strands: a trigger may condition a head under the refined formulation exactly when no proform strands it from the head.
• DistributedMorphology.localSet_replaceAt, DistributedMorphology.x0At_replaceAt: embedding a phrase leaves the complex heads of its nodes and the labels local to them unchanged.

References

• [Bob12]
• [BH17]
• [Har14b]
• [vC14]

The two formulations

def DistributedMorphology.crossed (α β : Core.Order.TreePath) : List Core.Order.TreePath

The nodes crossed going from α to β, those that dominate α and not β.

Equations

• DistributedMorphology.crossed α β = List.filter (fun (p : Core.Order.TreePath) => decide ¬p ≤ β) (List.map Core.Order.TreePath.mk α.toList.inits)

theorem DistributedMorphology.mem_crossed {α β p : Core.Order.TreePath} : p ∈ crossed α β ↔ p ≤ α ∧ ¬p ≤ β

def DistributedMorphology.MayCondition {C : Type u_1} {W : Type u_2} [DecidableEq C] (t : PhraseStructure.Tree C W) (α β : Core.Order.TreePath) : Prop

Locality, Bobaljik's formulation. A trigger at β may condition the head at α when no maximal projection is crossed going from α to β.

Equations

• DistributedMorphology.MayCondition t α β = ∀ p ∈ DistributedMorphology.crossed α β, t.IsHeadAt p ∨ ¬PhraseStructure.IsMaximalCategory t.ProjectsAt t.AdjoinsAt p

def DistributedMorphology.MayCondition' {C : Type u_1} {W : Type u_2} (t : PhraseStructure.Tree C W) (α β : Core.Order.TreePath) : Prop

Locality, the refined formulation. A trigger at β may condition the head at α when no phrasal node at all is crossed going from α to β.

Equations

• DistributedMorphology.MayCondition' t α β = ∀ p ∈ DistributedMorphology.crossed α β, t.IsHeadAt p

@[instance_reducible]

instance DistributedMorphology.instDecidableMayCondition {C : Type u_1} {W : Type u_2} [DecidableEq C] (t : PhraseStructure.Tree C W) (α β : Core.Order.TreePath) : Decidable (MayCondition t α β)

Equations

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

@[instance_reducible]

instance DistributedMorphology.instDecidableMayCondition' {C : Type u_1} {W : Type u_2} (t : PhraseStructure.Tree C W) (α β : Core.Order.TreePath) : Decidable (MayCondition' t α β)

Equations

• DistributedMorphology.instDecidableMayCondition' t α β = List.decidableBAll t.IsHeadAt (DistributedMorphology.crossed α β)

theorem DistributedMorphology.MayCondition'.mayCondition {C : Type u_1} {W : Type u_2} [DecidableEq C] {t : PhraseStructure.Tree C W} {α β : Core.Order.TreePath} (h : MayCondition' t α β) : MayCondition t α β

The refined formulation is the stricter one.

theorem DistributedMorphology.mayCondition'_iff {C : Type u_1} {W : Type u_2} {t : PhraseStructure.Tree C W} {α β : Core.Order.TreePath} : MayCondition' t α β ↔ ∀ p ≤ α, ¬p ≤ β → t.IsHeadAt p

Pronominal stranding

def DistributedMorphology.Replaceable {C : Type u_1} {W : Type u_2} (X : C) (t : PhraseStructure.Tree C W) (p : Core.Order.TreePath) : Prop

A proform of category X may stand for the node at p when it is a phrase of category X.

Equations

• DistributedMorphology.Replaceable X t p = ∃ s ∈ RoseTree.subtreeAt t p.toList, PhraseStructure.Tree.isHead s = false ∧ s.value.cat = X

def DistributedMorphology.Strands {C : Type u_1} {W : Type u_2} (X : C) (t : PhraseStructure.Tree C W) (α β : Core.Order.TreePath) : Prop

A proform of category X strands the node at β from the node at α when it may stand for a phrase that contains α and not β.

Equations

• DistributedMorphology.Strands X t α β = ∃ p ∈ DistributedMorphology.crossed α β, DistributedMorphology.Replaceable X t p

@[instance_reducible]

instance DistributedMorphology.instDecidableReplaceableOfDecidableEq {C : Type u_1} {W : Type u_2} [DecidableEq C] (X : C) (t : PhraseStructure.Tree C W) (p : Core.Order.TreePath) : Decidable (Replaceable X t p)

Equations

• DistributedMorphology.instDecidableReplaceableOfDecidableEq X t p = DistributedMorphology.instDecidableReplaceableOfDecidableEq._aux_1 X t p

@[instance_reducible]

instance DistributedMorphology.instDecidableStrandsOfDecidableEq {C : Type u_1} {W : Type u_2} [DecidableEq C] (X : C) (t : PhraseStructure.Tree C W) (α β : Core.Order.TreePath) : Decidable (Strands X t α β)

Equations

• DistributedMorphology.instDecidableStrandsOfDecidableEq X t α β = List.decidableBEx (DistributedMorphology.Replaceable X t) (DistributedMorphology.crossed α β)

theorem DistributedMorphology.not_replaceable_of_isHeadAt {C : Type u_1} {W : Type u_2} {X : C} {t : PhraseStructure.Tree C W} {p : Core.Order.TreePath} (h : t.IsHeadAt p) : ¬Replaceable X t p

theorem DistributedMorphology.mayCondition'_iff_forall_not_strands {C : Type u_1} {W : Type u_2} {t : PhraseStructure.Tree C W} {α β : Core.Order.TreePath} : MayCondition' t α β ↔ ∀ (X : C), ¬Strands X t α β

Locality is the absence of stranding. A trigger may condition a head under the refined formulation exactly when no proform strands it from the head.

Local labels and complex heads

def DistributedMorphology.localSet {C : Type u_1} {W : Type u_2} (t : PhraseStructure.Tree C W) (α : Core.Order.TreePath) : Set (C × W)

The labels of the terminals that may condition the head at α under the refined formulation.

Equations

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

def DistributedMorphology.localLabels {C : Type u_1} {W : Type u_2} (t : PhraseStructure.Tree C W) (α : Core.Order.TreePath) : List (C × W)

The labels of the terminals that may condition the head at α, in the order of the yield.

Equations

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

theorem DistributedMorphology.mem_localSet_iff {C : Type u_1} {W : Type u_2} {t : PhraseStructure.Tree C W} {α : Core.Order.TreePath} {l : C × W} : l ∈ localSet t α ↔ l ∈ localLabels t α

def DistributedMorphology.x0At {C : Type u_1} {W : Type u_2} (t : PhraseStructure.Tree C W) (α : Core.Order.TreePath) : Option (PhraseStructure.Tree C W)

The complex head containing the node at α, its highest head-level ancestor.

Equations

• DistributedMorphology.x0At t α = (List.find? (fun (p : List ℕ) => Option.all PhraseStructure.Tree.isHead (RoseTree.subtreeAt t p)) α.toList.inits).bind (RoseTree.subtreeAt t)

Embedding

theorem DistributedMorphology.isHeadAt_replaceAt_append {C : Type u_1} {W : Type u_2} {E t : PhraseStructure.Tree C W} {h : List ℕ} (hE : (RoseTree.subtreeAt E h).isSome = true) (q : List ℕ) : PhraseStructure.Tree.IsHeadAt (RoseTree.replaceAt E h t) { toList := h ++ q } ↔ t.IsHeadAt { toList := q }

theorem DistributedMorphology.mayCondition'_replaceAt_append {C : Type u_1} {W : Type u_2} {E t : PhraseStructure.Tree C W} {h : List ℕ} (hE : (RoseTree.subtreeAt E h).isSome = true) (α γ : List ℕ) : MayCondition' (RoseTree.replaceAt E h t) { toList := h ++ α } { toList := h ++ γ } ↔ MayCondition' t { toList := α } { toList := γ }

Within an embedded phrase, locality is what it was in the phrase.

theorem DistributedMorphology.not_mayCondition'_replaceAt {C : Type u_1} {W : Type u_2} {E t : PhraseStructure.Tree C W} {h : List ℕ} (hE : (RoseTree.subtreeAt E h).isSome = true) (ht : t.isHead = false) (α : List ℕ) {β : Core.Order.TreePath} (hβ : ¬{ toList := h } ≤ β) : ¬MayCondition' (RoseTree.replaceAt E h t) { toList := h ++ α } β

Nothing outside an embedded phrase with a phrasal root may condition a head within it.

theorem DistributedMorphology.localSet_replaceAt {C : Type u_1} {W : Type u_2} {E t : PhraseStructure.Tree C W} {h : List ℕ} (hE : (RoseTree.subtreeAt E h).isSome = true) (ht : t.isHead = false) (α : List ℕ) : localSet (RoseTree.replaceAt E h t) { toList := h ++ α } = localSet t { toList := α }

Embedding a phrase with a phrasal root leaves the labels local to its heads unchanged.

theorem DistributedMorphology.x0At_replaceAt {C : Type u_1} {W : Type u_2} {E t : PhraseStructure.Tree C W} {h : List ℕ} (hE : (RoseTree.subtreeAt E h).isSome = true) (ht : t.isHead = false) (α : List ℕ) : x0At (RoseTree.replaceAt E h t) { toList := h ++ α } = x0At t { toList := α }

Embedding a phrase with a phrasal root leaves the complex heads of its nodes unchanged.

theorem DistributedMorphology.strands_replaceAt_congr {C : Type u_1} {W : Type u_2} {E : PhraseStructure.Tree C W} {h : List ℕ} {t₁ t₂ : PhraseStructure.Tree C W} (hE : (RoseTree.subtreeAt E h).isSome = true) (h₁ : t₁.isHead = false) (h₂ : t₂.isHead = false) (hv : RoseTree.value t₁ = RoseTree.value t₂) {α : List ℕ} (hα : ∀ (p : List ℕ), p <+: α → p ≠ [] → RoseTree.subtreeAt t₁ p = RoseTree.subtreeAt t₂ p) (X : C) (β : Core.Order.TreePath) : Strands X (RoseTree.replaceAt E h t₁) { toList := h ++ α } β ↔ Strands X (RoseTree.replaceAt E h t₂) { toList := h ++ α } β

Two phrases with phrasal roots of one label and the same nodes along the path to α are stranded alike from α, wherever they are embedded.