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 ⋯

@[instance_reducible]

instance Extraction.instReprExtractionTarget : Repr ExtractionTarget

Equations

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

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

Equations

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

inductive Extraction.ArgumentRole : Type

The thematic category of an argument being extracted: agent (external argument), patient (internal argument), or oblique.

Coarser than ThetaRole (which distinguishes agent/experiencer/ causer, patient/theme, goal/source/instrument). Used when the relevant distinction is which macro-role is extracted, not fine- grained thematic relations or structural positions.

Complements ExtractionTarget (structural position): ArgumentRole identifies what is extracted; ExtractionTarget identifies where it was extracted. The two coincide in simple active clauses (agent = subject, patient = object) but diverge under voice alternation (in OV, the patient becomes the subject).

• agent : ArgumentRole
• patient : ArgumentRole
• oblique : ArgumentRole

@[instance_reducible]

instance Extraction.instDecidableEqArgumentRole : DecidableEq ArgumentRole

Equations

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

@[instance_reducible]

instance Extraction.instReprArgumentRole : Repr ArgumentRole

Equations

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

def Extraction.instReprArgumentRole.repr : ArgumentRole → ℕ → Std.Format

Equations

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

def Extraction.ArgumentRole.defaultPosition : ArgumentRole → ExtractionTarget

Default structural position for a given argument role (active voice).

Equations

• Extraction.ArgumentRole.agent.defaultPosition = Extraction.ExtractionTarget.subject
• Extraction.ArgumentRole.patient.defaultPosition = Extraction.ExtractionTarget.directObject
• Extraction.ArgumentRole.oblique.defaultPosition = Extraction.ExtractionTarget.oblique

inductive Extraction.Extractee : Type

What is being extracted: a DP argument (which has a thematic role and needs Case licensing) or a non-DP adjunct (which has no thematic role and is 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 : ArgumentRole → Extractee
• adjunct : Extractee

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.instDecidableEqExtractee : DecidableEq Extractee

Equations

• Extraction.instDecidableEqExtractee = Extraction.instDecidableEqExtractee.decEq

@[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 ([BE23]). 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