Economy of derivations

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.

References

• [MCB25]

theorem Minimalist.SyntacticObject.exists_eq_merge_of_count_terms {mover current : SyntacticObject} (h : Multiset.count mover current.terms = 1) (hne : current ≠ mover) : ∃ (l : SyntacticObject) (r : SyntacticObject), current = l.merge r

An object with a unique accessible proper term is a Merge.

theorem Minimalist.Step.value_isLeft_apply {step : Step} {current : SyntacticObject} {W : Workspace} (h : Admissible current W step) : Sum.isLeft (↑(step.apply current)).value = true

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.

theorem Minimalist.Step.noComplexityLoss {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 No Complexity Loss, graded by the size σ. External Merge is a term of Merge taking both objects whole, and Internal Merge sends the current object to the Merge of the mover and the remainder, whose sizes sum to its own (the book's (1.6.10)).

theorem Minimalist.Step.minimalYield {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) : MinimalYield UnorderedTree.accessibleCount (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.

noncomputable def Minimalist.Step.workspacesAfter : List Step → SyntacticObject → List Workspace

The workspaces after each of a list of steps hold the object built so far beside the items still to come.

Equations

• Minimalist.Step.workspacesAfter [] x✝ = []
• Minimalist.Step.workspacesAfter (step :: steps) x✝ = ({step.apply x✝} + Minimalist.Step.itemsList steps) :: Minimalist.Step.workspacesAfter steps (step.apply x✝)

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

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.

Equations

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

theorem Minimalist.Derivation.isChain_noComplexityLoss {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

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

theorem Minimalist.Derivation.isChain_minimalYield {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

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