Building and reading syntactic objects

Merge on the carrier is written *: External Merge of two objects, and the re-merge of a mover with the remainder in Internal Merge. Concrete objects are built ordered, as PlanarSyntacticObjects, and forgotten to the carrier by toSyntacticObject. The accessors read the root token, the leaf and node counts, and the trace predicate, which recognizes the trace leaves, bare or indexed.

Main definitions

• Minimalist.SyntacticObject.mkLeaf, mkLeafPhon: lexical leaves from features.
• Minimalist.SyntacticObject.token?, isTrace, leafCount, nodeCount, IsLeaf.

@[instance_reducible]

instance Minimalist.SyntacticObject.instInhabited : Inhabited SyntacticObject

The default syntactic object is the bare trace.

Equations

• Minimalist.SyntacticObject.instInhabited = { default := Minimalist.SyntacticObject.trace }

Merge as multiplication

@[instance_reducible]

noncomputable instance Minimalist.SyntacticObject.instMul : Mul SyntacticObject

Merge on the carrier is written l * r.

Equations

• Minimalist.SyntacticObject.instMul = { mul := Minimalist.SyntacticObject.merge }

@[simp]

theorem Minimalist.SyntacticObject.mul_def (l r : SyntacticObject) : l * r = l.merge r

theorem Minimalist.SyntacticObject.mul_comm (l r : SyntacticObject) : l * r = r * l

@[instance_reducible]

instance Minimalist.SyntacticObject.instCoeToken : Coe LexicalItem.Token SyntacticObject

A lexical item is a leaf.

Equations

• Minimalist.SyntacticObject.instCoeToken = { coe := Minimalist.SyntacticObject.leaf }

@[instance_reducible]

noncomputable instance Minimalist.SyntacticObject.instInsert : Insert SyntacticObject SyntacticObject

Merge in braces, as [MCB25] writes it: {l, r} = merge l r, with {s} = s.

Equations

• Minimalist.SyntacticObject.instInsert = { insert := Minimalist.SyntacticObject.merge }

@[instance_reducible]

instance Minimalist.SyntacticObject.instSingleton : Singleton SyntacticObject SyntacticObject

Equations

• Minimalist.SyntacticObject.instSingleton = { singleton := id }

@[simp]

theorem Minimalist.SyntacticObject.insert_def (l r : SyntacticObject) : {l, r} = l.merge r

@[instance_reducible]

instance Minimalist.PlanarSyntacticObject.instMul : Mul PlanarSyntacticObject

Merge on the ordered carrier, in the given order, is written l * r.

Equations

• Minimalist.PlanarSyntacticObject.instMul = { mul := Minimalist.PlanarSyntacticObject.merge }

@[simp]

theorem Minimalist.PlanarSyntacticObject.mul_def (l r : PlanarSyntacticObject) : l * r = l.merge r

@[instance_reducible]

instance Minimalist.PlanarSyntacticObject.instCoeToken : Coe LexicalItem.Token PlanarSyntacticObject

A lexical item is a leaf.

Equations

• Minimalist.PlanarSyntacticObject.instCoeToken = { coe := Minimalist.PlanarSyntacticObject.leaf }

@[instance_reducible]

instance Minimalist.PlanarSyntacticObject.instCoeSyntacticObject : Coe PlanarSyntacticObject SyntacticObject

An ordered object is an object.

Equations

• Minimalist.PlanarSyntacticObject.instCoeSyntacticObject = { coe := Minimalist.PlanarSyntacticObject.toSyntacticObject }

def Minimalist.PlanarSyntacticObject.toSyntacticObjectHom : PlanarSyntacticObject →ₙ* SyntacticObject

Forgetting the order is a homomorphism of magmas.

Equations

• Minimalist.PlanarSyntacticObject.toSyntacticObjectHom = { toFun := Minimalist.PlanarSyntacticObject.toSyntacticObject, map_mul' := Minimalist.PlanarSyntacticObject.toSyntacticObject_merge }

@[simp]

theorem Minimalist.PlanarSyntacticObject.toSyntacticObjectHom_apply (p : PlanarSyntacticObject) : toSyntacticObjectHom p = ↑p

@[simp]

theorem Minimalist.PlanarSyntacticObject.toSyntacticObject_mul (l r : PlanarSyntacticObject) : ↑(l * r) = ↑l * ↑r

Merge in braces

[MCB25] writes Merge as set formation, {α, β}. Lean's {a, b} is insert a {b}, so with {p} = p the object {T, {V, PossP}} is T * (V * PossP), in the given order; its elements are objects, a head entering as its leaf.

@[instance_reducible]

instance Minimalist.PlanarSyntacticObject.instSingleton : Singleton PlanarSyntacticObject PlanarSyntacticObject

Equations

• Minimalist.PlanarSyntacticObject.instSingleton = { singleton := id }

@[instance_reducible]

instance Minimalist.PlanarSyntacticObject.instInsert : Insert PlanarSyntacticObject PlanarSyntacticObject

Equations

• Minimalist.PlanarSyntacticObject.instInsert = { insert := Minimalist.PlanarSyntacticObject.merge }

@[simp]

theorem Minimalist.PlanarSyntacticObject.singleton_def (p : PlanarSyntacticObject) : {p} = p

@[simp]

theorem Minimalist.PlanarSyntacticObject.insert_def (l r : PlanarSyntacticObject) : {l, r} = l.merge r

Lexical leaves from features

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

A lexical leaf from a category and selectional stack.

Equations

• Minimalist.SyntacticObject.mkLeaf cat sel id = ↑{ item := Minimalist.LexicalItem.of cat sel, id := id }

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

A lexical leaf with a phonological form.

Equations

• Minimalist.SyntacticObject.mkLeafPhon cat sel phon id = ↑{ item := Minimalist.LexicalItem.of cat sel phon, id := id }

Accessors

def Minimalist.SyntacticObject.token? (s : SyntacticObject) : Option LexicalItem.Token

The lexical token at the root, if the root is a lexical leaf.

Equations

• s.token? = match (↑s).value with | Sum.inl o => o | Sum.inr val => none

@[simp]

theorem Minimalist.SyntacticObject.token?_leaf (tok : LexicalItem.Token) : (↑tok).token? = some tok

@[simp]

theorem Minimalist.SyntacticObject.token?_trace : trace.token? = none

@[simp]

theorem Minimalist.SyntacticObject.token?_traceOf (tok : LexicalItem.Token) : (traceOf tok).token? = none

def Minimalist.SyntacticObject.isLeafOf (c : Cat) (s : SyntacticObject) : Prop

s is a lexical leaf whose item's category is c.

Equations

• Minimalist.SyntacticObject.isLeafOf c s = (Option.map (fun (x : Minimalist.LexicalItem.Token) => x.item.cat) s.token? = some c)

@[instance_reducible]

instance Minimalist.SyntacticObject.instDecidablePredIsLeafOf (c : Cat) : DecidablePred (isLeafOf c)

Equations

• Minimalist.SyntacticObject.instDecidablePredIsLeafOf c x✝ = Minimalist.SyntacticObject.instDecidablePredIsLeafOf._aux_1 c x✝

@[simp]

theorem Minimalist.SyntacticObject.isLeafOf_leaf (c : Cat) (tok : LexicalItem.Token) : isLeafOf c ↑tok ↔ tok.item.cat = c

@[simp]

theorem Minimalist.SyntacticObject.not_isLeafOf_trace (c : Cat) : ¬isLeafOf c trace

theorem Minimalist.SyntacticObject.traceOf_ne_trace (tok : LexicalItem.Token) : traceOf tok ≠ trace

@[simp]

theorem Minimalist.SyntacticObject.token?_merge (l r : SyntacticObject) : (l.merge r).token? = none

def Minimalist.SyntacticObject.isTrace (s : SyntacticObject) : Prop

A trace leaf, bare or indexed.

Equations

• s.isTrace = (Sum.isRight (↑s).value = true ∧ (↑s).numNodes = 1)

@[instance_reducible]

instance Minimalist.SyntacticObject.instDecidableIsTrace (s : SyntacticObject) : Decidable s.isTrace

Equations

• s.instDecidableIsTrace = { decide := decide (Sum.isRight (↑s).value = true) && decide ((↑s).numNodes = 1), reflects_decide := ⋯ }

@[simp]

theorem Minimalist.SyntacticObject.isTrace_traceOf (tok : LexicalItem.Token) : (traceOf tok).isTrace

@[simp]

theorem Minimalist.SyntacticObject.not_isTrace_leaf (tok : LexicalItem.Token) : ¬(↑tok).isTrace

@[simp]

theorem Minimalist.SyntacticObject.isTrace_trace : trace.isTrace

def Minimalist.SyntacticObject.leafCount (s : SyntacticObject) : ℕ

The number of leaves, traces included.

Equations

• s.leafCount = (↑s).numLeaves

def Minimalist.SyntacticObject.IsLeaf (s : SyntacticObject) : Prop

An object is a lexical or trace leaf exactly when its leaf count is one.

Equations

• s.IsLeaf = (s.leafCount = 1)

@[instance_reducible]

instance Minimalist.SyntacticObject.instDecidablePredIsLeaf : DecidablePred IsLeaf

Equations

• x✝.instDecidablePredIsLeaf = { decide := x✝.leafCount.beq 1, reflects_decide := ⋯ }

@[simp]

theorem Minimalist.SyntacticObject.isLeaf_leaf (tok : LexicalItem.Token) : (↑tok).IsLeaf

@[simp]

theorem Minimalist.SyntacticObject.isLeaf_trace : trace.IsLeaf

@[instance_reducible]

instance Minimalist.SyntacticObject.instRepr : Repr SyntacticObject

A shape summary; the full tree is a quotient with no faithful readout.

Equations

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

def Minimalist.SyntacticObject.nodeCount (s : SyntacticObject) : ℕ

nodeCount s = leafCount s - 1, the number of internal vertices of a full binary tree.

Equations

• s.nodeCount = (↑s).numLeaves - 1

@[simp]

theorem Minimalist.SyntacticObject.leafCount_leaf (tok : LexicalItem.Token) : (↑tok).leafCount = 1

@[simp]

theorem Minimalist.SyntacticObject.leafCount_trace : trace.leafCount = 1

Carrier tests