Heads of labelled trees

On a tree whose nodes carry categories, the head daughter of a node is the one daughter of its category, the rule the Head Feature Principle imposes on a headed phrase and its head daughter. A node of the clause category with no daughter of that category is exocentric, and so is a node with two daughters of its category, as in a compound or a coordination labelled by its conjuncts' category; a study that resolves such ties supplies its own head relation. A node labelled as the mother of an adjunction is a further segment of its head daughter's category, so the head relation splits into projection and adjunction. The maximal projections of a tree and the MAX-command they generate are read off the tree, and the Head Feature Principle holds along every projection line.

Main definitions

• PhraseStructure.Tree.headIndex?, PhraseStructure.Tree.headIndexAt: the head daughter's index.
• PhraseStructure.Tree.HeadDaughterAt, PhraseStructure.Tree.IsSegmentAt, PhraseStructure.Tree.ProjectsAt, PhraseStructure.Tree.AdjoinsAt: the head relation and its split into projection and adjunction.
• PhraseStructure.Tree.maximalProjectionsAt, PhraseStructure.Tree.maxCommand.
• PhraseStructure.Tree.isHead, PhraseStructure.Tree.IsHeadAt: head-level nodes, a terminal or an adjunction of heads.

Main results

• PhraseStructure.Tree.cat_eq_of_isProjectionOf: a projection has the category of what it projects from.
• PhraseStructure.Tree.maximalProjectionsAt_eq_of_forall_not_isSegmentAt: without adjunction the maximal projections are the nodes that are no head daughter.

References

• [PS94]
• [BP90]

def PhraseStructure.Tree.headIndex? {C : Type u_1} {W : Type u_2} [DecidableEq C] (t : Tree C W) : Option ℕ

The index of the head daughter at the root, the one daughter of the root's category.

Equations

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

def PhraseStructure.Tree.headIndexAt {C : Type u_1} {W : Type u_2} [DecidableEq C] (t : Tree C W) (p : Core.Order.TreePath) : Option ℕ

The index of the head daughter at a position of t.

Equations

• t.headIndexAt p = (RoseTree.subtreeAt t p.toList).bind PhraseStructure.Tree.headIndex?

@[reducible, inline]

abbrev PhraseStructure.Tree.HeadDaughterAt {C : Type u_1} {W : Type u_2} [DecidableEq C] (t : Tree C W) : Core.Order.TreePath → Core.Order.TreePath → Prop

HeadDaughterAt t m d says that d is the head daughter of m in t.

Equations

• t.HeadDaughterAt = PhraseStructure.headDaughterRel t.headIndexAt

@[reducible, inline]

abbrev PhraseStructure.Tree.IsSegmentAt {C : Type u_1} {W : Type u_2} (t : Tree C W) (p : Core.Order.TreePath) : Prop

A position of t is a segment when its label marks the mother of an adjunction.

Equations

• t.IsSegmentAt p = (p ∈ RoseTree.positionsWhere (fun (s : RoseTree (PhraseStructure.Tree.Label C W)) => s.value.IsSegment) t)

@[reducible, inline]

abbrev PhraseStructure.Tree.ProjectsAt {C : Type u_1} {W : Type u_2} [DecidableEq C] (t : Tree C W) : Core.Order.TreePath → Core.Order.TreePath → Prop

ProjectsAt t m d says that m projects from its head daughter d, a new category.

Equations

• t.ProjectsAt = PhraseStructure.headDaughterRel (PhraseStructure.projectionIndex t.headIndexAt t.IsSegmentAt)

@[reducible, inline]

abbrev PhraseStructure.Tree.AdjoinsAt {C : Type u_1} {W : Type u_2} [DecidableEq C] (t : Tree C W) : Core.Order.TreePath → Core.Order.TreePath → Prop

AdjoinsAt t m d says that m is the segment above its host d, of one category with it.

Equations

• t.AdjoinsAt = PhraseStructure.headDaughterRel (PhraseStructure.adjunctionIndex t.headIndexAt t.IsSegmentAt)

theorem PhraseStructure.Tree.headDaughterAt_eq_sup {C : Type u_1} {W : Type u_2} [DecidableEq C] (t : Tree C W) : t.HeadDaughterAt = t.ProjectsAt ⊔ t.AdjoinsAt

The head daughter of a node is the daughter it projects from or the host it is a segment above.

@[reducible, inline]

abbrev PhraseStructure.Tree.maximalProjectionsAt {C : Type u_1} {W : Type u_2} [DecidableEq C] (t : Tree C W) : Set Core.Order.TreePath

The maximal projections of t, the lowest segments of its maximal categories.

Equations

• t.maximalProjectionsAt = PhraseStructure.maximalProjections t.ProjectsAt t.AdjoinsAt

theorem PhraseStructure.Tree.maximalProjectionsAt_eq_of_forall_not_isSegmentAt {C : Type u_1} {W : Type u_2} [DecidableEq C] {t : Tree C W} (h : ∀ (p : Core.Order.TreePath), ¬t.IsSegmentAt p) : t.maximalProjectionsAt = {p : Core.Order.TreePath | IsMaximalProjection t.HeadDaughterAt p}

On a tree without adjunction the maximal projections are the nodes that are no node's head daughter.

@[reducible, inline]

abbrev PhraseStructure.Tree.maxCommand {C : Type u_1} {W : Type u_2} [DecidableEq C] (t : Tree C W) : SetRel Core.Order.TreePath Core.Order.TreePath

MAX-command on t is generated by its maximal projections.

Equations

• t.maxCommand = PhraseStructure.commandRelation t.maximalProjectionsAt

@[simp]

theorem PhraseStructure.Tree.headIndex?_terminal {C : Type u_1} {W : Type u_2} [DecidableEq C] (c : C) (w : W) : (terminal c w).headIndex? = none

theorem PhraseStructure.Tree.cat_eq_of_headIndex? {C : Type u_1} {W : Type u_2} [DecidableEq C] {t : Tree C W} {i : ℕ} (h : t.headIndex? = some i) : ∃ (d : RoseTree (Label C W)), (RoseTree.children t)[i]? = some d ∧ cat d = t.cat

The head daughter has its mother's category.

theorem PhraseStructure.Tree.cat_eq_of_isProjectionOf {C : Type u_1} {W : Type u_2} [DecidableEq C] {t : Tree C W} {h p : Core.Order.TreePath} (hp : IsProjectionOf t.HeadDaughterAt h p) {s s' : Tree C W} (hs : RoseTree.subtreeAt t p.toList = some s) (hs' : RoseTree.subtreeAt t h.toList = some s') : s.cat = s'.cat

A projection has the category of what it projects from.

Head-level nodes

def PhraseStructure.Tree.isHead {C : Type u_1} {W : Type u_2} : Tree C W → Bool

A head-level node, an X⁰, is a terminal or an adjunction of heads.

Equations

• PhraseStructure.Tree.isHead (RoseTree.node (PhraseStructure.Tree.Label.terminal a a_1) []) = true
• PhraseStructure.Tree.isHead (RoseTree.node (PhraseStructure.Tree.Label.segment a) ts) = PhraseStructure.Tree.allHeads ts
• x✝.isHead = false

def PhraseStructure.Tree.allHeads {C : Type u_1} {W : Type u_2} : List (Tree C W) → Bool

Every tree of a list is head-level.

Equations

• PhraseStructure.Tree.allHeads [] = true
• PhraseStructure.Tree.allHeads (t :: ts) = (t.isHead && PhraseStructure.Tree.allHeads ts)

theorem PhraseStructure.Tree.allHeads_iff {C : Type u_1} {W : Type u_2} (l : List (Tree C W)) : allHeads l = true ↔ ∀ x ∈ l, x.isHead = true

theorem PhraseStructure.Tree.isHead_of_isHead_replaceAt {C : Type u_1} {W : Type u_2} (s : Tree C W) (q : List ℕ) (t : Tree C W) : (RoseTree.subtreeAt s q).isSome = true → isHead (RoseTree.replaceAt s q t) = true → t.isHead = true

What a head-level node contains is head-level: a head-level tree with t inside has t head-level.

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

The node at position p of t is head-level.

Equations

• t.IsHeadAt p = (Option.all PhraseStructure.Tree.isHead (RoseTree.subtreeAt t p.toList) = true)

@[instance_reducible]

instance PhraseStructure.Tree.instDecidableIsHeadAt {C : Type u_1} {W : Type u_2} (t : Tree C W) (p : Core.Order.TreePath) : Decidable (t.IsHeadAt p)

Equations

• t.instDecidableIsHeadAt p = PhraseStructure.Tree.instDecidableIsHeadAt._aux_1 t p