Command relations

A dominance order has the root at ⊥ and x ≤ y for x dominates y. A set P of nodes generates a command relation: a commands b when every P-node properly dominating a dominates b. The relations of the literature differ in the generator alone, c-command taking the branching nodes, S-command the S nodes and MAX-command the maximal projections.

The relation is an upper polar in the generator, so that its dependence on P is mathlib's polarity API: a union of generators gives the intersection of the relations by upperPolar_union, the map is antitone by upperPolar_anti, and the relations some property generates are the Order.IsIntent sets. In the commanded node it is a set of upper bounds, and on a tree it is the cone of one node, the lowest generator above the commander.

Main definitions

• PhraseStructure.commandRelation: the command relation a set of nodes generates.
• PhraseStructure.mateRelation: its symmetric part, each node commanding the other.
• RoseTree.IsBranchingAt, RoseTree.cCommand: the branching positions of a rose tree and Barker and Pullum's c-command, the command relation they generate.
• RoseTree.CCommands: Reinhart's c-command, between positions neither of which dominates the other, and RoseTree.cCommandDomain, the positions a position c-commands.

Main statements

• PhraseStructure.mem_commandRelation_iff_mem_upperBounds: the nodes a commands are the upper bounds of the generators properly dominating a.
• PhraseStructure.mem_commandRelation_iff_le: when those generators have a greatest member, a commands exactly what it dominates.
• PhraseStructure.mem_commandRelation_iff_le_of_covBy, PhraseStructure.mem_commandRelation_iff_of_covBy: on a tree a node commands what its mother dominates if the mother is a generator, and what its mother commands if not. By PhraseStructure.eq_commandRelation_of_forall_covBy the command relation is the only relation obeying these two rules in which the root commands every node.
• RoseTree.cCommands_iff_parent_lt: c-command is sisterhood plus dominance.

Implementation notes

• commandRelation is an abbrev for an upper polar, so the lemmas of Mathlib/Order/Concept.lean apply to it as they stand and are not restated here.
• The relations are SetRels, written a ~[commandRelation P] b, since they are intersected, inverted and compared; dominance, which is only ever applied, stays ≤.
• Barker and Pullum's own theorems, their generation by relations and their definition of c-command through the mother relation are in Studies/BarkerPullum1990.lean.

References

• [BP90]
• [Rei76]

Command relations

@[reducible, inline]

abbrev PhraseStructure.Admits {α : Type u_1} [Preorder α] (x : α) (ab : α × α) : Prop

A node x admits the pair (a, b) when it dominates b if it properly dominates a, so that it does not bound a away from b.

Equations

• PhraseStructure.Admits x ab = (x < ab.1 → x ≤ ab.2)

@[reducible, inline]

abbrev PhraseStructure.commandRelation {α : Type u_1} [Preorder α] (P : Set α) : SetRel α α

The command relation generated by P, in which a commands b when every P-node properly dominating a dominates b: the upper polar of P along Admits.

Equations

• PhraseStructure.commandRelation P = upperPolar PhraseStructure.Admits P

theorem PhraseStructure.mem_commandRelation {α : Type u_1} [Preorder α] {P : Set α} {a b : α} : (a, b) ∈ commandRelation P ↔ ∀ x ∈ P, x < a → x ≤ b

theorem PhraseStructure.mem_commandRelation_iff_mem_upperBounds {α : Type u_1} [Preorder α] {P : Set α} {a b : α} : (a, b) ∈ commandRelation P ↔ b ∈ upperBounds (P ∩ Set.Iio a)

The nodes a commands are the upper bounds of the P-nodes properly dominating a.

instance PhraseStructure.instIsReflCommandRelation {α : Type u_1} [Preorder α] {P : Set α} : (commandRelation P).IsRefl

theorem PhraseStructure.mem_commandRelation_of_le {α : Type u_1} [Preorder α] {P : Set α} {a b c : α} (h : (a, b) ∈ commandRelation P) (hbc : b ≤ c) : (a, c) ∈ commandRelation P

A node commands everything below what it commands.

theorem PhraseStructure.mem_commandRelation_congr {α : Type u_1} [Preorder α] {P Q : Set α} {a b : α} (h : ∀ x < a, x ∈ P ↔ x ∈ Q) : (a, b) ∈ commandRelation P ↔ (a, b) ∈ commandRelation Q

What a node commands depends only on the generators properly dominating it.

theorem PhraseStructure.mem_commandRelation_iff_le {α : Type u_1} [Preorder α] {P : Set α} {a b m : α} (h : IsGreatest (P ∩ Set.Iio a) m) : (a, b) ∈ commandRelation P ↔ m ≤ b

When the P-nodes properly dominating a have a greatest member m, the lowest of them in the tree, a commands exactly what m dominates.

Command on trees

On an order whose ancestors are linearly ordered a node's command domain is fixed by its mother, the node it covers.

theorem PhraseStructure.mem_commandRelation_iff_of_le {α : Type u_1} [PartialOrder α] [IsLeftLinear α] {P : Set α} {a b c : α} (hcb : c ≤ b) (hca : ¬c < a) : (a, b) ∈ commandRelation P ↔ (a, c) ∈ commandRelation P

In a tree order a node commands a node below c exactly when it commands c, unless c properly dominates it.

theorem PhraseStructure.mem_commandRelation_of_covBy {α : Type u_1} [PartialOrder α] [IsLeftLinear α] {P : Set α} {a b m : α} (ha : m ⋖ a) (hb : m ≤ b) : (a, b) ∈ commandRelation P

A node commands whatever its mother dominates, whatever the generator.

theorem PhraseStructure.mem_commandRelation_iff_le_of_covBy {α : Type u_1} [PartialOrder α] [IsLeftLinear α] {P : Set α} {a b m : α} (ha : m ⋖ a) (hm : m ∈ P) : (a, b) ∈ commandRelation P ↔ m ≤ b

A node whose mother is a generator commands exactly what its mother dominates.

theorem PhraseStructure.mem_commandRelation_iff_of_covBy {α : Type u_1} [PartialOrder α] [IsLeftLinear α] {P : Set α} {a b m : α} (ha : m ⋖ a) (hm : m ∉ P) : (a, b) ∈ commandRelation P ↔ (m, b) ∈ commandRelation P

A node whose mother is not a generator commands exactly what its mother commands.

theorem PhraseStructure.eq_commandRelation_of_forall_covBy {α : Type u_1} [PartialOrder α] [IsLeftLinear α] {P : Set α} [OrderBot α] [WellFoundedLT α] [IsStronglyCoatomic α] {R : SetRel α α} (hbot : ∀ (b : α), (⊥, b) ∈ R) (hmem : ∀ ⦃m a : α⦄, m ⋖ a → m ∈ P → ∀ (b : α), (a, b) ∈ R ↔ m ≤ b) (hnot : ∀ ⦃m a : α⦄, m ⋖ a → m ∉ P → ∀ (b : α), (a, b) ∈ R ↔ (m, b) ∈ R) : R = commandRelation P

The command relation of P is the only relation in which the root commands every node and a node commands what its mother dominates or what its mother commands, according as the mother is in P or not.

Mates

@[reducible, inline]

abbrev PhraseStructure.mateRelation {α : Type u_1} [Preorder α] (P : Set α) : SetRel α α

Two nodes are P-mates when each P-commands the other.

Equations

• PhraseStructure.mateRelation P = (PhraseStructure.commandRelation P).symmetrize

theorem PhraseStructure.mem_mateRelation {α : Type u_1} [Preorder α] {P : Set α} {a b : α} : (a, b) ∈ mateRelation P ↔ (a, b) ∈ commandRelation P ∧ (b, a) ∈ commandRelation P

Command relations on the positions of a tree

Membership in commandRelation P at concrete positions is decidable: the nodes properly dominating a position are its proper prefixes, a finite list, so the defining universal is a List-bounded one. The branching property of a position is read off the tree, at least two children, the geometric reading of [Rei76]'s "branching node".

theorem PhraseStructure.mem_commandRelation_iff_inits (P : Set Core.Order.TreePath) (a b : Core.Order.TreePath) : (a, b) ∈ commandRelation P ↔ ∀ x ∈ List.map Core.Order.TreePath.mk a.toList.inits, x ≠ a → x ∈ P → x ≤ b

The nodes properly dominating a position are its proper prefixes.

@[instance_reducible]

instance PhraseStructure.instDecidableMemProdTreePathSetRelCommandRelationMkOfDecidablePredSet (P : Set Core.Order.TreePath) [DecidablePred fun (x : Core.Order.TreePath) => x ∈ P] (a b : Core.Order.TreePath) : Decidable ((a, b) ∈ commandRelation P)

Equations

• PhraseStructure.instDecidableMemProdTreePathSetRelCommandRelationMkOfDecidablePredSet P a b = decidable_of_iff (∀ x ∈ List.map Core.Order.TreePath.mk a.toList.inits, x ≠ a → x ∈ P → x ≤ b) ⋯

@[instance_reducible]

instance PhraseStructure.instDecidableMemProdTreePathSetRelMateRelationOfDecidablePredSet (P : Set Core.Order.TreePath) [DecidablePred fun (x : Core.Order.TreePath) => x ∈ P] (ab : Core.Order.TreePath × Core.Order.TreePath) : Decidable (ab ∈ mateRelation P)

Equations

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

C-command on the positions of a rose tree

def RoseTree.IsBranchingAt {β : Type u_1} (t : RoseTree β) (p : Core.Order.TreePath) : Prop

A position of t is branching when its subtree has at least two children, the geometric reading of [Rei76]'s "first branching node".

Equations

• t.IsBranchingAt p = (p ∈ RoseTree.positionsWhere (fun (s : RoseTree β) => 2 ≤ s.arity) t)

@[instance_reducible]

instance RoseTree.instDecidableIsBranchingAt {β : Type u_1} (t : RoseTree β) (p : Core.Order.TreePath) : Decidable (t.IsBranchingAt p)

Equations

• t.instDecidableIsBranchingAt p = RoseTree.instDecidableIsBranchingAt._aux_1 t p

@[reducible, inline]

abbrev RoseTree.cCommand {β : Type u_1} (t : RoseTree β) : SetRel Core.Order.TreePath Core.Order.TreePath

Barker and Pullum's c-command on the positions of t, the command relation its branching positions generate. It is reflexive and a position commands what it dominates, unlike RoseTree.CCommands; it is read off the tree, so decidable.

Equations

• t.cCommand = PhraseStructure.commandRelation {p : Core.Order.TreePath | t.IsBranchingAt p}

def RoseTree.CCommands {β : Type u_1} (t : RoseTree β) (a b : Core.Order.TreePath) : Prop

a c-commands b in t when neither dominates the other and every branching node properly dominating a dominates b: [Rei76]'s c-command, RoseTree.cCommand without dominance.

Equations

• t.CCommands a b = ((a, b) ∈ t.cCommand ∧ ¬a ≤ b ∧ ¬b ≤ a)

@[instance_reducible]

instance RoseTree.instDecidableRelTreePathCCommands {β : Type u_1} (t : RoseTree β) : DecidableRel t.CCommands

Equations

• t.instDecidableRelTreePathCCommands x✝¹ x✝ = { decide := decide ((x✝¹, x✝) ∈ t.cCommand) && decide (¬x✝¹ ≤ x✝ ∧ ¬x✝ ≤ x✝¹), reflects_decide := ⋯ }

theorem RoseTree.cCommands_iff {β : Type u_1} {t : RoseTree β} {a b : Core.Order.TreePath} : t.CCommands a b ↔ (a, b) ∈ t.cCommand ∧ ¬a ≤ b ∧ ¬b ≤ a

def RoseTree.cCommandDomain {β : Type u_1} (t : RoseTree β) (a : Core.Order.TreePath) : Set Core.Order.TreePath

The c-command domain of a position, the positions it c-commands.

Equations

• t.cCommandDomain a = {b : Core.Order.TreePath | t.CCommands a b}

@[simp]

theorem RoseTree.mem_cCommandDomain {β : Type u_1} {t : RoseTree β} {a b : Core.Order.TreePath} : b ∈ t.cCommandDomain a ↔ t.CCommands a b

@[instance_reducible]

instance RoseTree.instDecidableMemTreePathSetCCommandDomain {β : Type u_1} (t : RoseTree β) (a b : Core.Order.TreePath) : Decidable (b ∈ t.cCommandDomain a)

Equations

• t.instDecidableMemTreePathSetCCommandDomain a b = { decide := decide ((a, b) ∈ t.cCommand) && decide (¬a ≤ b ∧ ¬b ≤ a), reflects_decide := ⋯ }

theorem RoseTree.cCommands_iff_parent_lt {β : Type u_1} {t : RoseTree β} {a b : Core.Order.TreePath} (ha : a ≠ ⊥) (hp : t.IsBranchingAt a.parent) : t.CCommands a b ↔ a.parent < b ∧ ¬a ≤ b

C-command is sisterhood plus dominance: a position whose parent branches c-commands exactly the positions properly below its parent and not below itself.

theorem RoseTree.isBranchingAt_map {β : Type u_1} {γ : Type u_2} (f : β → γ) (t : RoseTree β) (p : Core.Order.TreePath) : (map f t).IsBranchingAt p ↔ t.IsBranchingAt p

Relabelling preserves the branching positions.

theorem RoseTree.cCommand_map {β : Type u_1} {γ : Type u_2} (f : β → γ) (t : RoseTree β) : (map f t).cCommand = t.cCommand

Relabelling preserves c-command.

theorem RoseTree.isBranchingAt_replaceAt {β : Type u_1} {t new : RoseTree β} {c x : Core.Order.TreePath} (h : ¬c ≤ x) : (t.replaceAt c.toList new).IsBranchingAt x ↔ t.IsBranchingAt x

Replacing the subtree at c leaves the branching positions outside it as they were.

theorem RoseTree.mem_cCommand_replaceAt {β : Type u_1} {t new : RoseTree β} {a b c : Core.Order.TreePath} (h : ¬c < a) : (a, b) ∈ (t.replaceAt c.toList new).cCommand ↔ (a, b) ∈ t.cCommand

Unless c lies properly above a, what a c-commands is unchanged by replacing the subtree at c.

theorem RoseTree.cCommands_replaceAt_of_le {β : Type u_1} {t new : RoseTree β} {a b c : Core.Order.TreePath} (hcb : c ≤ b) (hca : ¬c ≤ a) (hac : ¬a ≤ c) : (t.replaceAt c.toList new).CCommands a b ↔ t.CCommands a c

A position outside the subtree at c c-commands a position of its replacement exactly when it c-commands c.

theorem RoseTree.cCommands_replaceAt_self {β : Type u_1} {t new : RoseTree β} {a c : Core.Order.TreePath} : (t.replaceAt c.toList new).CCommands c a ↔ t.CCommands c a

The root of the replacement c-commands what the replaced subtree c-commanded.