Docs / Syntax / Minimalist / SyntacticObject / Lift

The universal property of the syntactic-object carrier

import Linglib.Syntax.Minimalist.SyntacticObject.Lift · namespace Minimalist.SyntacticObject

Leaf data valued in a commutative magma with zero extends to a morphism of magmas out of SyntacticObject L (lift, the FreeMagma.lift analogue), and two such morphisms agreeing on the leaves are equal (hom_ext). The zero absorbs the off-carrier arities, so one total algebra (mergeAlgebra) drives the fold, the quotient descent, and the subtype restriction once and for all: consumers supply a lexical-leaf value and a trace value, the latter for the bare trace (none) and for the trace of each token (some tok), the three kinds of leaf hom_ext distinguishes, and inherit Perm-invariance from mul_comm via a private permutation-invariance lemma — no bespoke step induction.

Main declarations

Minimalist.SyntacticObject.mergeAlgebra: the node algebra induced by a magma-with-zero — lexical leaf ↦ ℓ, trace leaf ↦ τ of its token if any, bare binary node ↦ *, other arities ↦ 0.
Minimalist.SyntacticObject.liftN: its evaluation on the nonplanar carrier.
Minimalist.SyntacticObject.liftFun, Minimalist.SyntacticObject.lift: the induced map on syntactic objects, unbundled (computable) and as →ₙ*.

Main results

Minimalist.SyntacticObject.hom_ext: morphisms of magmas out of SyntacticObject L agreeing on lexical and trace leaves are equal.
Minimalist.SyntacticObject.liftN_merge: the magma law on the unordered carrier.
Minimalist.SyntacticObject.liftEquiv, Minimalist.SyntacticObject.equivFreeCommMagma: the universal property, and the carrier as the free commutative magma on its leaf alphabet.

Declarations

The node algebra of a magma-with-zero: lexical leaf ↦ ℓ, trace leaf ↦ τ of the token it is the trace of, if any, bare binary node ↦ *, off-carrier arities ↦ 0.

def mergeAlgebra L55–63

{L : Type} {β : Type u_1} [Mul β] [Zero β] (ℓ : L → β) (τ : Option L → β) :

Vertex L → List β → β

mergeAlgebra ℓ τ (Sum.inl (some tok)) x✝ = ℓ tok
mergeAlgebra ℓ τ (Sum.inl none) [x_2, y] = x_2 * y
mergeAlgebra ℓ τ (Sum.inl none) x✝ = 0
mergeAlgebra ℓ τ (Sum.inr u) [] = τ u
mergeAlgebra ℓ τ (Sum.inr val) x✝ = 0

Used by mergeAlgebra_perm, liftN, liftN_mk

Used in Syntax/Minimalist/Label/Selection

L108–121

The catamorphism descends to the nonplanar carrier by mergeAlgebra_perm, giving the induced algebra.

def liftN L123–127

{L : Type} {β : Type u_1} [CommMagma β] [Zero β] (ℓ : L → β) (τ : Option L → β) :

UnorderedTree (Vertex L) → β

liftN ℓ τ = Quotient.lift (RoseTree.fold (mergeAlgebra ℓ τ)) ⋯

Built from

Used by liftN_mk, liftN_merge, liftFun

Used in Syntax/Minimalist/Label/Selection

L129–130

Merge multiplies values, the nonplanar magma law.

theorem liftN_merge L132–137

{L : Type} {β : Type u_1} [CommMagma β] [Zero β] (ℓ : L → β) (τ : Option L → β) (a b : UnorderedTree (Vertex L)) :

liftN ℓ τ (UnorderedTree.node Vertex.bare {a, b}) = liftN ℓ τ a * liftN ℓ τ b

Built from

The induced map on syntactic objects, unbundled — computable, decide-friendly.

def liftFun L139–140

{L : Type} {β : Type u_1} [CommMagma β] [Zero β] (ℓ : L → β) (τ : Option L → β) (s : SyntacticObject L) :

liftFun ℓ τ s = liftN ℓ τ ↑s

Built from

Used by liftFun_leaf, liftFun_trace, liftFun_traceOf, liftFun_merge, lift, lift_apply, liftFun_coe_ne_zero, coe_liftHom

Leaf data extends to a morphism of magmas out of the carrier, the existence half of the universal property (cf. FreeMagma.lift).

lift L156–160

noncomputable def Minimalist.SyntacticObject.lift {L : Type} {β : Type u_1} [CommMagma β] [Zero β] (ℓ : L → β) (τ : Option L → β) :

SyntacticObject L →ₙ* β

lift ℓ τ = { toFun := liftFun ℓ τ, map_mul' := ⋯ }

Built from

Used by lift_apply

Used in Syntax/Minimalist/Label/Selection

L162

Morphisms agreeing on the leaves are equal, the uniqueness half of the universal property.

theorem hom_ext L166–177

{L : Type} {β : Type u_1} [Mul β] {f g : SyntacticObject L →ₙ* β} (hlex : ∀ (tok : L), f ↑tok = g ↑tok) (htrace : f trace = g trace) (htraceOf : ∀ (tok : L), f (traceOf tok) = g (traceOf tok)) :

f = g

Freeness

The universal property of the carrier: leaf data valued in a commutative magma M corresponds to magma homomorphisms out of SyntacticObject L, so the carrier is the free commutative magma on L ⊕ Option L, its lexical items and traces.

liftEquiv L227–237