structure Minimalism.NumerationEntry : Type

A numeration entry: a lexical item with a count (how many times it can be used)

The count allows the same LI to appear multiple times in a derivation. E.g., "John said John left" uses 'John' twice.

• item : ExtendedLI
• count : ℕ
• countPos : self.count > 0

instance Minimalism.instReprNumerationEntry : Repr NumerationEntry

Equations

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

def Minimalism.instReprNumerationEntry.repr : NumerationEntry → ℕ → Std.Format

Equations

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

structure Minimalism.Numeration : Type

A numeration is a collection of LIs available for the derivation

• entries : List NumerationEntry

instance Minimalism.instReprNumeration : Repr Numeration

Equations

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

def Minimalism.instReprNumeration.repr : Numeration → ℕ → Std.Format

Equations

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

def Minimalism.Numeration.empty : Numeration

Empty numeration

Equations

• Minimalism.Numeration.empty = { entries := [] }

def Minimalism.Numeration.add (n : Numeration) (li : ExtendedLI) (count : ℕ) (h : count > 0) : Numeration

Add an LI to the numeration

Equations

• n.add li count h = { entries := { item := li, count := count, countPos := h } :: n.entries }

def Minimalism.Numeration.exhausted (n : Numeration) : Bool

Check if numeration is exhausted (all counts = 0)

Equations

• n.exhausted = n.entries.all fun (x : Minimalism.NumerationEntry) => x.count == 0

def Minimalism.Numeration.contains (n : Numeration) (li : ExtendedLI) : Bool

Check if numeration contains a given LI

Equations

• n.contains li = n.entries.any fun (e : Minimalism.NumerationEntry) => e.item.base == li.base && decide (e.count > 0)

def Minimalism.Numeration.totalCount (n : Numeration) : ℕ

Total items remaining in numeration

Equations

• n.totalCount = List.foldl (fun (acc : ℕ) (e : Minimalism.NumerationEntry) => acc + e.count) 0 n.entries

structure Minimalism.Workspace : Type

The workspace contains the active syntactic objects being combined

At any point in a derivation, the workspace contains:

• SOs that have been built so far
• LIs that have been selected but not yet merged

• objects : List SyntacticObject
• nextId : ℕ

def Minimalism.instReprWorkspace.repr : Workspace → ℕ → Std.Format

Equations

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

instance Minimalism.instReprWorkspace : Repr Workspace

Equations

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

def Minimalism.Workspace.empty : Workspace

Empty workspace

Equations

• Minimalism.Workspace.empty = { objects := [], nextId := 0 }

def Minimalism.Workspace.size (w : Workspace) : ℕ

Number of objects in workspace

Equations

• w.size = w.objects.length

def Minimalism.Workspace.isSingleton (w : Workspace) : Bool

Check if workspace contains a single object (derivation complete condition)

Equations

• w.isSingleton = (w.objects.length == 1)

def Minimalism.Workspace.getResult (w : Workspace) : Option SyntacticObject

Get the result if workspace is singleton

Equations

• w.getResult = match w.objects with | [so] => some so | x => none

structure Minimalism.SelectResult : Type

Result of a select operation

• numeration : Numeration
• workspace : Workspace
• selected : SyntacticObject

def Minimalism.select (n : Numeration) (w : Workspace) (li : ExtendedLI) : Option SelectResult

Select: Move an LI from numeration to workspace

This operation:

1. Finds the LI in the numeration
2. Decrements its count
3. Creates a token and adds it to the workspace

Equations

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

def Minimalism.select.findAndDecrement (li : ExtendedLI) (entries acc : List NumerationEntry) : Option (List NumerationEntry)

Equations

• One or more equations did not get rendered due to their size.
• Minimalism.select.findAndDecrement li [] acc = none

inductive Minimalism.MergeTrigger : Type

What triggers Merge? In Minimalism, uninterpretable features drive operations

• selection : Cat → MergeTrigger
• epp : MergeTrigger
• theta : MergeTrigger

instance Minimalism.instReprMergeTrigger : Repr MergeTrigger

Equations

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

def Minimalism.instReprMergeTrigger.repr : MergeTrigger → ℕ → Std.Format

Equations

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

def Minimalism.instDecidableEqMergeTrigger.decEq (x✝ x✝¹ : MergeTrigger) : Decidable (x✝ = x✝¹)

Equations

• Minimalism.instDecidableEqMergeTrigger.decEq (Minimalism.MergeTrigger.selection a) (Minimalism.MergeTrigger.selection b) = if h : a = b then h ▸ isTrue ⋯ else isFalse ⋯
• Minimalism.instDecidableEqMergeTrigger.decEq (Minimalism.MergeTrigger.selection a) Minimalism.MergeTrigger.epp = isFalse ⋯
• Minimalism.instDecidableEqMergeTrigger.decEq (Minimalism.MergeTrigger.selection a) Minimalism.MergeTrigger.theta = isFalse ⋯
• Minimalism.instDecidableEqMergeTrigger.decEq Minimalism.MergeTrigger.epp (Minimalism.MergeTrigger.selection a) = isFalse ⋯
• Minimalism.instDecidableEqMergeTrigger.decEq Minimalism.MergeTrigger.epp Minimalism.MergeTrigger.epp = isTrue ⋯
• Minimalism.instDecidableEqMergeTrigger.decEq Minimalism.MergeTrigger.epp Minimalism.MergeTrigger.theta = isFalse Minimalism.instDecidableEqMergeTrigger.decEq._proof_6
• Minimalism.instDecidableEqMergeTrigger.decEq Minimalism.MergeTrigger.theta (Minimalism.MergeTrigger.selection a) = isFalse ⋯
• Minimalism.instDecidableEqMergeTrigger.decEq Minimalism.MergeTrigger.theta Minimalism.MergeTrigger.epp = isFalse Minimalism.instDecidableEqMergeTrigger.decEq._proof_8
• Minimalism.instDecidableEqMergeTrigger.decEq Minimalism.MergeTrigger.theta Minimalism.MergeTrigger.theta = isTrue ⋯

instance Minimalism.instDecidableEqMergeTrigger : DecidableEq MergeTrigger

Equations

• Minimalism.instDecidableEqMergeTrigger = Minimalism.instDecidableEqMergeTrigger.decEq

def Minimalism.needsMerge (li : ExtendedLI) : Bool

Check if an LI needs to merge (has unsatisfied selectional features)

Equations

• Minimalism.needsMerge li = !List.isEmpty li.base.outerSel

def Minimalism.getSelectionalTarget (li : ExtendedLI) : Option Cat

Get the category that an LI selects (if any)

Equations

• Minimalism.getSelectionalTarget li = List.head? li.base.outerSel

structure Minimalism.ExternalMergeOp : Type

External Merge: combine two separate SOs from the workspace

This is feature-driven: we merge when there's a selectional relationship

• selector : SyntacticObject
• selected : SyntacticObject
• trigger : MergeTrigger

instance Minimalism.instReprExternalMergeOp : Repr ExternalMergeOp

Equations

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

def Minimalism.instReprExternalMergeOp.repr : ExternalMergeOp → ℕ → Std.Format

Equations

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

def Minimalism.applyExternalMerge (w : Workspace) (op : ExternalMergeOp) : Option Workspace

Apply external merge to the workspace

Equations

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

def Minimalism.validExternalMerge (op : ExternalMergeOp) : Bool

Check if external merge is valid (selector selects the selected)

Equations

• Minimalism.validExternalMerge op = Minimalism.selectsB op.selector op.selected

structure Minimalism.InternalMergeOp : Type

Internal Merge: re-merge an SO already in the structure (movement)

This handles cases where an element moves to a new position

• target : SyntacticObject
• mover : SyntacticObject
• trigger : MergeTrigger

def Minimalism.instReprInternalMergeOp.repr : InternalMergeOp → ℕ → Std.Format

Equations

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

instance Minimalism.instReprInternalMergeOp : Repr InternalMergeOp

Equations

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

def Minimalism.moverInTarget (op : InternalMergeOp) : Bool

Check if mover is contained in target

Equations

• Minimalism.moverInTarget op = Minimalism.moverInTarget.checkContains op op.target

def Minimalism.moverInTarget.checkContains (op : InternalMergeOp) (so : SyntacticObject) : Bool

Equations

• Minimalism.moverInTarget.checkContains op (Minimalism.SyntacticObject.leaf a) = if (Minimalism.SyntacticObject.leaf a == op.mover) = true then true else false
• Minimalism.moverInTarget.checkContains op (a.node b) = if (a.node b == op.mover) = true then true else Minimalism.moverInTarget.checkContains op a || Minimalism.moverInTarget.checkContains op b

def Minimalism.applyInternalMerge (w : Workspace) (op : InternalMergeOp) : Option Workspace

Apply internal merge to workspace

Equations

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

structure Minimalism.DerivationState : Type

A derivation state captures everything needed to continue a derivation.

features maps token IDs to their current feature bundles, tracking feature state across Agree operations. Populated by selectStep (which registers an LI's features under its token ID) and modified by agreeStep (which values the probe's features from the goal).

• numeration : Numeration
• workspace : Workspace
• features : List (ℕ × FeatureBundle)

instance Minimalism.instReprDerivationState : Repr DerivationState

Equations

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

def Minimalism.instReprDerivationState.repr : DerivationState → ℕ → Std.Format

Equations

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

def Minimalism.DerivationState.init (n : Numeration) : DerivationState

Initial state from a numeration

Equations

• Minimalism.DerivationState.init n = { numeration := n, workspace := Minimalism.Workspace.empty }

def Minimalism.DerivationState.isComplete (s : DerivationState) : Bool

Is the derivation complete?

A derivation is complete when:

1. The numeration is exhausted (all items used)
2. The workspace contains exactly one SO

Equations

• s.isComplete = (s.numeration.exhausted && s.workspace.isSingleton)

def Minimalism.DerivationState.getResult (s : DerivationState) : Option SyntacticObject

Get the derived structure if complete

Equations

• s.getResult = if s.isComplete = true then s.workspace.getResult else none

structure Minimalism.AgreeOp : Type

An Agree operation between a probe and a goal, identified by token ID.

Records which feature type is being checked, enabling the derivation trace to track feature valuation step by step.

• probeId : ℕ
• goalId : ℕ
• feature : FeatureVal

instance Minimalism.instReprAgreeOp : Repr AgreeOp

Equations

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

def Minimalism.instReprAgreeOp.repr : AgreeOp → ℕ → Std.Format

Equations

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

def Minimalism.lookupFeatures (fs : List (ℕ × FeatureBundle)) (id : ℕ) : Option FeatureBundle

Look up the current feature bundle for a token by ID.

Equations

• Minimalism.lookupFeatures fs id = Option.map Prod.snd (List.find? (fun (p : ℕ × Minimalism.FeatureBundle) => p.fst == id) fs)

def Minimalism.updateFeatures (fs : List (ℕ × FeatureBundle)) (id : ℕ) (fb : FeatureBundle) : List (ℕ × FeatureBundle)

Update the feature bundle for a token by ID.

Equations

• Minimalism.updateFeatures fs id fb = List.map (fun (p : ℕ × Minimalism.FeatureBundle) => if (p.fst == id) = true then (p.fst, fb) else p) fs

inductive Minimalism.DerivationStep : Type

A single step in a derivation

• selectStep : ExtendedLI → DerivationStep
• externalMergeStep : ExternalMergeOp → DerivationStep
• internalMergeStep : InternalMergeOp → DerivationStep
• transferStep : SyntacticObject → DerivationStep
• agreeStep : AgreeOp → DerivationStep

def Minimalism.instReprDerivationStep.repr : DerivationStep → ℕ → Std.Format

Equations

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

instance Minimalism.instReprDerivationStep : Repr DerivationStep

Equations

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

def Minimalism.applyStep (s : DerivationState) (step : DerivationStep) : Option DerivationState

Apply a derivation step to a state

Equations

• One or more equations did not get rendered due to their size.
• Minimalism.applyStep s (Minimalism.DerivationStep.transferStep a) = some s

structure Minimalism.FullDerivation : Type

A derivation is a sequence of steps from initial state to completion

• initial : Numeration
• steps : List DerivationStep
• final : DerivationState
• valid : self.final.isComplete = true

def Minimalism.executeSteps (n : Numeration) (steps : List DerivationStep) : Option DerivationState

Execute a list of steps from an initial numeration

Equations

• Minimalism.executeSteps n steps = List.foldlM (fun (s : Minimalism.DerivationState) (step : Minimalism.DerivationStep) => Minimalism.applyStep s step) (Minimalism.DerivationState.init n) steps

def Minimalism.workspaceStageAt (n : Numeration) (steps : List DerivationStep) (k : ℕ) : Option DerivationState

Intermediate workspace state after the first k steps.

Analogous to Derivation.stageAt but for the workspace model. Returns none if any step in the prefix fails.

Equations

• Minimalism.workspaceStageAt n steps k = Minimalism.executeSteps n (List.take k steps)

def Minimalism.featureStateAt (n : Numeration) (steps : List DerivationStep) (k tokenId : ℕ) : Option FeatureBundle

Look up a token's feature state at a given derivation stage.

Equations

• Minimalism.featureStateAt n steps k tokenId = match Minimalism.workspaceStageAt n steps k with | some state => Minimalism.lookupFeatures state.features tokenId | none => none

def Minimalism.FullDerivation.resultTree (fd : FullDerivation) : Option SyntacticObject

Extract the final syntactic object from a completed derivation.

Equations

• fd.resultTree = fd.final.workspace.getResult

def Minimalism.FullDerivation.agreesWithDerivation (fd : FullDerivation) (d : Derivation) : Prop

A workspace FullDerivation agrees with a core Derivation when both produce the same final tree. This connects the feature-driven workspace model to the step-by-step tree-building model.

Equations

• fd.agreesWithDerivation d = (fd.resultTree = some d.final)

def Minimalism.theCatNumeration : Numeration

Example: Numeration for "the cat"

Equations

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

structure Minimalism.MinimalistGrammar : Type

A Minimalist grammar specifies the lexicon as a list of extended LIs.

• lexicon : List ExtendedLI

structure Minimalism.MinDerivation (g : MinimalistGrammar) : Type

Minimalist derivations link a formal derivation to a clause type.

• deriv : FullDerivation
• clauseType : ClauseType

instance Minimalism.instGrammarMinimalistGrammar : Grammar MinimalistGrammar

Minimalism Grammar instance.

Derivations are formal FullDerivations from Workspace.lean. Realization checks that the phonological yield matches.

Equations

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