Docs / Syntax / Minimalist / Workspace / Derivation

Economy of derivations

import Linglib.Syntax.Minimalist.Workspace.Derivation · namespace Minimalist

An admissible derivation step relates the workspace of the current object, its items and the items still to come to the workspace of the object it builds and those items. When its operands are not traces, that transformation satisfies No Complexity Loss graded by the size σ and Minimal Yield under trace counting (§1.6 of Marcolli, Chomsky and Berwick). An External Merge step is the term of Merge taking both objects whole and leaving the spectators uncut, so its component map loses no complexity. Along an admissible derivation the workspaces of its stages therefore form a chain of economical transformations.

Main definitions

Minimalist.Derivation.workspaces: the workspaces of a derivation's stages.

Main results

Minimalist.Step.noComplexityLoss, Step.minimalYield: an admissible step whose operands are not traces is economical.
Minimalist.Derivation.isChain_noComplexityLoss, isChain_minimalYield: so is every step of an admissible derivation.
Minimalist.Derivation.isChain_merge: every step of an admissible derivation is MERGE, an Internal Merge step leaving the trace of the mover's head.

References

Marcolli et al. 2025, Mathematical Structure of Syntactic Merge: An Algebraic Model for Generative Linguistics formalized

Declarations

L47–60

L68–73

External Merge as a term of Merge

External Merge of S and S' beside spectators W is the term of Merge taking S and S' whole and leaving every spectator uncut.

An admissible step whose operands are not traces satisfies No Complexity Loss under the size σ (the book's (1.6.10)).

theorem Step.noComplexityLoss L125–174

{step : Step} {current : SyntacticObject} {W : Workspace} (h : Admissible current W step) (hcur : Sum.isLeft (↑current).value = true) (hitems : ∀ i ∈ step.items, Sum.isLeft (↑i).value = true) :

NoComplexityLoss (fun (T : UnorderedTree (Option LexicalItem.Token ⊕ Option LexicalItem.Token)) => Forest.accessibleSize {T}) (Multiset.map Subtype.val ({current} + step.items + W)) (Multiset.map Subtype.val ({step.apply current} + W))

An admissible step whose operands are not traces satisfies Minimal Yield under trace counting.

theorem Step.minimalYield L176–198

MinimalYield UnorderedTree.accessibleCount (Multiset.map Subtype.val ({current} + step.items + W)) (Multiset.map Subtype.val ({step.apply current} + W))

L200–206

The workspaces of a derivation's stages hold the initial object beside its items, then after each step the object built so far beside the items still to come.

Derivation.workspaces L227–230

noncomputable def Minimalist.Derivation.workspaces (d : Derivation) :

List Workspace

d.workspaces = ({d.initial} + d.items) :: Step.workspacesAfter d.steps d.initial

Built from

Used by Derivation.isChain_merge, Derivation.isChain_noComplexityLoss, Derivation.isChain_minimalYield

Each step of an admissible derivation is MERGE on the workspaces of its stages: an External Merge step leaving copies, and an Internal Merge step leaving the trace of the mover's head.

theorem Derivation.isChain_merge L232–247

{d : Derivation} (hd : d.Admissible) :

List.IsChain (fun (W W' : Workspace) => ∃ (P : SyntacticObject) (Q : SyntacticObject), W' = W.merge P Q ∨ W' = Workspace.mergeWith (fun (x : SyntacticObject) => x.headTrace) W P Q) d.workspaces

Built from

Every step of an admissible derivation whose initial object and items are not traces satisfies No Complexity Loss, graded by the size σ.

theorem Derivation.isChain_noComplexityLoss L249–257

{d : Derivation} (hd : d.Admissible) (hinit : Sum.isLeft (↑d.initial).value = true) (hitems : ∀ i ∈ d.items, Sum.isLeft (↑i).value = true) :

List.IsChain (fun (W W' : Workspace) => NoComplexityLoss (fun (T : UnorderedTree (Option LexicalItem.Token ⊕ Option LexicalItem.Token)) => Forest.accessibleSize {T}) (Multiset.map Subtype.val W) (Multiset.map Subtype.val W')) d.workspaces

Built from

Every step of an admissible derivation whose initial object and items are not traces satisfies Minimal Yield under trace counting.

theorem Derivation.isChain_minimalYield L259–266

{d : Derivation} (hd : d.Admissible) (hinit : Sum.isLeft (↑d.initial).value = true) (hitems : ∀ i ∈ d.items, Sum.isLeft (↑i).value = true) :

List.IsChain (fun (W W' : Workspace) => MinimalYield UnorderedTree.accessibleCount (Multiset.map Subtype.val W) (Multiset.map Subtype.val W')) d.workspaces

Built from