Documentation

Linglib.Syntax.Minimalist.Movement.Freezing

Freezing #

A constituent a derivation has moved is an island for later extraction, the freezing effect that descends from [ross-1967]'s Sentential Subject Constraint and that [chung-2006] makes the test of VP-raising analyses of VOS order: whatever a raised VP still contains cannot be extracted, whatever left it before it raised can. Frozen d x says that x sits inside some mover of d. Movers carry the traces of what evacuated them earlier, not the evacuees, so an evacuee is not frozen by the constituent it left; and a mover is itself available to move again. Freezing is monotone under extending the derivation and blind to the sides of External Merge.

Main definitions #

Main results #

References #

source
def Minimalist.SyntacticObject.Derivation.Frozen (d : Derivation) (x : SyntacticObject) :
Prop

x sits inside a constituent d has moved.

Equations
Instances For
    source
    @[instance_reducible]
    instance Minimalist.SyntacticObject.Derivation.instDecidableFrozen (d : Derivation) (x : SyntacticObject) :
    Decidable (d.Frozen x)
    Equations
    source
    theorem Minimalist.SyntacticObject.Derivation.frozen_append_iff {d : Derivation} {steps : List Step} {x : SyntacticObject} :
    (d.append steps).Frozen x ↔ d.Frozen x ∨ ∃ m ∈ List.filterMap Step.mover? steps, m.contains x

    Extending a derivation freezes what its new movers contain and nothing else.

    source
    theorem Minimalist.SyntacticObject.Derivation.Frozen.append {d : Derivation} {steps : List Step} {x : SyntacticObject} (h : d.Frozen x) :
    (d.append steps).Frozen x

    Freezing is monotone under extension.

    source
    @[simp]
    theorem Minimalist.SyntacticObject.Derivation.frozen_leftward_iff {d : Derivation} {x : SyntacticObject} :
    d.leftward.Frozen x ↔ d.Frozen x

    Freezing is blind to the sides of External Merge.