Docs / Syntax / Minimalist / Locality / Transfer

Transfer and the Phase Impenetrability Condition

import Linglib.Syntax.Minimalist.Locality.Transfer · namespace Minimalist

Transfer seals the domain of a phase head, so that an operation at a later stage cannot inspect it: the Phase Impenetrability Condition is the effect of Transfer on the search space. A stage is the root of the object built so far, a position of the finished object, and a cut assigns to each stage the positions sealed by then. A phase head's domain is its complement, or the whole phase short of its root, transferred once the phase is complete or once the next phase head merges; a deleted phase head passes its phasehood to the head of its complement. A position reaches its phase level when the phase of the lowest phase head whose complement contains it is complete.

Main definitions

Minimalist.Cut: the positions sealed at each stage.
Minimalist.complementDomain, Minimalist.wholePhaseDomain: transfer domains.
Minimalist.Pic1, Minimalist.Pic2: when a phase head's domain is transferred.
Minimalist.sealed: the positions the transferred domains seal.
Minimalist.transferSlice: what a phase head transfers on its own, outside inner domains.
Minimalist.phaseLevel: the stage at which a position reaches its phase level.
Minimalist.LinkLeaves: a link of a chain leaves the positions a cut seals.

Main results

Minimalist.isUpperSet_sealed, Minimalist.sealed_anti: sealed sets are closed under dominance and grow as the derivation proceeds.
Minimalist.sealed_pic2_subset_pic1: the next-phase condition seals less.
Minimalist.escapes_iff, Minimalist.crosses_iff: islands and the condition on chain links are cuts.

Implementation notes

A stage is a position of the finished object, so the derivation is taken to be cyclic.
The phase heads, and the deleted ones, are supplied by the analysis.

References

Chomsky 2000, Minimalist Inquiries: The Framework
Chomsky 2001, Derivation by Phase
Chomsky 2015, Problems of Projection: Extensions formalized

Declarations

A cut assigns to each stage, the root of the object built so far, the positions an operation at that stage cannot inspect.

@[reducible, inline] abbrev Cut L57–59

Type

Cut = (Core.Order.TreePath → Set Core.Order.TreePath)

Used by sealed, LinkLeaves, instDecidableLinkLeavesOfDecidablePredTreePathMemSet

L61–63

L67–70

The complement of the head that transfers, Chomsky 2000's transfer domain.

def complementDomain L72–74

(hd : HeadFunction) (t : LinearizedSyntacticObject) (deleted : Finset Core.Order.TreePath) (h : Core.Order.TreePath) :

Set Core.Order.TreePath

complementDomain hd t deleted h = Set.Ici (complement (transferHead hd t deleted h))

Built from

Used by instDecidablePredTreePathMemSetComplementDomain, isUpperSet_complementDomain, crosses_iff

Used in Syntax/Minimalist/Locality/AntiLocality, Syntax/Minimalist/Locality/Horizon, Ke2026

The phase short of its root, transferred whole.

def wholePhaseDomain L76–77

(hd : HeadFunction) (t : LinearizedSyntacticObject) (h : Core.Order.TreePath) :

Set Core.Order.TreePath

wholePhaseDomain hd t h = Set.Ioi (projectionAt hd t h)

Used by instDecidablePredTreePathMemSetWholePhaseDomain, isUpperSet_wholePhaseDomain

Used in Ke2026

Chomsky 2000's schedule: the domain of h is transferred once its phase is complete, at every stage above it.

def Pic1 L79–81

(hd : HeadFunction) (t : LinearizedSyntacticObject) :

Schedule

Pic1 hd t x✝ h s = (s < projectionAt hd t h)

Built from

Used by instDecidablePic1, antitone_pic1, pic1_of_pic2, sealed_pic2_subset_pic1, crosses_iff

Used in Syntax/Minimalist/Locality/AntiLocality, Ke2026

Chomsky 2001's schedule: the domain of h is transferred once a phase head whose complement contains the phase of h has merged.

def Pic2 L83–85

(hd : HeadFunction) (t : LinearizedSyntacticObject) :

Schedule

Pic2 hd t Φ h s = ∃ z ∈ Φ, s ≤ z.parent ∧ complement z ≤ projectionAt hd t h

Built from

Used by instDecidablePic2, antitone_pic2, pic1_of_pic2, sealed_pic2_subset_pic1

The positions sealed at stage s: the domains of the phase heads transferred by then.

def sealed L87–89

(Φ : Finset Core.Order.TreePath) (D : Core.Order.TreePath → Set Core.Order.TreePath) (σ : Schedule) :

Cut

sealed Φ D σ s = {q : Core.Order.TreePath | ∃ h ∈ Φ, σ Φ h s ∧ q ∈ D h}

Built from ,

Used by instDecidablePredTreePathMemSetSealedOfDecidable, isUpperSet_sealed, sealed_anti, sealed_pic2_subset_pic1, escapes_iff, crosses_iff

Used in Syntax/Minimalist/Locality/AntiLocality, Syntax/Minimalist/Locality/Horizon

Sealed positions dominate only sealed positions.

theorem isUpperSet_sealed L117–119

{Φ : Finset Core.Order.TreePath} {D : Core.Order.TreePath → Set Core.Order.TreePath} {σ : Schedule} {s : Core.Order.TreePath} (hD : ∀ (h : Core.Order.TreePath), IsUpperSet (D h)) :

IsUpperSet (sealed Φ D σ s)

Built from ,

A schedule under which a domain stays transferred seals more at every later stage.

theorem sealed_anti L121–123

{Φ : Finset Core.Order.TreePath} {D : Core.Order.TreePath → Set Core.Order.TreePath} {σ : Schedule} (hσ : ∀ (h : Core.Order.TreePath), Antitone (σ Φ h)) :

Antitone (sealed Φ D σ)

Built from ,

L125

L127–128

L130–132

Chomsky 2001's condition seals less than Chomsky 2000's.

theorem sealed_pic2_subset_pic1 L134–136

{hd : HeadFunction} {t : LinearizedSyntacticObject} {Φ : Finset Core.Order.TreePath} {D : Core.Order.TreePath → Set Core.Order.TreePath} {s : Core.Order.TreePath} :

sealed Φ D (Pic2 hd t) s ⊆ sealed Φ D (Pic1 hd t) s

Built from , ,

What a phase head transfers on its own

The positions in the domain of h outside the domain of every phase head inside it: what the domain of h transfers on its own.

def transferSlice L140–144

(Φ : Finset Core.Order.TreePath) (D : Core.Order.TreePath → Set Core.Order.TreePath) (h : Core.Order.TreePath) :

Set Core.Order.TreePath

transferSlice Φ D h = {q : Core.Order.TreePath | q ∈ D h ∧ ∀ h' ∈ Φ, h' ∈ D h → q ∉ D h'}

Used by instDecidablePredTreePathMemSetTransferSlice, transferSlice_subset, disjoint_transferSlice

Used in Syntax/Minimalist/Case/SyntacticObject

L146–147

L149

L151–153

The phase level

The phase level of a position: the phase of the lowest phase head whose complement contains it, or the root where there is none. Chomsky 2015 computes labels there.

def phaseLevel L158–163

(hd : HeadFunction) (t : LinearizedSyntacticObject) (Φ : Finset Core.Order.TreePath) (q : (↑t).Positions) :

(↑t).Positions

The definition is too large to print here; read it in the source.

Used by phaseLevel_le, projectionAt_le_phaseLevel, phaseLevel_eq_bot

Used in Chomsky2015

L165–166

L168–172

L174–177

Chain links that leave a cut

A link of the chain of tok leaves the positions cut seals at the stage of its landing site, the mother of the phrase that lands.

def LinkLeaves L182–185

(hd : HeadFunction) (t : LinearizedSyntacticObject) (tok : LexicalItem.Token) (cut : Cut) :

Prop

LinkLeaves hd t tok cut = ∃ x ∈ links hd t tok, x.2 ∈ cut x.1.parent

Built from

Used by instDecidableLinkLeavesOfDecidablePredTreePathMemSet, escapes_iff, crosses_iff

An island is a cut: a link escapes the domain at D exactly when it leaves the positions D dominates, sealed at every stage above D.

theorem escapes_iff L233–241

{hd : HeadFunction} {t : LinearizedSyntacticObject} {tok : LexicalItem.Token} {D : Core.Order.TreePath} :

Escapes hd t tok D ↔ LinkLeaves hd t tok (sealed {D} Set.Ici fun (x : Finset Core.Order.TreePath) (h s : Core.Order.TreePath) => s < h)

Built from ,

The condition on chain links is a cut: a link leaves the phase of h exactly when it leaves the complement of h, sealed at every stage above the phase.

theorem crosses_iff L243–258

{hd : HeadFunction} {t : LinearizedSyntacticObject} {tok : LexicalItem.Token} {h : Core.Order.TreePath} (hh : h ∈ (↑t).validPaths) (h0 : h ≠ ⊥) (hproj : projectionAt hd t h ≤ h.parent) :

Crosses hd t tok h ↔ LinkLeaves hd t tok (sealed {h} (complementDomain hd t ∅) (Pic1 hd t))

Built from , , ,