Extraction Morphology Interface

@cite{elkins-torrence-brown-2026} @cite{erlewine-2018} @cite{mccloskey-2002} @cite{erlewine-2016}

Theory-neutral interface for cross-linguistic extraction morphology — how languages morphologically mark that a constituent has undergone Ā-movement (wh-movement, relativization, focus fronting, etc.).

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

This interface parametrizes these strategies without committing to a particular syntactic theory of how extraction works.

inductive Interfaces.ExtractionMarkingStrategy : Type

How a language morphologically marks extraction (Ā-movement).

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

• none : ExtractionMarkingStrategy

  No overt marking of extraction. The extracted position is a silent gap. E.g., English "What did you buy __?"

• voiceAlternation : ExtractionMarkingStrategy

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

• dedicatedMorpheme : ExtractionMarkingStrategy

  A dedicated morpheme appears on the verbal complex when extraction occurs. E.g., Mam =(y)a' on Voice⁰/Dir⁰, K'iche' wi, 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).

• structuralRestriction : ExtractionMarkingStrategy

  Extraction is structurally restricted to a designated position (the "pivot"), not by surface morphology but by clause-structural factors such as predicate fronting + anti-locality. Voice morphology determines which argument occupies the pivot, but the restriction itself is structural. E.g., Toba Batak.

• agentFocusAlternation : ExtractionMarkingStrategy

  Clause-local extraction of a specific argument role (typically agent/ergative) triggers an alternation in clause structure — a "repair" that avoids a locality crash. The canonical case is Kaqchikel Agent Focus: clause-local agent extraction crashes the normal transitive because movement from Spec,TP to Spec,CP violates Spec-to-Spec Anti-Locality (SSAL), so the grammar selects an intransitive-like AF structure with distinct verbal morphology (-Vn, no Set A). Long-distance agent extraction does NOT trigger AF — the repair is locality-sensitive.

instance Interfaces.instDecidableEqExtractionMarkingStrategy : DecidableEq ExtractionMarkingStrategy

Equations

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

def Interfaces.instBEqExtractionMarkingStrategy.beq : ExtractionMarkingStrategy → ExtractionMarkingStrategy → Bool

Equations

• Interfaces.instBEqExtractionMarkingStrategy.beq x✝ y✝ = (x✝.ctorIdx == y✝.ctorIdx)

instance Interfaces.instBEqExtractionMarkingStrategy : BEq ExtractionMarkingStrategy

Equations

• Interfaces.instBEqExtractionMarkingStrategy = { beq := Interfaces.instBEqExtractionMarkingStrategy.beq }

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

Equations

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

instance Interfaces.instReprExtractionMarkingStrategy : Repr ExtractionMarkingStrategy

Equations

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

inductive Interfaces.ExtractionTarget : Type

The grammatical position from which extraction occurs.

This intersects with the @cite{keenan-comrie-1977} Accessibility Hierarchy (see FillerGap/Typology.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 Interfaces.instDecidableEqExtractionTarget : DecidableEq ExtractionTarget

Equations

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

def Interfaces.instBEqExtractionTarget.beq : ExtractionTarget → ExtractionTarget → Bool

Equations

• Interfaces.instBEqExtractionTarget.beq x✝ y✝ = (x✝.ctorIdx == y✝.ctorIdx)

instance Interfaces.instBEqExtractionTarget : BEq ExtractionTarget

Equations

• Interfaces.instBEqExtractionTarget = { beq := Interfaces.instBEqExtractionTarget.beq }

instance Interfaces.instReprExtractionTarget : Repr ExtractionTarget

Equations

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

def Interfaces.instReprExtractionTarget.repr : ExtractionTarget → Nat → Std.Format

Equations

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

inductive Interfaces.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 Interfaces.instDecidableEqArgumentRole : DecidableEq ArgumentRole

Equations

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

instance Interfaces.instBEqArgumentRole : BEq ArgumentRole

Equations

• Interfaces.instBEqArgumentRole = { beq := Interfaces.instBEqArgumentRole.beq }

def Interfaces.instBEqArgumentRole.beq : ArgumentRole → ArgumentRole → Bool

Equations

• Interfaces.instBEqArgumentRole.beq x✝ y✝ = (x✝.ctorIdx == y✝.ctorIdx)

def Interfaces.instReprArgumentRole.repr : ArgumentRole → Nat → Std.Format

Equations

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

instance Interfaces.instReprArgumentRole : Repr ArgumentRole

Equations

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

def Interfaces.ArgumentRole.defaultPosition : ArgumentRole → ExtractionTarget

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

Equations

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

inductive Interfaces.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 Interfaces.instDecidableEqExtractee.decEq (x✝ x✝¹ : Extractee) : Decidable (x✝ = x✝¹)

Equations

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

instance Interfaces.instDecidableEqExtractee : DecidableEq Extractee

Equations

• Interfaces.instDecidableEqExtractee = Interfaces.instDecidableEqExtractee.decEq

def Interfaces.instBEqExtractee.beq : Extractee → Extractee → Bool

Equations

• Interfaces.instBEqExtractee.beq (Interfaces.Extractee.dpArg a) (Interfaces.Extractee.dpArg b) = (a == b)
• Interfaces.instBEqExtractee.beq Interfaces.Extractee.adjunct Interfaces.Extractee.adjunct = true
• Interfaces.instBEqExtractee.beq x✝¹ x✝ = false

instance Interfaces.instBEqExtractee : BEq Extractee

Equations

• Interfaces.instBEqExtractee = { beq := Interfaces.instBEqExtractee.beq }

instance Interfaces.instReprExtractee : Repr Extractee

Equations

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

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

Equations

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

structure Interfaces.ExtractionProfile : Type

A language's extraction morphology profile: what strategy it uses, which positions are marked, and whether the marking distinguishes between different extracted positions.

Follows the RelativizationProfile pattern from FillerGap/Typology.lean.

• language : String

  Language name

• strategy : ExtractionMarkingStrategy

  Primary extraction-marking strategy

• markedPositions : List ExtractionTarget

  Which extraction targets trigger overt marking. Empty for none strategy languages.

• distinguishesPosition : Bool

  Does the marking distinguish which position was extracted? E.g., Tagalog voice distinguishes subject/object/oblique; Mam =(y)a' marks only oblique.

• notes : String

  Notes

def Interfaces.instReprExtractionProfile.repr : ExtractionProfile → Nat → Std.Format

Equations

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

instance Interfaces.instReprExtractionProfile : Repr ExtractionProfile

Equations

• Interfaces.instReprExtractionProfile = { reprPrec := Interfaces.instReprExtractionProfile.repr }

def Interfaces.ExtractionProfile.marks (p : ExtractionProfile) (t : ExtractionTarget) : Bool

Does this profile mark extraction from a given position?

Equations

• p.marks t = p.markedPositions.any fun (x : Interfaces.ExtractionTarget) => x == t

def Interfaces.ExtractionProfile.hasOvertMarking (p : ExtractionProfile) : Bool

Does this profile use any overt extraction marking?

Equations

• p.hasOvertMarking = (p.strategy != Interfaces.ExtractionMarkingStrategy.none)