Documentation

Linglib.Typology.Relativization.ExtractionBridge

Extraction Morphology ↔ Accessibility Hierarchy Bridge #

@cite{keenan-comrie-1977}

Maps between Typology.ExtractionTarget (5 structural positions from extraction morphology, defined in Typology/Extraction.lean) and Core.AHPosition (6 positions on the @cite{keenan-comrie-1977} Accessibility Hierarchy).

Both type systems encode overlapping Ā-movement phenomena: extraction focuses on where extraction occurs (used by Mayan, Austronesian, Celtic Fragments); the AH focuses on what can be relativized (used by relativization Fragments and the Keenan-Comrie hierarchy constraints). The bridge is partial: AHPosition.objComparison (object of comparison, specific to the relativization literature) has no standard ExtractionTarget equivalent. In the other direction, ExtractionTarget.possessor maps to AHPosition.genitive.

source
def Typology.Relativization.extractionTargetToAH :
ExtractionTarget → Core.AHPosition

Map an extraction target to its AH position. Possessor extraction corresponds to the genitive position on the AH.

Equations
Instances For
    source
    def Typology.Relativization.ahToExtractionTarget :
    Core.AHPosition → Option ExtractionTarget

    Map an AH position to an extraction target (partial: objComparison has no standard ExtractionTarget equivalent).

    Equations
    Instances For
      source
      theorem Typology.Relativization.extraction_ah_roundtrip (t : ExtractionTarget) :
      ahToExtractionTarget (extractionTargetToAH t) = some t

      ExtractionTarget → AH → ExtractionTarget is the identity.

      source
      theorem Typology.Relativization.ah_extraction_roundtrip (p : Core.AHPosition) (h : p ≠ Core.AHPosition.objComparison) :
      ∃ (t : ExtractionTarget), ahToExtractionTarget p = some t ∧ extractionTargetToAH t = p

      AH → ExtractionTarget → AH is the identity for every position except objComparison (which has no ExtractionTarget).

      source
      theorem Typology.Relativization.objComparison_no_extraction_target :
      ahToExtractionTarget Core.AHPosition.objComparison = none

      objComparison is the only AH position without an ExtractionTarget.

      source
      theorem Typology.Relativization.non_ocomp_have_extraction_target (p : Core.AHPosition) (h : p ≠ Core.AHPosition.objComparison) :
      (ahToExtractionTarget p).isSome = true

      Every non-objComparison AH position has an ExtractionTarget equivalent.