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 -Vn, 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).

@[implicit_reducible]

instance Extraction.instDecidableEqExtractionMarkingStrategy : DecidableEq ExtractionMarkingStrategy

Equations

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

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

Equations

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

@[implicit_reducible]

instance Extraction.instReprExtractionMarkingStrategy : Repr ExtractionMarkingStrategy

Equations

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

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

@[implicit_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 → Nat → Std.Format

Equations

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

@[implicit_reducible]

instance Extraction.instReprExtractionTarget : Repr ExtractionTarget

Equations

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

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

@[implicit_reducible]

instance Extraction.instDecidableEqArgumentRole : DecidableEq ArgumentRole

Equations

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

@[implicit_reducible]

instance Extraction.instReprArgumentRole : Repr ArgumentRole

Equations

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

def Extraction.instReprArgumentRole.repr : ArgumentRole → Nat → 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 ⋯

@[implicit_reducible]

instance Extraction.instDecidableEqExtractee : DecidableEq Extractee

Equations

• Extraction.instDecidableEqExtractee = Extraction.instDecidableEqExtractee.decEq

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

Equations

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

@[implicit_reducible]

instance Extraction.instReprExtractee : Repr Extractee

Equations

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

Extraction-profile queries

The ExtractionProfile bundle is retired: a language exposes its extraction data as bare defs (…Strategy : ExtractionMarkingStrategy, …MarkedPositions : List ExtractionTarget, …DistinguishesPosition : Bool), and these queries operate on the marked-positions list / strategy.

def Extraction.Marks (markedPositions : List ExtractionTarget) (t : ExtractionTarget) : Prop

Does a marked-positions list mark extraction from a given target?

Equations

• Extraction.Marks markedPositions t = (t ∈ markedPositions)

@[implicit_reducible]

instance Extraction.instDecidableMarks (mp : List ExtractionTarget) (t : ExtractionTarget) : Decidable (Marks mp t)

Equations

• Extraction.instDecidableMarks mp t = Extraction.instDecidableMarks._aux_1 mp t

def Extraction.HasOvertMarking (strategy : ExtractionMarkingStrategy) : Prop

Does an extraction-marking strategy use any overt marking?

Equations

• Extraction.HasOvertMarking strategy = (strategy ≠ Extraction.ExtractionMarkingStrategy.unmarked)

@[implicit_reducible]

instance Extraction.instDecidableHasOvertMarking (s : ExtractionMarkingStrategy) : Decidable (HasOvertMarking s)

Equations

• Extraction.instDecidableHasOvertMarking s = Extraction.instDecidableHasOvertMarking._aux_1 s