Barker & Pullum (1990): A Theory of Command Relations

Barker and Pullum generate a command relation from a property of nodes: a commands b when every node with the property that properly dominates a dominates b. The literature's relations differ only in the generator: S-command comes from the S nodes, K-command from S and NP, MAX-command from the maximal projections, c-command from the branching nodes, and IDC-command from every node. Mate relations intersect a command relation with its inverse, and government relations intersect one with the composition of head-of and command.

The definition is Syntax/Command.lean's, an upper polar in the generator, and the paper's theorems are proved here from it. The Intersection Theorem and what follows from it are mathlib's facts about polars; Descent, Fairness, Constituency and Embeddability are facts about the upper bounds of a node's ancestors; and the maximal generator of a relation, which the paper defines as a union over all relations generating the same command relation, is the closure of its upper bounds under lowerBounds ∘ upperBounds.

Two questions the paper raises are settled. The characteristics it lists as common to all command relations do not single them out, since dominance has all of them: a relation on a tree is generated by a property exactly when it contains IDC-command and is fair. And its last footnote leaves open whether the command relations carry a Boolean algebra. Ordered by inclusion, those that properties generate do, corresponding with the order reversed to the sets of nodes that are neither the root nor a leaf; those that relations generate, with the intersection and union the paper gives them as meet and join, do not, since a relation can lack a complement.

Two of the paper's claims fail on its own definitions: the characterization of mates by equal sets of upper bounds is strictly stronger than mutual command once a node may be its mate's upper bound, and so is the prose characterization by equal command domains. On the paper's government tree, whose maximal projections are read off its heads, Davis's definition of government fails where the paper's restatement holds, and the government schema with head-of reaches the head of a governed phrase.

Main statements

• isIntent_admits_iff, fair_le_and_not_isIntent_le: a relation on a tree is generated by a property exactly when it contains the relation every node generates and is fair, and dominance, which is fair, is not so generated.
• exists_forall_mem_commandRelation_iff_le, mem_commandRelation_Ici_iff: on a tree what a node commands is the cone of one node, and command in a subtree is command in the tree.
• maximalGenerator_iff, commandByRelation_union: the maximal generator of a relation is a closure of its upper bounds, and on a tree the union of two relation-generated command relations is generated by the intersection of their maximal generators.
• commandRelationIso, not_exists_isCompl_commandByRelation: on a tree the command relations that properties generate are, under inclusion, the sets of internal nodes under reverse inclusion, while those that relations generate have no complements under intersection and union.

Implementation notes

• A tree is a left-linear order with a least element that is well founded and in which every node but the root covers a mother; finite trees and the positions TreePath are instances.
• A relation is one that some property generates exactly when it is an intent of Admits, mathlib's Order.IsIntent, and closure under intersection is Order.IsIntent.iInter.
• A relation as generator pairs a bound with the commander it bounds, as in the paper, and counts only when the bound properly dominates the commander.
• The government tree leaves one maximal projection unexpanded in the paper; here it has a head.

References

• [BP90]
• [Kli64]
• [Las76]
• [RV80]
• [Dav87]

def BarkerPullum1990.government {Node : Type u_1} (C : SetRel Node Node) (H : Node → Node → Prop) : SetRel Node Node

In the government schema a governs b when a commands b and b bears to a the composition of head-of with command.

Equations

• BarkerPullum1990.government C H = {ab : Node × Node | (ab.1, ab.2) ∈ C ∧ ∃ (x : Node), Relation.ReflTransGen H ab.2 x ∧ (x, ab.1) ∈ C}

theorem BarkerPullum1990.government_subset {Node : Type u_1} (C : SetRel Node Node) (H : Node → Node → Prop) : government C H ⊆ C

Trees

Definition 1 adopts Wall's definition of a tree. Dominance is reflexive and antisymmetric with a single root; precedence is irreflexive, asymmetric and transitive; two nodes are related by dominance exactly when neither precedes the other (the Exclusivity Condition); and precedence passes to the nodes each relatum dominates (the Nontangling Condition).

theorem BarkerPullum1990.treePath_isTree : (∀ (a : Core.Order.TreePath), ⊥ ≤ a) ∧ IsStrictOrder Core.Order.TreePath Core.Order.TreePath.Precedes ∧ (∀ (a b : Core.Order.TreePath), a ≤ b ∨ b ≤ a ↔ ¬(a.Precedes b ∨ b.Precedes a)) ∧ ∀ ⦃a b c d : Core.Order.TreePath⦄, a.Precedes b → a ≤ c → b ≤ d → c.Precedes d

Positions under prefix dominance and branch-order precedence satisfy the conditions of Definition 1 on dominance and precedence.

Command relations

By Definition 2 the upper bounds of a with respect to P are the members of P properly dominating a, the set P ∩ Set.Iio a, and by Definition 3 a commands what every one of them dominates, their upper bounds in the dominance order (mem_commandRelation_iff_mem_upperBounds). As a function of P the relation is an upper polar, which gives Theorems 1 and 2.

theorem BarkerPullum1990.commandRelation_union {Node : Type u_1} [PartialOrder Node] (P Q : Set Node) : PhraseStructure.commandRelation (P ∪ Q) = PhraseStructure.commandRelation P ∩ PhraseStructure.commandRelation Q

Theorem 1, the Intersection Theorem: a union of generators generates the intersection of their relations.

theorem BarkerPullum1990.commandRelation_univ_subset {Node : Type u_1} [PartialOrder Node] (P : Set Node) : PhraseStructure.commandRelation Set.univ ⊆ PhraseStructure.commandRelation P

Theorem 2: IDC-command, generated by every node, is the smallest command relation.

theorem BarkerPullum1990.mem_commandRelation_univ_iff {Node : Type u_1} [PartialOrder Node] {a b m : Node} [IsLeftLinear Node] (ha : m ⋖ a) : (a, b) ∈ PhraseStructure.commandRelation Set.univ ↔ m ≤ b

On a tree a IDC-commands b exactly when the mother of a dominates b, the informal definition (21).

theorem BarkerPullum1990.commandRelation_insert_of_isBot {Node : Type u_1} [PartialOrder Node] {r : Node} (hr : IsBot r) (P : Set Node) : PhraseStructure.commandRelation (insert r P) = PhraseStructure.commandRelation P

Theorem 4, Boundedness: a root adds nothing to a generator.

theorem BarkerPullum1990.not_isIntent_of_not_descent {Node : Type u_1} [PartialOrder Node] {a b c : Node} {R : SetRel Node Node} (hab : (a, b) ∈ R) (hbc : b ≤ c) (hac : (a, c) ∉ R) : ¬Order.IsIntent PhraseStructure.Admits R

A relation that fails Descent, Theorem 5 and mem_commandRelation_of_le, is generated by no property.

def BarkerPullum1990.Fair {Node : Type u_1} [PartialOrder Node] (R : SetRel Node Node) : Prop

A relation is fair when an upper bound is an upper bound for every node it properly dominates.

Equations

• BarkerPullum1990.Fair R = ∀ (a b c : Node), (a, b) ∈ R → (b, c) ∈ R → (a, c) ∉ R → ∀ (d : Node), (a, d) ∈ R → b ≤ d

theorem BarkerPullum1990.fair_commandRelation {Node : Type u_1} [PartialOrder Node] (P : Set Node) : Fair (PhraseStructure.commandRelation P)

Theorem 6, Fairness: when a commands b, b commands c and a does not command c, the generator separating a from c is b itself, which therefore dominates all a commands.

theorem BarkerPullum1990.exists_forall_mem_commandRelation_iff_le {Node : Type u_1} [PartialOrder Node] [OrderBot Node] [IsLeftLinear Node] [WellFoundedLT Node] [IsStronglyCoatomic Node] (P : Set Node) (a : Node) : ∃ (x : Node), ∀ (b : Node), (a, b) ∈ PhraseStructure.commandRelation P ↔ x ≤ b

Theorem 7, Constituency: on a rooted tree the nodes a commands are those one node dominates. The node is found by climbing from a to the first mother that is a generator.

theorem BarkerPullum1990.mem_commandRelation_Ici_iff {Node : Type u_1} [PartialOrder Node] [IsLeftLinear Node] (r : Node) (P : Set Node) (a b : ↑(Set.Ici r)) : (a, b) ∈ PhraseStructure.commandRelation (Subtype.val ⁻¹' P) ↔ (↑a, ↑b) ∈ PhraseStructure.commandRelation P

Theorem 8, Embeddability: on a tree, command among the nodes r dominates is command in the whole tree, since a generator outside the subtree that dominates one of its nodes dominates r.

Characterizing command relations

The paper lists reflexivity, Descent, Constituency and Fairness among the characteristics common to all command relations. They do not single the command relations out, since dominance has all of them. What does is Fairness together with Theorem 2: a relation on a tree is generated by a property exactly when it contains IDC-command and is fair, and Descent and Constituency follow.

theorem BarkerPullum1990.fair_iff {Node : Type u_1} [PartialOrder Node] {R : SetRel Node Node} : Fair R ↔ ∀ (a b : Node), (a, b) ∈ R → (∀ (c : Node), (b, c) ∈ R → (a, c) ∈ R) ∨ ∀ (d : Node), (a, d) ∈ R → b ≤ d

Fairness as a dichotomy: when a commands b, either a commands all that b commands or b dominates all that a commands.

theorem BarkerPullum1990.isIntent_admits_iff {Node : Type u_1} [PartialOrder Node] [OrderBot Node] [IsLeftLinear Node] [WellFoundedLT Node] [IsStronglyCoatomic Node] {R : SetRel Node Node} : Order.IsIntent PhraseStructure.Admits R ↔ PhraseStructure.commandRelation Set.univ ⊆ R ∧ Fair R

A relation on a tree is generated by a property exactly when it contains IDC-command and is fair. Fairness makes a daughter command no more than her mother, hence either what her mother dominates or all her mother commands, and makes sisters agree on which; so the relation obeys the rules that fix the command relation of the mothers that bound a daughter.

theorem BarkerPullum1990.descent_and_constituency_of_fair {Node : Type u_1} [PartialOrder Node] [OrderBot Node] [IsLeftLinear Node] [WellFoundedLT Node] [IsStronglyCoatomic Node] {R : SetRel Node Node} (hI : PhraseStructure.commandRelation Set.univ ⊆ R) (hF : Fair R) : (∀ (a b c : Node), (a, b) ∈ R → b ≤ c → (a, c) ∈ R) ∧ ∀ (a : Node), ∃ (x : Node), ∀ (b : Node), (a, b) ∈ R ↔ x ≤ b

So Descent and Constituency follow from Fairness, for a relation that contains IDC-command.

theorem BarkerPullum1990.fair_le_and_not_isIntent_le {Node : Type u_1} [PartialOrder Node] {a m : Node} [IsLeftLinear Node] (h : m ⋖ a) : Fair {ab : Node × Node | ab.1 ≤ ab.2} ∧ ¬Order.IsIntent PhraseStructure.Admits {ab : Node × Node | ab.1 ≤ ab.2}

Dominance is fair, and like every order it is reflexive and satisfies Descent and Constituency; but on a tree with an edge no property generates it, since a node commands its mother and does not dominate her.

The literature's relations

@[reducible, inline]

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

Rouveret and Vergnaud's c-command is generated by the branching nodes together with the maximal projections.

Equations

• BarkerPullum1990.rvCommand t = PhraseStructure.commandRelation ({p : Core.Order.TreePath | RoseTree.IsBranchingAt t p} ∪ t.maximalProjectionsAt)

theorem BarkerPullum1990.rvCommand_eq {C : Type u_2} {W : Type u_3} [DecidableEq C] (t : PhraseStructure.Tree C W) : rvCommand t = RoseTree.cCommand t ∩ t.maxCommand

Rouveret and Vergnaud's relation is c-command ∩ MAX-command.

@[reducible, inline]

abbrev BarkerPullum1990.npCommand {W : Type u_3} (t : PhraseStructure.Tree PhraseStructure.Cat W) : SetRel Core.Order.TreePath Core.Order.TreePath

NP-command is generated by the NP nodes, the maximal projections of nouns.

Equations

• BarkerPullum1990.npCommand t = PhraseStructure.commandRelation (t.labeled {PhraseStructure.Cat.N} ∩ t.maximalProjectionsAt)

@[reducible, inline]

abbrev BarkerPullum1990.kCommand {W : Type u_3} (t : PhraseStructure.Tree PhraseStructure.Cat W) : SetRel Core.Order.TreePath Core.Order.TreePath

Lasnik's kommand is generated by the cyclic nodes, S and NP.

Equations

• BarkerPullum1990.kCommand t = PhraseStructure.commandRelation (t.labeled {PhraseStructure.Cat.S} ∪ t.labeled {PhraseStructure.Cat.N} ∩ t.maximalProjectionsAt)

theorem BarkerPullum1990.kCommand_eq {W : Type u_3} (t : PhraseStructure.Tree PhraseStructure.Cat W) : kCommand t = t.sCommand ∩ npCommand t

K-command is S-command ∩ NP-command.

@[reducible, inline]

abbrev BarkerPullum1990.inConstructionWith {W : Type u_2} (t : PhraseStructure.Tree PhraseStructure.Cat W) : SetRel Core.Order.TreePath Core.Order.TreePath

Klima's in-construction-with is the inverse of c-command.

Equations

• BarkerPullum1990.inConstructionWith t = (RoseTree.cCommand t).inv

@[instance_reducible]

instance BarkerPullum1990.instDecidableMemProdTreePathSetRelInConstructionWith {W : Type u_2} (t : PhraseStructure.Tree PhraseStructure.Cat W) (ab : Core.Order.TreePath × Core.Order.TreePath) : Decidable (ab ∈ inConstructionWith t)

Equations

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

def BarkerPullum1990.witness : PhraseStructure.Tree PhraseStructure.Cat Unit

In [S [NP N N] V] the verb is in construction with the NP, which dominates its first noun, but not with that noun.

Equations

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

theorem BarkerPullum1990.not_isIntent_inConstructionWith : ¬Order.IsIntent PhraseStructure.Admits (inConstructionWith witness)

In-construction-with is generated by no property, so the inverse of a command relation need not be one.

C-command through the mother relation

Definition 9 takes the mother relation to be covering in the dominance order, and Definition 10 takes c-command to be generated by the nodes that are mothers of two distinct nodes. On the positions of a tree these are the positions with at least two children, so the relation is the substrate's RoseTree.cCommand.

def BarkerPullum1990.branchingNodes {Node : Type u_1} [PartialOrder Node] : Set Node

The branching nodes of Definition 10: the mothers of two distinct nodes.

Equations

• BarkerPullum1990.branchingNodes = {n : Node | ∃ (a : Node) (b : Node), a ≠ b ∧ n ⋖ a ∧ n ⋖ b}

def BarkerPullum1990.cCommand {Node : Type u_1} [PartialOrder Node] : SetRel Node Node

Definition 10: c-command is generated by the branching nodes.

Equations

• BarkerPullum1990.cCommand = PhraseStructure.commandRelation BarkerPullum1990.branchingNodes

theorem BarkerPullum1990.mem_commandRelation_subtype_iff {Node : Type u_1} [PartialOrder Node] {D : Set Node} (hD : IsLowerSet D) (P : Set Node) (a b : ↑D) : (a, b) ∈ PhraseStructure.commandRelation (Subtype.val ⁻¹' P) ↔ (↑a, ↑b) ∈ PhraseStructure.commandRelation P

On a set closed under ancestors, the relation the restriction of P generates is the restriction of the relation P generates.

theorem BarkerPullum1990.mem_branchingNodes_iff {β : Type u_2} {t : RoseTree β} (p : t.Positions) : p ∈ branchingNodes ↔ t.IsBranchingAt ↑p

A position is a branching node of the rooted tree Positions t iff it is branching in t, since its covers are its valid daughters, two of which exist iff its subtree has two.

theorem BarkerPullum1990.branchingNodes_eq_preimage {β : Type u_2} (t : RoseTree β) : branchingNodes = Subtype.val ⁻¹' {p : Core.Order.TreePath | t.IsBranchingAt p}

theorem BarkerPullum1990.mem_cCommand_iff {β : Type u_2} {t : RoseTree β} (a b : t.Positions) : (a, b) ∈ cCommand ↔ (↑a, ↑b) ∈ t.cCommand

On the rooted tree of positions, c-command is the c-command of t.

Mates

@[reducible, inline]

abbrev BarkerPullum1990.clausemates {W : Type u_2} (t : PhraseStructure.Tree PhraseStructure.Cat W) : SetRel Core.Order.TreePath Core.Order.TreePath

Clausemates are S-mates.

Equations

• BarkerPullum1990.clausemates t = PhraseStructure.mateRelation (t.labeled {PhraseStructure.Cat.S})

theorem BarkerPullum1990.mateRelation_empty {Node : Type u_1} [PartialOrder Node] : PhraseStructure.mateRelation ∅ = PhraseStructure.commandRelation ∅

The relation generated by the empty property holds of every pair, so it is its own inverse and its own mate relation.

def BarkerPullum1990.nested : PhraseStructure.Tree PhraseStructure.Cat Unit

In [S [S N N] V] a noun and the S above it are clausemates.

Equations

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

theorem BarkerPullum1990.clausemates_not_sameUpperBounds : ({ toList := [0, 0] }, { toList := [0] }) ∈ clausemates nested ∧ nested.labeled {PhraseStructure.Cat.S} ∩ Set.Iio { toList := [0, 0] } ≠ nested.labeled {PhraseStructure.Cat.S} ∩ Set.Iio { toList := [0] }

Mutual command does not give equal upper-bound sets, since the noun's bounds are both S nodes and the lower S's bound is the root alone.

theorem BarkerPullum1990.clausemates_not_sameDomain : ({ toList := [0] }, { toList := [1] }) ∈ nested.sCommand ∧ ({ toList := [0, 0] }, { toList := [1] }) ∉ nested.sCommand

Nor does it give equal command domains, since the lower S commands the verb and the noun does not.

Government

A governor is a minimal projection related to what it governs through the maximal projections, here read off the tree's heads, one of the "more tree-dependent" ways of defining MAX that Barker and Pullum allow. The head-of relation of the government schema is the head-daughter relation reversed.

def BarkerPullum1990.davis {Node : Type u_1} [PartialOrder Node] (max : Set Node) (a b : Node) : Prop

On Davis's definition (24b) a governs b when every maximal projection dominates b iff it dominates a.

Equations

• BarkerPullum1990.davis max a b = ∀ P ∈ max, P ≤ b ↔ P ≤ a

def BarkerPullum1990.davisRestated {Node : Type u_1} [PartialOrder Node] (max : Set Node) (a b : Node) : Prop

The restatement (26c–d) of Davis's definition asks that a and b be MAX-mates and that neither dominate the other.

Equations

• BarkerPullum1990.davisRestated max a b = ((a, b) ∈ PhraseStructure.mateRelation max ∧ ¬a ≤ b ∧ ¬b ≤ a)

def BarkerPullum1990.Governs {W : Type u_2} (t : PhraseStructure.Tree PhraseStructure.Cat W) (a b : Core.Order.TreePath) : Prop

By the restatement (26), a governs b in t when a is a minimal projection, of bar level 0, and the two are MAX-mates neither dominating the other. Clause (b), on INFL, is left out, since no category here is INFL.

Equations

• BarkerPullum1990.Governs t a b = (PhraseStructure.IsMinimalProjection t.HeadDaughterAt a ∧ BarkerPullum1990.davisRestated t.maximalProjectionsAt a b)

def BarkerPullum1990.tree25 : PhraseStructure.Tree PhraseStructure.Cat Unit

Tree (25) has X² over X¹ and Y², and X¹ over X⁰ alone; here X is a verb and Y a noun, and Y², which the figure leaves unexpanded, has a head Y⁰.

Equations

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

theorem BarkerPullum1990.tree25_davis_fails : ¬davis tree25.maximalProjectionsAt { toList := [0, 0] } { toList := [1] }

X⁰ does not govern Y² on Davis's definition, since Y² is a maximal projection that dominates itself but not X⁰.

theorem BarkerPullum1990.tree25_governs : Governs tree25 { toList := [0, 0] } { toList := [1] }

On the restatement it does.

theorem BarkerPullum1990.tree25_not_governs_bar : davisRestated tree25.maximalProjectionsAt { toList := [0] } { toList := [1] } ∧ ¬Governs tree25 { toList := [0] } { toList := [1] }

X¹ and Y² are MAX-mates, but X¹ does not govern Y², since it projects from X⁰.

theorem BarkerPullum1990.tree25_governs_head : ({ toList := [0, 0] }, { toList := [1, 0] }) ∈ government tree25.maxCommand (flip tree25.HeadDaughterAt)

In the government schema with MAX-command and head-of, Aoun and Lightfoot's government, X⁰ governs the head Y⁰ of Y², as they intend and their own definition fails to ensure.

Relations as generators

Definition 19 lets the candidates for bounding a commander depend on it: the upper bounds of a with respect to a relation R are the nodes that properly dominate a and bear R to it.

def BarkerPullum1990.commandByRelation {Node : Type u_1} [PartialOrder Node] (R : Node → Node → Prop) : SetRel Node Node

The command relation a relation R generates: a commands b when every node that properly dominates a and bears R to it dominates b.

Equations

• BarkerPullum1990.commandByRelation R = {ab : Node × Node | ab.2 ∈ upperBounds {x : Node | x < ab.1 ∧ R x ab.1}}

theorem BarkerPullum1990.mem_commandByRelation {Node : Type u_1} [PartialOrder Node] {a b : Node} {R : Node → Node → Prop} : (a, b) ∈ commandByRelation R ↔ ∀ x < a, R x a → x ≤ b

theorem BarkerPullum1990.commandByRelation_mem {Node : Type u_1} [PartialOrder Node] (P : Set Node) : (commandByRelation fun (x x_1 : Node) => x ∈ P) = PhraseStructure.commandRelation P

A property generates the command relation of the relation its members bear to every node.

def BarkerPullum1990.unfairGenerator (x a : Core.Order.TreePath) : Prop

Relations generate fair command relations no more than by accident. This generator gives the first noun of witness its NP as sole bound and every other node none.

Equations

• BarkerPullum1990.unfairGenerator x a = (x = { toList := [0] } ∧ a = { toList := [0, 0] })

theorem BarkerPullum1990.not_fair_unfairGenerator : ¬Fair (commandByRelation unfairGenerator)

The first noun commands its sister and itself and the sister commands the verb, while the noun does not command the verb and the sister does not dominate the noun.

def BarkerPullum1990.maximalGenerator {Node : Type u_1} [PartialOrder Node] (R : Node → Node → Prop) : Node → Node → Prop

Definition 21: the maximal generator of R is the union of the relations containing R that generate the same command relation.

Equations

• BarkerPullum1990.maximalGenerator R x a = ∃ (S : Node → Node → Prop), R ≤ S ∧ BarkerPullum1990.commandByRelation S = BarkerPullum1990.commandByRelation R ∧ S x a

theorem BarkerPullum1990.le_maximalGenerator {Node : Type u_1} [PartialOrder Node] (R : Node → Node → Prop) : R ≤ maximalGenerator R

theorem BarkerPullum1990.maximalGenerator_iff {Node : Type u_1} [PartialOrder Node] {a : Node} {R : Node → Node → Prop} {x : Node} : maximalGenerator R x a ↔ x < a → x ∈ lowerBounds (upperBounds {y : Node | y < a ∧ R y a})

The maximal generator relates to a whatever does not properly dominate it, and of its proper dominators those in the closure of its upper bounds under lowerBounds ∘ upperBounds: the nodes dominating everything a commands.

theorem BarkerPullum1990.commandByRelation_maximalGenerator {Node : Type u_1} [PartialOrder Node] (R : Node → Node → Prop) : commandByRelation (maximalGenerator R) = commandByRelation R

The maximal generator generates the same command relation.

theorem BarkerPullum1990.commandByRelation_union {Node : Type u_1} [PartialOrder Node] [IsLeftLinear Node] (R S : Node → Node → Prop) : commandByRelation R ∪ commandByRelation S = commandByRelation fun (x a : Node) => maximalGenerator R x a ∧ maximalGenerator S x a

Theorem 9, the Union Theorem: on a tree the union of two command relations is generated by the intersection of their maximal generators, so the relations that relations generate are closed under union.

theorem BarkerPullum1990.not_exists_isCompl_commandByRelation : ¬∃ (S : Fin 4 → Fin 4 → Prop), ((commandByRelation fun (x a : Fin 4) => x = 1 ∧ a = 3) ∩ commandByRelation S = commandByRelation fun (x x_1 : Fin 4) => True) ∧ (commandByRelation fun (x a : Fin 4) => x = 1 ∧ a = 3) ∪ commandByRelation S = Set.univ

The relations that relations generate are a lattice under intersection and union by Theorem 9, with the relation holding of every pair on top and IDC-command at the bottom, but not a Boolean one: on the chain of four nodes the relation that bounds the last node by the second has no complement.

The lattice of command relations

The relations that properties generate are closed under intersection and have a least member, and the paper's last footnote asks whether command relations carry a Boolean algebra. On a tree a generator matters only through its internal nodes, and distinct sets of internal nodes generate distinct relations, so under inclusion these relations are the sets of internal nodes under reverse inclusion. The join in that order is generated by the intersection of the generators; as the paper notes, the union of two such relations need not be one.

def BarkerPullum1990.internalNodes (Node : Type u_1) [PartialOrder Node] [OrderBot Node] : Set Node

The internal nodes are those that are neither the root nor a leaf.

Equations

• BarkerPullum1990.internalNodes Node = {x : Node | x ≠ ⊥ ∧ ¬IsMax x}

theorem BarkerPullum1990.commandRelation_inter_internalNodes {Node : Type u_1} [PartialOrder Node] [OrderBot Node] (P : Set Node) : PhraseStructure.commandRelation (P ∩ internalNodes Node) = PhraseStructure.commandRelation P

The root and the leaves of a generator do not affect the relation it generates.

theorem BarkerPullum1990.commandRelation_subset_commandRelation_iff {Node : Type u_1} [PartialOrder Node] {P Q : Set Node} [OrderBot Node] [IsLeftLinear Node] [WellFoundedLT Node] [IsStronglyCoatomic Node] : PhraseStructure.commandRelation P ⊆ PhraseStructure.commandRelation Q ↔ Q ∩ internalNodes Node ⊆ P

On a tree one command relation is included in another exactly when its generator contains the internal nodes of the other's. An internal node x missing from P shows in what a daughter of x commands: under P that includes the mother of x, which x does not dominate.

theorem BarkerPullum1990.commandRelation_eq_commandRelation_iff {Node : Type u_1} [PartialOrder Node] {P Q : Set Node} [OrderBot Node] [IsLeftLinear Node] [WellFoundedLT Node] [IsStronglyCoatomic Node] : PhraseStructure.commandRelation P = PhraseStructure.commandRelation Q ↔ P ∩ internalNodes Node = Q ∩ internalNodes Node

Two properties generate the same command relation on a tree exactly when they have the same internal nodes.

noncomputable def BarkerPullum1990.commandRelationIso {Node : Type u_1} [PartialOrder Node] [OrderBot Node] [IsLeftLinear Node] [WellFoundedLT Node] [IsStronglyCoatomic Node] : (Set ↑(internalNodes Node))ᵒᵈ ≃o ↑(Set.range PhraseStructure.commandRelation)

On a tree the command relations that properties generate, ordered by inclusion, are the sets of internal nodes ordered by reverse inclusion, and so a Boolean algebra.

Equations

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