Terms, containment, and c-command

This file develops the theory of terms of syntactic objects: containment as a closure of the daughter relation, the multisets of terms and accessible terms that enumerate it, and sisterhood and c-command relative to a root. Containment lowers the vertex count, which makes it a well-founded strict order and decides it.

Main definitions

• SyntacticObject.ImmediatelyContains: x immediately contains y when y is a root daughter of x.
• SyntacticObject.Contains: the transitive closure of immediate containment.
• SyntacticObject.ContainsOrEq: the reflexive transitive closure of immediate containment.
• SyntacticObject.terms: the terms of an object, itself included, one per vertex.
• SyntacticObject.accessibleTerms: the terms at the non-root vertices, the accessible terms of [MCB25].
• SyntacticObject.Sisters: x and y are sisters in root when they are distinct daughters of one term of root.
• SyntacticObject.CCommands: x c-commands y in root when a sister of x reflexively contains y ([Rei76]).
• SyntacticObject.AsymmCCommands: c-command in one direction only.
• SyntacticObject.cCommandDomain: the c-command domain of x in root, the terms it c-commands.

Main results

• SyntacticObject.mem_terms, mem_accessibleTerms: the terms of x are the objects it reflexively contains, and the accessible terms those it strictly contains.
• SyntacticObject.wellFounded_flip_contains: the proper term relation is well-founded.
• SyntacticObject.card_accessibleTerms: one accessible term per edge.

Implementation notes

Syntactic objects are values, not occurrences: a term sitting at two vertices is one object of multiplicity two in terms, and containment and c-command relate values, so the two daughters of merge x x are not sisters.

References

• [MCB25], Definition 1.2.2
• [Rei76]

Immediate containment

def Minimalist.SyntacticObject.ImmediatelyContains (x y : SyntacticObject) : Prop

y is one of x's root daughters.

Equations

• x.ImmediatelyContains y = (↑y ∈ (↑x).children)

@[instance_reducible]

instance Minimalist.SyntacticObject.instDecidableImmediatelyContains (x y : SyntacticObject) : Decidable (x.ImmediatelyContains y)

Equations

• x.instDecidableImmediatelyContains y = Minimalist.SyntacticObject.instDecidableImmediatelyContains._aux_1 x y

@[simp]

theorem Minimalist.SyntacticObject.immediatelyContains_leaf (tok : LexicalItem.Token) (y : SyntacticObject) : ¬(↑tok).ImmediatelyContains y

@[simp]

theorem Minimalist.SyntacticObject.immediatelyContains_trace (y : SyntacticObject) : ¬trace.ImmediatelyContains y

@[simp]

theorem Minimalist.SyntacticObject.immediatelyContains_traceOf (tok : LexicalItem.Token) (y : SyntacticObject) : ¬(traceOf tok).ImmediatelyContains y

@[simp]

theorem Minimalist.SyntacticObject.immediatelyContains_merge (l r y : SyntacticObject) : (l.merge r).ImmediatelyContains y ↔ y = l ∨ y = r

Containment

def Minimalist.SyntacticObject.Contains : SyntacticObject → SyntacticObject → Prop

Containment, the transitive closure of immediate containment.

Equations

• Minimalist.SyntacticObject.Contains = Relation.TransGen Minimalist.SyntacticObject.ImmediatelyContains

def Minimalist.SyntacticObject.ContainsOrEq : SyntacticObject → SyntacticObject → Prop

Reflexive containment, the reflexive transitive closure of immediate containment.

Equations

• Minimalist.SyntacticObject.ContainsOrEq = Relation.ReflTransGen Minimalist.SyntacticObject.ImmediatelyContains

theorem Minimalist.SyntacticObject.ImmediatelyContains.Contains {x y : SyntacticObject} (h : x.ImmediatelyContains y) : x.Contains y

theorem Minimalist.SyntacticObject.Contains.trans {x y z : SyntacticObject} (hxy : x.Contains y) (hyz : y.Contains z) : x.Contains z

instance Minimalist.SyntacticObject.instIsPreorderContainsOrEq : IsPreorder SyntacticObject ContainsOrEq

theorem Minimalist.SyntacticObject.containsOrEq_iff_eq_or_contains {x y : SyntacticObject} : x.ContainsOrEq y ↔ y = x ∨ x.Contains y

theorem Minimalist.SyntacticObject.contains_iff_exists_immediatelyContains {x y : SyntacticObject} : x.Contains y ↔ ∃ (z : SyntacticObject), x.ImmediatelyContains z ∧ z.ContainsOrEq y

@[simp]

theorem Minimalist.SyntacticObject.contains_leaf (tok : LexicalItem.Token) (y : SyntacticObject) : ¬(↑tok).Contains y

@[simp]

theorem Minimalist.SyntacticObject.contains_trace (y : SyntacticObject) : ¬trace.Contains y

@[simp]

theorem Minimalist.SyntacticObject.contains_traceOf (tok : LexicalItem.Token) (y : SyntacticObject) : ¬(traceOf tok).Contains y

@[simp]

theorem Minimalist.SyntacticObject.contains_merge {y l r : SyntacticObject} : (l.merge r).Contains y ↔ l.ContainsOrEq y ∨ r.ContainsOrEq y

@[simp]

theorem Minimalist.SyntacticObject.containsOrEq_leaf {y : SyntacticObject} (tok : LexicalItem.Token) : (↑tok).ContainsOrEq y ↔ y = ↑tok

@[simp]

theorem Minimalist.SyntacticObject.containsOrEq_trace {y : SyntacticObject} : trace.ContainsOrEq y ↔ y = trace

@[simp]

theorem Minimalist.SyntacticObject.containsOrEq_traceOf {y : SyntacticObject} (tok : LexicalItem.Token) : (traceOf tok).ContainsOrEq y ↔ y = traceOf tok

@[simp]

theorem Minimalist.SyntacticObject.containsOrEq_merge {y l r : SyntacticObject} : (l.merge r).ContainsOrEq y ↔ y = l.merge r ∨ l.ContainsOrEq y ∨ r.ContainsOrEq y

The vertex count grades containment

theorem Minimalist.SyntacticObject.numNodes_lt_of_immediatelyContains {x y : SyntacticObject} (h : x.ImmediatelyContains y) : (↑y).numNodes < (↑x).numNodes

theorem Minimalist.SyntacticObject.numNodes_lt_of_contains {x y : SyntacticObject} (h : x.Contains y) : (↑y).numNodes < (↑x).numNodes

theorem Minimalist.SyntacticObject.wellFounded_flip_contains : WellFounded (flip Contains)

Being a proper term is well-founded: an object has finitely many terms.

instance Minimalist.SyntacticObject.instIsStrictOrderContains : IsStrictOrder SyntacticObject Contains

theorem Minimalist.SyntacticObject.contains_irrefl (x : SyntacticObject) : ¬x.Contains x

Terms

theorem Minimalist.isSyntacticObject_of_mem_subtrees (s : SyntacticObject) (m : UnorderedTree SyntacticObject.Vertex) : m ∈ (↑s).subtrees → IsSyntacticObject m

The subtrees of a syntactic object are its terms, hence syntactic objects.

def Minimalist.SyntacticObject.terms (s : SyntacticObject) : Multiset SyntacticObject

The terms of a syntactic object, itself included.

Equations

• s.terms = Multiset.pmap Subtype.mk (↑s).subtrees ⋯

@[simp]

theorem Minimalist.SyntacticObject.map_val_terms (s : SyntacticObject) : Multiset.map Subtype.val s.terms = (↑s).subtrees

@[simp]

theorem Minimalist.SyntacticObject.terms_leaf (tok : LexicalItem.Token) : (↑tok).terms = {↑tok}

@[simp]

theorem Minimalist.SyntacticObject.terms_trace : trace.terms = {trace}

@[simp]

theorem Minimalist.SyntacticObject.terms_traceOf (tok : LexicalItem.Token) : (traceOf tok).terms = {traceOf tok}

@[simp]

theorem Minimalist.SyntacticObject.terms_merge (l r : SyntacticObject) : (l.merge r).terms = l.merge r ::ₘ (l.terms + r.terms)

@[simp]

theorem Minimalist.SyntacticObject.mem_terms {x y : SyntacticObject} : y ∈ x.terms ↔ x.ContainsOrEq y

The terms of x are the objects it reflexively contains.

theorem Minimalist.SyntacticObject.self_mem_terms (s : SyntacticObject) : s ∈ s.terms

theorem Minimalist.SyntacticObject.terms_subset_terms {x y : SyntacticObject} (h : x.ContainsOrEq y) : y.terms ⊆ x.terms

theorem Minimalist.SyntacticObject.card_terms (s : SyntacticObject) : s.terms.card = (↑s).numNodes

One term per vertex.

@[instance_reducible]

instance Minimalist.SyntacticObject.instDecidableContainsOrEq (x y : SyntacticObject) : Decidable (x.ContainsOrEq y)

Equations

• x.instDecidableContainsOrEq y = decidable_of_iff (y ∈ x.terms) ⋯

Accessible terms

def Minimalist.SyntacticObject.accessibleTerms (s : SyntacticObject) : Multiset SyntacticObject

The accessible terms, the terms at the non-root vertices.

Equations

• s.accessibleTerms = s.terms.erase s

theorem Minimalist.SyntacticObject.cons_accessibleTerms (s : SyntacticObject) : s ::ₘ s.accessibleTerms = s.terms

@[simp]

theorem Minimalist.SyntacticObject.accessibleTerms_leaf (tok : LexicalItem.Token) : (↑tok).accessibleTerms = 0

@[simp]

theorem Minimalist.SyntacticObject.accessibleTerms_trace : trace.accessibleTerms = 0

@[simp]

theorem Minimalist.SyntacticObject.accessibleTerms_traceOf (tok : LexicalItem.Token) : (traceOf tok).accessibleTerms = 0

@[simp]

theorem Minimalist.SyntacticObject.accessibleTerms_merge (l r : SyntacticObject) : (l.merge r).accessibleTerms = l.terms + r.terms

@[simp]

theorem Minimalist.SyntacticObject.mem_accessibleTerms {x y : SyntacticObject} : y ∈ x.accessibleTerms ↔ x.Contains y

The accessible terms of x are the objects it contains.

theorem Minimalist.SyntacticObject.card_accessibleTerms (s : SyntacticObject) : s.accessibleTerms.card = (↑s).numEdges

One accessible term per edge.

@[instance_reducible]

instance Minimalist.SyntacticObject.instDecidableContains (x y : SyntacticObject) : Decidable (x.Contains y)

Equations

• x.instDecidableContains y = decidable_of_iff (y ∈ x.accessibleTerms) ⋯

C-command

def Minimalist.SyntacticObject.Sisters (root x y : SyntacticObject) : Prop

x and y are sisters in root when they are distinct daughters of some term of root.

Equations

• root.Sisters x y = ∃ z ∈ root.terms, z.ImmediatelyContains x ∧ z.ImmediatelyContains y ∧ x ≠ y

@[instance_reducible]

instance Minimalist.SyntacticObject.instDecidableSisters (root x y : SyntacticObject) : Decidable (root.Sisters x y)

Equations

• root.instDecidableSisters x y = Multiset.decidableExistsMultiset

theorem Minimalist.SyntacticObject.Sisters.symm {x y root : SyntacticObject} (h : root.Sisters x y) : root.Sisters y x

theorem Minimalist.SyntacticObject.Sisters.mem_left {x y root : SyntacticObject} (h : root.Sisters x y) : x ∈ root.terms

theorem Minimalist.SyntacticObject.Sisters.mem_right {x y root : SyntacticObject} (h : root.Sisters x y) : y ∈ root.terms

def Minimalist.SyntacticObject.CCommands (root x y : SyntacticObject) : Prop

x c-commands y in root when a sister of x contains or equals y.

Equations

• root.CCommands x y = ∃ z ∈ root.terms, root.Sisters x z ∧ z.ContainsOrEq y

@[instance_reducible]

instance Minimalist.SyntacticObject.instDecidableCCommands (root x y : SyntacticObject) : Decidable (root.CCommands x y)

Equations

• root.instDecidableCCommands x y = Multiset.decidableExistsMultiset

theorem Minimalist.SyntacticObject.Sisters.cCommands {x y root : SyntacticObject} (h : root.Sisters x y) : root.CCommands x y

Sisters c-command each other.

theorem Minimalist.SyntacticObject.CCommands.mem_terms {x y root : SyntacticObject} (h : root.CCommands x y) : y ∈ root.terms

A c-commanded object is a term of the root.

def Minimalist.SyntacticObject.cCommandDomain (root x : SyntacticObject) : Multiset SyntacticObject

The c-command domain of x in root, the search space of a probe sitting at x.

Equations

• root.cCommandDomain x = Multiset.filter (root.CCommands x) root.terms

@[simp]

theorem Minimalist.SyntacticObject.mem_cCommandDomain {x y root : SyntacticObject} : y ∈ root.cCommandDomain x ↔ root.CCommands x y

def Minimalist.SyntacticObject.AsymmCCommands (root x y : SyntacticObject) : Prop

x c-commands y in root and y does not c-command x.

Equations

• root.AsymmCCommands x y = (root.CCommands x y ∧ ¬root.CCommands y x)

@[instance_reducible]

instance Minimalist.SyntacticObject.instDecidableAsymmCCommands (root x y : SyntacticObject) : Decidable (root.AsymmCCommands x y)

Equations

• root.instDecidableAsymmCCommands x y = { decide := decide (root.CCommands x y) && decide ¬root.CCommands y x, reflects_decide := ⋯ }

theorem Minimalist.SyntacticObject.Sisters.not_asymmCCommands {x y root : SyntacticObject} (h : root.Sisters x y) : ¬root.AsymmCCommands x y

Sisters never asymmetrically c-command each other.