Derivation steps on the SyntacticObject carrier #
P4-pre-b of the single-carrier program: the ordered derivation layer on the SyntacticObject
carrier — the sequence of Merge/Move operations producing a syntactic object — replacing
the legacy FreeCommMagma-based Step/Derivation.
The derivation's Merge is the workspace Merge by construction. Each step applies a
canonical MCB Merge operator (Workspace.lean): External Merge is SyntacticObject.merge (Lemma
1.4.1), Internal Merge is SyntacticObject.intMerge (Prop 1.4.2's M_{T/β,β}) on the deletion
remainder SyntacticObject.deleteAccessible mover current (= T/mover). So Step.apply unfolds
to the coproduct operators (SyntacticObject.Step.apply_emL/apply_im); the Δ^ρ-coproduct identity
is SyntacticObject.merge_toForest/SyntacticObject.intMerge_toForest — nothing is independently
stipulated then
bridged.
Index-free traces (D2): Internal Merge leaves the bare SyntacticObject.traceLeaf; chain
identity
is workspace-level (Workspace, chainMultiplicity, #795, MCB Def 1.2.1), not a
per-step Nat. The deletion remainder is realized by SyntacticObject.replace (#804): for a
uniquely-accessible mover this is exactly the Δ^ρ cut remainder SyntacticObject.intMerge_toForest
extracts, and replace-all is its total extension to the multi-occurrence (chain) case.
Because SyntacticObject.node is noncomputable, so are Step.apply/Derivation.final — concrete
trees are reasoned about structurally, not by decide. The computable, decide-able
surface order (externalization replay + the Π bridge, the Cinque-style word-order
readout) lives in Linearization/Replay.lean; it replays the linear choices on an
ordered planar accumulator, since final (a Nonplanar quotient) is unordered.
Steps #
A single derivation step on the SyntacticObject carrier. Index-free (D2): im records
only the mover; the trace it leaves is the bare SyntacticObject.traceLeaf, and the mover ↔
trace
chain lives at the workspace level (#795), not in a per-step index.
- emL
(item : SyntacticObject)
: Step
External Merge, new item as the left daughter.
- emR
(item : SyntacticObject)
: Step
External Merge, new item as the right daughter.
- im
(mover : SyntacticObject)
: Step
Internal Merge: raise
mover, leaving the bare trace in its place.
Instances For
Internal-Merge deletion remainder T/mover ([MCB25]
Def 1.2.7, the ρ-form): the syntactic object left when the moved constituent's
accessible occurrence is cut, with the bare SyntacticObject.traceLeaf in its place. For a
uniquely-accessible mover this is the Δ^ρ deletion remainder p0.2 that
SyntacticObject.intMerge_toForest extracts from cutSummandsN; SyntacticObject.replace
(replace-all) is
its total extension to the multi-occurrence case (the chain is then read at the
workspace level, Def 1.2.1).
Equations
- mover.deleteAccessible current = current.replace mover Minimalist.SyntacticObject.traceLeaf
Instances For
Apply a derivation step to the current tree. The derivation Merge is the
workspace Merge by construction: External Merge is SyntacticObject.merge (Lemma 1.4.1),
Internal Merge is SyntacticObject.intMerge (Prop 1.4.2's M_{T/β,β}) applied to the deletion
remainder SyntacticObject.deleteAccessible mover current (= T/mover). The coproduct identity
of each is SyntacticObject.merge_toForest/SyntacticObject.intMerge_toForest. Since
SyntacticObject.merge is commutative
(SyntacticObject.mul_comm), emL/emR and the mover-left/remainder-left orders give the
same
SyntacticObject (apply_emL_eq_emR); the left/right distinction matters only for the surface
(PF) order, recovered downstream by the externalization replay.
Equations
- (Minimalist.SyntacticObject.Step.emL item).apply current = item.merge current
- (Minimalist.SyntacticObject.Step.emR item).apply current = current.merge item
- (Minimalist.SyntacticObject.Step.im mover).apply current = mover.intMerge (mover.deleteAccessible current)
Instances For
External Merge unfolds to the canonical workspace EM SyntacticObject.merge (Lemma 1.4.1).
External Merge unfolds to the canonical workspace EM SyntacticObject.merge (Lemma 1.4.1).
Internal Merge unfolds to the coproduct operator by construction. The im step
is the canonical workspace IM SyntacticObject.intMerge (MCB Prop 1.4.2) on the deletion
remainder — definitionally, not via a bridge. Composing with SyntacticObject.intMerge_toForest
gives the Δ^ρ-coproduct identity on the workspace.
External Merge is side-indifferent on the unordered carrier: emL and emR build
the same syntactic object (they diverge only at externalization).
Derivations #
An ordered derivation: an initial SyntacticObject together with a sequence of steps.
- initial : SyntacticObject
The initial syntactic object (a lexical item, in canonical derivations).
- steps : List Step
The ordered sequence of Merge/Move steps.
Instances For
The final tree produced by applying every step in order.
Equations
- d.final = List.foldl (fun (so : Minimalist.SyntacticObject) (step : Minimalist.SyntacticObject.Step) => step.apply so) d.initial d.steps
Instances For
The intermediate tree after the first n steps.
Equations
- d.stageAt n = List.foldl (fun (so : Minimalist.SyntacticObject) (step : Minimalist.SyntacticObject.Step) => step.apply so) d.initial (List.take n d.steps)
Instances For
The number of derivation steps.
Instances For
The movers — the subtrees that underwent Internal Merge.
Equations
- d.movedItems = List.filterMap (fun (x : Minimalist.SyntacticObject.Step) => match x with | Minimalist.SyntacticObject.Step.im mover => some mover | x => none) d.steps
Instances For
Stage 0 is the initial tree (no steps applied).
The stage at full length is the final tree.