Derivations

An ordered derivation is an initial syntactic object with a sequence of Merge steps, each placing its new daughter on a side. External Merge adds an item, and Internal Merge raises a mover: the step re-merges the mover with the remainder deleteAccessible mover current, the current object with the mover's occurrences replaced by the trace of the mover's head. Which item heads the mover is a theory's choice, so the steps and stages take the trace encoder as a parameter, by default the head by selection. Internal Merge also comes in its two stages: extract puts a copy of the mover on a stack beside the object, leaving its trace, and remerge merges the copy on top back, so a derivation runs on a configuration of the object and the stack (Derivation.run) and copies extracted in one order merge back in the reverse. Each step is the algebraic Merge on the workspace of the current object, the items it introduces, and the items still to come, when it matches no accessible term of those items and an Internal Merge raises a uniquely accessible term (Step.mergeOp_workspace); an admissible derivation is then the iterated algebraic Merge on the workspace of its initial object and its items (Derivation.mergeOpList_initial). The node being commutative, the two sides build the same object; the side is a planarization datum that matters only for the surface order, which Linearization/Replay.lean recovers on an ordered planar accumulator, since the final object is an unordered quotient. Since node is noncomputable, so are Step.apply and Derivation.final, while the movers are read off the steps. A derivation extends by further steps, whose early stages and movers are the original's, and normalizes by moving every new daughter to the left, which changes no stage and no mover.

Main definitions

• Minimalist.Step, Step.apply, Step.run, Step.mover?, Step.mergeOp, Step.Admissible
• Minimalist.Derivation, Derivation.Cfg, Derivation.run, final, stageAt, movedItems, mover?, take, append, leftward, items, Admissible

Main results

• Minimalist.Step.apply_em: the sides build the same object.
• Minimalist.Step.run_im: Internal Merge is an extraction followed by merging back.
• Minimalist.Step.mergeOp_workspace: an admissible step is the algebraic Merge on the workspace.
• Minimalist.Derivation.mergeOpList_initial: an admissible derivation is the iterated algebraic Merge.
• Minimalist.Derivation.stageAt_append_of_le, movedItems_append: extension keeps the early stages and the movers.
• Minimalist.Derivation.stageAt_leftward, movedItems_leftward: the sides change no stage and no mover.

TODO

• Extend Step.Admissible and Step.mergeOp_workspace to extract and remerge, the two stages of Internal Merge, on the workspace of the object, its stack and the items still to come.

References

• [MCB25], §1.2 (Definition 1.2.6) and §1.4 (Lemma 1.4.1, Proposition 1.4.2)

Steps

inductive Minimalist.Step : Type

A derivation step. A Merge step attaches its new daughter on an Edge of the mother, a planarization datum that externalization reads and the derived object ignores. im records only the mover; the trace it leaves is that of its head under the trace encoder the step is applied with. Internal Merge is also available in its two stages, extract and remerge ([MCB25] Proposition 1.4.2), so that several copies can wait on the stack of the workspace.

• em (side : Edge) (item : SyntacticObject) : Step

  External Merge, the new item as the daughter on side.

• im (mover : SyntacticObject) (side : Edge := Edge.left) : Step

  Internal Merge raises mover to the daughter on side, the left unless stated otherwise, leaving the trace of its head in its place.

• extract (mover : SyntacticObject) : Step

  The unit stage of Internal Merge puts a copy of mover on top of the stack, leaving the trace of its head in its place.

• remerge (side : Edge := Edge.left) : Step

  The copy on top of the stack merges back as the daughter on side.

structure Minimalist.Derivation.Cfg (α : Type u_1) : Type u_1

A configuration of a derivation is the object under construction and the stack of copies extracted from it, the top first.

• current : α

  The object under construction.

• stack : List α

  The extracted copies not yet merged back, the top first.

def Minimalist.Derivation.Cfg.map {α : Type u_1} {β : Type u_2} (f : α → β) (c : Cfg α) : Cfg β

A map applied to the object and to every copy on the stack.

Equations

• Minimalist.Derivation.Cfg.map f c = { current := f c.current, stack := List.map f c.stack }

@[simp]

theorem Minimalist.Derivation.Cfg.map_current {α : Type u_1} {β : Type u_2} (f : α → β) (c : Cfg α) : (map f c).current = f c.current

@[simp]

theorem Minimalist.Derivation.Cfg.map_stack {α : Type u_1} {β : Type u_2} (f : α → β) (c : Cfg α) : (map f c).stack = List.map f c.stack

noncomputable def Minimalist.Step.apply (step : Step) (current : SyntacticObject) (τ : SyntacticObject → Option LexicalItem.Token := SyntacticObject.selHead) : SyntacticObject

The object a step builds from the current one, the copies on the stack aside. External Merge adds the item on the given side, Internal Merge merges the remainder and the mover, leaving the trace of its head under τ, and an extraction leaves the remainder. remerge needs the stack (Step.run).

Equations

• (Minimalist.Step.em Edge.left item).apply current τ = item.merge current
• (Minimalist.Step.em Edge.right item).apply current τ = current.merge item
• (Minimalist.Step.im mover side).apply current τ = (mover.deleteAccessible current τ).merge mover
• (Minimalist.Step.extract mover).apply current τ = mover.deleteAccessible current τ
• (Minimalist.Step.remerge side).apply current τ = current

noncomputable def Minimalist.Step.run (step : Step) (c : Derivation.Cfg SyntacticObject) (τ : SyntacticObject → Option LexicalItem.Token := SyntacticObject.selHead) : Derivation.Cfg SyntacticObject

A step on a configuration. An extraction pushes the mover's copy onto the stack, remerge merges the copy on top back by External Merge, and the other steps leave the stack alone.

Equations

• (Minimalist.Step.extract mover).run c τ = { current := (Minimalist.Step.extract mover).apply c.current τ, stack := mover :: c.stack }
• (Minimalist.Step.remerge side).run c τ = { current := (Minimalist.Step.em side m).apply c.current τ, stack := st }
• step✝.run c τ = { current := step✝.apply c.current τ, stack := c.stack }

theorem Minimalist.Step.apply_em_left {τ : SyntacticObject → Option LexicalItem.Token} (item current : SyntacticObject) : (em Edge.left item).apply current τ = item.merge current

theorem Minimalist.Step.apply_em_right {τ : SyntacticObject → Option LexicalItem.Token} (item current : SyntacticObject) : (em Edge.right item).apply current τ = current.merge item

theorem Minimalist.Step.apply_im {τ : SyntacticObject → Option LexicalItem.Token} (mover : SyntacticObject) (side : Edge) (current : SyntacticObject) : (im mover side).apply current τ = (mover.deleteAccessible current τ).merge mover

theorem Minimalist.Step.apply_em {τ : SyntacticObject → Option LexicalItem.Token} (side : Edge) (item current : SyntacticObject) : (em side item).apply current τ = item.merge current

The sides build the same object; they differ only at externalization.

def Minimalist.Step.mover? : Step → Option SyntacticObject

The mover of an Internal-Merge step or an extraction.

Equations

• (Minimalist.Step.im mover side).mover? = some mover
• (Minimalist.Step.extract mover).mover? = some mover
• (Minimalist.Step.em side item).mover? = none
• (Minimalist.Step.remerge side).mover? = none

@[simp]

theorem Minimalist.Step.mover?_em (side : Edge) (item : SyntacticObject) : (em side item).mover? = none

@[simp]

theorem Minimalist.Step.mover?_im (mover : SyntacticObject) (side : Edge) : (im mover side).mover? = some mover

def Minimalist.Step.leftward : Step → Step

The step with its new daughter on the left.

Equations

• (Minimalist.Step.em side item).leftward = Minimalist.Step.em Edge.left item
• (Minimalist.Step.im mover side).leftward = Minimalist.Step.im mover
• (Minimalist.Step.extract mover).leftward = Minimalist.Step.extract mover
• (Minimalist.Step.remerge side).leftward = Minimalist.Step.remerge

@[simp]

theorem Minimalist.Step.leftward_em (side : Edge) (item : SyntacticObject) : (em side item).leftward = em Edge.left item

@[simp]

theorem Minimalist.Step.leftward_im (mover : SyntacticObject) (side : Edge) : (im mover side).leftward = im mover

@[simp]

theorem Minimalist.Step.mover?_leftward (step : Step) : step.leftward.mover? = step.mover?

theorem Minimalist.Step.apply_leftward {τ : SyntacticObject → Option LexicalItem.Token} (step : Step) (current : SyntacticObject) : step.leftward.apply current τ = step.apply current τ

A step and its leftward form build the same object.

theorem Minimalist.Step.run_leftward {τ : SyntacticObject → Option LexicalItem.Token} (step : Step) (c : Derivation.Cfg SyntacticObject) : step.leftward.run c τ = step.run c τ

A step and its leftward form reach the same configuration.

theorem Minimalist.Step.run_im {τ : SyntacticObject → Option LexicalItem.Token} (mover : SyntacticObject) (side : Edge) (c : Derivation.Cfg SyntacticObject) : (im mover side).run c τ = (remerge side).run ((extract mover).run c τ) τ

Internal Merge is an extraction followed by merging the copy back ([MCB25] Proposition 1.4.2).

Derivations as workspace Merges

A step merges the current object with the items it introduces, beside a spectator workspace of the items still to come. When it matches no accessible term of the spectators, and an Internal Merge raises a uniquely accessible proper term, the step is the algebraic Merge on the workspace (Step.mergeOp_workspace), and a derivation is the iterated algebraic Merge on the workspace of its initial object and its items (mergeOpList_initial). The two stages of Internal Merge, extract and remerge, act on the stack beside the object, which this workspace leaves out, so they are not admissible here.

def Minimalist.Step.items : Step → Workspace

The item an External Merge step introduces.

Equations

• (Minimalist.Step.em side item).items = {item}
• (Minimalist.Step.im mover side).items = 0
• (Minimalist.Step.extract mover).items = 0
• (Minimalist.Step.remerge side).items = 0

def Minimalist.Step.itemsList (steps : List Step) : Workspace

The items a list of steps introduces.

Equations

• Minimalist.Step.itemsList steps = (List.map Minimalist.Step.items steps).sum

@[simp]

theorem Minimalist.Step.itemsList_nil : itemsList [] = 0

@[simp]

theorem Minimalist.Step.itemsList_cons (step : Step) (steps : List Step) : itemsList (step :: steps) = step.items + itemsList steps

noncomputable def Minimalist.Step.mergeOp (step : Step) (current : SyntacticObject) : ConnesKreimer ℤ (UnorderedTree SyntacticObject.Vertex) →ₗ[ℤ] ConnesKreimer ℤ (UnorderedTree SyntacticObject.Vertex)

A step applies an algebraic Merge at the current object, External Merge with the item or the unit stage followed by External Merge of the remainder with the mover.

Equations

• One or more equations did not get rendered due to their size.
• (Minimalist.Step.em side item).mergeOp current = Minimalist.Merge.mergeOpC Minimalist.SyntacticObject.traceEncoder Minimalist.SyntacticObject.Vertex.bare ↑current ↑item
• (Minimalist.Step.extract mover).mergeOp current = Minimalist.Merge.mergeOpUnitC Minimalist.SyntacticObject.traceEncoder ↑mover
• (Minimalist.Step.remerge side).mergeOp current = 0

def Minimalist.Step.Admissible (current : SyntacticObject) (W : Workspace) : Step → Prop

A step at the current object is admissible beside a spectator workspace W when it matches no accessible term of W, and an Internal Merge raises a uniquely accessible proper term that is not a trace.

Equations

• One or more equations did not get rendered due to their size.
• Minimalist.Step.Admissible current W (Minimalist.Step.em side item) = ∀ U ∈ W, current ∉ U.terms ∧ item ∉ U.terms
• Minimalist.Step.Admissible current W (Minimalist.Step.extract mover) = False
• Minimalist.Step.Admissible current W (Minimalist.Step.remerge side) = False

theorem Minimalist.Step.mergeOp_workspace {step : Step} {current : SyntacticObject} {W : Workspace} (h : Admissible current W step) : (step.mergeOp current) (ConnesKreimer.of' (Multiset.map Subtype.val ({current} + step.items + W))) = ConnesKreimer.of' (Multiset.map Subtype.val ({step.apply current} + W))

An admissible step is the algebraic Merge on the workspace of the current object, the items it introduces, and the spectators.

noncomputable def Minimalist.Step.mergeOpList : List Step → SyntacticObject → ConnesKreimer ℤ (UnorderedTree SyntacticObject.Vertex) →ₗ[ℤ] ConnesKreimer ℤ (UnorderedTree SyntacticObject.Vertex)

The algebraic Merges of a list of steps from the current object, composed in order.

Equations

• Minimalist.Step.mergeOpList [] x✝ = LinearMap.id
• Minimalist.Step.mergeOpList (step :: steps) x✝ = Minimalist.Step.mergeOpList steps (step.apply x✝) ∘ₗ step.mergeOp x✝

def Minimalist.Step.AdmissibleList : List Step → SyntacticObject → Prop

Every step of a list is admissible beside the items still to come.

Equations

• Minimalist.Step.AdmissibleList [] x✝ = True
• Minimalist.Step.AdmissibleList (step :: steps) x✝ = (Minimalist.Step.Admissible x✝ (Minimalist.Step.itemsList steps) step ∧ Minimalist.Step.AdmissibleList steps (step.apply x✝))

theorem Minimalist.Step.mergeOpList_workspace (steps : List Step) (current : SyntacticObject) : AdmissibleList steps current → (mergeOpList steps current) (ConnesKreimer.of' (Multiset.map Subtype.val ({current} + itemsList steps))) = ConnesKreimer.of' {↑(List.foldl (fun (so : SyntacticObject) (step : Step) => step.apply so) current steps)}

Admissible steps compose to the algebraic Merge from the workspace of the current object and the items they introduce to the object they build.

theorem Minimalist.Step.foldl_run_of_admissibleList (steps : List Step) (current : SyntacticObject) (st : List SyntacticObject) : AdmissibleList steps current → List.foldl (fun (c : Derivation.Cfg SyntacticObject) (step : Step) => step.run c) { current := current, stack := st } steps = { current := List.foldl (fun (so : SyntacticObject) (step : Step) => step.apply so) current steps, stack := st }

Admissible steps leave the stack alone and build what they build on the object.

Derivations

structure Minimalist.Derivation : Type

An initial syntactic object with a sequence of steps.

• initial : SyntacticObject

  The initial syntactic object (a lexical item, in canonical derivations).

• steps : List Step

  The ordered sequence of Merge/Move steps.

noncomputable def Minimalist.Derivation.run (d : Derivation) (τ : SyntacticObject → Option LexicalItem.Token := SyntacticObject.selHead) : Cfg SyntacticObject

The configuration after every step, under the trace encoder τ.

Equations

• d.run τ = List.foldl (fun (c : Minimalist.Derivation.Cfg Minimalist.SyntacticObject) (step : Minimalist.Step) => step.run c τ) { current := d.initial, stack := [] } d.steps

noncomputable def Minimalist.Derivation.final (d : Derivation) (τ : SyntacticObject → Option LexicalItem.Token := SyntacticObject.selHead) : SyntacticObject

The object after every step, under the trace encoder τ.

Equations

• d.final τ = (d.run τ).current

def Minimalist.Derivation.length (d : Derivation) : ℕ

The number of derivation steps.

Equations

• d.length = d.steps.length

def Minimalist.Derivation.movedItems (d : Derivation) : List SyntacticObject

The movers of the im and extract steps.

Equations

• d.movedItems = List.filterMap Minimalist.Step.mover? d.steps

def Minimalist.Derivation.mover? (d : Derivation) (i : ℕ) : Option SyntacticObject

The mover of step i, when that step is an Internal Merge or an extraction.

Equations

• d.mover? i = d.steps[i]? >>= Minimalist.Step.mover?

def Minimalist.Derivation.take (d : Derivation) (n : ℕ) : Derivation

The first n steps.

Equations

• d.take n = { initial := d.initial, steps := List.take n d.steps }

def Minimalist.Derivation.append (d : Derivation) (steps : List Step) : Derivation

The derivation continued by steps.

Equations

• d.append steps = { initial := d.initial, steps := d.steps ++ steps }

noncomputable def Minimalist.Derivation.stageAt (d : Derivation) (n : ℕ) (τ : SyntacticObject → Option LexicalItem.Token := SyntacticObject.selHead) : SyntacticObject

The object after the first n steps, under the trace encoder τ.

Equations

• d.stageAt n τ = (d.take n).final τ

@[simp]

theorem Minimalist.Derivation.stageAt_zero {τ : SyntacticObject → Option LexicalItem.Token} (d : Derivation) : d.stageAt 0 τ = d.initial

theorem Minimalist.Derivation.stageAt_length {τ : SyntacticObject → Option LexicalItem.Token} (d : Derivation) : d.stageAt d.steps.length τ = d.final τ

@[simp]

theorem Minimalist.Derivation.final_take {τ : SyntacticObject → Option LexicalItem.Token} (d : Derivation) (n : ℕ) : (d.take n).final τ = d.stageAt n τ

Extension

The early stages and the movers of an extended derivation are the original's.

@[simp]

theorem Minimalist.Derivation.length_append (d : Derivation) (steps : List Step) : (d.append steps).length = d.length + steps.length

@[simp]

theorem Minimalist.Derivation.append_assoc (d : Derivation) (steps steps' : List Step) : (d.append steps).append steps' = d.append (steps ++ steps')

theorem Minimalist.Derivation.take_append_of_le {d : Derivation} {n : ℕ} (h : n ≤ d.length) (steps : List Step) : (d.append steps).take n = d.take n

The first n ≤ d.length steps of an extension are d's.

@[simp]

theorem Minimalist.Derivation.take_length_append (d : Derivation) (steps : List Step) : (d.append steps).take d.length = d

theorem Minimalist.Derivation.stageAt_append_of_le {τ : SyntacticObject → Option LexicalItem.Token} {d : Derivation} {n : ℕ} (h : n ≤ d.length) (steps : List Step) : (d.append steps).stageAt n τ = d.stageAt n τ

theorem Minimalist.Derivation.run_append {τ : SyntacticObject → Option LexicalItem.Token} (d : Derivation) (steps : List Step) : (d.append steps).run τ = List.foldl (fun (c : Cfg SyntacticObject) (step : Step) => step.run c τ) (d.run τ) steps

@[simp]

theorem Minimalist.Derivation.movedItems_append (d : Derivation) (steps : List Step) : (d.append steps).movedItems = d.movedItems ++ List.filterMap Step.mover? steps

theorem Minimalist.Derivation.lt_length_of_mem_mover? {d : Derivation} {i : ℕ} {m : SyntacticObject} (h : m ∈ d.mover? i) : i < d.length

A step at index i has a mover only if i indexes a step.

theorem Minimalist.Derivation.mem_movedItems_of_mem_mover? {d : Derivation} {i : ℕ} {m : SyntacticObject} (h : m ∈ d.mover? i) : m ∈ d.movedItems

The mover of a step is one of the derivation's movers.

theorem Minimalist.Derivation.mover?_append_of_lt {d : Derivation} {i : ℕ} (h : i < d.length) (steps : List Step) : (d.append steps).mover? i = d.mover? i

The early steps of an extension have the original's movers.

The sides of Merge

The node being commutative, the derived object does not depend on the sides at which the steps attach their daughters; leftward is the normal form, and the stages and movers of a derivation are those of its normal form.

def Minimalist.Derivation.leftward (d : Derivation) : Derivation

The derivation with every new daughter on the left.

Equations

• d.leftward = { initial := d.initial, steps := List.map Minimalist.Step.leftward d.steps }

@[simp]

theorem Minimalist.Derivation.run_leftward {τ : SyntacticObject → Option LexicalItem.Token} (d : Derivation) : d.leftward.run τ = d.run τ

@[simp]

theorem Minimalist.Derivation.final_leftward {τ : SyntacticObject → Option LexicalItem.Token} (d : Derivation) : d.leftward.final τ = d.final τ

@[simp]

theorem Minimalist.Derivation.stageAt_leftward {τ : SyntacticObject → Option LexicalItem.Token} (d : Derivation) (n : ℕ) : d.leftward.stageAt n τ = d.stageAt n τ

@[simp]

theorem Minimalist.Derivation.movedItems_leftward (d : Derivation) : d.leftward.movedItems = d.movedItems

def Minimalist.Derivation.items (d : Derivation) : Workspace

The items a derivation introduces by External Merge.

Equations

• d.items = Minimalist.Step.itemsList d.steps

def Minimalist.Derivation.Admissible (d : Derivation) : Prop

A derivation is admissible when each of its steps is, beside the items still to come.

Equations

• d.Admissible = Minimalist.Step.AdmissibleList d.steps d.initial

theorem Minimalist.Derivation.mergeOpList_initial {d : Derivation} (hd : d.Admissible) : (Step.mergeOpList d.steps d.initial) (ConnesKreimer.of' (Multiset.map Subtype.val ({d.initial} + d.items))) = ConnesKreimer.of' {↑d.final}

An admissible derivation is the iterated algebraic Merge on the workspace of its initial object and its items: the composite of its steps' Merges sends that workspace to its final object.

Carrier tests