Command Relations on Abstract Trees

[BP90]'s algebraic theory of command relations.

A command relation generated by a property P is the set of node pairs (a, b) such that every P-node properly dominating a also dominates b. Different syntactic theories pick different P (branching nodes, maximal projections, S-nodes, dependency heads), and the Intersection Theorem shows the map P ↦ C_P is antitone — converting ∪ of properties into ∩ of command relations.

This is the core insight that lets the same lattice structure subsume c-command (Minimalism), o-command (HPSG), d-command (Dependency Grammar), and s-command ([Lan69]).

Main Definitions

• commandRelation T P — pairs (a, b) where every P-upper-bound of a dominates b.
• branchingNodes T / cCommand T — the branching-node generating property and [Rei76]'s c-command it generates.
• commandByRelation T R — relation-based variant generalizing the property-based definition.
• mateRelation T P — symmetric closure: C_P ∩ (C_P)⁻¹.
• maximalGenerator T R — largest relation generating the same C_R.

Main Theorems

• intersection_theorem — C_P ∩ C_Q = C_{P∪Q}.
• command_antitone — P ⊆ Q → C_Q ⊆ C_P.
• configurational_equivalence — when upper bounds coincide, command relations agree (explains why theories converge on configurational clauses).
• command_ambidextrous — every node either has a P-upper-bound or commands everything.
• command_bounded — adding the root to P does not change C_P.
• command_fair — the fairness/transitivity-failure condition.
• relation_union_theorem/_reverse — full B&P Theorem 9.

References

[BP90] "A theory of command relations".

def Core.Order.commandRelation {Node : Type} [PartialOrder Node] (T : TreeOrder Node) (P : Set Node) : Set (Node × Node)

Command relation generated by property P ([BP90] Definition 3).

C_P = {(a, b) | ∀ x ∈ UB(a, P). x dominates b}.

a P-commands b iff every P-node properly dominating a also dominates b.

Equations

• Core.Order.commandRelation T P = {ab : Node × Node | ∀ x ∈ Core.Order.upperBounds T ab.1 P, x ≤ ab.2}

theorem Core.Order.intersection_theorem {Node : Type} [PartialOrder Node] (T : TreeOrder Node) (P Q : Set Node) : commandRelation T P ∩ commandRelation T Q = commandRelation T (P ∪ Q)

Theorem 1 (Intersection Theorem) of [BP90]: C_P ∩ C_Q = C_{P ∪ Q}.

Union of properties gives intersection of command relations.

theorem Core.Order.command_antitone {Node : Type} [PartialOrder Node] (T : TreeOrder Node) (P Q : Set Node) (hPQ : P ⊆ Q) : commandRelation T Q ⊆ commandRelation T P

The map P ↦ C_P is antitone (order-reversing).

def Core.Order.maximalProperty {Node : Type} [PartialOrder Node] (T : TreeOrder Node) : Set Node

Maximal property: all nodes.

Equations

• Core.Order.maximalProperty T = T.nodes

def Core.Order.emptyProperty {Node : Type} : Set Node

Empty property.

Equations

• Core.Order.emptyProperty = ∅

def Core.Order.idcCommand {Node : Type} [PartialOrder Node] (T : TreeOrder Node) : Set (Node × Node)

IDc-command: C_{all nodes} — the most restrictive command relation.

Equations

• Core.Order.idcCommand T = Core.Order.commandRelation T (Core.Order.maximalProperty T)

def Core.Order.universalCommand {Node : Type} [PartialOrder Node] (T : TreeOrder Node) : Set (Node × Node)

Universal command: C_∅ — the least restrictive (everything commands everything).

Equations

• Core.Order.universalCommand T = Core.Order.commandRelation T Core.Order.emptyProperty

def Core.Order.mother {Node : Type} [PartialOrder Node] (T : TreeOrder Node) (a b : Node) : Prop

Mother relation ([BP90] Definition 9): a is the mother of b iff both are tree nodes and a properly dominates b with no tree node strictly between — the minimal proper dominator. Membership in T.nodes is required throughout because upperBounds and the ambient order range over the whole carrier.

Equations

• Core.Order.mother T a b = (a ∈ T.nodes ∧ b ∈ T.nodes ∧ T.properDom a b ∧ ¬∃ x ∈ T.nodes, T.properDom a x ∧ T.properDom x b)

def Core.Order.branchingNodes {Node : Type} [PartialOrder Node] (T : TreeOrder Node) : Set Node

Branching nodes ([BP90] P₅, eq. (19), via the Definition 9 mother relation): nodes that are the mother of two distinct nodes. On Branching.toTreeOrder positions this coincides with the carrier-geometric Branching.isBranchingAt (≥ 2 children).

Equations

• Core.Order.branchingNodes T = {n : Node | ∃ (a : Node) (b : Node), a ≠ b ∧ Core.Order.mother T n a ∧ Core.Order.mother T n b}

def Core.Order.cCommand {Node : Type} [PartialOrder Node] (T : TreeOrder Node) : Set (Node × Node)

C-command ([BP90] Definition 10; [Rei76] def. 36): the command relation generated by branching nodes. Distinct from Lasnik's K-command ([BP90] Definition 7), which is generated by the label-based property "labeled S or NP" and is not definable on a bare TreeOrder.

Equations

• Core.Order.cCommand T = Core.Order.commandRelation T (Core.Order.branchingNodes T)

theorem Core.Order.idc_is_bottom {Node : Type} [PartialOrder Node] (T : TreeOrder Node) (P : Set Node) (hP : P ⊆ T.nodes) : idcCommand T ⊆ commandRelation T P

IDc-command is the bottom of the lattice: IDc ⊆ C_P for all P ⊆ T.nodes.

theorem Core.Order.universal_is_top {Node : Type} [PartialOrder Node] (T : TreeOrder Node) (P : Set Node) : commandRelation T P ⊆ universalCommand T

Universal command is the top: C_P ⊆ Universal for all P.

theorem Core.Order.command_reflexive {Node : Type} [PartialOrder Node] (T : TreeOrder Node) (P : Set Node) (a : Node) : a ∈ T.nodes → (a, a) ∈ commandRelation T P

All command relations are reflexive on tree nodes.

theorem Core.Order.command_descent {Node : Type} [PartialOrder Node] (T : TreeOrder Node) (P : Set Node) (a b c : Node) : (a, b) ∈ commandRelation T P → b ≤ c → (a, c) ∈ commandRelation T P

All command relations satisfy descent on the second argument.

theorem Core.Order.configurational_equivalence {Node : Type} [PartialOrder Node] (T : TreeOrder Node) (P Q : Set Node) (a : Node) (hub : upperBounds T a P = upperBounds T a Q) (b : Node) : (a, b) ∈ commandRelation T P ↔ (a, b) ∈ commandRelation T Q

Configurational Equivalence Corollary: If the upper bounds of node a are the same for properties P and Q, then C_P and C_Q agree on all pairs starting from a.

This formalizes the configurational assumption: different theories (using different P's) agree when their upper bounds coincide.

theorem Core.Order.same_upper_bounds_same_command {Node : Type} [PartialOrder Node] (T : TreeOrder Node) (P Q : Set Node) (a b : Node) (hub : upperBounds T a P = upperBounds T a Q) : (a, b) ∈ commandRelation T P ↔ (a, b) ∈ commandRelation T Q

If P and Q have the same upper bounds at a, C_P(a, –) = C_Q(a, –).

theorem Core.Order.unique_upper_bound_equivalence {Node : Type} [PartialOrder Node] (T : TreeOrder Node) (P Q : Set Node) (s x : Node) (h_unique : ∀ (y : Node), T.properDom y s ↔ y = x) (h_equiv : x ∈ P ↔ x ∈ Q) (b : Node) : (s, b) ∈ commandRelation T P ↔ (s, b) ∈ commandRelation T Q

Configurational Clause Condition: For subject position s, if there is exactly one node x properly dominating s, and x ∈ P ↔ x ∈ Q, then C_P and C_Q agree on pairs from s.

In a standard clause [S [NP_subj] [VP …]], the only node properly dominating the subject NP is S. So any P containing S agrees with any Q containing S.

Lattice Structure

def Core.Order.CommandRels {Node : Type} [PartialOrder Node] (T : TreeOrder Node) : Set (Set (Node × Node))

The set of command relations on a tree.

Equations

• Core.Order.CommandRels T = {C : Set (Node × Node) | ∃ (P : Set Node), C = Core.Order.commandRelation T P}

theorem Core.Order.command_converts_sup_to_inf {Node : Type} [PartialOrder Node] (T : TreeOrder Node) (P Q : Set Node) : commandRelation T (P ⊔ Q) = commandRelation T P ⊓ commandRelation T Q

The Intersection Theorem restated: P ↦ C_P converts ⊔ to ⊓.

theorem Core.Order.command_sInter {Node : Type} [PartialOrder Node] (T : TreeOrder Node) (S : Set (Set Node)) : commandRelation T (⋃₀ S) = ⋂₀ {C : Set (Node × Node) | ∃ P ∈ S, C = commandRelation T P}

Generalized intersection theorem for arbitrary unions.

def Core.Order.commandMap {Node : Type} [PartialOrder Node] (T : TreeOrder Node) : Set Node →o (Set (Node × Node))ᵒᵈ

The command map as an order-reversing function Set Node →o (Set (Node × Node))ᵒᵈ.

Equations

• Core.Order.commandMap T = { toFun := fun (P : Set Node) => OrderDual.toDual (Core.Order.commandRelation T P), monotone' := ⋯ }

theorem Core.Order.command_order_reversing {Node : Type} [PartialOrder Node] (T : TreeOrder Node) (P Q : Set Node) : P ⊆ Q → commandRelation T Q ⊆ commandRelation T P

The command map is order-reversing.

theorem Core.Order.command_ambidextrous {Node : Type} [PartialOrder Node] (T : TreeOrder Node) (P : Set Node) (a : Node) : (∃ (x : Node), x ∈ upperBounds T a P) ∨ ∀ (b : Node), (a, b) ∈ commandRelation T P

A command relation C_P is ambidextrous iff for all a: either ∃x. x ∈ UB(a, P) or (a, b) ∈ C_P for all b.

[BP90] Theorem 3: All command relations are ambidextrous.

theorem Core.Order.command_bounded {Node : Type} [PartialOrder Node] (T : TreeOrder Node) (P : Set Node) (hb : ∀ (a b : Node), (a, b) ∈ commandRelation T P → b ∈ T.nodes) : commandRelation T P = commandRelation T (P ∪ {T.root})

Boundedness ([BP90] Theorem 4): Adding a root node to the generating property does not alter the command relation: C_P = C_{P ∪ {r}}.

theorem Core.Order.root_upper_bound_trivial {Node : Type} [PartialOrder Node] (T : TreeOrder Node) (a b : Node) (hb : b ∈ T.nodes) (_hprop : T.properDom T.root a) : T.root ≤ b

The root dominates every tree node, so it is a trivial upper bound.

theorem Core.Order.command_bounded_witness {Node : Type} [PartialOrder Node] (T : TreeOrder Node) (P : Set Node) (a b : Node) (h : (a, b) ∈ commandRelation T P) (hub : ∃ (x : Node), x ∈ upperBounds T a P) : ∃ x ∈ upperBounds T a P, x ≤ b

If UB(a, P) is nonempty and (a, b) ∈ C_P, then ∃x ∈ UB(a, P). x dominates b.

theorem Core.Order.command_noncommand_witness {Node : Type} [PartialOrder Node] (T : TreeOrder Node) (P : Set Node) (a c : Node) (hnac : (a, c) ∉ commandRelation T P) : ∃ x ∈ upperBounds T a P, ¬x ≤ c

Fairness witness: ¬(a C_P c) implies ∃ x ∈ UB(a, P). ¬(x dom c).

Contrapositive of the command definition.

theorem Core.Order.command_fair {Node : Type} [PartialOrder Node] (T : TreeOrder Node) (P : Set Node) (a b c : Node) (hab : (a, b) ∈ commandRelation T P) (hbc : (b, c) ∈ commandRelation T P) (hnac : (a, c) ∉ commandRelation T P) (d : Node) : (a, d) ∈ commandRelation T P → b ≤ d

Fairness ([BP90] Theorem 6): (a C b) ∧ (b C c) ∧ ¬(a C c) → ∀d. (a C d) → b dominates d.

def Core.Order.mateRelation {Node : Type} [PartialOrder Node] (T : TreeOrder Node) (P : Set Node) : Set (Node × Node)

Mate relation: M_P = C_P ∩ (C_P)⁻¹.

Two nodes are P-mates iff they mutually P-command each other. Examples: clause-mates (S-command), co-arguments (NP-command).

Equations

• Core.Order.mateRelation T P = {ab : Node × Node | (ab.1, ab.2) ∈ Core.Order.commandRelation T P ∧ (ab.2, ab.1) ∈ Core.Order.commandRelation T P}

theorem Core.Order.mate_symmetric {Node : Type} [PartialOrder Node] (T : TreeOrder Node) (P : Set Node) (a b : Node) : (a, b) ∈ mateRelation T P → (b, a) ∈ mateRelation T P

theorem Core.Order.mate_reflexive {Node : Type} [PartialOrder Node] (T : TreeOrder Node) (P : Set Node) (a : Node) (ha : a ∈ T.nodes) : (a, a) ∈ mateRelation T P

theorem Core.Order.mate_intersection {Node : Type} [PartialOrder Node] (T : TreeOrder Node) (P Q : Set Node) : mateRelation T P ∩ mateRelation T Q = mateRelation T (P ∪ Q)

theorem Core.Order.command_descent' {Node : Type} [PartialOrder Node] (T : TreeOrder Node) (P : Set Node) (a b c : Node) : (a, b) ∈ commandRelation T P → b ≤ c → (a, c) ∈ commandRelation T P

Descent ([BP90] Theorem 5) restated: C_P is closed under descent on the second argument.

theorem Core.Order.command_constituency {Node : Type} [PartialOrder Node] (T : TreeOrder Node) (P : Set Node) (a : Node) (hmax : (upperBounds T a P).Nonempty → ∃ x ∈ upperBounds T a P, ∀ y ∈ upperBounds T a P, y ≤ x) : ∃ (x : Node), ∀ b ∈ T.nodes, (a, b) ∈ commandRelation T P ↔ x ≤ b

Constituency ([BP90] Theorem 7, p. 30): every command domain C_P(a, ·) (restricted to tree nodes) is the cone of a single node — Reinhart's "first branching node" rendered order-theoretically. The witness is the greatest element of UB(a, P), which exists when UB is nonempty (the CAC makes UB a chain, so "greatest" is well-defined); when UB(a, P) is empty, C_P(a, ·) is universal on the tree and the witness is the root.

Stated as: ∃ x, ∀ b ∈ T.nodes, (a, b) ∈ commandRelation T P ↔ x ≤ b. The hypothesis hmax asks for the greatest element when UB is nonempty — a one-line consequence of finiteness, which B&P assume but which we state explicitly here so the theorem holds for the abstract TreeOrder (which need not be finite).

The "first branching node" reading: when P = branchingNodes T, the greatest element of UB(a, P) is the lowest branching ancestor of a, and Reinhart's c-command domain is exactly its cone.

theorem Core.Order.command_embeddable_simple {Node : Type} [PartialOrder Node] (T : TreeOrder Node) (P : Set Node) (a b c : Node) (_hdom : T.properDom a b) (hac : (a, c) ∈ commandRelation T P) (x : Node) : x ∈ upperBounds T b P → T.properDom x a → x ≤ c

Embeddability (simple form): if x properly dominates a, then commands transfer through that upper bound.

theorem Core.Order.command_embeddable_cac {Node : Type} [PartialOrder Node] (T : TreeOrder Node) (P : Set Node) (a b c : Node) (_hdom : T.properDom a b) (hac : (a, c) ∈ commandRelation T P) (h_upper_bounds_above : ∀ x ∈ upperBounds T b P, T.properDom x a ∨ a ≤ x ∧ x ≤ c) : (b, c) ∈ commandRelation T P

Embeddability with CAC ([BP90] Theorem 8): If every P-upper-bound of b either properly dominates a or sits between a and c on the dominance path, then (a, c) ∈ C_P implies (b, c) ∈ C_P.

def Core.Order.commandByRelation {Node : Type} [PartialOrder Node] (T : TreeOrder Node) (R : Node → Node → Prop) : Set (Node × Node)

A command relation generated by a binary relation rather than a property.

C_R(a, b) iff ∀x. (a R x) → (x dominates b).

Equations

• Core.Order.commandByRelation T R = {ab : Node × Node | ∀ (x : Node), R ab.1 x → x ≤ ab.2}

theorem Core.Order.command_as_relation {Node : Type} [PartialOrder Node] (T : TreeOrder Node) (P : Set Node) : commandRelation T P = commandByRelation T fun (a x : Node) => T.properDom x a ∧ x ∈ P

The property-based command is a special case of relation-based.

def Core.Order.commandEquivalent {Node : Type} [PartialOrder Node] (T : TreeOrder Node) (R S : Node → Node → Prop) : Prop

Command equivalence ([BP90] Definition 20): R ~ S iff C_R = C_S.

Equations

• Core.Order.commandEquivalent T R S = (Core.Order.commandByRelation T R = Core.Order.commandByRelation T S)

def Core.Order.maximalGenerator {Node : Type} [PartialOrder Node] (T : TreeOrder Node) (R : Node → Node → Prop) : Node → Node → Prop

Maximal generator ([BP90] Definition 21): R̂ = ⋃ {S | S ⊇ R ∧ S ~ R}.

The largest relation generating the same command relation as R.

Equations

• Core.Order.maximalGenerator T R a x = ∃ (S : Node → Node → Prop), (∀ (a' x' : Node), R a' x' → S a' x') ∧ Core.Order.commandEquivalent T R S ∧ S a x

theorem Core.Order.maximalGenerator_contains {Node : Type} [PartialOrder Node] (T : TreeOrder Node) (R : Node → Node → Prop) (a x : Node) : R a x → maximalGenerator T R a x

Maximal generator contains the original relation.

theorem Core.Order.nonminimal_in_maximalGenerator {Node : Type} [PartialOrder Node] (T : TreeOrder Node) (R : Node → Node → Prop) (a c d : Node) (hRad : R a d) (hcd : c ≤ d) (_hcpropa : T.properDom c a) (_hR_proper : ∀ (a' x' : Node), R a' x' → T.properDom x' a') : maximalGenerator T R a c

Key lemma for the Union Theorem: non-minimal upper bounds are in the maximal generator.

theorem Core.Order.maximalGenerator_equivalent {Node : Type} [PartialOrder Node] (T : TreeOrder Node) (R : Node → Node → Prop) : commandEquivalent T R (maximalGenerator T R)

Maximal generator is command-equivalent to original.

theorem Core.Order.relation_intersection_theorem {Node : Type} [PartialOrder Node] (T : TreeOrder Node) (R S : Node → Node → Prop) : commandByRelation T R ∩ commandByRelation T S = commandByRelation T fun (a x : Node) => R a x ∨ S a x

Intersection Theorem for Relations: C_R ∩ C_S = C_{R ∪ S}.

theorem Core.Order.relation_union_theorem {Node : Type} [PartialOrder Node] (T : TreeOrder Node) (R S : Node → Node → Prop) : commandByRelation T R ∪ commandByRelation T S ⊆ commandByRelation T fun (a x : Node) => maximalGenerator T R a x ∧ maximalGenerator T S a x

Union Theorem ([BP90] Theorem 9, forward): C_R ∪ C_S ⊆ C_{R̂ ∩ Ŝ}.

theorem Core.Order.relation_union_theorem_reverse {Node : Type} [PartialOrder Node] (T : TreeOrder Node) (R S : Node → Node → Prop) (hR_proper : ∀ (a x : Node), R a x → T.properDom x a) (hS_proper : ∀ (a x : Node), S a x → T.properDom x a) : (commandByRelation T fun (a x : Node) => maximalGenerator T R a x ∧ maximalGenerator T S a x) ⊆ commandByRelation T R ∪ commandByRelation T S

Union Theorem ([BP90] Theorem 9, reverse) — uses CAC.

def Core.Order.commandImage {Node : Type} [PartialOrder Node] (T : TreeOrder Node) : Set (Set (Node × Node))

The image of the command map: all command relations on T.

Equations

• Core.Order.commandImage T = Set.range (Core.Order.commandRelation T)

theorem Core.Order.commandImage_closed_under_sInter {Node : Type} [PartialOrder Node] (T : TreeOrder Node) (S : Set (Set (Node × Node))) (hS : S ⊆ commandImage T) (_hne : S.Nonempty) : ⋂₀ S ∈ commandImage T

Command relations are closed under arbitrary nonempty intersection.

theorem Core.Order.command_closure_system {Node : Type} [PartialOrder Node] (T : TreeOrder Node) (S : Set (Set (Node × Node))) : S ⊆ commandImage T → S.Nonempty → ⋂₀ S ∈ commandImage T

The command relations form a closure system.