Documentation

Linglib.Syntax.Minimalist.Derivation.Freezing

Freezing #

A constituent that has moved is an island for later extraction, though it may itself move again. This is the Freezing condition, and it is what makes VP-raising analyses of VOS order testable, since whatever a raised VP still contains cannot be extracted and whatever left it before it raised can. Frozen d x says that x sits inside some mover of d, and ObeysFreezing d that no mover of d sits inside an earlier one, a pairwise condition on the list of movers in the shape of List.Nodup. Movers carry the traces of what evacuated them earlier, not the evacuees, so a remnant freezes nothing that left it.

Main definitions #

Main results #

References #

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

x sits inside a constituent d has moved.

Equations
Instances For
    source
    @[instance_reducible]
    instance Minimalist.Derivation.instDecidableFrozen (d : Derivation) (x : SyntacticObject) :
    Decidable (d.Frozen x)
    Equations
    source
    theorem Minimalist.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.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.Derivation.frozen_leftward_iff {d : Derivation} {x : SyntacticObject} :
    d.leftward.Frozen x ↔ d.Frozen x

    Freezing is blind to the sides of External Merge.

    source
    def Minimalist.Derivation.ObeysFreezing (d : Derivation) :
    Prop

    A derivation obeys Freezing when no step moves a constituent that an earlier mover contains.

    Equations
    Instances For
      source
      @[instance_reducible]
      instance Minimalist.Derivation.instDecidableObeysFreezing (d : Derivation) :
      Decidable d.ObeysFreezing
      Equations
      source
      theorem Minimalist.Derivation.obeysFreezing_append_iff {d : Derivation} {steps : List Step} :
      (d.append steps).ObeysFreezing ↔ d.ObeysFreezing ∧ List.Pairwise (fun (m m' : SyntacticObject) => ¬m.Contains m') (List.filterMap Step.mover? steps) ∧ ∀ m ∈ List.filterMap Step.mover? steps, ¬d.Frozen m
      source
      @[simp]
      theorem Minimalist.Derivation.obeysFreezing_append_im_iff {d : Derivation} {m : SyntacticObject} {side : Edge} :
      (d.append [Step.im m side]).ObeysFreezing ↔ d.ObeysFreezing ∧ ¬d.Frozen m

      A further movement obeys Freezing exactly when its mover is not frozen.

      source
      @[simp]
      theorem Minimalist.Derivation.obeysFreezing_append_em_iff {d : Derivation} {item : SyntacticObject} {side : Edge} :
      (d.append [Step.em side item]).ObeysFreezing ↔ d.ObeysFreezing

      A further External Merge obeys Freezing exactly when the derivation does.