Root categorization

A Root is categorized by a functional head, and the configurations proposed for it differ in how the Root and its internal argument are merged. The Root may be the complement of the categorizer and take the argument as its own complement, or it may be merged with the categorizer as a modifier, the argument then the categorizer's complement. Head movement brings the Root into the categorizer's complex head in the first configuration, where Direct Merge puts it in the second, so morphology meets the two in one shape.

This file proves that no observable that sees only the complex head containing the Root and the labels local to it can tell the two configurations apart, and that whether the Root labels a phrase of its own is the only further information that can. An observable is invariant across the configurations exactly when it factors through that profile, and every observable factors through the profile together with that one bit. The invariance holds wherever the configured phrase is embedded. An argument in the specifier of the categorizer, by contrast, is not local to the Root, so locality does separate that configuration from the other two.

Pronominalization reads what locality reads, whether a phrase separates the Root from its argument, since a proform of some category strands the argument exactly when the argument may not condition the Root. Neither attachment separates them, so pronominalization cannot decide between the attachments, in any context. Selection reads the further bit, if a selection restriction relates an argument to the head it is merged with: the argument is merged with the Root under the complement attachment and with the categorizer under the modifier attachment.

Main definitions

• DistributedMorphology.RootCategorization.Attachment: the Root merged as a complement or as a modifier.
• DistributedMorphology.RootCategorization.profile: the complex head containing a node with the labels local to it.
• DistributedMorphology.RootCategorization.rootProjects: the Root labels a phrase.

Main statements

• profile_replaceAt_eq: the two attachments give the Root one profile, in every context.
• invariant_iff_factorsThrough: an observable is invariant across the attachments exactly when it factors through the profile.
• injective_profile_rootProjects: the profile and whether the Root projects determine the configuration, so every observable factors through them.
• strands_replaceAt_iff: a proform strands from the Root under one attachment whatever it strands under the other, in every context.

Implementation notes

• The configurations are taken after head movement, as morphology receives them, the Root's base position marked by a trace. The argument is a terminal of category D, the label of a DP carrying the features that condition the Root.
• The specifier configuration puts the Root in the categorizer's complement and the argument in its specifier, as Embick's resultative participles do.
• The linking hypotheses are that a proform stands for a phrase of its category (DistributedMorphology.Replaceable) and that a selection restriction relates a node to the head it is merged with (selector).

References

• [AL17]
• [Har14b]
• [Emb04]
• [BH17]
• [vC14]

inductive DistributedMorphology.RootCategorization.Cat : Type

The categories of a categorized Root's phrase are the Root's, a categorizer's, that of a functional head that categorizes nothing, and those of the DPs and PPs it combines with.

• root : Cat
• cat (x : Categorizer) : Cat
• f : Cat
• d : Cat
• p : Cat

def DistributedMorphology.RootCategorization.instDecidableEqCat.decEq (x✝ x✝¹ : Cat) : Decidable (x✝ = x✝¹)

Equations

• One or more equations did not get rendered due to their size.
• DistributedMorphology.RootCategorization.instDecidableEqCat.decEq DistributedMorphology.RootCategorization.Cat.root DistributedMorphology.RootCategorization.Cat.root = isTrue ⋯
• DistributedMorphology.RootCategorization.instDecidableEqCat.decEq DistributedMorphology.RootCategorization.Cat.root (DistributedMorphology.RootCategorization.Cat.cat x_2) = isFalse ⋯
• DistributedMorphology.RootCategorization.instDecidableEqCat.decEq (DistributedMorphology.RootCategorization.Cat.cat x_2) DistributedMorphology.RootCategorization.Cat.root = isFalse ⋯
• DistributedMorphology.RootCategorization.instDecidableEqCat.decEq (DistributedMorphology.RootCategorization.Cat.cat x_2) DistributedMorphology.RootCategorization.Cat.f = isFalse ⋯
• DistributedMorphology.RootCategorization.instDecidableEqCat.decEq (DistributedMorphology.RootCategorization.Cat.cat x_2) DistributedMorphology.RootCategorization.Cat.d = isFalse ⋯
• DistributedMorphology.RootCategorization.instDecidableEqCat.decEq (DistributedMorphology.RootCategorization.Cat.cat x_2) DistributedMorphology.RootCategorization.Cat.p = isFalse ⋯
• DistributedMorphology.RootCategorization.instDecidableEqCat.decEq DistributedMorphology.RootCategorization.Cat.f (DistributedMorphology.RootCategorization.Cat.cat x_2) = isFalse ⋯
• DistributedMorphology.RootCategorization.instDecidableEqCat.decEq DistributedMorphology.RootCategorization.Cat.f DistributedMorphology.RootCategorization.Cat.f = isTrue ⋯
• DistributedMorphology.RootCategorization.instDecidableEqCat.decEq DistributedMorphology.RootCategorization.Cat.d (DistributedMorphology.RootCategorization.Cat.cat x_2) = isFalse ⋯
• DistributedMorphology.RootCategorization.instDecidableEqCat.decEq DistributedMorphology.RootCategorization.Cat.d DistributedMorphology.RootCategorization.Cat.d = isTrue ⋯
• DistributedMorphology.RootCategorization.instDecidableEqCat.decEq DistributedMorphology.RootCategorization.Cat.p (DistributedMorphology.RootCategorization.Cat.cat x_2) = isFalse ⋯
• DistributedMorphology.RootCategorization.instDecidableEqCat.decEq DistributedMorphology.RootCategorization.Cat.p DistributedMorphology.RootCategorization.Cat.p = isTrue ⋯

@[instance_reducible]

instance DistributedMorphology.RootCategorization.instDecidableEqCat : DecidableEq Cat

Equations

• DistributedMorphology.RootCategorization.instDecidableEqCat = DistributedMorphology.RootCategorization.instDecidableEqCat.decEq

def DistributedMorphology.RootCategorization.instReprCat.repr : Cat → ℕ → Std.Format

Equations

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

@[instance_reducible]

instance DistributedMorphology.RootCategorization.instReprCat : Repr Cat

Equations

• DistributedMorphology.RootCategorization.instReprCat = { reprPrec := DistributedMorphology.RootCategorization.instReprCat.repr }

@[instance_reducible]

instance DistributedMorphology.RootCategorization.instFintypeCat : Fintype Cat

Equations

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

structure DistributedMorphology.RootCategorization.Lexicon (W : Type u_2) : Type u_2

The material of a categorized Root is its categorizer and the words of the Root, the categorizer and the argument.

• x : Categorizer
• root : W
• head : W
• arg : W

def DistributedMorphology.RootCategorization.complexHead {W : Type u_1} (L : Lexicon W) : PhraseStructure.Tree Cat W

The complex head of the categorizer with the Root adjoined to it.

Equations

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

inductive DistributedMorphology.RootCategorization.Attachment : Type

How the Root is merged with its categorizer.

• complement : Attachment

  The Root is the categorizer's complement and takes the argument as its own.

• modifier : Attachment

  The Root modifies the categorizer, whose complement the argument is.

@[instance_reducible]

instance DistributedMorphology.RootCategorization.instDecidableEqAttachment : DecidableEq Attachment

Equations

• DistributedMorphology.RootCategorization.instDecidableEqAttachment x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

@[instance_reducible]

instance DistributedMorphology.RootCategorization.instReprAttachment : Repr Attachment

Equations

• DistributedMorphology.RootCategorization.instReprAttachment = { reprPrec := DistributedMorphology.RootCategorization.instReprAttachment.repr }

def DistributedMorphology.RootCategorization.instReprAttachment.repr : Attachment → ℕ → Std.Format

Equations

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

def DistributedMorphology.RootCategorization.Attachment.tree {W : Type u_1} (L : Lexicon W) : Attachment → PhraseStructure.Tree Cat W

The phrase of a categorized Root after head movement.

Equations

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

def DistributedMorphology.RootCategorization.specifierTree {W : Type u_1} (L : Lexicon W) : PhraseStructure.Tree Cat W

The phrase with the Root in the categorizer's complement and the argument in its specifier.

Equations

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

def DistributedMorphology.RootCategorization.profile {W : Type u_1} (t : PhraseStructure.Tree Cat W) (α : Core.Order.TreePath) : Option (PhraseStructure.Tree Cat W) × Set (Cat × W)

The profile of the node at α is the complex head containing it together with the labels that may condition it.

Equations

• DistributedMorphology.RootCategorization.profile t α = (DistributedMorphology.x0At t α, DistributedMorphology.localSet t α)

def DistributedMorphology.RootCategorization.rootProjects {W : Type u_1} (t : PhraseStructure.Tree Cat W) : Bool

The Root labels a phrase.

Equations

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

def DistributedMorphology.RootCategorization.rootPos : Core.Order.TreePath

The position of the Root in a configured phrase.

Equations

• DistributedMorphology.RootCategorization.rootPos = { toList := [0, 0] }

theorem DistributedMorphology.RootCategorization.localLabels_tree {W : Type u_1} (a : Attachment) (L : Lexicon W) : localLabels (Attachment.tree L a) rootPos = [(Cat.root, L.root), (Cat.cat L.x, L.head), (Cat.d, L.arg)]

theorem DistributedMorphology.RootCategorization.x0At_tree {W : Type u_1} (a : Attachment) (L : Lexicon W) : x0At (Attachment.tree L a) rootPos = some (complexHead L)

theorem DistributedMorphology.RootCategorization.profile_tree {W : Type u_1} (a : Attachment) (L : Lexicon W) : profile (Attachment.tree L a) rootPos = (some (complexHead L), {l : Cat × W | l ∈ [(Cat.root, L.root), (Cat.cat L.x, L.head), (Cat.d, L.arg)]})

theorem DistributedMorphology.RootCategorization.profile_eq {W : Type u_1} (L : Lexicon W) : profile (Attachment.tree L Attachment.complement) rootPos = profile (Attachment.tree L Attachment.modifier) rootPos

The two attachments give the Root one profile.

theorem DistributedMorphology.RootCategorization.profile_replaceAt {W : Type u_1} {E : PhraseStructure.Tree Cat W} {h : List ℕ} (hE : (RoseTree.subtreeAt E h).isSome = true) (a : Attachment) (L : Lexicon W) : profile (RoseTree.replaceAt E h (Attachment.tree L a)) { toList := h ++ rootPos.toList } = profile (Attachment.tree L a) rootPos

Embedding a configured phrase leaves the profile of its Root unchanged.

theorem DistributedMorphology.RootCategorization.profile_replaceAt_eq {W : Type u_1} {E : PhraseStructure.Tree Cat W} {h : List ℕ} (hE : (RoseTree.subtreeAt E h).isSome = true) (L : Lexicon W) : profile (RoseTree.replaceAt E h (Attachment.tree L Attachment.complement)) { toList := h ++ rootPos.toList } = profile (RoseTree.replaceAt E h (Attachment.tree L Attachment.modifier)) { toList := h ++ rootPos.toList }

In every context the two attachments give the Root one profile.

theorem DistributedMorphology.RootCategorization.profile_specifier_ne {W : Type u_1} (a : Attachment) (L : Lexicon W) : profile (specifierTree L) { toList := [1, 0, 0] } ≠ profile (Attachment.tree L a) rootPos

An argument in the specifier is not local to the Root.

Invariance and completeness

theorem DistributedMorphology.RootCategorization.lexicon_eq_of_profile_eq {W : Type u_1} {a a' : Attachment} {L L' : Lexicon W} (h : profile (Attachment.tree L a) rootPos = profile (Attachment.tree L' a') rootPos) : L = L'

@[reducible, inline]

abbrev DistributedMorphology.RootCategorization.Observable (W : Type u_2) (X : Type u_3) : Type (max u_3 u_2)

An observable of a phrase and the position of its Root.

Equations

• DistributedMorphology.RootCategorization.Observable W X = (PhraseStructure.Tree DistributedMorphology.RootCategorization.Cat W × Core.Order.TreePath → X)

theorem DistributedMorphology.RootCategorization.invariant_iff_factorsThrough {W : Type u_1} {X : Type u_2} (O : Observable W X) : (∀ (L : Lexicon W), O (Attachment.tree L Attachment.complement, rootPos) = O (Attachment.tree L Attachment.modifier, rootPos)) ↔ Function.FactorsThrough (fun (p : Attachment × Lexicon W) => O (Attachment.tree p.2 p.1, rootPos)) fun (p : Attachment × Lexicon W) => profile (Attachment.tree p.2 p.1) rootPos

Invariance. An observable takes one value on the two attachments of every Root exactly when it factors through the profile.

theorem DistributedMorphology.RootCategorization.rootProjects_complement {W : Type u_1} (L : Lexicon W) : rootProjects (Attachment.tree L Attachment.complement) = true

theorem DistributedMorphology.RootCategorization.rootProjects_modifier {W : Type u_1} (L : Lexicon W) : rootProjects (Attachment.tree L Attachment.modifier) = false

theorem DistributedMorphology.RootCategorization.injective_profile_rootProjects {W : Type u_1} : Function.Injective fun (p : Attachment × Lexicon W) => (profile (Attachment.tree p.2 p.1) rootPos, rootProjects (Attachment.tree p.2 p.1))

Completeness. The profile and whether the Root labels a phrase determine the configuration.

theorem DistributedMorphology.RootCategorization.factorsThrough_profile_rootProjects {W : Type u_1} {X : Type u_2} (O : Observable W X) : Function.FactorsThrough (fun (p : Attachment × Lexicon W) => O (Attachment.tree p.2 p.1, rootPos)) fun (p : Attachment × Lexicon W) => (profile (Attachment.tree p.2 p.1) rootPos, rootProjects (Attachment.tree p.2 p.1))

Every observable is a function of the profile and of whether the Root labels a phrase.

Diagnostics

A diagnostic reads a judgment off an observable through a linking hypothesis. Pronominalization reads whether a phrase separates the Root from its argument and cannot decide between the attachments; selection reads the head the argument is merged with, and can.

def DistributedMorphology.RootCategorization.Attachment.argPos : Attachment → Core.Order.TreePath

The position of the argument in a configured phrase.

Equations

• DistributedMorphology.RootCategorization.Attachment.complement.argPos = { toList := [1, 1] }
• DistributedMorphology.RootCategorization.Attachment.modifier.argPos = { toList := [1] }

theorem DistributedMorphology.RootCategorization.mayCondition'_argPos {W : Type u_1} (a : Attachment) (L : Lexicon W) : MayCondition' (Attachment.tree L a) rootPos a.argPos

theorem DistributedMorphology.RootCategorization.not_strands_argPos {W : Type u_1} {E : PhraseStructure.Tree Cat W} {h : List ℕ} (hE : (RoseTree.subtreeAt E h).isSome = true) (a : Attachment) (L : Lexicon W) (X : Cat) : ¬Strands X (RoseTree.replaceAt E h (Attachment.tree L a)) { toList := h ++ rootPos.toList } { toList := h ++ a.argPos.toList }

No proform strands the argument from the Root, under either attachment and in every context.

theorem DistributedMorphology.RootCategorization.strands_replaceAt_iff {W : Type u_1} {E : PhraseStructure.Tree Cat W} {h : List ℕ} (hE : (RoseTree.subtreeAt E h).isSome = true) (L : Lexicon W) (X : Cat) (β : Core.Order.TreePath) : Strands X (RoseTree.replaceAt E h (Attachment.tree L Attachment.complement)) { toList := h ++ rootPos.toList } β ↔ Strands X (RoseTree.replaceAt E h (Attachment.tree L Attachment.modifier)) { toList := h ++ rootPos.toList } β

Pronominalization cannot decide. In every context a proform strands from the Root under one attachment whatever it strands under the other.

theorem DistributedMorphology.RootCategorization.strands_specifier {W : Type u_1} (L : Lexicon W) : Strands (Cat.cat L.x) (specifierTree L) { toList := [1, 0, 0] } { toList := [0] }

A proform of the categorizer's category strands an argument in its specifier from the Root.

def DistributedMorphology.RootCategorization.selector {W : Type u_1} (t : PhraseStructure.Tree Cat W) (β : Core.Order.TreePath) : Option Cat

The category of the head a node below the root is merged with, that of its mother.

Equations

• DistributedMorphology.RootCategorization.selector t β = Option.map PhraseStructure.Tree.cat (RoseTree.subtreeAt t β.parent.toList)

def DistributedMorphology.RootCategorization.argPositions {W : Type u_1} (t : PhraseStructure.Tree Cat W) : List Core.Order.TreePath

The positions of the arguments of a phrase, its DPs.

Equations

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

theorem DistributedMorphology.RootCategorization.argPositions_tree {W : Type u_1} (a : Attachment) (L : Lexicon W) : argPositions (Attachment.tree L a) = [a.argPos]

def DistributedMorphology.RootCategorization.StrandsArgument {W : Type u_1} (X : Cat) : Observable W Prop

A proform of category X strands an argument from the node.

Equations

• DistributedMorphology.RootCategorization.StrandsArgument X o = ∃ β ∈ DistributedMorphology.RootCategorization.argPositions o.1, DistributedMorphology.Strands X o.1 o.2 β

def DistributedMorphology.RootCategorization.SelectsArgument {W : Type u_1} (c : Cat) : Observable W Prop

An argument is merged with a head of category c.

Equations

• DistributedMorphology.RootCategorization.SelectsArgument c o = ∃ β ∈ DistributedMorphology.RootCategorization.argPositions o.1, DistributedMorphology.RootCategorization.selector o.1 β = some c

theorem DistributedMorphology.RootCategorization.factorsThrough_strandsArgument {W : Type u_1} (X : Cat) : Function.FactorsThrough (fun (p : Attachment × Lexicon W) => StrandsArgument X (Attachment.tree p.2 p.1, rootPos)) fun (p : Attachment × Lexicon W) => profile (Attachment.tree p.2 p.1) rootPos

Pronominalization factors through the profile, so it cannot tell the attachments apart.

theorem DistributedMorphology.RootCategorization.selectsArgument_root {W : Type u_1} (a : Attachment) (L : Lexicon W) : SelectsArgument Cat.root (Attachment.tree L a, rootPos) ↔ a = Attachment.complement

Selection can decide. An argument is merged with the Root under the complement attachment and not under the modifier attachment.