Projection from heads

Every phrase-structure framework designates in each headed constituent one daughter as its head, and a phrase is a projection of the head reached from it through head daughters. The frameworks differ in how they find the head daughter, so here a head relation H is a parameter, H m d saying that d is the head daughter of m. The levels of projection are derived, as relational properties of nodes rather than parts of their labels: a node is a maximal projection when it is no node's head daughter and a minimal projection when it has no head daughter.

Adjunction makes no new category. The head relation splits into projection P and adjunction A, where A m d says that m is a further segment of the category of its host d, as in May's multimembered projections and Chomsky's two-segment categories. A category dominates what all its segments dominate and excludes what none of them dominates, a category is maximal when no segment of it projects further, and Barker and Pullum's MAX-command is generated by the maximal categories, each read at its lowest segment. Without adjunction these are the maximal projections, and an adjunct to a maximal category commands out of it.

On the positions of a rose tree a head relation is given by the index of each position's head daughter, which makes projection, the levels, categories and the maximal projection decidable.

Main definitions

• PhraseStructure.IsProjectionOf: the reflexive-transitive closure of the head relation.
• PhraseStructure.IsMaximalProjection, PhraseStructure.IsMinimalProjection, PhraseStructure.IsLexicalHeadOf.
• PhraseStructure.segments, PhraseStructure.Includes, PhraseStructure.Excludes, PhraseStructure.Contains: the segments of a category and what it dominates.
• PhraseStructure.IsMaximalCategory, PhraseStructure.maximalProjections, PhraseStructure.maxCommand: maximal categories and MAX-command from them.
• PhraseStructure.headDaughterRel, PhraseStructure.maximalProjectionAt, PhraseStructure.projectionIndex, PhraseStructure.adjunctionIndex: head relations from head-daughter indices on tree positions.

Main results

• PhraseStructure.isLeast_projections_iff, PhraseStructure.exists_isLeast_projections: the maximal projection of a node is the least of its projections, and it exists.
• PhraseStructure.isChain_segments, PhraseStructure.includes_iff, PhraseStructure.excludes_iff: the segments of a category form a chain, so inclusion is decided at the lowest segment and exclusion at the top.
• PhraseStructure.not_includes_of_covBy, PhraseStructure.maxCommand_adjunct: an adjunct is not included in the category it adjoins to, and it MAX-commands out of it.
• PhraseStructure.mem_maxCommand_iff_le: the MAX-command domain of a node that projects further is the cone of the lowest segment of its maximal category.
• PhraseStructure.IsLexicalHeadOf.unique: along a functional head relation a node has one lexical head.
• PhraseStructure.isLeast_maximalProjectionAt: maximalProjectionAt computes the maximal projection.

Implementation notes

A minimal projection is a node with no head daughter, so on a tree whose phrases are not all headed, an exocentric node is minimal as well; on an endocentric tree the minimal projections are the leaves. A leaf that is not its mother's head daughter, such as a pronoun standing for a noun phrase, is minimal and maximal at once. Lasnik and Saito's alternative, on which adjunction makes a further maximal projection, is node-level maximality IsMaximalProjection P on the same relations.

References

• [BP90]
• [May85]
• [Cho86]
• [Cho95b]
• [Cho13]
• [LS92]
• [PS94]
• [KF99]

def PhraseStructure.IsProjectionOf {α : Type u_1} (H : α → α → Prop) (h p : α) : Prop

IsProjectionOf H h p says that p is a projection of h, that is, h is reached from p through head daughters.

Equations

• PhraseStructure.IsProjectionOf H h p = Relation.ReflTransGen H p h

def PhraseStructure.IsMaximalProjection {α : Type u_1} (H : α → α → Prop) (p : α) : Prop

A node is a maximal projection when it projects no further, being no node's head daughter.

Equations

• PhraseStructure.IsMaximalProjection H p = ∀ (m : α), ¬H m p

def PhraseStructure.IsMinimalProjection {α : Type u_1} (H : α → α → Prop) (p : α) : Prop

A node is a minimal projection when it is no projection, having no head daughter.

Equations

• PhraseStructure.IsMinimalProjection H p = ∀ (d : α), ¬H p d

def PhraseStructure.IsLexicalHeadOf {α : Type u_1} (H : α → α → Prop) (h p : α) : Prop

h is the lexical head of p when p projects from h and h is a minimal projection.

Equations

• PhraseStructure.IsLexicalHeadOf H h p = (PhraseStructure.IsProjectionOf H h p ∧ PhraseStructure.IsMinimalProjection H h)

theorem PhraseStructure.IsProjectionOf.refl {α : Type u_1} {H : α → α → Prop} (h : α) : IsProjectionOf H h h

theorem PhraseStructure.IsProjectionOf.head {α : Type u_1} {H : α → α → Prop} {h m d : α} (hmd : H m d) (hd : IsProjectionOf H h d) : IsProjectionOf H h m

theorem PhraseStructure.IsProjectionOf.trans {α : Type u_1} {H : α → α → Prop} {h p q : α} (hp : IsProjectionOf H h p) (hq : IsProjectionOf H p q) : IsProjectionOf H h q

theorem PhraseStructure.isProjectionOf_iff_eq_or {α : Type u_1} {H : α → α → Prop} {h p : α} : IsProjectionOf H h p ↔ p = h ∨ ∃ (d : α), H p d ∧ IsProjectionOf H h d

theorem PhraseStructure.IsMaximalProjection.eq_of_isProjectionOf {α : Type u_1} {H : α → α → Prop} {h p : α} (hp : IsMaximalProjection H p) (hph : IsProjectionOf H p h) : h = p

A maximal projection is a projection of nothing but itself.

theorem PhraseStructure.IsLexicalHeadOf.unique {α : Type u_1} {H : α → α → Prop} (hfun : Relator.RightUnique H) {p h h' : α} (hh : IsLexicalHeadOf H h p) (hh' : IsLexicalHeadOf H h' p) : h = h'

Along a functional head relation a node has one lexical head.

theorem PhraseStructure.IsProjectionOf.le {α : Type u_1} [PartialOrder α] {H : α → α → Prop} (hH : ∀ (m d : α), H m d → m ⋖ d) {h p : α} (hp : IsProjectionOf H h p) : p ≤ h

A projection dominates what it projects from.

theorem PhraseStructure.IsProjectionOf.of_le_of_le {α : Type u_1} [PartialOrder α] {H : α → α → Prop} (hH : ∀ (m d : α), H m d → m ⋖ d) [IsLeftLinear α] {h p x : α} (hp : IsProjectionOf H h p) (hpx : p ≤ x) (hxh : x ≤ h) : IsProjectionOf H h x

Projection lines are intervals, so everything between a projection and its head is a projection of the head.

theorem PhraseStructure.IsProjectionOf.reflTransGen_of_le {α : Type u_1} [PartialOrder α] {H : α → α → Prop} (hH : ∀ (m d : α), H m d → m ⋖ d) [IsLeftLinear α] {h p q : α} (hp : IsProjectionOf H h p) (hq : IsProjectionOf H h q) (hpq : p ≤ q) : Relation.ReflTransGen H p q

Of two projections of one head, the higher is reached from the lower through head daughters.

theorem PhraseStructure.IsProjectionOf.exists_of_lt {α : Type u_1} [PartialOrder α] {H : α → α → Prop} (hH : ∀ (m d : α), H m d → m ⋖ d) [IsLeftLinear α] {h p q : α} (hp : IsProjectionOf H h p) (hq : IsProjectionOf H h q) (hpq : p < q) : ∃ (m : α), H m q

A projection of h below another one is a head daughter.

theorem PhraseStructure.isLeast_projections_iff {α : Type u_1} [PartialOrder α] {H : α → α → Prop} (hH : ∀ (m d : α), H m d → m ⋖ d) [IsLeftLinear α] {h m : α} : IsLeast {p : α | IsProjectionOf H h p} m ↔ IsProjectionOf H h m ∧ IsMaximalProjection H m

The maximal projection of h is the least of its projections.

theorem PhraseStructure.exists_isLeast_projections {α : Type u_1} [PartialOrder α] {H : α → α → Prop} (hH : ∀ (m d : α), H m d → m ⋖ d) [IsLeftLinear α] [WellFoundedLT α] (h : α) : ∃ (m : α), IsLeast {p : α | IsProjectionOf H h p} m

Every node has a maximal projection.

Segments and categories

An adjunction relation A, with A m d saying that m is the segment of a category immediately above its host d, groups nodes into categories: the segments of a category are the nodes joined by adjunction steps. A category dominates what every one of its segments dominates and excludes what none of them dominates; the segments of a category form a chain, so domination by the category is domination by its lowest segment.

def PhraseStructure.segments {α : Type u_1} (A : α → α → Prop) (x : α) : Set α

The segments of the category of x are the nodes joined to x by adjunction steps.

Equations

• PhraseStructure.segments A x = {y : α | Relation.EqvGen A x y}

@[simp]

theorem PhraseStructure.mem_segments_self {α : Type u_1} {A : α → α → Prop} (x : α) : x ∈ segments A x

theorem PhraseStructure.mem_segments_comm {α : Type u_1} {A : α → α → Prop} {x y : α} : y ∈ segments A x ↔ x ∈ segments A y

theorem PhraseStructure.segments_eq_of_mem {α : Type u_1} {A : α → α → Prop} {x y : α} (h : y ∈ segments A x) : segments A y = segments A x

Segments of one category have the same segments.

theorem PhraseStructure.mem_segments_of_reflTransGen {α : Type u_1} {A : α → α → Prop} {x y : α} (h : Relation.ReflTransGen A x y) : y ∈ segments A x

@[simp]

theorem PhraseStructure.segments_bot {α : Type u_1} (x : α) : segments ⊥ x = {x}

Without adjunction every category has one segment.

def PhraseStructure.Includes {α : Type u_1} (A : α → α → Prop) [PartialOrder α] (x y : α) : Prop

The category of x includes y when every segment of it dominates y.

Equations

• PhraseStructure.Includes A x y = ∀ s ∈ PhraseStructure.segments A x, s ≤ y

def PhraseStructure.Excludes {α : Type u_1} (A : α → α → Prop) [PartialOrder α] (x y : α) : Prop

The category of x excludes y when no segment of it dominates y.

Equations

• PhraseStructure.Excludes A x y = ∀ s ∈ PhraseStructure.segments A x, ¬s ≤ y

def PhraseStructure.Contains {α : Type u_1} (A : α → α → Prop) [PartialOrder α] (x y : α) : Prop

The category of x contains y when some segment of it dominates y.

Equations

• PhraseStructure.Contains A x y = ∃ s ∈ PhraseStructure.segments A x, s ≤ y

theorem PhraseStructure.Includes.contains {α : Type u_1} {A : α → α → Prop} [PartialOrder α] {x y : α} (h : Includes A x y) : Contains A x y

theorem PhraseStructure.not_excludes_iff_contains {α : Type u_1} {A : α → α → Prop} [PartialOrder α] {x y : α} : ¬Excludes A x y ↔ Contains A x y

theorem PhraseStructure.includes_congr {α : Type u_1} {A : α → α → Prop} [PartialOrder α] {x x' y : α} (h : x' ∈ segments A x) : Includes A x' y ↔ Includes A x y

theorem PhraseStructure.excludes_congr {α : Type u_1} {A : α → α → Prop} [PartialOrder α] {x x' y : α} (h : x' ∈ segments A x) : Excludes A x' y ↔ Excludes A x y

@[simp]

theorem PhraseStructure.includes_bot {α : Type u_1} [PartialOrder α] {x y : α} : Includes ⊥ x y ↔ x ≤ y

@[simp]

theorem PhraseStructure.excludes_bot {α : Type u_1} [PartialOrder α] {x y : α} : Excludes ⊥ x y ↔ ¬x ≤ y

theorem PhraseStructure.contains_of_covBy {α : Type u_1} {A : α → α → Prop} [PartialOrder α] {m a : α} (ha : m ⋖ a) : Contains A m a

The category an adjunct adjoins to contains it.

theorem PhraseStructure.eq_of_covBy_covBy {α : Type u_1} [PartialOrder α] [IsLeftLinear α] {m m' d : α} (hm : m ⋖ d) (hm' : m' ⋖ d) : m = m'

On a left-linear order a node covers at most one node: it has one mother.

theorem PhraseStructure.not_le_of_covBy {α : Type u_1} [PartialOrder α] {m a d : α} (ha : m ⋖ a) (hd : m ⋖ d) (had : a ≠ d) : ¬a ≤ d

Two distinct daughters of one mother are incomparable.

theorem PhraseStructure.leftUnique_of_covBy {α : Type u_1} {A : α → α → Prop} [PartialOrder α] (hA : ∀ (m d : α), A m d → m ⋖ d) [IsLeftLinear α] : Relator.LeftUnique A

An adjunction relation on a left-linear order has unique mothers.

theorem PhraseStructure.mem_segments_iff {α : Type u_1} {A : α → α → Prop} [PartialOrder α] (hA : ∀ (m d : α), A m d → m ⋖ d) [IsLeftLinear α] (hU : Relator.RightUnique A) {x y : α} : y ∈ segments A x ↔ Relation.ReflTransGen A x y ∨ Relation.ReflTransGen A y x

A segment lies above or below every segment of its category.

theorem PhraseStructure.isChain_segments {α : Type u_1} {A : α → α → Prop} [PartialOrder α] (hA : ∀ (m d : α), A m d → m ⋖ d) [IsLeftLinear α] (hU : Relator.RightUnique A) (x : α) : IsChain (fun (x1 x2 : α) => x1 ≤ x2) (segments A x)

The segments of a category form a chain.

theorem PhraseStructure.includes_iff {α : Type u_1} {A : α → α → Prop} [PartialOrder α] (hA : ∀ (m d : α), A m d → m ⋖ d) [IsLeftLinear α] (hU : Relator.RightUnique A) {x y : α} : Includes A x y ↔ ∀ (s : α), Relation.ReflTransGen A x s → s ≤ y

A category includes what the segments at or below x dominate, since those above dominate whatever x does.

theorem PhraseStructure.excludes_iff {α : Type u_1} {A : α → α → Prop} [PartialOrder α] (hA : ∀ (m d : α), A m d → m ⋖ d) [IsLeftLinear α] (hU : Relator.RightUnique A) {x y : α} : Excludes A x y ↔ ∀ (s : α), Relation.ReflTransGen A s x → ¬s ≤ y

A category excludes what no segment at or above x dominates.

theorem PhraseStructure.includes_iff_forall_le {α : Type u_1} {A : α → α → Prop} [PartialOrder α] (hA : ∀ (m d : α), A m d → m ⋖ d) [IsLeftLinear α] (hU : Relator.RightUnique A) {x y : α} : Includes A x y ↔ x ≤ y ∧ ∀ (q : α), Relation.ReflTransGen A x q → q ≤ y → ∀ (d : α), A q d → d ≤ y

In the form that decides it, inclusion says that x dominates y and that every segment below x that dominates y hands that on to its host.

theorem PhraseStructure.not_includes_of_covBy {α : Type u_1} {A : α → α → Prop} [PartialOrder α] (hA : ∀ (m d : α), A m d → m ⋖ d) {m d a : α} (hmd : A m d) (ha : m ⋖ a) (had : a ≠ d) : ¬Includes A m a

An adjunct is not included in the category it adjoins to, since the host segment does not dominate it.

Maximal categories and MAX-command

With projection P and adjunction A the head relation is P ⊔ A. A category is maximal when no segment of it projects further, and MAX-command is generated by the maximal categories, each read at its lowest segment, the one whose domination is the category's. Without adjunction these are the maximal projections.

def PhraseStructure.IsMaximalCategory {α : Type u_1} (P A : α → α → Prop) (x : α) : Prop

A category is maximal when none of its segments projects further.

Equations

• PhraseStructure.IsMaximalCategory P A x = ∀ s ∈ PhraseStructure.segments A x, PhraseStructure.IsMaximalProjection P s

def PhraseStructure.maximalProjections {α : Type u_1} (P A : α → α → Prop) : Set α

The maximal projections, which generate MAX-command, are the lowest segments of the maximal categories.

Equations

• PhraseStructure.maximalProjections P A = {x : α | PhraseStructure.IsMinimalProjection A x ∧ PhraseStructure.IsMaximalCategory P A x}

theorem PhraseStructure.isMaximalCategory_congr {α : Type u_1} {P A : α → α → Prop} {x x' : α} (h : x' ∈ segments A x) : IsMaximalCategory P A x' ↔ IsMaximalCategory P A x

theorem PhraseStructure.IsMaximalCategory.isMaximalProjection {α : Type u_1} {P A : α → α → Prop} {x : α} (h : IsMaximalCategory P A x) : IsMaximalProjection P x

@[simp]

theorem PhraseStructure.isMaximalCategory_bot {α : Type u_1} {P : α → α → Prop} {x : α} : IsMaximalCategory P ⊥ x ↔ IsMaximalProjection P x

Without adjunction a maximal category is a maximal projection.

@[simp]

theorem PhraseStructure.maximalProjections_bot {α : Type u_1} {P : α → α → Prop} : maximalProjections P ⊥ = {x : α | IsMaximalProjection P x}

theorem PhraseStructure.eq_of_reflTransGen_sup {α : Type u_1} {P A : α → α → Prop} {b x : α} (hb : IsMinimalProjection A b) (hbx : Relation.ReflTransGen (P ⊔ A) b x) (hx : IsMaximalCategory P A x) : x = b

Along the head relation from the lowest segment of a maximal category, no node below is another maximal category: the path would leave the first category by a projection step.

@[reducible, inline]

abbrev PhraseStructure.maxCommand {α : Type u_1} (P A : α → α → Prop) [PartialOrder α] : SetRel α α

MAX-command is generated by the maximal categories.

Equations

• PhraseStructure.maxCommand P A = PhraseStructure.commandRelation (PhraseStructure.maximalProjections P A)

theorem PhraseStructure.maxCommand_adjunct {α : Type u_1} {P A : α → α → Prop} [PartialOrder α] (hA : ∀ (m d : α), A m d → m ⋖ d) [IsLeftLinear α] {m d a b : α} (hmd : A m d) (ha : m ⋖ a) (had : a ≠ d) (hd : d ∈ maximalProjections P A) (hdb : d < b) : (a, b) ∈ maxCommand P A ∧ (b, a) ∉ maxCommand P A

An adjunct to a maximal category MAX-commands out of it, while what the category dominates does not MAX-command the adjunct.

theorem PhraseStructure.isMaximalCategory_iff_forall_above {α : Type u_1} {P A : α → α → Prop} [PartialOrder α] (hA : ∀ (m d : α), A m d → m ⋖ d) [IsLeftLinear α] (hP : ∀ (m d : α), P m d → m ⋖ d) (hU : Relator.RightUnique A) (hdisj : ∀ (m d : α), A m d → ¬P m d) {x : α} : IsMaximalCategory P A x ↔ ∀ (s : α), Relation.ReflTransGen A s x → IsMaximalProjection P s

Only the segments at or above a node decide whether its category is maximal, since a segment with a host is no node's projection daughter.

theorem PhraseStructure.mem_maxCommand_iff_le {α : Type u_1} {P A : α → α → Prop} [PartialOrder α] (hA : ∀ (m d : α), A m d → m ⋖ d) [IsLeftLinear α] (hP : ∀ (m d : α), P m d → m ⋖ d) {h b x : α} (hb : IsProjectionOf (P ⊔ A) h b) (hmax : b ∈ maximalProjections P A) (hne : b ≠ h) : (h, x) ∈ maxCommand P A ↔ b ≤ x

A node that projects to the lowest segment b of a maximal category MAX-commands exactly what b dominates.

Head daughters at tree positions

def PhraseStructure.headDaughterRel (hd : Core.Order.TreePath → Option ℕ) (m d : Core.Order.TreePath) : Prop

headDaughterRel hd m d says that d is the daughter of m at the index hd m.

Equations

• PhraseStructure.headDaughterRel hd m d = ∃ (i : ℕ), hd m = some i ∧ d.toList = m.toList ++ [i]

@[instance_reducible]

instance PhraseStructure.instDecidableRelTreePathHeadDaughterRel (hd : Core.Order.TreePath → Option ℕ) : DecidableRel (headDaughterRel hd)

Equations

• PhraseStructure.instDecidableRelTreePathHeadDaughterRel hd m d = match h : hd m with | none => isFalse ⋯ | some i => decidable_of_iff (d.toList = m.toList ++ [i]) ⋯

theorem PhraseStructure.headDaughterRel_covBy (hd : Core.Order.TreePath → Option ℕ) {m d : Core.Order.TreePath} (h : headDaughterRel hd m d) : m ⋖ d

theorem PhraseStructure.headDaughterRel_rightUnique (hd : Core.Order.TreePath → Option ℕ) : Relator.RightUnique (headDaughterRel hd)

theorem PhraseStructure.isMinimalProjection_headDaughterRel_iff (hd : Core.Order.TreePath → Option ℕ) {p : Core.Order.TreePath} : IsMinimalProjection (headDaughterRel hd) p ↔ hd p = none

@[instance_reducible]

instance PhraseStructure.instDecidableIsMinimalProjectionTreePathHeadDaughterRel (hd : Core.Order.TreePath → Option ℕ) (p : Core.Order.TreePath) : Decidable (IsMinimalProjection (headDaughterRel hd) p)

Equations

• PhraseStructure.instDecidableIsMinimalProjectionTreePathHeadDaughterRel hd p = decidable_of_iff (hd p = none) ⋯

theorem PhraseStructure.isMaximalProjection_headDaughterRel_iff (hd : Core.Order.TreePath → Option ℕ) {p : Core.Order.TreePath} : IsMaximalProjection (headDaughterRel hd) p ↔ ¬headDaughterRel hd p.parent p

@[instance_reducible]

instance PhraseStructure.instDecidableIsMaximalProjectionTreePathHeadDaughterRel (hd : Core.Order.TreePath → Option ℕ) (p : Core.Order.TreePath) : Decidable (IsMaximalProjection (headDaughterRel hd) p)

Equations

• PhraseStructure.instDecidableIsMaximalProjectionTreePathHeadDaughterRel hd p = decidable_of_iff (¬PhraseStructure.headDaughterRel hd p.parent p) ⋯

theorem PhraseStructure.isProjectionOf_headDaughterRel_iff (hd : Core.Order.TreePath → Option ℕ) {h p : Core.Order.TreePath} : IsProjectionOf (headDaughterRel hd) h p ↔ p ≤ h ∧ ∀ q ∈ List.map Core.Order.TreePath.mk h.toList.inits, p < q → headDaughterRel hd q.parent q

p is a projection of h exactly when it dominates h and every position strictly below p down to h is the head daughter of its parent.

@[instance_reducible]

instance PhraseStructure.instDecidableIsProjectionOfTreePathHeadDaughterRel (hd : Core.Order.TreePath → Option ℕ) (h p : Core.Order.TreePath) : Decidable (IsProjectionOf (headDaughterRel hd) h p)

Equations

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

def PhraseStructure.maximalProjectionAt (hd : Core.Order.TreePath → Option ℕ) (h : Core.Order.TreePath) : Core.Order.TreePath

The maximal projection of h is its shortest prefix that is a projection of it.

Equations

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

theorem PhraseStructure.maximalProjectionAt_le (hd : Core.Order.TreePath → Option ℕ) (h : Core.Order.TreePath) : maximalProjectionAt hd h ≤ h

theorem PhraseStructure.isProjectionOf_maximalProjectionAt (hd : Core.Order.TreePath → Option ℕ) (h : Core.Order.TreePath) : IsProjectionOf (headDaughterRel hd) h (maximalProjectionAt hd h)

theorem PhraseStructure.isLeast_maximalProjectionAt (hd : Core.Order.TreePath → Option ℕ) (h : Core.Order.TreePath) : IsLeast {p : Core.Order.TreePath | IsProjectionOf (headDaughterRel hd) h p} (maximalProjectionAt hd h)

maximalProjectionAt hd h is the least projection of h.

Projection and adjunction at positions

def PhraseStructure.projectionIndex (hd : Core.Order.TreePath → Option ℕ) (seg : Core.Order.TreePath → Prop) [DecidablePred seg] (p : Core.Order.TreePath) : Option ℕ

The head daughter of a position that is not a segment, a projection step.

Equations

• PhraseStructure.projectionIndex hd seg p = if seg p then none else hd p

def PhraseStructure.adjunctionIndex (hd : Core.Order.TreePath → Option ℕ) (seg : Core.Order.TreePath → Prop) [DecidablePred seg] (p : Core.Order.TreePath) : Option ℕ

The head daughter of a segment, its host.

Equations

• PhraseStructure.adjunctionIndex hd seg p = if seg p then hd p else none

theorem PhraseStructure.headDaughterRel_eq_sup (hd : Core.Order.TreePath → Option ℕ) (seg : Core.Order.TreePath → Prop) [DecidablePred seg] : headDaughterRel hd = headDaughterRel (projectionIndex hd seg) ⊔ headDaughterRel (adjunctionIndex hd seg)

The head relation is projection together with adjunction.

theorem PhraseStructure.not_projection_of_adjunction (hd : Core.Order.TreePath → Option ℕ) (seg : Core.Order.TreePath → Prop) [DecidablePred seg] {m d : Core.Order.TreePath} (h : headDaughterRel (adjunctionIndex hd seg) m d) : ¬headDaughterRel (projectionIndex hd seg) m d

theorem PhraseStructure.isMaximalCategory_iff_inits (hd : Core.Order.TreePath → Option ℕ) (seg : Core.Order.TreePath → Prop) [DecidablePred seg] (x : Core.Order.TreePath) : IsMaximalCategory (headDaughterRel (projectionIndex hd seg)) (headDaughterRel (adjunctionIndex hd seg)) x ↔ ∀ s ∈ List.map Core.Order.TreePath.mk x.toList.inits, IsProjectionOf (headDaughterRel (adjunctionIndex hd seg)) x s → IsMaximalProjection (headDaughterRel (projectionIndex hd seg)) s

@[instance_reducible]

instance PhraseStructure.instDecidableIsMaximalCategoryTreePathHeadDaughterRelProjectionIndexAdjunctionIndex (hd : Core.Order.TreePath → Option ℕ) (seg : Core.Order.TreePath → Prop) [DecidablePred seg] (x : Core.Order.TreePath) : Decidable (IsMaximalCategory (headDaughterRel (projectionIndex hd seg)) (headDaughterRel (adjunctionIndex hd seg)) x)

Equations

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

@[instance_reducible]

instance PhraseStructure.instDecidableMemTreePathSetMaximalProjectionsHeadDaughterRelProjectionIndexAdjunctionIndex (hd : Core.Order.TreePath → Option ℕ) (seg : Core.Order.TreePath → Prop) [DecidablePred seg] (x : Core.Order.TreePath) : Decidable (x ∈ maximalProjections (headDaughterRel (projectionIndex hd seg)) (headDaughterRel (adjunctionIndex hd seg)))

Equations

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

theorem PhraseStructure.includes_iff_inits (hd : Core.Order.TreePath → Option ℕ) (seg : Core.Order.TreePath → Prop) [DecidablePred seg] (x y : Core.Order.TreePath) : Includes (headDaughterRel (adjunctionIndex hd seg)) x y ↔ x ≤ y ∧ ∀ q ∈ List.map Core.Order.TreePath.mk y.toList.inits, IsProjectionOf (headDaughterRel (adjunctionIndex hd seg)) q x → ∀ (i : ℕ), adjunctionIndex hd seg q = some i → { toList := q.toList ++ [i] } ≤ y

@[instance_reducible]

instance PhraseStructure.instDecidableIncludesTreePathHeadDaughterRelAdjunctionIndex (hd : Core.Order.TreePath → Option ℕ) (seg : Core.Order.TreePath → Prop) [DecidablePred seg] (x y : Core.Order.TreePath) : Decidable (Includes (headDaughterRel (adjunctionIndex hd seg)) x y)

Equations

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

theorem PhraseStructure.excludes_iff_inits (hd : Core.Order.TreePath → Option ℕ) (seg : Core.Order.TreePath → Prop) [DecidablePred seg] (x y : Core.Order.TreePath) : Excludes (headDaughterRel (adjunctionIndex hd seg)) x y ↔ ∀ s ∈ List.map Core.Order.TreePath.mk x.toList.inits, IsProjectionOf (headDaughterRel (adjunctionIndex hd seg)) x s → ¬s ≤ y

@[instance_reducible]

instance PhraseStructure.instDecidableExcludesTreePathHeadDaughterRelAdjunctionIndex (hd : Core.Order.TreePath → Option ℕ) (seg : Core.Order.TreePath → Prop) [DecidablePred seg] (x y : Core.Order.TreePath) : Decidable (Excludes (headDaughterRel (adjunctionIndex hd seg)) x y)

Equations

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

@[instance_reducible]

instance PhraseStructure.instDecidableContainsTreePathHeadDaughterRelAdjunctionIndex (hd : Core.Order.TreePath → Option ℕ) (seg : Core.Order.TreePath → Prop) [DecidablePred seg] (x y : Core.Order.TreePath) : Decidable (Contains (headDaughterRel (adjunctionIndex hd seg)) x y)

Equations

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