inductive Minimalism.Cat : Type

Categorial features (Definition 10)

• V : Cat
• N : Cat
• A : Cat
• P : Cat
• D : Cat
• T : Cat
• C : Cat
• v : Cat
• n : Cat
• a : Cat
• Place : Cat
• Path : Cat
• Num : Cat
• Q : Cat
• Voice : Cat
• Appl : Cat
• Foc : Cat
• Top : Cat
• Fin : Cat
• SA : Cat
• Force : Cat
• Neg : Cat
• Mod : Cat
• Rel : Cat
• Pol : Cat
• Asp : Cat
• Evid : Cat

instance Minimalism.instReprCat : Repr Cat

Equations

• Minimalism.instReprCat = { reprPrec := Minimalism.instReprCat.repr }

def Minimalism.instReprCat.repr : Cat → ℕ → Std.Format

Equations

• Minimalism.instReprCat.repr Minimalism.Cat.V prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Minimalism.Cat.V")).group prec✝
• Minimalism.instReprCat.repr Minimalism.Cat.N prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Minimalism.Cat.N")).group prec✝
• Minimalism.instReprCat.repr Minimalism.Cat.A prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Minimalism.Cat.A")).group prec✝
• Minimalism.instReprCat.repr Minimalism.Cat.P prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Minimalism.Cat.P")).group prec✝
• Minimalism.instReprCat.repr Minimalism.Cat.D prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Minimalism.Cat.D")).group prec✝
• Minimalism.instReprCat.repr Minimalism.Cat.T prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Minimalism.Cat.T")).group prec✝
• Minimalism.instReprCat.repr Minimalism.Cat.C prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Minimalism.Cat.C")).group prec✝
• Minimalism.instReprCat.repr Minimalism.Cat.v prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Minimalism.Cat.v")).group prec✝
• Minimalism.instReprCat.repr Minimalism.Cat.n prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Minimalism.Cat.n")).group prec✝
• Minimalism.instReprCat.repr Minimalism.Cat.a prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Minimalism.Cat.a")).group prec✝
• Minimalism.instReprCat.repr Minimalism.Cat.Place prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Minimalism.Cat.Place")).group prec✝
• Minimalism.instReprCat.repr Minimalism.Cat.Path prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Minimalism.Cat.Path")).group prec✝
• Minimalism.instReprCat.repr Minimalism.Cat.Num prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Minimalism.Cat.Num")).group prec✝
• Minimalism.instReprCat.repr Minimalism.Cat.Q prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Minimalism.Cat.Q")).group prec✝
• Minimalism.instReprCat.repr Minimalism.Cat.Voice prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Minimalism.Cat.Voice")).group prec✝
• Minimalism.instReprCat.repr Minimalism.Cat.Appl prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Minimalism.Cat.Appl")).group prec✝
• Minimalism.instReprCat.repr Minimalism.Cat.Foc prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Minimalism.Cat.Foc")).group prec✝
• Minimalism.instReprCat.repr Minimalism.Cat.Top prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Minimalism.Cat.Top")).group prec✝
• Minimalism.instReprCat.repr Minimalism.Cat.Fin prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Minimalism.Cat.Fin")).group prec✝
• Minimalism.instReprCat.repr Minimalism.Cat.SA prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Minimalism.Cat.SA")).group prec✝
• Minimalism.instReprCat.repr Minimalism.Cat.Force prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Minimalism.Cat.Force")).group prec✝
• Minimalism.instReprCat.repr Minimalism.Cat.Neg prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Minimalism.Cat.Neg")).group prec✝
• Minimalism.instReprCat.repr Minimalism.Cat.Mod prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Minimalism.Cat.Mod")).group prec✝
• Minimalism.instReprCat.repr Minimalism.Cat.Rel prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Minimalism.Cat.Rel")).group prec✝
• Minimalism.instReprCat.repr Minimalism.Cat.Pol prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Minimalism.Cat.Pol")).group prec✝
• Minimalism.instReprCat.repr Minimalism.Cat.Asp prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Minimalism.Cat.Asp")).group prec✝
• Minimalism.instReprCat.repr Minimalism.Cat.Evid prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Minimalism.Cat.Evid")).group prec✝

instance Minimalism.instDecidableEqCat : DecidableEq Cat

Equations

• Minimalism.instDecidableEqCat x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

instance Minimalism.instInhabitedCat : Inhabited Cat

Equations

• Minimalism.instInhabitedCat = { default := Minimalism.instInhabitedCat.default }

def Minimalism.instInhabitedCat.default : Cat

Equations

• Minimalism.instInhabitedCat.default = Minimalism.Cat.V

@[reducible, inline]

abbrev Minimalism.SelStack : Type

Selectional stack consumed left-to-right

Equations

• Minimalism.SelStack = List Minimalism.Cat

structure Minimalism.SimpleLI : Type

A simple LI is a ⟨CAT, SEL⟩ pair (Definition 10), optionally with a phonological form for linearization.

• cat : Cat
• sel : SelStack
• phonForm : String

def Minimalism.instReprSimpleLI.repr : SimpleLI → ℕ → Std.Format

Equations

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

instance Minimalism.instReprSimpleLI : Repr SimpleLI

Equations

• Minimalism.instReprSimpleLI = { reprPrec := Minimalism.instReprSimpleLI.repr }

instance Minimalism.instDecidableEqSimpleLI : DecidableEq SimpleLI

Equations

• Minimalism.instDecidableEqSimpleLI = Minimalism.instDecidableEqSimpleLI.decEq

def Minimalism.instDecidableEqSimpleLI.decEq (x✝ x✝¹ : SimpleLI) : Decidable (x✝ = x✝¹)

Equations

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

structure Minimalism.LexicalItem : Type

Lexical item (simple or complex from head movement, Definition 88)

• features : List SimpleLI
• nonempty : self.features ≠ []

def Minimalism.instReprLexicalItem.repr : LexicalItem → ℕ → Std.Format

Equations

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

instance Minimalism.instReprLexicalItem : Repr LexicalItem

Equations

• Minimalism.instReprLexicalItem = { reprPrec := Minimalism.instReprLexicalItem.repr }

instance Minimalism.instDecidableEqLexicalItem : DecidableEq LexicalItem

Equations

• Minimalism.instDecidableEqLexicalItem a b = if h : a.features = b.features then isTrue ⋯ else isFalse ⋯

def Minimalism.LexicalItem.simple (cat : Cat) (sel : SelStack) (phonForm : String := "") : LexicalItem

Create a simple (non-complex) LI

Equations

• Minimalism.LexicalItem.simple cat sel phonForm = { features := [{ cat := cat, sel := sel, phonForm := phonForm }], nonempty := ⋯ }

def Minimalism.LexicalItem.outerCat (li : LexicalItem) : Cat

Get the outer (projecting) category of an LI

Equations

• li.outerCat = match li.features with | [] => Minimalism.Cat.V | s :: tail => s.cat

def Minimalism.LexicalItem.outerSel (li : LexicalItem) : SelStack

Get the outer selectional requirements

Equations

• li.outerSel = match li.features with | [] => [] | s :: tail => s.sel

def Minimalism.LexicalItem.isComplex (li : LexicalItem) : Bool

Is this LI complex (result of head-to-head movement)?

Equations

• li.isComplex = decide (li.features.length > 1)

def Minimalism.LexicalItem.combine (target mover : LexicalItem) : LexicalItem

Combine two LIs for head-to-head movement (target reprojects)

Equations

• target.combine mover = { features := target.features ++ mover.features, nonempty := ⋯ }

structure Minimalism.LIToken : Type

LI token: specific instance of an LI in a derivation

• item : LexicalItem
• id : ℕ

instance Minimalism.instReprLIToken : Repr LIToken

Equations

• Minimalism.instReprLIToken = { reprPrec := Minimalism.instReprLIToken.repr }

def Minimalism.instReprLIToken.repr : LIToken → ℕ → Std.Format

Equations

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

instance Minimalism.instDecidableEqLIToken : DecidableEq LIToken

Equations

• Minimalism.instDecidableEqLIToken a b = if hid : a.id = b.id then if hitem : a.item = b.item then isTrue ⋯ else isFalse ⋯ else isFalse ⋯

inductive Minimalism.SyntacticObject : Type

Syntactic object: LI token or set of two SOs (Definition 11)

• leaf : LIToken → SyntacticObject
• node : SyntacticObject → SyntacticObject → SyntacticObject

def Minimalism.instReprSyntacticObject.repr : SyntacticObject → ℕ → Std.Format

Equations

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

instance Minimalism.instReprSyntacticObject : Repr SyntacticObject

Equations

• Minimalism.instReprSyntacticObject = { reprPrec := Minimalism.instReprSyntacticObject.repr }

def Minimalism.instDecidableEqSyntacticObject.decEq (x✝ x✝¹ : SyntacticObject) : Decidable (x✝ = x✝¹)

Equations

• One or more equations did not get rendered due to their size.
• Minimalism.instDecidableEqSyntacticObject.decEq (Minimalism.SyntacticObject.leaf a) (Minimalism.SyntacticObject.leaf b) = if h : a = b then h ▸ isTrue ⋯ else isFalse ⋯
• Minimalism.instDecidableEqSyntacticObject.decEq (Minimalism.SyntacticObject.leaf a) (a_1.node a_2) = isFalse ⋯
• Minimalism.instDecidableEqSyntacticObject.decEq (a.node a_1) (Minimalism.SyntacticObject.leaf a_2) = isFalse ⋯

instance Minimalism.instDecidableEqSyntacticObject : DecidableEq SyntacticObject

Equations

• Minimalism.instDecidableEqSyntacticObject = Minimalism.instDecidableEqSyntacticObject.decEq

def Minimalism.SyntacticObject.isLeaf : SyntacticObject → Bool

Equations

• (Minimalism.SyntacticObject.leaf a).isLeaf = true
• (a.node a_1).isLeaf = false

def Minimalism.SyntacticObject.isNode : SyntacticObject → Bool

Equations

• (Minimalism.SyntacticObject.leaf a).isNode = false
• (a.node a_1).isNode = true

def Minimalism.SyntacticObject.getLIToken : SyntacticObject → Option LIToken

Equations

• (Minimalism.SyntacticObject.leaf a).getLIToken = some a
• (a.node a_1).getLIToken = none

def Minimalism.SyntacticObject.getConstituents : SyntacticObject → Option (SyntacticObject × SyntacticObject)

Equations

• (Minimalism.SyntacticObject.leaf a).getConstituents = none
• (a.node a_1).getConstituents = some (a, a_1)

def Minimalism.merge (x y : SyntacticObject) : SyntacticObject

Merge: the fundamental structure-building operation (Definition 12)

Equations

• Minimalism.merge x y = x.node y

def Minimalism.validMerge (x y : SyntacticObject) : Prop

Equations

• Minimalism.validMerge x y = (x ≠ y)

def Minimalism.externalMerge (x y : SyntacticObject) (_h : x ≠ y) : SyntacticObject

Equations

• Minimalism.externalMerge x y _h = Minimalism.merge x y

def Minimalism.internalMerge (target mover : SyntacticObject) (_h : target ≠ mover) : SyntacticObject

Equations

• Minimalism.internalMerge target mover _h = Minimalism.merge mover target

def Minimalism.mkLeaf (cat : Cat) (sel : SelStack) (id : ℕ) : SyntacticObject

Create a leaf SO from category and selection

Equations

• Minimalism.mkLeaf cat sel id = Minimalism.SyntacticObject.leaf { item := Minimalism.LexicalItem.simple cat sel, id := id }

def Minimalism.mkLeafPhon (cat : Cat) (sel : SelStack) (phon : String) (id : ℕ) : SyntacticObject

Create a leaf SO with a phonological form

Equations

• Minimalism.mkLeafPhon cat sel phon id = Minimalism.SyntacticObject.leaf { item := Minimalism.LexicalItem.simple cat sel phon, id := id }

def Minimalism.uposToCat : UD.UPOS → Cat

Map UD UPOS tags to Minimalist categories.

This bridges the theory-neutral UD POS tags used in Core/Basic.lean and Fragments/ to the Minimalist Cat system.

Equations

• Minimalism.uposToCat UD.UPOS.VERB = Minimalism.Cat.V
• Minimalism.uposToCat UD.UPOS.AUX = Minimalism.Cat.T
• Minimalism.uposToCat UD.UPOS.NOUN = Minimalism.Cat.N
• Minimalism.uposToCat UD.UPOS.PROPN = Minimalism.Cat.N
• Minimalism.uposToCat UD.UPOS.ADJ = Minimalism.Cat.A
• Minimalism.uposToCat UD.UPOS.ADP = Minimalism.Cat.P
• Minimalism.uposToCat UD.UPOS.DET = Minimalism.Cat.D
• Minimalism.uposToCat UD.UPOS.SCONJ = Minimalism.Cat.C
• Minimalism.uposToCat UD.UPOS.CCONJ = Minimalism.Cat.C
• Minimalism.uposToCat x✝ = Minimalism.Cat.N

def Minimalism.SyntacticObject.phonYield : SyntacticObject → List String

Get the phonological yield of an SO (collect phonForms from leaves)

Equations

• One or more equations did not get rendered due to their size.
• (a.node a_1).phonYield = a.phonYield ++ a_1.phonYield

def Minimalism.linearize : SyntacticObject → List LIToken

Linearize a SyntacticObject by collecting leaf LITokens in left-to-right traversal order.

Equations

• Minimalism.linearize (Minimalism.SyntacticObject.leaf a) = [a]
• Minimalism.linearize (a.node a_1) = Minimalism.linearize a ++ Minimalism.linearize a_1

def Minimalism.LIToken.phonForm (tok : LIToken) : String

Extract the phonological form from an LIToken.

Equations

• tok.phonForm = (Option.map (fun (x : Minimalism.SimpleLI) => x.phonForm) tok.item.features.head?).getD ""

theorem Minimalism.phonYield_eq_linearize (so : SyntacticObject) : so.phonYield = List.filterMap (fun (tok : LIToken) => have p := tok.phonForm; if p.isEmpty = true then none else some p) (linearize so)

phonYield and linearize agree: phonYield extracts the non-empty phonological forms from the linearization.

def Minimalism.mkTrace (index : ℕ) : SyntacticObject

Create a trace SO. Traces are leaves with a distinguished sentinel: cat = N, sel = [], phonForm = "", and id = index + 10000. This encoding is detectable via isTrace.

Equations

• Minimalism.mkTrace index = Minimalism.SyntacticObject.leaf { item := Minimalism.LexicalItem.simple Minimalism.Cat.N [], id := index + 10000 }

def Minimalism.isTrace : SyntacticObject → Option ℕ

Detect if an SO is a trace (created via mkTrace). Returns the trace index if so.

Equations

• Minimalism.isTrace (Minimalism.SyntacticObject.leaf a) = if a.id ≥ 10000 then some (a.id - 10000) else none
• Minimalism.isTrace (a.node a_1) = none

def Minimalism.exampleVerb : SyntacticObject

Equations

• Minimalism.exampleVerb = Minimalism.mkLeaf Minimalism.Cat.V [Minimalism.Cat.D] 1

def Minimalism.exampleNoun : SyntacticObject

Equations

• Minimalism.exampleNoun = Minimalism.mkLeaf Minimalism.Cat.N [] 2

def Minimalism.exampleDet : SyntacticObject

Equations

• Minimalism.exampleDet = Minimalism.mkLeaf Minimalism.Cat.D [Minimalism.Cat.N] 3

def Minimalism.SyntacticObject.nodeCount : SyntacticObject → ℕ

Count nodes (Merge operations) in an SO

Equations

• (Minimalism.SyntacticObject.leaf a).nodeCount = 0
• (a.node a_1).nodeCount = 1 + a.nodeCount + a_1.nodeCount

def Minimalism.SyntacticObject.leafCount : SyntacticObject → ℕ

Equations

• (Minimalism.SyntacticObject.leaf a).leafCount = 1
• (a.node a_1).leafCount = a.leafCount + a_1.leafCount

theorem Minimalism.leaf_node_relation (so : SyntacticObject) : so.leafCount = so.nodeCount + 1

def Minimalism.subterms : SyntacticObject → List SyntacticObject

All nodes in a SyntacticObject, including the root itself.

Equations

• Minimalism.subterms (Minimalism.SyntacticObject.leaf a) = [Minimalism.SyntacticObject.leaf a]
• Minimalism.subterms (l.node r) = l.node r :: (Minimalism.subterms l ++ Minimalism.subterms r)

def Minimalism.terminalNodes : SyntacticObject → List SyntacticObject

The terminal (leaf) nodes of a SyntacticObject.

Equations

• Minimalism.terminalNodes (Minimalism.SyntacticObject.leaf a) = [Minimalism.SyntacticObject.leaf a]
• Minimalism.terminalNodes (l.node r) = Minimalism.terminalNodes l ++ Minimalism.terminalNodes r

theorem Minimalism.terminalNodes_are_leaves {so t : SyntacticObject} (h : t ∈ terminalNodes so) : t.isLeaf = true

Every terminal node is a leaf.

theorem Minimalism.terminalNodes_sub_subterms {so t : SyntacticObject} (h : t ∈ terminalNodes so) : t ∈ subterms so

Every terminal is a subterm.

theorem Minimalism.self_mem_subterms (so : SyntacticObject) : so ∈ subterms so

The root is always in its own subterms.

def Minimalism.immediatelyContains (x y : SyntacticObject) : Prop

X immediately contains Y iff Y is a member of X

"X immediately contains Y iff X = {Y, Z} for some SO Z"

Since our SOs are binary sets, this means Y is one of the two immediate daughters of X.

Equations

• Minimalism.immediatelyContains (Minimalism.SyntacticObject.leaf a) y = False
• Minimalism.immediatelyContains (a.node a_1) y = (y = a ∨ y = a_1)

instance Minimalism.decImmediatelyContains (x y : SyntacticObject) : Decidable (immediatelyContains x y)

Decidable immediate containment

Equations

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

inductive Minimalism.contains : SyntacticObject → SyntacticObject → Prop

Containment is the transitive closure of immediate containment

"X contains Y iff X immediately contains Y or X immediately contains some SO Z such that Z contains Y"

This is standard syntactic dominance.

• imm (x y : SyntacticObject) : immediatelyContains x y → contains x y
• trans (x y z : SyntacticObject) : immediatelyContains x z → contains z y → contains x y

theorem Minimalism.imm_implies_contains {x y : SyntacticObject} (h : immediatelyContains x y) : contains x y

Immediate containment implies containment

theorem Minimalism.contains_trans {x y z : SyntacticObject} (hxy : contains x y) (hyz : contains y z) : contains x z

Containment is transitive

theorem Minimalism.leaf_contains_nothing (tok : LIToken) (y : SyntacticObject) : ¬contains (SyntacticObject.leaf tok) y

Leaves contain nothing

theorem Minimalism.immediatelyContains_lt_nodeCount {x y : SyntacticObject} (h : immediatelyContains x y) : y.nodeCount < x.nodeCount

Immediate containment strictly decreases nodeCount

theorem Minimalism.contains_lt_nodeCount {x y : SyntacticObject} (h : contains x y) : y.nodeCount < x.nodeCount

Containment strictly decreases nodeCount

theorem Minimalism.contains_irrefl (x : SyntacticObject) : ¬contains x x

No element contains itself (containment is irreflexive)

def Minimalism.containsB : SyntacticObject → SyntacticObject → Bool

Boolean containment check: does x (strictly) contain y?

Equations

• Minimalism.containsB (Minimalism.SyntacticObject.leaf a) x✝ = false
• Minimalism.containsB (a.node b) x✝ = (a == x✝ || b == x✝ || Minimalism.containsB a x✝ || Minimalism.containsB b x✝)

theorem Minimalism.containsB_implies_contains {x y : SyntacticObject} (h : containsB x y = true) : contains x y

containsB implies contains.

theorem Minimalism.contains_implies_containsB {x y : SyntacticObject} (h : contains x y) : containsB x y = true

contains implies containsB.

theorem Minimalism.containsB_iff {x y : SyntacticObject} : containsB x y = true ↔ contains x y

Boolean and propositional containment are equivalent.

def Minimalism.isTermOf (x y : SyntacticObject) : Prop

X is a term of Y iff X = Y or Y contains X

"X is a term of SO Y iff X = Y or Y contains X"

This is useful for stating when an element is "somewhere in" a structure

Equations

• Minimalism.isTermOf x y = (x = y ∨ Minimalism.contains y x)

theorem Minimalism.self_is_term (x : SyntacticObject) : isTermOf x x

Every SO is a term of itself

theorem Minimalism.contained_is_term {x y : SyntacticObject} (h : contains y x) : isTermOf x y

If Y contains X, then X is a term of Y

def Minimalism.containsOrEq (x y : SyntacticObject) : Prop

Reflexive containment (useful for stating constraints)

Equations

• Minimalism.containsOrEq x y = (x = y ∨ Minimalism.contains x y)

theorem Minimalism.refl_containsOrEq (x : SyntacticObject) : containsOrEq x x

Every SO reflexively contains itself

theorem Minimalism.containsOrEq_trans {x y z : SyntacticObject} (hxy : containsOrEq x y) (hyz : containsOrEq y z) : containsOrEq x z

Reflexive containment is transitive

def Minimalism.areSistersIn (root x y : SyntacticObject) : Prop

X and Y are sisters IN tree root: they are distinct co-daughters of some node that is a subterm of root.

Equations

• Minimalism.areSistersIn root x y = ∃ (z : Minimalism.SyntacticObject), z ∈ Minimalism.subterms root ∧ Minimalism.immediatelyContains z x ∧ Minimalism.immediatelyContains z y ∧ x ≠ y

def Minimalism.cCommandsIn (root x y : SyntacticObject) : Prop

X c-commands Y IN tree root: X has a sister (in root) that contains-or-equals Y.

Equations

• Minimalism.cCommandsIn root x y = ∃ (z : Minimalism.SyntacticObject), Minimalism.areSistersIn root x z ∧ Minimalism.containsOrEq z y

def Minimalism.asymCCommandsIn (root x y : SyntacticObject) : Prop

X asymmetrically c-commands Y in tree root.

Equations

• Minimalism.asymCCommandsIn root x y = (Minimalism.cCommandsIn root x y ∧ ¬Minimalism.cCommandsIn root y x)

def Minimalism.cCommandsInB (root x y : SyntacticObject) : Bool

Boolean c-command check: does x c-command y in tree root?

Searches all subterms of root for a parent node whose children include x and some sibling z where z equals or contains y. Mirrors cCommandsIn but is decidable by computation.

Equations

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

Tree Shape — abstract geometry ignoring terminal labels

inductive Minimalism.TreeShape : Type

Abstract tree geometry: the shape of a SyntacticObject with all terminal labels erased. Two SOs are structurally isomorphic iff they have the same TreeShape.

• leaf : TreeShape
• node : TreeShape → TreeShape → TreeShape

instance Minimalism.instReprTreeShape : Repr TreeShape

Equations

• Minimalism.instReprTreeShape = { reprPrec := Minimalism.instReprTreeShape.repr }

def Minimalism.instReprTreeShape.repr : TreeShape → ℕ → Std.Format

Equations

• One or more equations did not get rendered due to their size.
• Minimalism.instReprTreeShape.repr Minimalism.TreeShape.leaf prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Minimalism.TreeShape.leaf")).group prec✝

def Minimalism.instDecidableEqTreeShape.decEq (x✝ x✝¹ : TreeShape) : Decidable (x✝ = x✝¹)

Equations

• One or more equations did not get rendered due to their size.
• Minimalism.instDecidableEqTreeShape.decEq Minimalism.TreeShape.leaf Minimalism.TreeShape.leaf = isTrue ⋯
• Minimalism.instDecidableEqTreeShape.decEq Minimalism.TreeShape.leaf (a.node a_1) = isFalse ⋯
• Minimalism.instDecidableEqTreeShape.decEq (a.node a_1) Minimalism.TreeShape.leaf = isFalse ⋯

instance Minimalism.instDecidableEqTreeShape : DecidableEq TreeShape

Equations

• Minimalism.instDecidableEqTreeShape = Minimalism.instDecidableEqTreeShape.decEq

def Minimalism.instBEqTreeShape.beq : TreeShape → TreeShape → Bool

Equations

• Minimalism.instBEqTreeShape.beq Minimalism.TreeShape.leaf Minimalism.TreeShape.leaf = true
• Minimalism.instBEqTreeShape.beq (a.node a_1) (b.node b_1) = (Minimalism.instBEqTreeShape.beq a b && Minimalism.instBEqTreeShape.beq a_1 b_1)
• Minimalism.instBEqTreeShape.beq x✝¹ x✝ = false

instance Minimalism.instBEqTreeShape : BEq TreeShape

Equations

• Minimalism.instBEqTreeShape = { beq := Minimalism.instBEqTreeShape.beq }

def Minimalism.SyntacticObject.shape : SyntacticObject → TreeShape

Strip labels from a syntactic object, yielding its abstract shape.

Equations

• (Minimalism.SyntacticObject.leaf a).shape = Minimalism.TreeShape.leaf
• (a.node a_1).shape = a.shape.node a_1.shape

def Minimalism.structurallyIsomorphic (x y : SyntacticObject) : Bool

Two syntactic objects are structurally isomorphic iff they have the same tree shape (ignoring all terminal labels).

Equations

• Minimalism.structurallyIsomorphic x y = (x.shape == y.shape)