Documentation

def Comparisons.CommandRelations.AbstractTree.properDom {Node : Type} (T : AbstractTree Node) (a b : Node) :

Proper dominance: a properly dominates b iff a dominates b and a ≠ b

Equations

T.properDom a b = (T.dom a b ∧ a ≠ b)

Instances For

def Comparisons.CommandRelations.upperBounds {Node : Type} (T : AbstractTree Node) (a : Node) (P : Set Node) :

Set Node

Upper bounds of a node with respect to property P (B&P Definition 2). UB(a, P) = {b | b properly dominates a ∧ b ∈ P}

Equations

Comparisons.CommandRelations.upperBounds T a P = {b : Node | T.properDom b a ∧ b ∈ P}

Instances For

def Comparisons.CommandRelations.commandRelation {Node : Type} (T : AbstractTree Node) (P : Set Node) :

Set (Node × Node)

Command relation generated by property P (B&P Definition 3). C_P = {(a,b) | ∀x ∈ UB(a,P). x dominates b}

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

Equations

Comparisons.CommandRelations.commandRelation T P = {ab : Node × Node | ∀ x ∈ Comparisons.CommandRelations.upperBounds T ab.1 P, T.dom x ab.2}

Instances For

theorem Comparisons.CommandRelations.intersection_theorem {Node : Type} (T : AbstractTree Node) (P Q : Set Node) :

commandRelation T P ∩ commandRelation T Q = commandRelation T (P ∪ Q)

Theorem 1 (Intersection Theorem): C_P ∩ C_Q = C_{P∪Q}

This is the central algebraic result: union of properties gives intersection of command relations.

theorem Comparisons.CommandRelations.command_antitone {Node : Type} (T : AbstractTree Node) (P Q : Set Node) (hPQ : P ⊆ Q) :

commandRelation T Q ⊆ commandRelation T P

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

def Comparisons.CommandRelations.maximalProperty {Node : Type} (T : AbstractTree Node) :

Set Node

Maximal property: all nodes

Equations

Comparisons.CommandRelations.maximalProperty T = T.nodes

Instances For

def Comparisons.CommandRelations.emptyProperty {Node : Type} :

Set Node

Empty property

Equations

Comparisons.CommandRelations.emptyProperty = ∅

Instances For

def Comparisons.CommandRelations.idcCommand {Node : Type} (T : AbstractTree Node) :

Set (Node × Node)

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

Equations

Comparisons.CommandRelations.idcCommand T = Comparisons.CommandRelations.commandRelation T (Comparisons.CommandRelations.maximalProperty T)

Instances For

def Comparisons.CommandRelations.universalCommand {Node : Type} (T : AbstractTree Node) :

Set (Node × Node)

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

Equations

Comparisons.CommandRelations.universalCommand T = Comparisons.CommandRelations.commandRelation T Comparisons.CommandRelations.emptyProperty

Instances For

theorem Comparisons.CommandRelations.idc_is_bottom {Node : Type} (T : AbstractTree 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

theorem Comparisons.CommandRelations.universal_is_top {Node : Type} (T : AbstractTree Node) (P : Set Node) :

commandRelation T P ⊆ universalCommand T

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

theorem Comparisons.CommandRelations.command_reflexive {Node : Type} (T : AbstractTree Node) (P : Set Node) (a : Node) :

a ∈ T.nodes → (a, a) ∈ commandRelation T P

All command relations are reflexive

theorem Comparisons.CommandRelations.command_descent {Node : Type} (T : AbstractTree Node) (P : Set Node) (a b c : Node) :

(a, b) ∈ commandRelation T P → T.dom b c → (a, c) ∈ commandRelation T P

All command relations satisfy constituency/descent

theorem Comparisons.CommandRelations.configurational_equivalence {Node : Type} (T : AbstractTree Node) (P Q : Set Node) (a : Node) :

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 Comparisons.CommandRelations.same_upper_bounds_same_command {Node : Type} (T : AbstractTree 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

Corollary: If P and Q have the same nodes above a, C_P(a,-) = C_Q(a,-)

theorem Comparisons.CommandRelations.unique_upper_bound_equivalence {Node : Type} (T : AbstractTree 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 that properly dominates 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.

inductive Comparisons.CommandRelations.PTree (α : Type) :

A minimal binary tree for phrase structure

leaf {α : Type} : α → PTree α
branch {α : Type} : PTree α → PTree α → PTree α

Instances For

def Comparisons.CommandRelations.instReprPTree.repr {α✝ : Type} [Repr α✝] :

PTree α✝ → ℕ → Std.Format

Equations

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

Instances For

instance Comparisons.CommandRelations.instReprPTree {α✝ : Type} [Repr α✝] :

Repr (PTree α✝)

Equations

Comparisons.CommandRelations.instReprPTree = { reprPrec := Comparisons.CommandRelations.instReprPTree.repr }

def Comparisons.CommandRelations.instDecidableEqPTree.decEq {α✝ : Type} [DecidableEq α✝] (x✝ x✝¹ : PTree α✝) :

Decidable (x✝ = x✝¹)

Equations

One or more equations did not get rendered due to their size.
Comparisons.CommandRelations.instDecidableEqPTree.decEq (Comparisons.CommandRelations.PTree.leaf a) (Comparisons.CommandRelations.PTree.leaf b) = if h : a = b then h ▸ isTrue ⋯ else isFalse ⋯
Comparisons.CommandRelations.instDecidableEqPTree.decEq (Comparisons.CommandRelations.PTree.leaf a) (a_1.branch a_2) = isFalse ⋯
Comparisons.CommandRelations.instDecidableEqPTree.decEq (a.branch a_1) (Comparisons.CommandRelations.PTree.leaf a_2) = isFalse ⋯

Instances For

instance Comparisons.CommandRelations.instDecidableEqPTree {α✝ : Type} [DecidableEq α✝] :

DecidableEq (PTree α✝)

Equations

Comparisons.CommandRelations.instDecidableEqPTree = Comparisons.CommandRelations.instDecidableEqPTree.decEq

inductive Comparisons.CommandRelations.Dir :

Directions in a binary tree

L : Dir
R : Dir

Instances For

def Comparisons.CommandRelations.instReprDir.repr :

Dir → ℕ → Std.Format

Equations

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

Instances For

instance Comparisons.CommandRelations.instReprDir :

Repr Dir

Equations

Comparisons.CommandRelations.instReprDir = { reprPrec := Comparisons.CommandRelations.instReprDir.repr }

instance Comparisons.CommandRelations.instDecidableEqDir :

DecidableEq Dir

Equations

Comparisons.CommandRelations.instDecidableEqDir x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

@[reducible, inline]

abbrev Comparisons.CommandRelations.Address :

Address = path from root

Equations

Comparisons.CommandRelations.Address = List Comparisons.CommandRelations.Dir

Instances For

def Comparisons.CommandRelations.PTree.at {α : Type} (t : PTree α) :

Address → Option (PTree α)

Get subtree at address

Equations

t.at [] = some t
(Comparisons.CommandRelations.PTree.leaf a).at (Comparisons.CommandRelations.Dir.L :: rest) = none
(a.branch a_1).at (Comparisons.CommandRelations.Dir.L :: rest) = a.at rest
(Comparisons.CommandRelations.PTree.leaf a).at (Comparisons.CommandRelations.Dir.R :: rest) = none
(a.branch a_1).at (Comparisons.CommandRelations.Dir.R :: rest) = a_1.at rest

Instances For

def Comparisons.CommandRelations.dominates (a b : Address) :

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

Equations

Comparisons.CommandRelations.dominates a b = List.isPrefixOf a b

Instances For

def Comparisons.CommandRelations.sister :

Address → Option Address

Sister of an address (flip last direction)

Equations

Instances For

def Comparisons.CommandRelations.cCommand (addrA addrB : Address) :

C-command: A c-commands B iff A's sister dominates B (or equals B).

This is the standard definition for binary branching trees.

Equations

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

Instances For

structure Comparisons.CommandRelations.ArgSt (α : Type) :

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

args : List α

Instances For

instance Comparisons.CommandRelations.instReprArgSt {α✝ : Type} [Repr α✝] :

Repr (ArgSt α✝)

Equations

Comparisons.CommandRelations.instReprArgSt = { reprPrec := Comparisons.CommandRelations.instReprArgSt.repr }

def Comparisons.CommandRelations.instReprArgSt.repr {α✝ : Type} [Repr α✝] :

ArgSt α✝ → ℕ → Std.Format

Equations

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

Instances For

def Comparisons.CommandRelations.findIdx {α : Type} [DecidableEq α] (xs : List α) (a : α) :

Option ℕ

Find index in list

Equations

Comparisons.CommandRelations.findIdx xs a = Comparisons.CommandRelations.findIdx.go a xs 0

Instances For

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

Option ℕ

Equations

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

Instances For

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

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

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

Equations

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

Instances For

structure Comparisons.CommandRelations.DepEdge (α : Type) :

A labeled dependency edge

dependent : α
head : α
label : String

Instances For

instance Comparisons.CommandRelations.instReprDepEdge {α✝ : Type} [Repr α✝] :

Repr (DepEdge α✝)

Equations

Comparisons.CommandRelations.instReprDepEdge = { reprPrec := Comparisons.CommandRelations.instReprDepEdge.repr }

def Comparisons.CommandRelations.instReprDepEdge.repr {α✝ : Type} [Repr α✝] :

DepEdge α✝ → ℕ → Std.Format

Equations

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

Instances For

structure Comparisons.CommandRelations.DepGraph (α : Type) :

Dependency graph = list of edges

edges : List (DepEdge α)

Instances For

def Comparisons.CommandRelations.instReprDepGraph.repr {α✝ : Type} [Repr α✝] :

DepGraph α✝ → ℕ → Std.Format

Equations

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

Instances For

instance Comparisons.CommandRelations.instReprDepGraph {α✝ : Type} [Repr α✝] :

Repr (DepGraph α✝)

Equations

Comparisons.CommandRelations.instReprDepGraph = { reprPrec := Comparisons.CommandRelations.instReprDepGraph.repr }

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

Is a a dependent of h?

Equations

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

Instances For

def Comparisons.CommandRelations.DepGraph.labelOf {α : Type} [DecidableEq α] (g : DepGraph α) (a h : α) :

Option String

Get label for dependency

Equations

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

Instances For

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

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

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

Instances For

structure Comparisons.CommandRelations.ConfigurationalClause :

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 : PTree String
subjAddr : Address
objAddr : Address
argSt : ArgSt String
depGraph : DepGraph String
tree_subj : self.tree.at self.subjAddr = some (PTree.leaf self.subj)
tree_obj : self.tree.at self.objAddr = some (PTree.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"

Instances For

theorem Comparisons.CommandRelations.cCommand_configurational :

cCommand [Dir.L ] [Dir.R , Dir.R ] = true

Helper: c-command holds for standard configurational addresses

theorem Comparisons.CommandRelations.oCommand_john_himself :

oCommand { args := ["John", "himself"] } "John" "himself" = true

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

theorem Comparisons.CommandRelations.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 Comparisons.CommandRelations.johnSeesHimself :

ConfigurationalClause

"John sees himself" as a configurational clause

Equations

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

Instances For

theorem Comparisons.CommandRelations.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

Main Agreement Theorem: Reflexive Coreference

All four theories correctly predict the reflexive coreference patterns.

def Comparisons.CommandRelations.testSentences :

List (List Word)

The key test sentences

Equations

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

Instances For

All four theories are pairwise equivalent on test sentences

def Comparisons.CommandRelations.totalPairsTested :

ℕ

Total minimal pairs tested

Equations

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

Instances For

inductive Comparisons.CommandRelations.Category :

Category labels for labeled trees

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

Instances For

def Comparisons.CommandRelations.instDecidableEqCategory.decEq (x✝ x✝¹ : Category) :

Decidable (x✝ = x✝¹)

Equations

Instances For

instance Comparisons.CommandRelations.instDecidableEqCategory :

DecidableEq Category

Equations

Comparisons.CommandRelations.instDecidableEqCategory = Comparisons.CommandRelations.instDecidableEqCategory.decEq

instance Comparisons.CommandRelations.instReprCategory :

Repr Category

Equations

Comparisons.CommandRelations.instReprCategory = { reprPrec := Comparisons.CommandRelations.instReprCategory.repr }

def Comparisons.CommandRelations.instReprCategory.repr :

Category → ℕ → Std.Format

Equations

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

Instances For

structure Comparisons.CommandRelations.LabeledTree (Node : Type) extends Comparisons.CommandRelations.AbstractTree Node :

Labeled tree extends abstract tree with category labels

nodes : Set Node
dom : Node → Node → Prop
root : Node
dom_refl (a : Node) : a ∈ self.nodes → self.dom a a
dom_antisymm (a b : Node) : self.dom a b → self.dom b a → a = b
dom_trans (a b c : Node) : self.dom a b → self.dom b c → self.dom a c
root_dom_all (a : Node) : a ∈ self.nodes → self.dom self.root a
root_in_nodes : self.root ∈ self.nodes
ancestor_connected (x y z : Node) : self.dom x z → self.dom y z → self.dom x y ∨ self.dom y x
nodes_closed (x y : Node) : x ∈ self.nodes → self.dom x y → y ∈ self.nodes
label : Node → Category

Instances For

def Comparisons.CommandRelations.sNodes {Node : Type} (T : LabeledTree Node) :

Set Node

S-nodes

Equations

Comparisons.CommandRelations.sNodes T = {n : Node | T.label n = Comparisons.CommandRelations.Category.S }

Instances For

def Comparisons.CommandRelations.npNodes {Node : Type} (T : LabeledTree Node) :

Set Node

NP-nodes

Equations

Comparisons.CommandRelations.npNodes T = {n : Node | T.label n = Comparisons.CommandRelations.Category.NP }

Instances For

def Comparisons.CommandRelations.branchingNodes {Node : Type} (T : AbstractTree Node) :

Set Node

Branching nodes

Equations

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

Instances For

def Comparisons.CommandRelations.maximalProjections {Node : Type} (T : LabeledTree Node) :

Set Node

Maximal projections (simplified)

Equations

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

Instances For

def Comparisons.CommandRelations.sCommand {Node : Type} (T : LabeledTree Node) :

Set (Node × Node)

S-command (Reinhart's original c-command)

Equations

Comparisons.CommandRelations.sCommand T = Comparisons.CommandRelations.commandRelation T.toAbstractTree (Comparisons.CommandRelations.sNodes T)

Instances For

def Comparisons.CommandRelations.npCommand {Node : Type} (T : LabeledTree Node) :

Set (Node × Node)

NP-command

Equations

Comparisons.CommandRelations.npCommand T = Comparisons.CommandRelations.commandRelation T.toAbstractTree (Comparisons.CommandRelations.npNodes T)

Instances For

def Comparisons.CommandRelations.kCommand {Node : Type} (T : AbstractTree Node) :

Set (Node × Node)

K-command (Kayne's version)

Equations

Comparisons.CommandRelations.kCommand T = Comparisons.CommandRelations.commandRelation T (Comparisons.CommandRelations.branchingNodes T)

Instances For

def Comparisons.CommandRelations.maxCommand {Node : Type} (T : LabeledTree Node) :

Set (Node × Node)

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

Equations

Comparisons.CommandRelations.maxCommand T = Comparisons.CommandRelations.commandRelation T.toAbstractTree (Comparisons.CommandRelations.maximalProjections T)

Instances For

theorem Comparisons.CommandRelations.sCommand_inter_npCommand {Node : Type} (T : LabeledTree Node) :

sCommand T ∩ npCommand T = commandRelation T.toAbstractTree (sNodes T ∪ npNodes T)

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

theorem Comparisons.CommandRelations.maxCommand_subset_sCommand {Node : Type} (T : LabeledTree Node) (h : sNodes T ⊆ maximalProjections T) :

maxCommand T ⊆ sCommand T

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

def Comparisons.CommandRelations.CommandRels {Node : Type} (T : AbstractTree Node) :

Set (Set (Node × Node))

The set of command relations on a tree

Equations

Comparisons.CommandRelations.CommandRels T = {C : Set (Node × Node) | ∃ (P : Set Node), C = Comparisons.CommandRelations.commandRelation T P}

Instances For

instance Comparisons.CommandRelations.instCompleteLatticeSetProd_linglib {Node : Type} :

CompleteLattice (Set (Node × Node))

Command relations inherit the complete lattice structure from Set

Equations

Comparisons.CommandRelations.instCompleteLatticeSetProd_linglib = inferInstance

theorem Comparisons.CommandRelations.command_converts_sup_to_inf {Node : Type} (T : AbstractTree 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 Comparisons.CommandRelations.command_sInter {Node : Type} (T : AbstractTree 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 Comparisons.CommandRelations.commandMap {Node : Type} (T : AbstractTree Node) :

Set Node →o (Set (Node × Node))ᵒᵈ

OrderDual for the powerset ordered by superset

Equations

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

Instances For

theorem Comparisons.CommandRelations.command_order_reversing {Node : Type} (T : AbstractTree Node) (P Q : Set Node) :

P ⊆ Q → commandRelation T Q ⊆ commandRelation T P

The command map is order-reversing (stated directly)

theorem Comparisons.CommandRelations.command_ambidextrous {Node : Type} (T : AbstractTree 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.

B&P Theorem 3: All command relations are ambidextrous.

theorem Comparisons.CommandRelations.command_bounded {Node : Type} (T : AbstractTree 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 (B&P Theorem 4): Adding a root node to the generating property does not alter the command relation.

C_P = C_{P ∪ {r}} when r is the root.

Proof: C_P ⊇ C_{P∪{r}} by the Intersection Theorem (antitone). For the reverse: if (a,b) ∈ C_P but (a,b) ∉ C_{P∪{r}}, there must be some c ∈ P ∪ {r} \ P that properly dominates a but doesn't dominate b. The only such c is the root. But the root dominates everything, contradiction.

theorem Comparisons.CommandRelations.root_upper_bound_trivial {Node : Type} (T : AbstractTree Node) (a b : Node) (hb : b ∈ T.nodes) (hprop : T.properDom T.root a) :

T.dom T.root b

Simpler Boundedness: The root is not a proper dominator of any node.

This is because the root dominates everything, so if root properly dominates a, then root ≠ a, which is possible. But the key point for command relations is that adding root to P doesn't change which pairs command each other.

theorem Comparisons.CommandRelations.command_bounded_witness {Node : Type} (T : AbstractTree 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, T.dom x b

Alternative Boundedness: If UB(a,P) is nonempty and (a,b) ∈ C_P, then ∃x ∈ UB(a,P). x dom b.

This is immediate from the definition but useful as a lemma.

theorem Comparisons.CommandRelations.command_noncommand_witness {Node : Type} (T : AbstractTree Node) (P : Set Node) (a c : Node) (hnac : (a, c) ∉ commandRelation T P) :

∃ x ∈ upperBounds T a P, ¬T.dom x c

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

This is the contrapositive of the command definition.

theorem Comparisons.CommandRelations.command_fair {Node : Type} (T : AbstractTree 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 → T.dom b d

Fairness (B&P Theorem 6): (aCb ∧ bCc ∧ ¬aCc) → (aCd → b dominates d).

If a commands b, b commands c, but a doesn't command c, then every node that a commands is dominated by b.

Proof: Let x be the witness from ¬aCc (x ∈ UB(a,P), x doesn't dominate c). From aCb, x dominates b. If x ≠ b, then x properly dominates b, so x ∈ UB(b,P). From bCc, x would dominate c - contradiction. So x = b. Then from aCd, x dominates d, i.e., b dominates d.

def Comparisons.CommandRelations.mateRelation {Node : Type} (T : AbstractTree 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

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

Instances For

theorem Comparisons.CommandRelations.mate_symmetric {Node : Type} (T : AbstractTree Node) (P : Set Node) (a b : Node) :

(a, b) ∈ mateRelation T P → (b, a) ∈ mateRelation T P

Mate relations are symmetric

theorem Comparisons.CommandRelations.mate_reflexive {Node : Type} (T : AbstractTree Node) (P : Set Node) (a : Node) (ha : a ∈ T.nodes) :

(a, a) ∈ mateRelation T P

Mate relations are reflexive on nodes in C_P

def Comparisons.CommandRelations.sMates {Node : Type} (T : LabeledTree Node) :

Set (Node × Node)

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

Equations

Comparisons.CommandRelations.sMates T = Comparisons.CommandRelations.mateRelation T.toAbstractTree (Comparisons.CommandRelations.sNodes T)

Instances For

def Comparisons.CommandRelations.npMates {Node : Type} (T : LabeledTree Node) :

Set (Node × Node)

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

Equations

Comparisons.CommandRelations.npMates T = Comparisons.CommandRelations.mateRelation T.toAbstractTree (Comparisons.CommandRelations.npNodes T)

Instances For

theorem Comparisons.CommandRelations.mate_intersection {Node : Type} (T : AbstractTree Node) (P Q : Set Node) :

mateRelation T P ∩ mateRelation T Q = mateRelation T (P ∪ Q)

Intersection theorem for mate relations

theorem Comparisons.CommandRelations.command_constituency {Node : Type} (T : AbstractTree Node) (P : Set Node) (a b c : Node) :

(a, b) ∈ commandRelation T P → T.dom b c → (a, c) ∈ commandRelation T P

Constituency/Descent (stronger form): If a commands b and b dominates c, then a commands c.

B&P Theorem 7: C_P is closed under descent on the second argument.

This is already proved as command_descent above. Here we restate it in the standard form.

theorem Comparisons.CommandRelations.command_embeddable_simple {Node : Type} (T : AbstractTree 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 → T.dom x c

Embeddability (B&P Theorem 8): Command relations are preserved under graph embedding.

B&P's actual Theorem 8 is about embedding one graph G₁ into another G₂: "A node a commands b in G₁ if and only if a commands b in G₂" when G₁ is rooted, G₂ satisfies CAC, and the embedding obeys Integrity.

Here we prove a simpler internal version using CAC: If x properly dominates b (with x ∈ P), and either x dominates a (giving x ∈ UB(a,P)) or a dominates x, then we can transfer command from a to b.

The key insight: in a tree with CAC, any upper bound of b is comparable to a.

theorem Comparisons.CommandRelations.command_embeddable_cac {Node : Type} (T : AbstractTree 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 ∨ T.dom a x ∧ T.dom x c) :

(b, c) ∈ commandRelation T P

Embeddability corollary: If every upper bound of b that properly dominates b also properly dominates a, then a commanding c implies b commands c.

This requires: UB(b,P) ⊆ {x | x properly dominates a} ∪ {x | a dominates x ∧ x dom c}

In a tree with CAC, the first disjunct covers most cases.

def Comparisons.CommandRelations.commandByRelation {Node : Type} (T : AbstractTree Node) (R : Node → Node → Prop) :

Set (Node × Node)

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

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

This generalizes the property-based definition: C_P = C_{R_P} where (a R_P x) iff x properly dominates a and x ∈ P.

Equations

Comparisons.CommandRelations.commandByRelation T R = {ab : Node × Node | ∀ (x : Node), R ab.1 x → T.dom x ab.2}

Instances For

theorem Comparisons.CommandRelations.command_as_relation {Node : Type} (T : AbstractTree 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 Comparisons.CommandRelations.commandEquivalent {Node : Type} (T : AbstractTree Node) (R S : Node → Node → Prop) :

Command equivalence (B&P Definition 20): R ~ S iff C_R = C_S

Equations

Comparisons.CommandRelations.commandEquivalent T R S = (Comparisons.CommandRelations.commandByRelation T R = Comparisons.CommandRelations.commandByRelation T S)

Instances For

def Comparisons.CommandRelations.maximalGenerator {Node : Type} (T : AbstractTree Node) (R : Node → Node → Prop) :

Node → Node → Prop

Maximal generator (B&P Definition 21): R̂ = ∪{S | S ⊇ R ∧ S ~ R}

The largest relation that generates the same command relation as R.

Key insight: if c dominates some upper bound b for a, then (c,a) can be added to R without changing C_R (non-minimal upper bounds don't affect command).

Equations

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

Instances For

theorem Comparisons.CommandRelations.maximalGenerator_contains {Node : Type} (T : AbstractTree Node) (R : Node → Node → Prop) (a x : Node) :

R a x → maximalGenerator T R a x

Maximal generator contains the original relation

theorem Comparisons.CommandRelations.nonminimal_in_maximalGenerator {Node : Type} (T : AbstractTree Node) (R : Node → Node → Prop) (a c d : Node) (hRad : R a d) (hcd : T.dom 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 Union Theorem: Non-minimal upper bounds are in the maximal generator.

If c dominates d, and (d, a) ∈ R (meaning d is an upper bound for a in R), then (c, a) ∈ R̂ (the maximal generator).

Proof: Adding (c, a) to R doesn't change C_R because any node that needed to be dominated by c would already be dominated by d (by transitivity).

theorem Comparisons.CommandRelations.maximalGenerator_equivalent {Node : Type} (T : AbstractTree Node) (R : Node → Node → Prop) :

commandEquivalent T R (maximalGenerator T R)

Maximal generator is command-equivalent to original

theorem Comparisons.CommandRelations.relation_intersection_theorem {Node : Type} (T : AbstractTree 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}

Analogous to property-based intersection theorem.

theorem Comparisons.CommandRelations.relation_union_theorem {Node : Type} (T : AbstractTree 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 (B&P Theorem 9): C_R ∪ C_S = C_{R̂ ∩ Ŝ}

Union over command relations corresponds to intersection over maximal generators.

The proof relies on CAC: if (a,b) ∈ C_{R̂∩Ŝ} but (a,b) ∉ C_R ∪ C_S, then there exist c with (c,a) ∈ R and d with (d,a) ∈ S, both properly dominating a but neither dominating b. By CAC, either c dom d or d dom c. Say c dom d. Then c is a non-minimal upper bound for a via S, so (c,a) ∈ Ŝ. And (c,a) ∈ R̂ since R̂ ⊇ R. So (c,a) ∈ R̂ ∩ Ŝ, contradicting (a,b) ∈ C_{R̂∩Ŝ}.

theorem Comparisons.CommandRelations.relation_union_theorem_reverse {Node : Type} (T : AbstractTree 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

The reverse inclusion requires CAC.

This is B&P's Theorem 9 reverse direction: C_{R̂∩Ŝ} ⊆ C_R ∪ C_S.

Proof sketch: If (a,b) ∈ C_{R̂∩Ŝ} but (a,b) ∉ C_R ∪ C_S, then there exist witnesses c with (c,a) ∈ R and d with (d,a) ∈ S, both properly dominating a but neither dominating b. By CAC, either c dom d or d dom c. Say c dom d. Then c is a non-minimal upper bound via d for S, so (c,a) ∈ Ŝ. And (c,a) ∈ R̂ since R̂ ⊇ R. So (c,a) ∈ R̂ ∩ Ŝ, meaning (a,b) ∈ C_{R̂∩Ŝ} implies c dom b. Contradiction.

The full proof requires showing that non-minimal upper bounds are in Ŝ, which needs the precise characterization of maximal generators.

def Comparisons.CommandRelations.commandImage {Node : Type} (T : AbstractTree Node) :

Set (Set (Node × Node))

The image of the command map: all command relations

Equations

Comparisons.CommandRelations.commandImage T = Set.range (Comparisons.CommandRelations.commandRelation T)

Instances For

theorem Comparisons.CommandRelations.commandImage_closed_under_sInter {Node : Type} (T : AbstractTree Node) (S : Set (Set (Node × Node))) (hS : S ⊆ commandImage T) (_hne : S.Nonempty) :

⋂₀ S ∈ commandImage T

Command relations are closed under arbitrary intersection

theorem Comparisons.CommandRelations.command_closure_system {Node : Type} (T : AbstractTree Node) (S : Set (Set (Node × Node))) :

S ⊆ commandImage T → S.Nonempty → ⋂₀ S ∈ commandImage T

The command relations form a closure system

@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	`AbstractTree`
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`

Theorems with `sorry` (Kracht Infrastructure) #

Reference	Issue
Kracht Prop 6	`command_comp_inter_left_rev` - composition distributivity reverse
Kracht Thm 2	`tight_implies_fair` - tight → fair (partial)
Kracht Thm 2	`fair_implies_tight_exists` - fair → tight (needs choice)

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

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:

Associated Functions: Each command relation C has an associated function f_C : T → T where C_x = ↓f_C(x) (downward closure)
Tight Relations: Relations satisfying: x < f(y) → f(x) ≤ f(y)
Fair = Tight (Theorem 2): The "fair" relations of B&P are exactly the "tight" relations defined by the associated function property.
Distributoid Structure: (Cr(T), ∩, ∪, ∘) where ∘ is relational composition. Composition distributes over both ∩ and ∪.
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 Comparisons.CommandRelations.AssociatedFunction {Node : Type} (T : AbstractTree Node) :

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):

f(r) = r (root maps to itself)
f(x) dominates x (f(x) is an upper bound)
f is monotone: x dom y → f(x) dom f(y)
f(f(x)) = f(x) (idempotent on range)
(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 → T.dom (self.f x) x
f(x) dominates x (Condition 2)
monotone (x y : Node) : T.dom x y → T.dom (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)

Instances For

def Comparisons.CommandRelations.AssociatedFunction.tight {Node : Type} {T : AbstractTree Node} (af : AssociatedFunction T) :

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 → T.dom (af.f x) (af.f y)

Instances For

structure Comparisons.CommandRelations.TightAssociatedFunction {Node : Type} (T : AbstractTree Node) extends Comparisons.CommandRelations.AssociatedFunction T :

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 → T.dom (self.f x) x
monotone (x y : Node) : T.dom x y → T.dom (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)

Instances For

def Comparisons.CommandRelations.commandFromFunction {Node : Type} (T : AbstractTree 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

Comparisons.CommandRelations.commandFromFunction T af = {ab : Node × Node | T.dom (af.f ab.1) ab.2}

Instances For

theorem Comparisons.CommandRelations.commandFromFunction_reflexive {Node : Type} (T : AbstractTree Node) (af : AssociatedFunction T) (a : Node) :

a ∈ T.nodes → (a, a) ∈ commandFromFunction T af

The command relation from a tight function is reflexive

theorem Comparisons.CommandRelations.commandFromFunction_descent {Node : Type} (T : AbstractTree Node) (af : AssociatedFunction T) (a b c : Node) :

(a, b) ∈ commandFromFunction T af → T.dom b c → (a, c) ∈ commandFromFunction T af

The command relation from a tight function satisfies descent

def Comparisons.CommandRelations.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

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

Instances For

theorem Comparisons.CommandRelations.composeRel_assoc {Node : Type} (R S U : Set (Node × Node)) :

composeRel R (composeRel S U) = composeRel (composeRel R S) U

Composition is associative

theorem Comparisons.CommandRelations.compose_associated_functions {Node : Type} (T : AbstractTree Node) (af ag : AssociatedFunction T) :

composeRel (commandFromFunction T af) (commandFromFunction T ag) ⊆ {ac : Node × Node | T.dom (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 Comparisons.CommandRelations.Distributoid (α : Type) extends Lattice α :

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

Instances

theorem Comparisons.CommandRelations.command_comp_inter_left {Node : Type} (T : AbstractTree Node) (P Q R : Set Node) :

composeRel (commandRelation T P) (commandRelation T Q ∩ commandRelation T R) ⊆ composeRel (commandRelation T P) (commandRelation T Q) ∩ composeRel (commandRelation T P) (commandRelation T R)

Composition distributes over intersection for command relations (one direction)

theorem Comparisons.CommandRelations.command_comp_inter_left_rev {Node : Type} (T : AbstractTree Node) (P Q R : Set Node) :

composeRel (commandRelation T P) (commandRelation T Q) ∩ composeRel (commandRelation T P) (commandRelation T R) ⊆ composeRel (commandRelation T P) (commandRelation T Q ∩ commandRelation T R)

Composition distributes over intersection (reverse direction).

This direction is more subtle: we have potentially different witnesses b1, b2. The proof uses the fact that if one witness properly dominates the other, the upper bounds are nested, allowing us to transfer the command relation.

Key insight: If b1 properly dominates b2 (b1 dom b2, b1 ≠ b2), then UB(b1, R) ⊆ UB(b2, R), so (b2, c) ∈ C_R implies (b1, c) ∈ C_R.

The general case when b1 and b2 are incomparable requires additional structure (e.g., using CAC to find a common dominator).

def Comparisons.CommandRelations.isFair {Node : Type} (T : AbstractTree Node) (C : Set (Node × Node)) :

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

Comparisons.CommandRelations.isFair T C = ∀ (a b c : Node), (a, b) ∈ C → (b, c) ∈ C → (a, c) ∉ C → ∀ (d : Node), (a, d) ∈ C → T.dom b d

Instances For

theorem Comparisons.CommandRelations.command_is_fair {Node : Type} (T : AbstractTree Node) (P : Set Node) :

isFair T (commandRelation T P)

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

theorem Comparisons.CommandRelations.tight_implies_fair {Node : Type} (T : AbstractTree Node) (tf : TightAssociatedFunction T) :

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

theorem Comparisons.CommandRelations.fair_implies_tight_exists {Node : Type} (T : AbstractTree Node) (C : Set (Node × Node)) (hC_refl : ∀ a ∈ T.nodes, (a, a) ∈ C) (hC_desc : ∀ (a b c : Node), (a, b) ∈ C → T.dom b c → (a, c) ∈ C) (hC_fair : isFair T C) (hC_from_prop : ∃ (P : Set Node), C = commandRelation T P) :

∃ (tf : TightAssociatedFunction T), commandFromFunction T tf.toAssociatedFunction = C

Kracht Theorem 2 (converse sketch): Every fair command relation comes from a tight associated function.

Proof idea: Given a fair relation C, define f(x) = minimal y s.t. (x,y) ∈ C. The fairness condition ensures this f is well-defined and tight.

def Comparisons.CommandRelations.antecedentInter {Node : Type} (T : AbstractTree 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

Comparisons.CommandRelations.antecedentInter T R S = {ac : Node × Node | ∃ (b : Node), (ac.1, b) ∈ R ∧ (ac.1, b) ∈ S ∧ T.dom b ac.2}

Instances For

theorem Comparisons.CommandRelations.union_elimination_forward {Node : Type} (T : AbstractTree Node) (P Q : Set Node) (a c : Node) (ha : a ∈ T.nodes) (hc : c ∈ T.nodes) (hac : T.dom a c) :

(a, c) ∈ commandRelation T P ∪ commandRelation T Q → (a, c) ∈ composeRel (commandRelation T P) (commandRelation T Q) ∩ composeRel (commandRelation T Q) (commandRelation T P) ∩ antecedentInter T (commandRelation T P) (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 Comparisons.CommandRelations.union_elimination_reverse {Node : Type} (T : AbstractTree Node) (P Q : Set Node) :

composeRel (commandRelation T P) (commandRelation T Q) ∩ composeRel (commandRelation T Q) (commandRelation T P) ∩ antecedentInter T (commandRelation T P) (commandRelation T Q) ⊆ commandRelation T P ∪ 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:

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

def Comparisons.CommandRelations.commandImplication {Node : Type} (_T : AbstractTree 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

Comparisons.CommandRelations.commandImplication _T C D = C ⇨ D

Instances For

theorem Comparisons.CommandRelations.commandImplication_eq_sUnion {Node : Type} (_T : AbstractTree 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 Comparisons.CommandRelations.command_heyting {Node : Type} (_T : AbstractTree 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 Comparisons.CommandRelations.command_modus_ponens {Node : Type} (_T : AbstractTree Node) (C D : Set (Node × Node)) :

(C ⇨ D) ∩ C ⊆ D

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

theorem Comparisons.CommandRelations.command_himp_trans {Node : Type} (_T : AbstractTree 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 Comparisons.CommandRelations.command_rels_complete_heyting {Node : Type} (_T : AbstractTree 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 Comparisons.CommandRelations.command_inf_sup_distrib {Node : Type} (_T : AbstractTree 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 Comparisons.CommandRelations.command_compl_eq_himp_bot {Node : Type} (_T : AbstractTree 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 Comparisons.CommandRelations.command_inf_compl {Node : Type} (_T : AbstractTree Node) (C : Set (Node × Node)) :

C ∩ Cᶜ = ∅

Pseudo-complement property: C ∩ Cᶜ = ∅

theorem Comparisons.CommandRelations.command_rels_not_boolean_explanation {Node : Type} (_T : AbstractTree 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 Comparisons.CommandRelations.command_himp_curry {Node : Type} (_T : AbstractTree 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 Comparisons.CommandRelations.command_himp_mono_right {Node : Type} (_T : AbstractTree Node) (A B C : Set (Node × Node)) (h : A ⊆ B) :

C ⇨ A ⊆ C ⇨ B

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

theorem Comparisons.CommandRelations.command_compl_anti {Node : Type} (_T : AbstractTree Node) (A B : Set (Node × Node)) (h : A ⊆ B) :

Bᶜ ⊆ Aᶜ

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

inductive Comparisons.CommandRelations.NormalForm {Node : Type} (T : AbstractTree Node) :

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} {T : AbstractTree Node} : Set Node → NormalForm T
meet {Node : Type} {T : AbstractTree Node} : NormalForm T → NormalForm T → NormalForm T
comp {Node : Type} {T : AbstractTree Node} : NormalForm T → NormalForm T → NormalForm T

Instances For

def Comparisons.CommandRelations.NormalForm.eval {Node : Type} (T : AbstractTree Node) :

NormalForm T → Set (Node × Node)

Evaluate a normal form expression to a command relation

Equations

One or more equations did not get rendered due to their size.
Comparisons.CommandRelations.NormalForm.eval T (Comparisons.CommandRelations.NormalForm.base P) = Comparisons.CommandRelations.commandRelation T P
Comparisons.CommandRelations.NormalForm.eval T (n1.meet n2) = Comparisons.CommandRelations.NormalForm.eval T n1 ∩ Comparisons.CommandRelations.NormalForm.eval T n2

Instances For