Derivation Steps and Traces

Ordered derivation tracking for Minimalist syntax: the sequence of Merge/Move operations that produces a SyntacticObject tree.

Key definitions

• SyntacticObject.replace — substitute a subtree, used to leave traces
• Step — a single derivation step (External or Internal Merge)
• Derivation — an ordered list of steps applied to an initial SO
• Derivation.final — the tree produced by applying all steps
• Derivation.stageAt — intermediate tree after n steps
• Derivation.movedItems — which subtrees underwent Internal Merge

def Minimalist.SyntacticObject.replace (so target replacement : SyntacticObject) : SyntacticObject

Equations

• so.replace target replacement = FreeCommMagma.lift (Minimalist.replaceAux✝ target replacement) ⋯ so

@[simp]

theorem Minimalist.SyntacticObject.replace_leaf (tok : LIToken) (target rep : SyntacticObject) : (leaf tok).replace target rep = if leaf tok = target then rep else leaf tok

@[simp]

theorem Minimalist.SyntacticObject.replace_trace (n : ℕ) (target rep : SyntacticObject) : (trace n).replace target rep = if trace n = target then rep else trace n

@[simp]

theorem Minimalist.SyntacticObject.replace_mul (l r target rep : SyntacticObject) : (l * r).replace target rep = if l * r = target then rep else l.replace target rep * r.replace target rep

inductive Minimalist.Step : Type

A single derivation step.

• emL (item : SyntacticObject) : Step

  External Merge: new item becomes left daughter.

• emR (item : SyntacticObject) : Step

  External Merge: new item becomes right daughter.

• im (mover : SyntacticObject) (traceId : ℕ) : Step

  Internal Merge: move mover to left edge, leaving a trace with traceId.

def Minimalist.instReprStep.repr : Step → ℕ → Std.Format

Equations

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

@[implicit_reducible]

instance Minimalist.instReprStep : Repr Step

Equations

• Minimalist.instReprStep = { reprPrec := Minimalist.instReprStep.repr }

def Minimalist.Step.apply (step : Step) (current : SyntacticObject) : SyntacticObject

Apply a derivation step to the current tree.

• emL: new item merges as left daughter (head/specifier above current)
• emR: new item merges as right daughter (complement of current)
• im: mover is extracted (replaced by trace) then re-merged at the left edge

Since * is commutative on SyntacticObject (the carrier is the free commutative magma), emL and emR produce the same SO; the distinction matters only for the planar projection at PF (which happens via linearize / phonYield, downstream of derivation).

Equations

• (Minimalist.Step.emL a).apply current = a * current
• (Minimalist.Step.emR a).apply current = current * a
• (Minimalist.Step.im a a_1).apply current = a * current.replace a (Minimalist.mkTrace a_1)

structure Minimalist.Derivation : Type

An ordered derivation: an initial SO plus a sequence of steps.

• initial : SyntacticObject
• steps : List Step

@[implicit_reducible]

instance Minimalist.instReprDerivation : Repr Derivation

Equations

• Minimalist.instReprDerivation = { reprPrec := Minimalist.instReprDerivation.repr }

def Minimalist.instReprDerivation.repr : Derivation → ℕ → Std.Format

Equations

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

def Minimalist.Derivation.final (d : Derivation) : SyntacticObject

The final tree produced by applying all derivation steps.

Equations

• d.final = List.foldl (fun (so : Minimalist.SyntacticObject) (step : Minimalist.Step) => step.apply so) d.initial d.steps

def Minimalist.Derivation.stageAt (d : Derivation) (n : ℕ) : SyntacticObject

The intermediate tree after the first n steps.

Equations

• d.stageAt n = List.foldl (fun (so : Minimalist.SyntacticObject) (step : Minimalist.Step) => step.apply so) d.initial (List.take n d.steps)

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

Number of derivation steps.

Equations

• d.length = d.steps.length

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

The subtrees that underwent Internal Merge (movement).

Equations

• d.movedItems = List.filterMap (fun (x : Minimalist.Step) => match x with | Minimalist.Step.im mover traceId => some mover | x => none) d.steps

theorem Minimalist.stageAt_zero (d : Derivation) : d.stageAt 0 = d.initial

Stage 0 is the initial tree (no steps applied).

theorem Minimalist.stageAt_length (d : Derivation) : d.stageAt d.steps.length = d.final

Stage at full length equals the final tree.

theorem Minimalist.replace_self (so replacement : SyntacticObject) : so.replace so replacement = replacement

Replacing so when it is the root returns the replacement.