Syntactic objects

A syntactic object is a binary rooted tree with leaves labelled by the lexical alphabet and no labels at internal vertices: an element of the free non-associative commutative magma on SO₀. This file builds two carriers for it over one alphabet of vertices, Vertex, an option of a token on either side. The left summand is structure: a lexical item Vertex.lex tok on a leaf, or the bare label Vertex.bare on a binary internal node. The right summand is a trace: the index-free Vertex.trace, or the trace Vertex.traceOf tok of a token, the cancellation T/T_v remembering the head of T_v. Traces are exactly the right summand, the convention of the trace coproduct. SyntacticObject is the well-formed unordered tree over Vertex, the object Merge builds, and PlanarSyntacticObject the well-formed ordered tree, [MCB25]'s planar embedding, the form linearization and PF read. Well-formedness is a local condition, each vertex licensing its children (Vertex.Licenses), so it descends to the quotient; PlanarSyntacticObject.toSyntacticObject forgets the order and is a homomorphism for the vocabulary the two carriers share, leaf, trace, traceOf and merge.

Main definitions

• Minimalist.SyntacticObject.Vertex, Minimalist.IsSyntacticObject
• Minimalist.SyntacticObject, Minimalist.PlanarSyntacticObject: the unordered and the ordered carrier, each with leaf, trace, traceOf and merge.
• Minimalist.PlanarSyntacticObject.toSyntacticObject: forgetting the order.

Main results

• Minimalist.SyntacticObject.ind, exists_form: induction and case analysis over the shapes.
• Minimalist.PlanarSyntacticObject.toSyntacticObject_merge: forgetting the order commutes with Merge.

References

• [MCB25], §1.1 (Definition 1.1.1, §1.1.3), §1.2 (Definitions 1.2.1, 1.2.6) and §1.12

@[reducible, inline]

abbrev Minimalist.SyntacticObject.Vertex : Type

A vertex carries structure on the left, a lexical token or the bare internal label, and a trace on the right, index-free or of a token.

Equations

• Minimalist.SyntacticObject.Vertex = (Option Minimalist.LexicalItem.Token ⊕ Option Minimalist.LexicalItem.Token)

@[reducible, match_pattern, inline]

abbrev Minimalist.SyntacticObject.Vertex.lex (tok : LexicalItem.Token) : Vertex

The lexical item tok on a leaf.

Equations

• Minimalist.SyntacticObject.Vertex.lex tok = Sum.inl (some tok)

@[reducible, match_pattern, inline]

abbrev Minimalist.SyntacticObject.Vertex.bare : Vertex

The bare label of a binary internal node.

Equations

• Minimalist.SyntacticObject.Vertex.bare = Sum.inl none

@[reducible, match_pattern, inline]

abbrev Minimalist.SyntacticObject.Vertex.trace : Vertex

The index-free trace.

Equations

• Minimalist.SyntacticObject.Vertex.trace = Sum.inr none

@[reducible, match_pattern, inline]

abbrev Minimalist.SyntacticObject.Vertex.traceOf (tok : LexicalItem.Token) : Vertex

The trace of the token tok.

Equations

• Minimalist.SyntacticObject.Vertex.traceOf tok = Sum.inr (some tok)

Well-formedness

def Minimalist.SyntacticObject.Vertex.Licenses : Vertex → Multiset Vertex → Prop

A vertex licenses its children when a lexical item or a trace has none and the bare label has two.

Equations

• Minimalist.SyntacticObject.Vertex.Licenses (Sum.inl (some val)) x✝ = (x✝ = 0)
• Minimalist.SyntacticObject.Vertex.Licenses (Sum.inl none) x✝ = (x✝.card = 2)
• Minimalist.SyntacticObject.Vertex.Licenses (Sum.inr val) x✝ = (x✝ = 0)

@[instance_reducible]

instance Minimalist.SyntacticObject.instDecidableLicenses (a : Vertex) (ks : Multiset Vertex) : Decidable (a.Licenses ks)

Equations

• Minimalist.SyntacticObject.instDecidableLicenses (Sum.inl (some val)) x✝ = Minimalist.SyntacticObject.instDecidableLicenses._aux_1 val x✝
• Minimalist.SyntacticObject.instDecidableLicenses (Sum.inl none) x✝ = { decide := x✝.card.beq 2, reflects_decide := ⋯ }
• Minimalist.SyntacticObject.instDecidableLicenses (Sum.inr val) x✝ = Minimalist.SyntacticObject.instDecidableLicenses._aux_4 val x✝

def Minimalist.IsSyntacticObject (t : UnorderedTree SyntacticObject.Vertex) : Prop

An unordered tree over Vertex is a syntactic object when every vertex licenses its children, so that lexical items and traces are leaves and bare vertices are binary.

Equations

• Minimalist.IsSyntacticObject t = UnorderedTree.Licensed Minimalist.SyntacticObject.Vertex.Licenses t

@[instance_reducible]

instance Minimalist.instDecidablePredUnorderedTreeVertexIsSyntacticObject : DecidablePred IsSyntacticObject

Equations

• Minimalist.instDecidablePredUnorderedTreeVertexIsSyntacticObject t = Minimalist.instDecidablePredUnorderedTreeVertexIsSyntacticObject._aux_1 t

@[simp]

theorem Minimalist.isSyntacticObject_mk (t : RoseTree SyntacticObject.Vertex) : IsSyntacticObject (UnorderedTree.mk t) ↔ RoseTree.Licensed (fun (a : SyntacticObject.Vertex) (ks : List SyntacticObject.Vertex) => a.Licenses ↑ks) t

theorem Minimalist.SyntacticObject.isSyntacticObject_mk_leaf {a : Vertex} (ha : a ≠ Vertex.bare) : IsSyntacticObject (UnorderedTree.mk (RoseTree.node a []))

A leaf carrying a lexical item or a trace is a syntactic object.

@[simp]

theorem Minimalist.SyntacticObject.isSyntacticObject_mk_merge (l r : RoseTree Vertex) : IsSyntacticObject (UnorderedTree.mk (RoseTree.node Vertex.bare [l, r])) ↔ IsSyntacticObject (UnorderedTree.mk l) ∧ IsSyntacticObject (UnorderedTree.mk r)

A bare binary node is a syntactic object exactly when both daughters are.

theorem Minimalist.SyntacticObject.length_eq_zero_or_two {a : Vertex} {cs : List (RoseTree Vertex)} (h : IsSyntacticObject (UnorderedTree.mk (RoseTree.node a cs))) : cs.length = 0 ∨ cs.length = 2

A node of a syntactic object has either no children or exactly two.

theorem Minimalist.SyntacticObject.eq_bare_of_ne_nil {a : Vertex} {cs : List (RoseTree Vertex)} (h : IsSyntacticObject (UnorderedTree.mk (RoseTree.node a cs))) (hcs : cs ≠ []) : a = Vertex.bare

A node of a syntactic object with children is bare.

theorem Minimalist.IsSyntacticObject.isFullBinary {t : UnorderedTree SyntacticObject.Vertex} (h : IsSyntacticObject t) : t.IsFullBinary

The vertices of a syntactic object have zero or two children.

def Minimalist.SyntacticObject : Type

The syntactic objects are the well-formed unordered trees over Vertex.

Equations

• Minimalist.SyntacticObject = { t : UnorderedTree Minimalist.SyntacticObject.Vertex // Minimalist.IsSyntacticObject t }

def Minimalist.PlanarSyntacticObject : Type

The planar syntactic objects are the well-formed ordered trees over Vertex, [MCB25] §1.12's planar embeddings.

Equations

• Minimalist.PlanarSyntacticObject = { t : RoseTree Minimalist.SyntacticObject.Vertex // Minimalist.IsSyntacticObject (UnorderedTree.mk t) }

@[instance_reducible]

instance Minimalist.instDecidableEqSyntacticObject : DecidableEq SyntacticObject

Equations

• Minimalist.instDecidableEqSyntacticObject = Subtype.instDecidableEq

@[instance_reducible]

instance Minimalist.instDecidableEqPlanarSyntacticObject : DecidableEq PlanarSyntacticObject

Equations

• Minimalist.instDecidableEqPlanarSyntacticObject = Subtype.instDecidableEq

The shapes

def Minimalist.SyntacticObject.leaf (tok : LexicalItem.Token) : SyntacticObject

A lexical leaf.

Equations

• ↑tok = ⟨UnorderedTree.leaf (Minimalist.SyntacticObject.Vertex.lex tok), ⋯⟩

def Minimalist.SyntacticObject.trace : SyntacticObject

The index-free trace, the mark an admissible cut leaves in the remaining tree ([MCB25], Definition 1.2.6); traceOf is the indexed trace.

Equations

• Minimalist.SyntacticObject.trace = ⟨UnorderedTree.leaf Minimalist.SyntacticObject.Vertex.trace, ⋯⟩

def Minimalist.SyntacticObject.traceOf (tok : LexicalItem.Token) : SyntacticObject

The trace of tok.

Equations

• Minimalist.SyntacticObject.traceOf tok = ⟨UnorderedTree.leaf (Minimalist.SyntacticObject.Vertex.traceOf tok), ⋯⟩

@[simp]

theorem Minimalist.SyntacticObject.leaf_val (tok : LexicalItem.Token) : ↑↑tok = UnorderedTree.leaf (Vertex.lex tok)

@[simp]

theorem Minimalist.SyntacticObject.leaf_inj {a b : LexicalItem.Token} : ↑a = ↑b ↔ a = b

@[simp]

theorem Minimalist.SyntacticObject.trace_val : ↑trace = UnorderedTree.leaf Vertex.trace

@[simp]

theorem Minimalist.SyntacticObject.traceOf_val (tok : LexicalItem.Token) : ↑(traceOf tok) = UnorderedTree.leaf (Vertex.traceOf tok)

theorem Minimalist.SyntacticObject.isSyntacticObject_merge_iff (a b : UnorderedTree Vertex) : IsSyntacticObject (UnorderedTree.node Vertex.bare {a, b}) ↔ IsSyntacticObject a ∧ IsSyntacticObject b

A bare binary node is a syntactic object exactly when both daughters are.

noncomputable def Minimalist.SyntacticObject.merge (l r : SyntacticObject) : SyntacticObject

Merge on the carrier, the bare binary node over two syntactic objects, also written *. Noncomputable, since it goes through the smart constructor UnorderedTree.node; concrete results are built ordered and forgotten by PlanarSyntacticObject.toSyntacticObject.

Equations

• l.merge r = ⟨UnorderedTree.node Minimalist.SyntacticObject.Vertex.bare {↑l, ↑r}, ⋯⟩

@[simp]

theorem Minimalist.SyntacticObject.merge_val (l r : SyntacticObject) : ↑(l.merge r) = UnorderedTree.node Vertex.bare {↑l, ↑r}

theorem Minimalist.SyntacticObject.merge_comm (l r : SyntacticObject) : l.merge r = r.merge l

theorem Minimalist.SyntacticObject.merge_mk (pl pr : RoseTree Vertex) (hl : IsSyntacticObject (UnorderedTree.mk pl)) (hr : IsSyntacticObject (UnorderedTree.mk pr)) : ↑(merge ⟨UnorderedTree.mk pl, hl⟩ ⟨UnorderedTree.mk pr, hr⟩) = UnorderedTree.mk (RoseTree.node Vertex.bare [pl, pr])

Merge of two ordered-built objects is the ordered binary node, so concrete results reduce.

def Minimalist.PlanarSyntacticObject.leaf (tok : LexicalItem.Token) : PlanarSyntacticObject

A lexical leaf.

Equations

• ↑tok = ⟨RoseTree.node (Minimalist.SyntacticObject.Vertex.lex tok) [], ⋯⟩

def Minimalist.PlanarSyntacticObject.trace : PlanarSyntacticObject

The index-free trace.

Equations

• Minimalist.PlanarSyntacticObject.trace = ⟨RoseTree.node Minimalist.SyntacticObject.Vertex.trace [], ⋯⟩

def Minimalist.PlanarSyntacticObject.traceOf (tok : LexicalItem.Token) : PlanarSyntacticObject

The trace of tok.

Equations

• Minimalist.PlanarSyntacticObject.traceOf tok = ⟨RoseTree.node (Minimalist.SyntacticObject.Vertex.traceOf tok) [], ⋯⟩

def Minimalist.PlanarSyntacticObject.merge (l r : PlanarSyntacticObject) : PlanarSyntacticObject

Merge, with the daughters in the given order.

Equations

• l.merge r = ⟨RoseTree.node Minimalist.SyntacticObject.Vertex.bare [↑l, ↑r], ⋯⟩

@[simp]

theorem Minimalist.PlanarSyntacticObject.leaf_val (tok : LexicalItem.Token) : ↑↑tok = RoseTree.node (SyntacticObject.Vertex.lex tok) []

@[simp]

theorem Minimalist.PlanarSyntacticObject.trace_val : ↑trace = RoseTree.node SyntacticObject.Vertex.trace []

@[simp]

theorem Minimalist.PlanarSyntacticObject.traceOf_val (tok : LexicalItem.Token) : ↑(traceOf tok) = RoseTree.node (SyntacticObject.Vertex.traceOf tok) []

@[simp]

theorem Minimalist.PlanarSyntacticObject.merge_val (l r : PlanarSyntacticObject) : ↑(l.merge r) = RoseTree.node SyntacticObject.Vertex.bare [↑l, ↑r]

def Minimalist.PlanarSyntacticObject.toSyntacticObject (p : PlanarSyntacticObject) : SyntacticObject

Forgetting the order is the quotient map to the syntactic object.

Equations

• ↑p = ⟨UnorderedTree.mk ↑p, ⋯⟩

@[simp]

theorem Minimalist.PlanarSyntacticObject.toSyntacticObject_val (p : PlanarSyntacticObject) : ↑↑p = UnorderedTree.mk ↑p

@[simp]

theorem Minimalist.PlanarSyntacticObject.toSyntacticObject_leaf (tok : LexicalItem.Token) : ↑↑tok = ↑tok

@[simp]

theorem Minimalist.PlanarSyntacticObject.toSyntacticObject_trace : ↑trace = SyntacticObject.trace

@[simp]

theorem Minimalist.PlanarSyntacticObject.toSyntacticObject_traceOf (tok : LexicalItem.Token) : ↑(traceOf tok) = SyntacticObject.traceOf tok

@[simp]

theorem Minimalist.PlanarSyntacticObject.toSyntacticObject_merge (l r : PlanarSyntacticObject) : ↑(l.merge r) = (↑l).merge ↑r

Forgetting the order commutes with Merge.

Induction and case analysis

theorem Minimalist.SyntacticObject.ind {motive : SyntacticObject → Prop} (leaf : ∀ (tok : LexicalItem.Token), motive ↑tok) (trace : motive trace) (traceOf : ∀ (tok : LexicalItem.Token), motive (traceOf tok)) (merge : ∀ (l r : SyntacticObject), motive l → motive r → motive (l.merge r)) (s : SyntacticObject) : motive s

Induction on syntactic objects, each of which is a lexical leaf, a trace, or the Merge of two syntactic objects.

theorem Minimalist.SyntacticObject.exists_form (s : SyntacticObject) : (∃ (tok : LexicalItem.Token), s = ↑tok) ∨ s = trace ∨ (∃ (tok : LexicalItem.Token), s = traceOf tok) ∨ ∃ (l : SyntacticObject) (r : SyntacticObject), s = l.merge r

Every syntactic object is a lexical leaf, a trace, or a Merge.