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 Minimalism.SyntacticObject.replace (so target replacement : SyntacticObject) : SyntacticObject

Replace all occurrences of target in so with replacement.

In well-formed derivations with unique LIToken IDs, each subtree appears exactly once, so this replaces at most one position.

Equations

• (Minimalism.SyntacticObject.leaf a).replace target replacement = if (Minimalism.SyntacticObject.leaf a == target) = true then replacement else Minimalism.SyntacticObject.leaf a
• (l.node r).replace target replacement = if (l.node r == target) = true then replacement else (l.replace target replacement).node (r.replace target replacement)

inductive Minimalism.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.

instance Minimalism.instReprStep : Repr Step

Equations

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

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

Equations

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

def Minimalism.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

Equations

• (Minimalism.Step.emL a).apply current = a.node current
• (Minimalism.Step.emR a).apply current = current.node a
• (Minimalism.Step.im a a_1).apply current = a.node (current.replace a (Minimalism.mkTrace a_1))

structure Minimalism.Derivation : Type

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

• initial : SyntacticObject
• steps : List Step

instance Minimalism.instReprDerivation : Repr Derivation

Equations

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

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

Equations

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

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

The final tree produced by applying all derivation steps.

Equations

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

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

The intermediate tree after the first n steps.

Equations

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

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

Number of derivation steps.

Equations

• d.length = d.steps.length

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

The subtrees that underwent Internal Merge (movement).

Equations

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

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

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

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

Stage at full length equals the final tree.

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

Replacing so when it is the root returns the replacement.