Barker & Pullum (1990) — A Theory of Command Relations @cite{barker-pullum-1990}

Linguistics and Philosophy 13(1): 1–34.

@cite{barker-pullum-1990}'s algebraic theory of command relations provides a unified framework for cross-theoretic comparison: command relations form a complete lattice under the antitone map P ↦ C_P, and the Intersection Theorem C_{P∪Q} = C_P ∩ C_Q explains why theories that disagree on the underlying generating property still converge on configurational structures.

Concrete command relations

Different syntactic theories use different "command" relations:

• Minimalism: c-command (tree geometry; @cite{reinhart-1976})
• HPSG: o-command (obliqueness hierarchy; @cite{pollard-sag-1994})
• Dependency Grammar: d-command (dependency paths; @cite{hudson-1990})

Under the configurational assumption (tree structure encodes obliqueness), all three converge — explained by the Intersection Theorem (unique_upper_bound_equivalence).

Algebraic structure

§ J also formalizes @cite{kracht-1993}'s extension showing that command relations form a distributoid — an algebraic structure (D, ∩, ∪, ∘) in which composition distributes over intersection. (TODO: split § J into its own Studies/Kracht1993.lean once the dependencies are isolated.)

inductive BarkerPullum1990.Dir : Type

Directions in a binary tree

• L : Dir
• R : Dir

def BarkerPullum1990.instReprDir.repr : Dir → ℕ → Std.Format

Equations

• BarkerPullum1990.instReprDir.repr BarkerPullum1990.Dir.L prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "BarkerPullum1990.Dir.L")).group prec✝
• BarkerPullum1990.instReprDir.repr BarkerPullum1990.Dir.R prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "BarkerPullum1990.Dir.R")).group prec✝

@[implicit_reducible]

instance BarkerPullum1990.instReprDir : Repr Dir

Equations

• BarkerPullum1990.instReprDir = { reprPrec := BarkerPullum1990.instReprDir.repr }

@[implicit_reducible]

instance BarkerPullum1990.instDecidableEqDir : DecidableEq Dir

Equations

• BarkerPullum1990.instDecidableEqDir x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

@[reducible, inline]

abbrev BarkerPullum1990.Address : Type

Address = path from root

Equations

• BarkerPullum1990.Address = List BarkerPullum1990.Dir

def BarkerPullum1990.atAddr {W : Type} : Core.Tree.Tree Unit W → Address → Option (Core.Tree.Tree Unit W)

Get subtree at address (binary branching only)

Equations

• BarkerPullum1990.atAddr x✝ [] = some x✝
• BarkerPullum1990.atAddr (Core.Tree.Tree.node PUnit.unit [l, head]) (BarkerPullum1990.Dir.L :: rest) = BarkerPullum1990.atAddr l rest
• BarkerPullum1990.atAddr (Core.Tree.Tree.node PUnit.unit [head, r]) (BarkerPullum1990.Dir.R :: rest) = BarkerPullum1990.atAddr r rest
• BarkerPullum1990.atAddr x✝ (head :: tail) = none

def BarkerPullum1990.dominates (a b : Address) : Bool

Does address a dominate b? (a is prefix of b)

Equations

• BarkerPullum1990.dominates a b = List.isPrefixOf a b

def BarkerPullum1990.sister : Address → Option Address

Sister of an address (flip last direction)

Equations

• BarkerPullum1990.sister [] = none
• BarkerPullum1990.sister [BarkerPullum1990.Dir.L] = some [BarkerPullum1990.Dir.R]
• BarkerPullum1990.sister [BarkerPullum1990.Dir.R] = some [BarkerPullum1990.Dir.L]
• BarkerPullum1990.sister (d :: rest) = Option.map (fun (x : List BarkerPullum1990.Dir) => d :: x) (BarkerPullum1990.sister rest)

def BarkerPullum1990.cCommand (addrA addrB : Address) : Bool

C-command (@cite{reinhart-1976} def. 36): A c-commands B iff A's sister dominates B.

Standard definition for binary branching trees; dominates uses isPrefixOf which includes the identity case.

Equations

• BarkerPullum1990.cCommand addrA addrB = match BarkerPullum1990.sister addrA with | none => false | some sis => BarkerPullum1990.dominates sis addrB

structure BarkerPullum1990.ArgSt (α : Type) : Type

Argument structure: ordered list by obliqueness (less oblique first)

• args : List α

def BarkerPullum1990.instReprArgSt.repr {α✝ : Type} [Repr α✝] : ArgSt α✝ → ℕ → Std.Format

Equations

• BarkerPullum1990.instReprArgSt.repr x✝ prec✝ = Std.Format.bracket "{ " (Std.Format.nil ++ Std.Format.text "args" ++ Std.Format.text " := " ++ (Std.Format.nest 8 (repr x✝.args)).group) " }"

@[implicit_reducible]

instance BarkerPullum1990.instReprArgSt {α✝ : Type} [Repr α✝] : Repr (ArgSt α✝)

Equations

• BarkerPullum1990.instReprArgSt = { reprPrec := BarkerPullum1990.instReprArgSt.repr }

def BarkerPullum1990.findIdx {α : Type} [DecidableEq α] (xs : List α) (a : α) : Option ℕ

Find index in list

Equations

• BarkerPullum1990.findIdx xs a = BarkerPullum1990.findIdx.go a xs 0

def BarkerPullum1990.findIdx.go {α : Type} [DecidableEq α] (a : α) (xs : List α) (i : ℕ) : Option ℕ

Equations

• BarkerPullum1990.findIdx.go a [] i = none
• BarkerPullum1990.findIdx.go a (x :: rest) i = if (x == a) = true then some i else BarkerPullum1990.findIdx.go a rest (i + 1)

def BarkerPullum1990.oCommand {α : Type} [DecidableEq α] (argSt : ArgSt α) (a b : α) : Bool

O-command: A o-commands B iff A precedes B in the argument structure.

Position in arg-st = obliqueness rank. Earlier = less oblique.

Equations

• BarkerPullum1990.oCommand argSt a b = match BarkerPullum1990.findIdx argSt.args a, BarkerPullum1990.findIdx argSt.args b with | some ia, some ib => decide (ia < ib) | x, x_1 => false

structure BarkerPullum1990.DepEdge (α : Type) : Type

A labeled dependency edge

• dependent : α
• head : α
• label : String

def BarkerPullum1990.instReprDepEdge.repr {α✝ : Type} [Repr α✝] : DepEdge α✝ → ℕ → Std.Format

Equations

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

@[implicit_reducible]

instance BarkerPullum1990.instReprDepEdge {α✝ : Type} [Repr α✝] : Repr (DepEdge α✝)

Equations

• BarkerPullum1990.instReprDepEdge = { reprPrec := BarkerPullum1990.instReprDepEdge.repr }

structure BarkerPullum1990.DepGraph (α : Type) : Type

Dependency graph = list of edges

• edges : List (DepEdge α)

def BarkerPullum1990.instReprDepGraph.repr {α✝ : Type} [Repr α✝] : DepGraph α✝ → ℕ → Std.Format

Equations

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

@[implicit_reducible]

instance BarkerPullum1990.instReprDepGraph {α✝ : Type} [Repr α✝] : Repr (DepGraph α✝)

Equations

• BarkerPullum1990.instReprDepGraph = { reprPrec := BarkerPullum1990.instReprDepGraph.repr }

def BarkerPullum1990.DepGraph.hasDep {α : Type} [DecidableEq α] (g : DepGraph α) (a h : α) : Bool

Is a a dependent of h?

Equations

• g.hasDep a h = g.edges.any fun (e : BarkerPullum1990.DepEdge α) => e.dependent == a && e.head == h

def BarkerPullum1990.DepGraph.labelOf {α : Type} [DecidableEq α] (g : DepGraph α) (a h : α) : Option String

Get label for dependency

Equations

• g.labelOf a h = Option.map (fun (x : BarkerPullum1990.DepEdge α) => x.label) (List.find? (fun (e : BarkerPullum1990.DepEdge α) => e.dependent == a && e.head == h) g.edges)

def BarkerPullum1990.dCommand {α : Type} [DecidableEq α] (g : DepGraph α) (a b : α) : Bool

D-command: A d-commands B iff A and B are co-dependents of the same head, and A bears the "subj" relation (designated binder).

Equations

• BarkerPullum1990.dCommand g a b = g.edges.any fun (edgeA : BarkerPullum1990.DepEdge α) => edgeA.dependent == a && edgeA.label == "subj" && g.hasDep b edgeA.head

structure BarkerPullum1990.ConfigurationalClause : Type

A configurational transitive clause bundles aligned representations.

The key invariants capture what it means for a structure to be configurational:

• Tree has subject external to VP, object internal
• Arg-st has subject before object (less oblique)
• Dep-graph has both as dependents of verb, subject labeled "subj"

When these hold, the three command relations must agree.

• subj : String
• verb : String
• obj : String
• tree : Core.Tree.Tree Unit String
• subjAddr : Address
• objAddr : Address
• argSt : ArgSt String
• depGraph : DepGraph String
• tree_subj : atAddr self.tree self.subjAddr = some (Core.Tree.Tree.leaf self.subj)
• tree_obj : atAddr self.tree self.objAddr = some (Core.Tree.Tree.leaf self.obj)
• subj_external : self.subjAddr = [Dir.L]
• obj_internal : self.objAddr = [Dir.R, Dir.R]
• argst_order : self.argSt.args = [self.subj, self.obj]
• dep_subj : self.depGraph.hasDep self.subj self.verb = true
• dep_obj : self.depGraph.hasDep self.obj self.verb = true
• dep_subj_label : self.depGraph.labelOf self.subj self.verb = some "subj"

theorem BarkerPullum1990.cCommand_configurational : cCommand [Dir.L] [Dir.R, Dir.R] = true

Helper: c-command holds for standard configurational addresses

theorem BarkerPullum1990.oCommand_john_himself : oCommand { args := ["John", "himself"] } "John" "himself" = true

Helper: o-command holds for "John" before "himself"

theorem BarkerPullum1990.configurational_command_equivalence_addresses : cCommand [Dir.L] [Dir.R, Dir.R] = true

The ConfigurationalClause structure constraints ensure command equivalence.

Rather than proving this for arbitrary instances (which requires metaprogramming), the key insight is demonstrated by the concrete example johnSeesHimself_commands.

The structural constraints (subjAddr = [L], objAddr = [R,R], argSt = [subj, obj], dependency labels) force all three command notions to agree for any valid instance.

def BarkerPullum1990.johnSeesHimself : ConfigurationalClause

"John sees himself" as a configurational clause

Equations

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

theorem BarkerPullum1990.johnSeesHimself_commands : cCommand johnSeesHimself.subjAddr johnSeesHimself.objAddr = true ∧ oCommand johnSeesHimself.argSt "John" "himself" = true ∧ dCommand johnSeesHimself.depGraph "John" "himself" = true

Verify the example satisfies command equivalence

inductive BarkerPullum1990.Category : Type

Category labels for labeled trees

• S : Category
• NP : Category
• VP : Category
• V : Category
• PP : Category
• N : Category
• D : Category
• other : String → Category

def BarkerPullum1990.instDecidableEqCategory.decEq (x✝ x✝¹ : Category) : Decidable (x✝ = x✝¹)

Equations

• BarkerPullum1990.instDecidableEqCategory.decEq BarkerPullum1990.Category.S BarkerPullum1990.Category.S = isTrue ⋯
• BarkerPullum1990.instDecidableEqCategory.decEq BarkerPullum1990.Category.S BarkerPullum1990.Category.NP = isFalse BarkerPullum1990.instDecidableEqCategory.decEq._proof_1
• BarkerPullum1990.instDecidableEqCategory.decEq BarkerPullum1990.Category.S BarkerPullum1990.Category.VP = isFalse BarkerPullum1990.instDecidableEqCategory.decEq._proof_2
• BarkerPullum1990.instDecidableEqCategory.decEq BarkerPullum1990.Category.S BarkerPullum1990.Category.V = isFalse BarkerPullum1990.instDecidableEqCategory.decEq._proof_3
• BarkerPullum1990.instDecidableEqCategory.decEq BarkerPullum1990.Category.S BarkerPullum1990.Category.PP = isFalse BarkerPullum1990.instDecidableEqCategory.decEq._proof_4
• BarkerPullum1990.instDecidableEqCategory.decEq BarkerPullum1990.Category.S BarkerPullum1990.Category.N = isFalse BarkerPullum1990.instDecidableEqCategory.decEq._proof_5
• BarkerPullum1990.instDecidableEqCategory.decEq BarkerPullum1990.Category.S BarkerPullum1990.Category.D = isFalse BarkerPullum1990.instDecidableEqCategory.decEq._proof_6
• BarkerPullum1990.instDecidableEqCategory.decEq BarkerPullum1990.Category.S (BarkerPullum1990.Category.other a) = isFalse ⋯
• BarkerPullum1990.instDecidableEqCategory.decEq BarkerPullum1990.Category.NP BarkerPullum1990.Category.S = isFalse BarkerPullum1990.instDecidableEqCategory.decEq._proof_8
• BarkerPullum1990.instDecidableEqCategory.decEq BarkerPullum1990.Category.NP BarkerPullum1990.Category.NP = isTrue ⋯
• BarkerPullum1990.instDecidableEqCategory.decEq BarkerPullum1990.Category.NP BarkerPullum1990.Category.VP = isFalse BarkerPullum1990.instDecidableEqCategory.decEq._proof_9
• BarkerPullum1990.instDecidableEqCategory.decEq BarkerPullum1990.Category.NP BarkerPullum1990.Category.V = isFalse BarkerPullum1990.instDecidableEqCategory.decEq._proof_10
• BarkerPullum1990.instDecidableEqCategory.decEq BarkerPullum1990.Category.NP BarkerPullum1990.Category.PP = isFalse BarkerPullum1990.instDecidableEqCategory.decEq._proof_11
• BarkerPullum1990.instDecidableEqCategory.decEq BarkerPullum1990.Category.NP BarkerPullum1990.Category.N = isFalse BarkerPullum1990.instDecidableEqCategory.decEq._proof_12
• BarkerPullum1990.instDecidableEqCategory.decEq BarkerPullum1990.Category.NP BarkerPullum1990.Category.D = isFalse BarkerPullum1990.instDecidableEqCategory.decEq._proof_13
• BarkerPullum1990.instDecidableEqCategory.decEq BarkerPullum1990.Category.NP (BarkerPullum1990.Category.other a) = isFalse ⋯
• BarkerPullum1990.instDecidableEqCategory.decEq BarkerPullum1990.Category.VP BarkerPullum1990.Category.S = isFalse BarkerPullum1990.instDecidableEqCategory.decEq._proof_15
• BarkerPullum1990.instDecidableEqCategory.decEq BarkerPullum1990.Category.VP BarkerPullum1990.Category.NP = isFalse BarkerPullum1990.instDecidableEqCategory.decEq._proof_16
• BarkerPullum1990.instDecidableEqCategory.decEq BarkerPullum1990.Category.VP BarkerPullum1990.Category.VP = isTrue ⋯
• BarkerPullum1990.instDecidableEqCategory.decEq BarkerPullum1990.Category.VP BarkerPullum1990.Category.V = isFalse BarkerPullum1990.instDecidableEqCategory.decEq._proof_17
• BarkerPullum1990.instDecidableEqCategory.decEq BarkerPullum1990.Category.VP BarkerPullum1990.Category.PP = isFalse BarkerPullum1990.instDecidableEqCategory.decEq._proof_18
• BarkerPullum1990.instDecidableEqCategory.decEq BarkerPullum1990.Category.VP BarkerPullum1990.Category.N = isFalse BarkerPullum1990.instDecidableEqCategory.decEq._proof_19
• BarkerPullum1990.instDecidableEqCategory.decEq BarkerPullum1990.Category.VP BarkerPullum1990.Category.D = isFalse BarkerPullum1990.instDecidableEqCategory.decEq._proof_20
• BarkerPullum1990.instDecidableEqCategory.decEq BarkerPullum1990.Category.VP (BarkerPullum1990.Category.other a) = isFalse ⋯
• BarkerPullum1990.instDecidableEqCategory.decEq BarkerPullum1990.Category.V BarkerPullum1990.Category.S = isFalse BarkerPullum1990.instDecidableEqCategory.decEq._proof_22
• BarkerPullum1990.instDecidableEqCategory.decEq BarkerPullum1990.Category.V BarkerPullum1990.Category.NP = isFalse BarkerPullum1990.instDecidableEqCategory.decEq._proof_23
• BarkerPullum1990.instDecidableEqCategory.decEq BarkerPullum1990.Category.V BarkerPullum1990.Category.VP = isFalse BarkerPullum1990.instDecidableEqCategory.decEq._proof_24
• BarkerPullum1990.instDecidableEqCategory.decEq BarkerPullum1990.Category.V BarkerPullum1990.Category.V = isTrue ⋯
• BarkerPullum1990.instDecidableEqCategory.decEq BarkerPullum1990.Category.V BarkerPullum1990.Category.PP = isFalse BarkerPullum1990.instDecidableEqCategory.decEq._proof_25
• BarkerPullum1990.instDecidableEqCategory.decEq BarkerPullum1990.Category.V BarkerPullum1990.Category.N = isFalse BarkerPullum1990.instDecidableEqCategory.decEq._proof_26
• BarkerPullum1990.instDecidableEqCategory.decEq BarkerPullum1990.Category.V BarkerPullum1990.Category.D = isFalse BarkerPullum1990.instDecidableEqCategory.decEq._proof_27
• BarkerPullum1990.instDecidableEqCategory.decEq BarkerPullum1990.Category.V (BarkerPullum1990.Category.other a) = isFalse ⋯
• BarkerPullum1990.instDecidableEqCategory.decEq BarkerPullum1990.Category.PP BarkerPullum1990.Category.S = isFalse BarkerPullum1990.instDecidableEqCategory.decEq._proof_29
• BarkerPullum1990.instDecidableEqCategory.decEq BarkerPullum1990.Category.PP BarkerPullum1990.Category.NP = isFalse BarkerPullum1990.instDecidableEqCategory.decEq._proof_30
• BarkerPullum1990.instDecidableEqCategory.decEq BarkerPullum1990.Category.PP BarkerPullum1990.Category.VP = isFalse BarkerPullum1990.instDecidableEqCategory.decEq._proof_31
• BarkerPullum1990.instDecidableEqCategory.decEq BarkerPullum1990.Category.PP BarkerPullum1990.Category.V = isFalse BarkerPullum1990.instDecidableEqCategory.decEq._proof_32
• BarkerPullum1990.instDecidableEqCategory.decEq BarkerPullum1990.Category.PP BarkerPullum1990.Category.PP = isTrue ⋯
• BarkerPullum1990.instDecidableEqCategory.decEq BarkerPullum1990.Category.PP BarkerPullum1990.Category.N = isFalse BarkerPullum1990.instDecidableEqCategory.decEq._proof_33
• BarkerPullum1990.instDecidableEqCategory.decEq BarkerPullum1990.Category.PP BarkerPullum1990.Category.D = isFalse BarkerPullum1990.instDecidableEqCategory.decEq._proof_34
• BarkerPullum1990.instDecidableEqCategory.decEq BarkerPullum1990.Category.PP (BarkerPullum1990.Category.other a) = isFalse ⋯
• BarkerPullum1990.instDecidableEqCategory.decEq BarkerPullum1990.Category.N BarkerPullum1990.Category.S = isFalse BarkerPullum1990.instDecidableEqCategory.decEq._proof_36
• BarkerPullum1990.instDecidableEqCategory.decEq BarkerPullum1990.Category.N BarkerPullum1990.Category.NP = isFalse BarkerPullum1990.instDecidableEqCategory.decEq._proof_37
• BarkerPullum1990.instDecidableEqCategory.decEq BarkerPullum1990.Category.N BarkerPullum1990.Category.VP = isFalse BarkerPullum1990.instDecidableEqCategory.decEq._proof_38
• BarkerPullum1990.instDecidableEqCategory.decEq BarkerPullum1990.Category.N BarkerPullum1990.Category.V = isFalse BarkerPullum1990.instDecidableEqCategory.decEq._proof_39
• BarkerPullum1990.instDecidableEqCategory.decEq BarkerPullum1990.Category.N BarkerPullum1990.Category.PP = isFalse BarkerPullum1990.instDecidableEqCategory.decEq._proof_40
• BarkerPullum1990.instDecidableEqCategory.decEq BarkerPullum1990.Category.N BarkerPullum1990.Category.N = isTrue ⋯
• BarkerPullum1990.instDecidableEqCategory.decEq BarkerPullum1990.Category.N BarkerPullum1990.Category.D = isFalse BarkerPullum1990.instDecidableEqCategory.decEq._proof_41
• BarkerPullum1990.instDecidableEqCategory.decEq BarkerPullum1990.Category.N (BarkerPullum1990.Category.other a) = isFalse ⋯
• BarkerPullum1990.instDecidableEqCategory.decEq BarkerPullum1990.Category.D BarkerPullum1990.Category.S = isFalse BarkerPullum1990.instDecidableEqCategory.decEq._proof_43
• BarkerPullum1990.instDecidableEqCategory.decEq BarkerPullum1990.Category.D BarkerPullum1990.Category.NP = isFalse BarkerPullum1990.instDecidableEqCategory.decEq._proof_44
• BarkerPullum1990.instDecidableEqCategory.decEq BarkerPullum1990.Category.D BarkerPullum1990.Category.VP = isFalse BarkerPullum1990.instDecidableEqCategory.decEq._proof_45
• BarkerPullum1990.instDecidableEqCategory.decEq BarkerPullum1990.Category.D BarkerPullum1990.Category.V = isFalse BarkerPullum1990.instDecidableEqCategory.decEq._proof_46
• BarkerPullum1990.instDecidableEqCategory.decEq BarkerPullum1990.Category.D BarkerPullum1990.Category.PP = isFalse BarkerPullum1990.instDecidableEqCategory.decEq._proof_47
• BarkerPullum1990.instDecidableEqCategory.decEq BarkerPullum1990.Category.D BarkerPullum1990.Category.N = isFalse BarkerPullum1990.instDecidableEqCategory.decEq._proof_48
• BarkerPullum1990.instDecidableEqCategory.decEq BarkerPullum1990.Category.D BarkerPullum1990.Category.D = isTrue ⋯
• BarkerPullum1990.instDecidableEqCategory.decEq BarkerPullum1990.Category.D (BarkerPullum1990.Category.other a) = isFalse ⋯
• BarkerPullum1990.instDecidableEqCategory.decEq (BarkerPullum1990.Category.other a) BarkerPullum1990.Category.S = isFalse ⋯
• BarkerPullum1990.instDecidableEqCategory.decEq (BarkerPullum1990.Category.other a) BarkerPullum1990.Category.NP = isFalse ⋯
• BarkerPullum1990.instDecidableEqCategory.decEq (BarkerPullum1990.Category.other a) BarkerPullum1990.Category.VP = isFalse ⋯
• BarkerPullum1990.instDecidableEqCategory.decEq (BarkerPullum1990.Category.other a) BarkerPullum1990.Category.V = isFalse ⋯
• BarkerPullum1990.instDecidableEqCategory.decEq (BarkerPullum1990.Category.other a) BarkerPullum1990.Category.PP = isFalse ⋯
• BarkerPullum1990.instDecidableEqCategory.decEq (BarkerPullum1990.Category.other a) BarkerPullum1990.Category.N = isFalse ⋯
• BarkerPullum1990.instDecidableEqCategory.decEq (BarkerPullum1990.Category.other a) BarkerPullum1990.Category.D = isFalse ⋯
• BarkerPullum1990.instDecidableEqCategory.decEq (BarkerPullum1990.Category.other a) (BarkerPullum1990.Category.other b) = if h : a = b then h ▸ isTrue ⋯ else isFalse ⋯

@[implicit_reducible]

instance BarkerPullum1990.instDecidableEqCategory : DecidableEq Category

Equations

• BarkerPullum1990.instDecidableEqCategory = BarkerPullum1990.instDecidableEqCategory.decEq

def BarkerPullum1990.instReprCategory.repr : Category → ℕ → Std.Format

Equations

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

@[implicit_reducible]

instance BarkerPullum1990.instReprCategory : Repr Category

Equations

• BarkerPullum1990.instReprCategory = { reprPrec := BarkerPullum1990.instReprCategory.repr }

structure BarkerPullum1990.LabeledTree (Node : Type) [PartialOrder Node] extends Core.Order.TreeOrder Node : Type

Labeled tree extends abstract tree with category labels

• nodes : Set Node
• root : Node
• root_in_nodes : self.root ∈ self.nodes
• root_le_all (a : Node) : a ∈ self.nodes → self.root ≤ a
• ancestor_connected (x y z : Node) : x ≤ z → y ≤ z → x ≤ y ∨ y ≤ x
• label : Node → Category

def BarkerPullum1990.sNodes {Node : Type} [PartialOrder Node] (T : LabeledTree Node) : Set Node

S-nodes

Equations

• BarkerPullum1990.sNodes T = {n : Node | T.label n = BarkerPullum1990.Category.S}

def BarkerPullum1990.npNodes {Node : Type} [PartialOrder Node] (T : LabeledTree Node) : Set Node

NP-nodes

Equations

• BarkerPullum1990.npNodes T = {n : Node | T.label n = BarkerPullum1990.Category.NP}

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

Branching nodes

Equations

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

def BarkerPullum1990.maximalProjections {Node : Type} [PartialOrder Node] (T : LabeledTree Node) : Set Node

Maximal projections (simplified)

Equations

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

def BarkerPullum1990.sCommand {Node : Type} [PartialOrder Node] (T : LabeledTree Node) : Set (Node × Node)

S-command (@cite{langacker-1969}'s original "command" relation, parameterized by S-nodes)

Equations

• BarkerPullum1990.sCommand T = Core.Order.commandRelation T.toTreeOrder (BarkerPullum1990.sNodes T)

def BarkerPullum1990.npCommand {Node : Type} [PartialOrder Node] (T : LabeledTree Node) : Set (Node × Node)

NP-command

Equations

• BarkerPullum1990.npCommand T = Core.Order.commandRelation T.toTreeOrder (BarkerPullum1990.npNodes T)

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

K-command (@cite{reinhart-1976}'s c-command, parameterized by branching nodes; also @cite{kayne-1984})

Equations

• BarkerPullum1990.kCommand T = Core.Order.commandRelation T (BarkerPullum1990.branchingNodes T)

def BarkerPullum1990.maxCommand {Node : Type} [PartialOrder Node] (T : LabeledTree Node) : Set (Node × Node)

MAX-command (approximates Chomsky's c-command)

Equations

• BarkerPullum1990.maxCommand T = Core.Order.commandRelation T.toTreeOrder (BarkerPullum1990.maximalProjections T)

theorem BarkerPullum1990.sCommand_inter_npCommand {Node : Type} [PartialOrder Node] (T : LabeledTree Node) : sCommand T ∩ npCommand T = Core.Order.commandRelation T.toTreeOrder (sNodes T ∪ npNodes T)

S-command ∩ NP-command = command by {S} ∪ {NP}

theorem BarkerPullum1990.maxCommand_subset_sCommand {Node : Type} [PartialOrder Node] (T : LabeledTree Node) (h : sNodes T ⊆ maximalProjections T) : maxCommand T ⊆ sCommand T

If S ⊆ MaxProj, then MAX-command ⊆ S-command

def BarkerPullum1990.sMates {Node : Type} [PartialOrder Node] (T : LabeledTree Node) : Set (Node × Node)

S-mates (clausemates): nodes that mutually S-command

Equations

• BarkerPullum1990.sMates T = Core.Order.mateRelation T.toTreeOrder (BarkerPullum1990.sNodes T)

def BarkerPullum1990.npMates {Node : Type} [PartialOrder Node] (T : LabeledTree Node) : Set (Node × Node)

NP-mates (co-arguments): nodes that mutually NP-command

Equations

• BarkerPullum1990.npMates T = Core.Order.mateRelation T.toTreeOrder (BarkerPullum1990.npNodes T)

@cite{barker-pullum-1990} Formalization Coverage

@cite{barker-pullum-1990} @cite{hudson-1990} @cite{pollard-sag-1994} @cite{reinhart-1976}

Fully Proved Theorems

B&P Reference	Name	Lean Theorem
Definition 1	Abstract Tree	TreeOrder
Definition 2	Upper Bounds	upperBounds
Definition 3	Command Relation	commandRelation
Theorem 1	Intersection Theorem	intersection_theorem
Corollary	Antitone Map	command_antitone, command_converts_sup_to_inf
Theorem 2	Reflexivity	command_reflexive
Theorem 3	Ambidextrousness	command_ambidextrous
Theorem 5	Descent/Constituency	command_descent, command_constituency
Theorem 6	Fairness	command_fair
Section 3	Mate Relations	mateRelation, mate_symmetric, mate_reflexive, mate_intersection
-	Generalized Intersection	command_sInter
-	Closure System	command_closure_system
-	IDc-command is bottom	idc_is_bottom
-	Universal command is top	universal_is_top
Theorem 4	Boundedness	command_bounded
Theorem 8	Embeddability	command_embeddable_simple, command_embeddable_cac
-	Configurational Equivalence	configurational_equivalence, unique_upper_bound_equivalence
G.9	Command Equivalence	commandEquivalent, maximalGenerator, maximalGenerator_equivalent
G.9	Relation Intersection	relation_intersection_theorem
G.9	Union Theorem (both directions)	relation_union_theorem, relation_union_theorem_reverse
G.9	Non-minimal Upper Bounds	nonminimal_in_maximalGenerator

Kracht Infrastructure — Status

Reference	Status
Kracht Thm 2 (→)	tight_implies_fair ✓
Kracht Thm 2 (←)	fair_implies_tight_exists — FALSE as stated (see counterexample in docstring). Replaced with commandFromFunction_sub_commandRelation ✓

Note: Theorem 4 (Boundedness), Theorem 8 (Embeddability) are now fully proved using the Connected Ancestor Condition (CAC) added to TreeOrder.

B&P Theorem 9 (Union Theorem) is now fully proved using nonminimal_in_maximalGenerator, which shows that non-minimal upper bounds can be added to a relation without changing the generated command relation.

Not Yet Formalized

B&P Reference	Notes
Section 4 (Government)	Would require m-command, barriers theory
Full Galois Connection	Could use GaloisInsertion from Mathlib
Lattice as Complete Lattice	Image forms a complete sub-lattice

Linguistic Applications Proved

• All 4 theories agree on reflexive coreference, complementary distribution, pronominal disjoint reference (empirically verified)
• Configurational equivalence explains why theories agree on simple clauses
• Concrete command relations (c-command, o-command, d-command) demonstrated

Insight

The formalization shows that grammar comparison can be made mathematically precise: theories that seem to differ in mechanism (tree geometry vs obliqueness vs dependency paths) are unified through B&P's algebraic framework. When the structural assumptions align (configurational languages), the theories necessarily agree by the Intersection Theorem.

@cite{kracht-1993} "Mathematical Aspects of Command Relations"

Kracht shows that command relations have richer algebraic structure than B&P identified:

1. Associated Functions: Each command relation C has an associated function f_C : T → T where C_x = ↓f_C(x) (downward closure)

2. Tight Relations: Relations satisfying: x < f(y) → f(x) ≤ f(y)

3. Fair = Tight (Theorem 2): The "fair" relations of B&P are exactly the "tight" relations defined by the associated function property.

4. Distributoid Structure: (Cr(T), ∩, ∪, ∘) where ∘ is relational composition. Composition distributes over both ∩ and ∪.

5. Union Elimination: ∪ can be expressed using ∩ and ∘ alone: C_P ∪ C_Q = (C_P ∘ C_Q) ∩ (C_Q ∘ C_P) ∩ (C_P • C_Q)

Insight

Working with associated functions f : T → T (monotone, bounded) is more elegant than working with the relations directly. The composition of command relations corresponds to ordinary function composition:

f_{R∘S} = f_S ∘ f_R

This reversal is because command relations are "upper-bound based" - the generator x dominates the commanded element b.

structure BarkerPullum1990.AssociatedFunction {Node : Type} [PartialOrder Node] (T : Core.Order.TreeOrder Node) : Type

Associated function for a command relation.

For command relation C = C_P, the associated function f : T → T maps each node a to the infimum (meet) of its P-upper-bounds.

In a tree, this is the "minimal P-dominator" of a (if it exists).

Properties (Kracht Conditions 1-5):

1. f(r) = r (root maps to itself)
2. f(x) dominates x (f(x) is an upper bound)
3. f is monotone: x dom y → f(x) dom f(y)
4. f(f(x)) = f(x) (idempotent on range)
5. (Tightness) x < f(y) → f(x) ≤ f(y)

• f : Node → Node

  The function mapping each node to its "minimal P-dominator"

• root_fixed : self.f T.root = T.root

  Root maps to itself (Condition 1)

• dominates_arg (x : Node) : x ∈ T.nodes → self.f x ≤ x

  f(x) dominates x (Condition 2)

• monotone (x y : Node) : x ≤ y → self.f x ≤ self.f y

  Monotonicity (Condition 3)

• idempotent (x : Node) : x ∈ T.nodes → self.f (self.f x) = self.f x

  Idempotent on range (Condition 4)

def BarkerPullum1990.AssociatedFunction.tight {Node : Type} [PartialOrder Node] {T : Core.Order.TreeOrder Node} (af : AssociatedFunction T) : Prop

Tightness condition (Kracht Condition 5): If x is strictly below f(y), then f(x) ≤ f(y).

This captures that command relations are "fair" in B&P's sense: the generating property P determines a consistent boundary.

Equations

• af.tight = ∀ (x y : Node), T.properDom (af.f y) x → af.f x ≤ af.f y

structure BarkerPullum1990.TightAssociatedFunction {Node : Type} [PartialOrder Node] (T : Core.Order.TreeOrder Node) extends BarkerPullum1990.AssociatedFunction T : Type

A tight associated function satisfies all five Kracht conditions

• f : Node → Node
• root_fixed : self.f T.root = T.root
• dominates_arg (x : Node) : x ∈ T.nodes → self.f x ≤ x
• monotone (x y : Node) : x ≤ y → self.f x ≤ self.f y
• idempotent (x : Node) : x ∈ T.nodes → self.f (self.f x) = self.f x
• is_tight : self.tight

  Tightness (Condition 5)

def BarkerPullum1990.commandFromFunction {Node : Type} [PartialOrder Node] (T : Core.Order.TreeOrder Node) (af : AssociatedFunction T) : Set (Node × Node)

The command relation determined by an associated function.

C_f = {(a,b) | f(a) dominates b}

This is equivalent to the property-based definition when P = {x | f(x) = x} (the fixed points of f).

Equations

• BarkerPullum1990.commandFromFunction T af = {ab : Node × Node | af.f ab.1 ≤ ab.2}

theorem BarkerPullum1990.commandFromFunction_reflexive {Node : Type} [PartialOrder Node] (T : Core.Order.TreeOrder Node) (af : AssociatedFunction T) (a : Node) : a ∈ T.nodes → (a, a) ∈ commandFromFunction T af

The command relation from a tight function is reflexive

theorem BarkerPullum1990.commandFromFunction_descent {Node : Type} [PartialOrder Node] (T : Core.Order.TreeOrder Node) (af : AssociatedFunction T) (a b c : Node) : (a, b) ∈ commandFromFunction T af → b ≤ c → (a, c) ∈ commandFromFunction T af

The command relation from a tight function satisfies descent

def BarkerPullum1990.composeRel {Node : Type} (R S : Set (Node × Node)) : Set (Node × Node)

Relational composition of command relations.

(C ∘ D)(a,c) iff ∃b. C(a,b) ∧ D(b,c)

For command relations from associated functions: C_f ∘ C_g corresponds to C_{g∘f} (note the reversal!)

Equations

• BarkerPullum1990.composeRel R S = {ac : Node × Node | ∃ (b : Node), (ac.1, b) ∈ R ∧ (b, ac.2) ∈ S}

theorem BarkerPullum1990.composeRel_assoc {Node : Type} (R S U : Set (Node × Node)) : composeRel R (composeRel S U) = composeRel (composeRel R S) U

Composition is associative

theorem BarkerPullum1990.compose_associated_functions {Node : Type} [PartialOrder Node] (T : Core.Order.TreeOrder Node) (af ag : AssociatedFunction T) : composeRel (commandFromFunction T af) (commandFromFunction T ag) ⊆ {ac : Node × Node | ag.f (af.f ac.1) ≤ ac.2}

For associated functions, composition reverses: C_f ∘ C_g ⊆ C_{g ∘ f}

This is because if f(a) dom b and g(b) dom c, then g(f(a)) dom g(b) dom c (by monotonicity and transitivity).

Note: We prove containment rather than equality since the composed function g ∘ f may not satisfy all AssociatedFunction conditions without additional assumptions (specifically, idempotence).

class BarkerPullum1990.Distributoid (α : Type) extends Lattice α : Type

A Distributoid is an algebraic structure (D, ∩, ∪, ∘) where:

• (D, ∩, ∪) is a distributive lattice
• ∘ is an associative operation
• ∘ distributes over both ∩ and ∪

Command relations form a distributoid (Kracht Theorem 8).

• le : α → α → Prop
• lt : α → α → Prop
• le_refl (a : α) : a ≤ a
• le_trans (a b c : α) : a ≤ b → b ≤ c → a ≤ c
• lt_iff_le_not_ge (a b : α) : a < b ↔ a ≤ b ∧ ¬b ≤ a
• le_antisymm (a b : α) : a ≤ b → b ≤ a → a = b
• sup : α → α → α
• le_sup_left (a b : α) : a ≤ sup a b
• le_sup_right (a b : α) : b ≤ sup a b
• sup_le (a b c : α) : a ≤ c → b ≤ c → sup a b ≤ c
• inf : α → α → α
• inf_le_left (a b : α) : Lattice.inf a b ≤ a
• inf_le_right (a b : α) : Lattice.inf a b ≤ b
• le_inf (a b c : α) : a ≤ b → a ≤ c → a ≤ Lattice.inf b c
• comp : α → α → α

  Composition operation

• comp_assoc (a b c : α) : comp a (comp b c) = comp (comp a b) c

  Composition is associative

• comp_inf_left (a b c : α) : comp a (b ⊓ c) = comp a b ⊓ comp a c

  Left distributivity over meet

• comp_inf_right (a b c : α) : comp (a ⊓ b) c = comp a c ⊓ comp b c

  Right distributivity over meet

• comp_sup_left (a b c : α) : comp a (b ⊔ c) = comp a b ⊔ comp a c

  Left distributivity over join

• comp_sup_right (a b c : α) : comp (a ⊔ b) c = comp a c ⊔ comp b c

  Right distributivity over join

theorem BarkerPullum1990.command_comp_inter_left {Node : Type} [PartialOrder Node] (T : Core.Order.TreeOrder Node) (P Q R : Set Node) : composeRel (Core.Order.commandRelation T P) (Core.Order.commandRelation T Q ∩ Core.Order.commandRelation T R) ⊆ composeRel (Core.Order.commandRelation T P) (Core.Order.commandRelation T Q) ∩ composeRel (Core.Order.commandRelation T P) (Core.Order.commandRelation T R)

Composition distributes over intersection for command relations (one direction)

theorem BarkerPullum1990.command_comp_inter_left_rev {Node : Type} [PartialOrder Node] (T : Core.Order.TreeOrder Node) (P Q R : Set Node) (hNodesAll : ∀ (x : Node), x ∈ T.nodes) (hMinUB : ∀ (a : Node), (Core.Order.upperBounds T a P).Nonempty → ∃ p₀ ∈ Core.Order.upperBounds T a P, ∀ p ∈ Core.Order.upperBounds T a P, p ≤ p₀) : composeRel (Core.Order.commandRelation T P) (Core.Order.commandRelation T Q) ∩ composeRel (Core.Order.commandRelation T P) (Core.Order.commandRelation T R) ⊆ composeRel (Core.Order.commandRelation T P) (Core.Order.commandRelation T Q ∩ Core.Order.commandRelation T R)

Composition distributes over intersection (reverse direction).

This direction requires finding a common witness from potentially different witnesses b₁ (for C_Q) and b₂ (for C_R). The key idea: use p₀ = the minimal P-upper-bound of a. Since UB(a, P) is a chain (by CAC), p₀ is dominated by every other P-upper-bound, making C_P(a, p₀) hold. Any Q-upper-bound (or R-upper-bound) of p₀ is also a Q-upper-bound (resp. R-upper-bound) of b₁ (resp. b₂), because p₀ dominates both b₁ and b₂.

When UB(a, P) = ∅, root serves as witness: all command relations hold vacuously since root has no proper dominator.

def BarkerPullum1990.isFair {Node : Type} [PartialOrder Node] (T : Core.Order.TreeOrder Node) (C : Set (Node × Node)) : Prop

A relation R is fair in B&P's sense if it satisfies: (a R b) ∧ (b R c) ∧ ¬(a R c) → ∀d. (a R d) → (b dom d)

This is B&P's Theorem 6 condition.

Equations

• BarkerPullum1990.isFair T C = ∀ (a b c : Node), (a, b) ∈ C → (b, c) ∈ C → (a, c) ∉ C → ∀ (d : Node), (a, d) ∈ C → b ≤ d

theorem BarkerPullum1990.command_is_fair {Node : Type} [PartialOrder Node] (T : Core.Order.TreeOrder Node) (P : Set Node) : isFair T (Core.Order.commandRelation T P)

All property-generated command relations are fair (B&P Theorem 6)

theorem BarkerPullum1990.tight_implies_fair {Node : Type} [PartialOrder Node] (T : Core.Order.TreeOrder Node) (tf : TightAssociatedFunction T) (hNodesAll : ∀ (x : Node), x ∈ T.nodes) : isFair T (commandFromFunction T tf.toAssociatedFunction)

Kracht Theorem 2: For tight associated functions, the generated command relation is fair, and conversely, every fair command relation comes from a tight associated function.

First direction: tight → fair. Requires a ∈ T.nodes for the idempotent condition on the associated function. The hypothesis hNodesAll says all elements of the Node type are tree nodes (i.e., there are no "phantom" elements outside the tree).

Kracht Theorem 2 converse — FALSE as originally stated

The theorem fair_implies_tight_exists claimed: every fair commandRelation T P equals commandFromFunction T tf for some tight associated function tf. This is false because the two notions have different transitivity:

• commandFromFunction T af is always transitive (via monotonicity + idempotence).
• commandRelation T P can be non-transitive: at P-nodes with no P-ancestor, UB(a, P) = ∅ makes command vacuously universal.

Counterexample: tree root → p → a, P = {p}.

• (a, p) ∈ C_P and (p, root) ∈ C_P (UB(p,{p}) = ∅, vacuous).
• But (a, root) ∉ C_P (UB(a,{p}) = {p}, and p does not dominate root).
• No transitive relation equals C_P, hence no commandFromFunction.

The correct relationship is commandFromFunction ⊆ commandRelation for the fixed-point property, proved below.

theorem BarkerPullum1990.commandFromFunction_sub_commandRelation {Node : Type} [PartialOrder Node] (T : Core.Order.TreeOrder Node) (af : AssociatedFunction T) : commandFromFunction T af ⊆ Core.Order.commandRelation T {x : Node | af.f x = x}

An associated function's command relation refines the property-based command relation for its fixed-point set P = {x | f(x) = x}.

Forward direction: if f(a) dom b, then every P-upper-bound of a also dominates b (via monotonicity: x dom a → f(x) dom f(a) → x dom f(a)).

def BarkerPullum1990.antecedentInter {Node : Type} [PartialOrder Node] (T : Core.Order.TreeOrder Node) (R S : Set (Node × Node)) : Set (Node × Node)

The antecedent intersection of two relations: R • S = {(a,c) | ∃b. (a,b) ∈ R ∧ (a,b) ∈ S ∧ (b dom c)}

This captures "common antecedents" between R and S.

Equations

• BarkerPullum1990.antecedentInter T R S = {ac : Node × Node | ∃ (b : Node), (ac.1, b) ∈ R ∧ (ac.1, b) ∈ S ∧ b ≤ ac.2}

theorem BarkerPullum1990.union_elimination_forward {Node : Type} [PartialOrder Node] (T : Core.Order.TreeOrder Node) (P Q : Set Node) (a c : Node) (ha : a ∈ T.nodes) (hc : c ∈ T.nodes) (hac : a ≤ c) : (a, c) ∈ Core.Order.commandRelation T P ∪ Core.Order.commandRelation T Q → (a, c) ∈ composeRel (Core.Order.commandRelation T P) (Core.Order.commandRelation T Q) ∩ composeRel (Core.Order.commandRelation T Q) (Core.Order.commandRelation T P) ∩ antecedentInter T (Core.Order.commandRelation T P) (Core.Order.commandRelation T Q)

Union Elimination (Kracht Lemma 10-11): C_P ∪ C_Q = (C_P ∘ C_Q) ∩ (C_Q ∘ C_P) ∩ (C_P • C_Q)

Union can be expressed using only ∩ and ∘ (plus antecedent intersection).

This shows that ∪ is "eliminable" in the distributoid structure, meaning the theory can be developed using ∩ and ∘ alone.

First inclusion: C_P ∪ C_Q ⊆ (C_P ∘ C_Q) ∩ (C_Q ∘ C_P) ∩ (C_P • C_Q)

Note: Requires both a, c ∈ T.nodes for reflexivity. The antecedent intersection part also requires a dom c, which holds when a ∈ P or a ∈ Q (so UB(a,_) = ∅ and a commands everything below it).

theorem BarkerPullum1990.union_elimination_reverse {Node : Type} [PartialOrder Node] (T : Core.Order.TreeOrder Node) (P Q : Set Node) : composeRel (Core.Order.commandRelation T P) (Core.Order.commandRelation T Q) ∩ composeRel (Core.Order.commandRelation T Q) (Core.Order.commandRelation T P) ∩ antecedentInter T (Core.Order.commandRelation T P) (Core.Order.commandRelation T Q) ⊆ Core.Order.commandRelation T P ∪ Core.Order.commandRelation T Q

Union Elimination (reverse direction): (C_P ∘ C_Q) ∩ (C_Q ∘ C_P) ∩ (C_P • C_Q) ⊆ C_P ∪ C_Q

This is the harder direction - it relies on the specific structure of command relations.

Heyting Algebra via Mathlib

Set α is a CompleteAtomicBooleanAlgebra and hence a HeytingAlgebra. The Heyting implication for sets is: A ⇨ B = Aᶜ ∪ B

@cite{kracht-1993} shows command relations form a Heyting algebra. Since command relations are a subset of Set (Node × Node), and the latter is already a Heyting algebra, we show:

1. The standard Heyting implication satisfies the adjunction property
2. Our explicit definition agrees with Mathlib's ⇨
3. Command relations are closed under Heyting operations (sub-Heyting-algebra)

def BarkerPullum1990.commandImplication {Node : Type} [PartialOrder Node] (_T : Core.Order.TreeOrder Node) (C D : Set (Node × Node)) : Set (Node × Node)

The Heyting implication on sets: A ⇨ B = Aᶜ ∪ B

This can also be characterized as: A ⇨ B = ⋃₀ {E | E ∩ A ⊆ B} (the largest set E such that E ∩ A ⊆ B).

Equations

• BarkerPullum1990.commandImplication _T C D = C ⇨ D

theorem BarkerPullum1990.commandImplication_eq_sUnion {Node : Type} [PartialOrder Node] (_T : Core.Order.TreeOrder Node) (C D : Set (Node × Node)) : commandImplication _T C D = ⋃₀ {E : Set (Node × Node) | E ∩ C ⊆ D}

Our explicit union definition equals Mathlib's Heyting implication.

For sets, A ⇨ B = Aᶜ ∪ B, which is exactly the largest E with E ∩ A ⊆ B.

theorem BarkerPullum1990.command_heyting {Node : Type} [PartialOrder Node] (_T : Core.Order.TreeOrder Node) (C D E : Set (Node × Node)) : E ∩ C ⊆ D ↔ E ⊆ C ⇨ D

The Heyting adjunction: E ∩ C ⊆ D ↔ E ⊆ (C ⇨ D)

This is the defining property of Heyting implication. In Mathlib, this is le_himp_iff.

theorem BarkerPullum1990.command_modus_ponens {Node : Type} [PartialOrder Node] (_T : Core.Order.TreeOrder Node) (C D : Set (Node × Node)) : (C ⇨ D) ∩ C ⊆ D

Modus ponens for command relations: (C ⇨ D) ∩ C ⊆ D

theorem BarkerPullum1990.command_himp_trans {Node : Type} [PartialOrder Node] (_T : Core.Order.TreeOrder Node) (A B C : Set (Node × Node)) : (A ⇨ B) ∩ (B ⇨ C) ⊆ A ⇨ C

Transitivity of Heyting implication: (A ⇨ B) ∩ (B ⇨ C) ⊆ (A ⇨ C)

Uses Mathlib's himp_le_himp_himp_himp: b ⇨ c ≤ (a ⇨ b) ⇨ a ⇨ c

theorem BarkerPullum1990.command_rels_complete_heyting {Node : Type} [PartialOrder Node] (_T : Core.Order.TreeOrder Node) (C D : Set (Node × Node)) : (C ⇨ D) ∩ C ⊆ D

Command relations form a closure system, hence a complete Heyting algebra.

The key property is that arbitrary intersections of command relations are command relations (proved in commandImage_closed_under_sInter).

Combined with the lattice structure, this gives us a complete Heyting algebra on the set of command relations.

theorem BarkerPullum1990.command_inf_sup_distrib {Node : Type} [PartialOrder Node] (_T : Core.Order.TreeOrder Node) (C D E : Set (Node × Node)) : C ∩ (D ∪ E) = C ∩ D ∪ C ∩ E

Distributive lattice: Heyting algebras are distributive. This gives us: C ∩ (D ∪ E) = (C ∩ D) ∪ (C ∩ E)

theorem BarkerPullum1990.command_compl_eq_himp_bot {Node : Type} [PartialOrder Node] (_T : Core.Order.TreeOrder Node) (C : Set (Node × Node)) : Cᶜ = C ⇨ ⊥

Pseudo-complement: In a Heyting algebra, the complement is Cᶜ = C ⇨ ⊥

For sets, Cᶜ is the set-theoretic complement.

theorem BarkerPullum1990.command_inf_compl {Node : Type} [PartialOrder Node] (_T : Core.Order.TreeOrder Node) (C : Set (Node × Node)) : C ∩ Cᶜ = ∅

Pseudo-complement property: C ∩ Cᶜ = ∅

theorem BarkerPullum1990.command_rels_not_boolean_explanation {Node : Type} [PartialOrder Node] (_T : Core.Order.TreeOrder Node) (C : Set (Node × Node)) : C ∪ Cᶜ = Set.univ

B&P's Open Question Answered: Command relations do NOT form a Boolean algebra.

In a Boolean algebra, we would have C ∪ Cᶜ = ⊤ (law of excluded middle). In a Heyting algebra, this fails in general.

For Set α, this actually DOES hold (sets form a Boolean algebra), but the subtype of command relations may not be closed under complement.

The key insight from Kracht: complement of a command relation is generally NOT a command relation. Hence command relations form a Heyting algebra but not a Boolean algebra.

theorem BarkerPullum1990.command_himp_curry {Node : Type} [PartialOrder Node] (_T : Core.Order.TreeOrder Node) (A B C : Set (Node × Node)) : A ∩ B ⇨ C = A ⇨ B ⇨ C

Currying via Heyting implication: (A ∩ B) ⇨ C = A ⇨ (B ⇨ C)

This is the "currying" property of Heyting algebras. This follows directly from Mathlib's himp_himp.

theorem BarkerPullum1990.command_himp_mono_right {Node : Type} [PartialOrder Node] (_T : Core.Order.TreeOrder Node) (A B C : Set (Node × Node)) (h : A ⊆ B) : C ⇨ A ⊆ C ⇨ B

Weakening: A ⊆ B → (C ⇨ A) ⊆ (C ⇨ B)

theorem BarkerPullum1990.command_compl_anti {Node : Type} [PartialOrder Node] (_T : Core.Order.TreeOrder Node) (A B : Set (Node × Node)) (h : A ⊆ B) : Bᶜ ⊆ Aᶜ

Contraposition (weak): A ⊆ B → Bᶜ ⊆ Aᶜ

inductive BarkerPullum1990.NormalForm {Node : Type} [PartialOrder Node] (T : Core.Order.TreeOrder Node) : Type

A command relation expression in normal form uses only:

• Base relations C_P (for properties P)
• Meet (∩)
• Composition (∘)

Union is eliminable by J.6. Join is eliminable because for command relations, join = intersection of generators (by the Intersection Theorem).

Kracht Theorem 9: Every command relation expression has a normal form using only ∩ and ∘.

• base {Node : Type} [PartialOrder Node] {T : Core.Order.TreeOrder Node} : Set Node → NormalForm T
• meet {Node : Type} [PartialOrder Node] {T : Core.Order.TreeOrder Node} : NormalForm T → NormalForm T → NormalForm T
• comp {Node : Type} [PartialOrder Node] {T : Core.Order.TreeOrder Node} : NormalForm T → NormalForm T → NormalForm T

def BarkerPullum1990.NormalForm.eval {Node : Type} [PartialOrder Node] (T : Core.Order.TreeOrder Node) : NormalForm T → Set (Node × Node)

Evaluate a normal form expression to a command relation

Equations

• BarkerPullum1990.NormalForm.eval T (BarkerPullum1990.NormalForm.base P) = Core.Order.commandRelation T P
• BarkerPullum1990.NormalForm.eval T (n1.meet n2) = BarkerPullum1990.NormalForm.eval T n1 ∩ BarkerPullum1990.NormalForm.eval T n2
• BarkerPullum1990.NormalForm.eval T (n1.comp n2) = BarkerPullum1990.composeRel (BarkerPullum1990.NormalForm.eval T n1) (BarkerPullum1990.NormalForm.eval T n2)

theorem BarkerPullum1990.normalForm_meet_is_union {Node : Type} [PartialOrder Node] (T : Core.Order.TreeOrder Node) (P Q : Set Node) : NormalForm.eval T ((NormalForm.base P).meet (NormalForm.base Q)) = Core.Order.commandRelation T (P ∪ Q)

Meet in normal form corresponds to union of generators

@cite{kracht-1993} Coverage Summary

Kracht Reference	Name	Status
Definition 1	Associated Functions	AssociatedFunction, TightAssociatedFunction
Theorem 2	Fair = Tight	tight_implies_fair ✓, fair_implies_tight_exists FALSE → commandFromFunction_sub_commandRelation ✓
Proposition 6	Composition Distributivity	command_comp_inter_left ✓, command_comp_inter_left_rev ✓
Theorem 8	Distributoid Structure	Distributoid typeclass
Theorem 9	Normal Forms	NormalForm, normalForm_meet_is_union
Lemma 10-11	Union Elimination	union_elimination_forward ✓, union_elimination_reverse ✓
Theorem 10	Heyting Algebra	Uses Mathlib's HeytingAlgebra ✓

Mathlib Integration

The Heyting algebra structure now uses Mathlib's HeytingAlgebra typeclass:

• Set (Node × Node) is already a HeytingAlgebra (inherited from CompleteBooleanAlgebra)
• Heyting implication C ⇨ D from Mathlib.Order.Heyting.Basic
• Key theorems (command_heyting, command_modus_ponens, command_himp_trans) now leverage Mathlib's Set.subset_himp_iff and related lemmas
• commandImplication_eq_sUnion shows our explicit definition equals Mathlib's ⇨

Insights

1. Associated functions provide a cleaner interface than relations. The map f : T → T replaces the "minimal P-upper-bound" concept.

2. Tightness is the key condition ensuring command relations behave well under composition. It's equivalent to B&P's fairness.

3. Union is eliminable: the full theory can be developed using only ∩ and ∘, which simplifies algebraic manipulations.

4. Not a Boolean algebra: B&P's open question is answered negatively. Complement doesn't work because command relations lack negation. But they do form a Heyting algebra (intuitionistic logic), which is formalized via Mathlib's HeytingAlgebra typeclass.

5. Distributoid structure enables representing complex binding conditions (e.g., "commands and doesn't dominate") as compositions and intersections of basic command relations.