A pronounced head occupies the position.
- IsHeadPosition t p = ∃ x ∈ tokenList ↑t, x.1 = p
Used by instDecidableIsHeadPosition, compToSpec_or_mem_sealed
Docs / Syntax / Minimalist / Locality / AntiLocality
Anti-locality
import Linglib.Syntax.Minimalist.Locality.AntiLocality · namespace Minimalist
Anti-locality bars movement that is too short. Abels's version bars the complement of a head from moving to a specifier of the head's phrase; Erlewine's bars a specifier from moving unless it crosses a maximal projection other than the one it leaves, a projection being crossed when it dominates the phrase that moves but not its landing site. With the PIC, Abels's version leaves the complement of a phase head no way out, so that a phase head cannot be stranded.
Main definitions
Minimalist.crossed: the maximal projections a link of a chain crosses.Minimalist.SpecToSpec,Minimalist.CompToSpec: links too short in Erlewine's and in Abels's sense.
Main results
Minimalist.compToSpec_or_mem_sealed: a link that moves the complement of a phase head is Comp-to-Spec or leaves the positions the PIC seals.
Implementation notes
- A link pairs the phrase that lands with the position of the lower copy (
Minimalist.links); the phrase that moves is the projection of the lower copy. - Erlewine restricts his version to Ā-movement. The definitions apply to any link, and an analysis picks the links it constrains.
References
- Abels 2003, Successive cyclicity, anti-locality, and adposition stranding
- Erlewine 2016, Anti-locality and Optimality in Kaqchikel Agent Focus formalized
Declarations
Built from
The maximal projections a link crosses, those dominating the phrase that moves but not its landing site (Erlewine 2016).
(hd : HeadFunction) (t : LinearizedSyntacticObject) (x : Core.Order.TreePath × Core.Order.TreePath) :
Finset Core.Order.TreePath
The definition is too large to print here; read it in the source.
A link moves a specifier, a phrase whose sister is no head, across no maximal projection but the one it leaves, which Erlewine 2016's Spec-to-Spec anti-locality bans.
(hd : HeadFunction) (t : LinearizedSyntacticObject) (x : Core.Order.TreePath × Core.Order.TreePath) :
The definition is too large to print here; read it in the source.
Used by instDecidableSpecToSpec
Used in Erlewine2020
(hd : HeadFunction) (t : LinearizedSyntacticObject) (x : Core.Order.TreePath × Core.Order.TreePath) :
Decidable (SpecToSpec hd t x)
The definition is too large to print here; read it in the source.
Built from
A link moves the complement of a head to a specifier of the head's phrase, which Abels 2003's anti-locality bans.
(hd : HeadFunction) (t : LinearizedSyntacticObject) (x : Core.Order.TreePath × Core.Order.TreePath) :
The definition is too large to print here; read it in the source.
(hd : HeadFunction) (t : LinearizedSyntacticObject) (x : Core.Order.TreePath × Core.Order.TreePath) :
Decidable (CompToSpec hd t x)
The definition is too large to print here; read it in the source.
Built from
A link that moves the complement of a phase head, landing outside it, moves it to a specifier of the head's phrase or leaves the complement after the phase is complete: with the PIC, Abels's anti-locality leaves the complement of a phase head no way out.
{hd : HeadFunction} {t : LinearizedSyntacticObject} {tok : LexicalItem.Token} {x : Core.Order.TreePath × Core.Order.TreePath} {h : Core.Order.TreePath} (hh : h ∈ (↑t).validPaths) (h0 : h ≠ ⊥) (hhead : IsHeadPosition t h) (hx : x ∈ links hd t tok) (hr : projectionAt hd t x.2 = complement h) (hin : ¬complement h ≤ x.1.parent) :
CompToSpec hd t x ∨ x.2 ∈ sealed {h} (complementDomain hd t ∅) (Pic1 hd t) x.1.parent
Built from ,