Extraction Morphology

[ETB26] [Erl18] [Erl16]

Theory-neutral substrate for cross-linguistic extraction morphology — how languages morphologically mark that a constituent has undergone A-bar-movement (wh-movement, relativization, focus fronting, etc.). Bare-root Extraction namespace in Syntax/ (graduated from the dissolving Typology/). Per-language data are bare defs in Fragments/<Lang>/….

Languages vary dramatically in whether and how they track extraction:

• English: no overt marking (gap strategy)
• Austronesian (Tagalog, Malagasy): voice alternation marks which argument has been extracted
• Mayan (Mam, K'iche'): dedicated morphemes on verbal complex (Mam =(y)a', K'iche' wi)
• Celtic (Irish): complementizer changes form (aL vs. aN)
• Chamorro: agreement morphology tracks extracted position

inductive Extraction.ExtractionMarkingStrategy : Type

How a language morphologically marks extraction (A-bar-movement).

This is a descriptive typology of the surface strategy; different syntactic theories will derive these differently.

• unmarked : ExtractionMarkingStrategy

  No overt morphology marks extraction. The extracted position is a silent gap. E.g., English "What did you buy __?". (Renamed from none to avoid shadowing Option.none.)

• voiceAlternation : ExtractionMarkingStrategy

  Voice alternation: verbal voice morphology changes to mark which argument has been extracted. E.g., Tagalog Actor/Patient/Locative voice; Toba Batak Actor/Object voice.

• dedicatedMorpheme : ExtractionMarkingStrategy

  A dedicated morpheme appears on the verbal complex when extraction occurs. E.g., Mam =(y)a' on Voice0/Dir0, K'iche' wi, Kaqchikel AF -ö or -n, Irish complementizer aL.

• agreementTracking : ExtractionMarkingStrategy

  Agreement morphology on the verb tracks the extracted position. E.g., Chamorro wh-agreement.

• complementizerChange : ExtractionMarkingStrategy

  The complementizer changes form depending on whether extraction has occurred through its clause. E.g., Irish aL (direct) vs. aN (indirect).

@[instance_reducible]

instance Extraction.instDecidableEqExtractionMarkingStrategy : DecidableEq ExtractionMarkingStrategy

Equations

• Extraction.instDecidableEqExtractionMarkingStrategy x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

@[instance_reducible]

instance Extraction.instReprExtractionMarkingStrategy : Repr ExtractionMarkingStrategy

Equations

• Extraction.instReprExtractionMarkingStrategy = { reprPrec := Extraction.instReprExtractionMarkingStrategy.repr }

def Extraction.instReprExtractionMarkingStrategy.repr : ExtractionMarkingStrategy → ℕ → Std.Format

Equations

• One or more equations did not get rendered due to their size.

The 5 cases above are descriptive surface-typology categories. The analytical claims that competing accounts give for why a language has the surface pattern it does — e.g., Erlewine [erlewine-2016] [erlewine-2018] on Kaqchikel/Mayan AF as Spec-to-Spec Anti-Locality repair; Erlewine 2018 on Toba Batak extraction as a structural pivot restriction; Aldridge, Coon, Coon & Mateo Pedro & Preminger, Coon & Keine, Henderson, etc. with rival analyses — live in Studies/ files anchored on the specific paper. They are not enum cases here.

inductive Extraction.ExtractionTarget : Type

The grammatical position from which extraction occurs.

This intersects with the [KC77] Accessibility Hierarchy (see Typology/RelativeClause/Basic.lean), but is defined independently because extraction morphology may make finer distinctions than relativization.

• subject : ExtractionTarget

  Subject (ergative/nominative) extraction

• directObject : ExtractionTarget

  Direct object (accusative/absolutive) extraction

• indirectObject : ExtractionTarget

  Indirect object (dative/applicative) extraction

• oblique : ExtractionTarget

  Oblique (instrumental, locative, etc.) extraction

• possessor : ExtractionTarget

  Possessor extraction

@[instance_reducible]

instance Extraction.instDecidableEqExtractionTarget : DecidableEq ExtractionTarget

Equations

• Extraction.instDecidableEqExtractionTarget x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

def Extraction.instReprExtractionTarget.repr : ExtractionTarget → ℕ → Std.Format

Equations

• One or more equations did not get rendered due to their size.

@[instance_reducible]

instance Extraction.instReprExtractionTarget : Repr ExtractionTarget

Equations

• Extraction.instReprExtractionTarget = { reprPrec := Extraction.instReprExtractionTarget.repr }

inductive Extraction.Extractee : Type

What is being extracted: a DP argument, identified by its ThetaRole label (it needs Case licensing), or a non-DP adjunct (no thematic role, Case-exempt).

This distinction drives the DP/non-DP extraction asymmetry: in predicate-fronting languages like Toba Batak, only DP extraction is restricted to the pivot; adjuncts extract freely.

• dpArg : ThetaRole → Extractee
• adjunct : Extractee

@[instance_reducible]

instance Extraction.instDecidableEqExtractee : DecidableEq Extractee

Equations

• Extraction.instDecidableEqExtractee = Extraction.instDecidableEqExtractee.decEq

def Extraction.instDecidableEqExtractee.decEq (x✝ x✝¹ : Extractee) : Decidable (x✝ = x✝¹)

Equations

• Extraction.instDecidableEqExtractee.decEq (Extraction.Extractee.dpArg a) (Extraction.Extractee.dpArg b) = if h : a = b then h ▸ isTrue ⋯ else isFalse ⋯
• Extraction.instDecidableEqExtractee.decEq (Extraction.Extractee.dpArg a) Extraction.Extractee.adjunct = isFalse ⋯
• Extraction.instDecidableEqExtractee.decEq Extraction.Extractee.adjunct (Extraction.Extractee.dpArg a) = isFalse ⋯
• Extraction.instDecidableEqExtractee.decEq Extraction.Extractee.adjunct Extraction.Extractee.adjunct = isTrue ⋯

@[instance_reducible]

instance Extraction.instReprExtractee : Repr Extractee

Equations

• Extraction.instReprExtractee = { reprPrec := Extraction.instReprExtractee.repr }

def Extraction.instReprExtractee.repr : Extractee → ℕ → Std.Format

Equations

• One or more equations did not get rendered due to their size.

Extraction marking as morphological reflexes

A language's extraction marking is the overt morphosyntactic response to extraction from each target position, as Features.Reflex lists — the movement itself is not a reflex ([branan-erlewine-2023]). Per-language data are a nested Lang.Extraction namespace with a host type Site and

realize : ExtractionTarget → List (Features.Reflex Site)

(Site := Empty for languages that mark nothing). Languages with several markers place them at their cells — K'iche' AF at .subject and wi at .oblique are different cells of one function, not competing profiles. Marker-specific claims are reflex-membership statements. A coarse strategy : ExtractionMarkingStrategy label may accompany the data as WALS-style typology. Per-language Lang.Extraction namespaces must not redeclare root Extraction leaf names, so unqualified references keep resolving.

def Extraction.Marked {C : Type u_1} (realize : ExtractionTarget → List (Features.Reflex C)) (t : ExtractionTarget) : Prop

Does the language overtly mark extraction from a given target? The shared overtness predicate of Features/Reflex.lean.

Equations

• Extraction.Marked realize t = Features.Reflex.Overt (realize t)

@[instance_reducible]

instance Extraction.instDecidableMarked {C : Type u_1} (realize : ExtractionTarget → List (Features.Reflex C)) (t : ExtractionTarget) : Decidable (Marked realize t)

Equations

• Extraction.instDecidableMarked realize t = Extraction.instDecidableMarked._aux_1 realize t