Documentation

Linglib.Core.Relativization.Extraction

Bridge: Extraction Morphology ↔ Accessibility Hierarchy #

@cite{keenan-comrie-1977}

Maps between ExtractionTarget (5 structural positions from extraction morphology) and AHPosition (6 positions on the Accessibility Hierarchy).

The two type systems encode overlapping Ā-movement phenomena:

The bridge is partial: AHPosition.objComparison has no standard ExtractionTarget equivalent (object of comparison is a position specific to the relativization literature). In the other direction, possessor maps to genitive.

source
def Core.extractionTargetToAH :
Interfaces.ExtractionTarget → AHPosition

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

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

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

    Equations
    Instances For
      source
      theorem Core.extraction_ah_roundtrip :
      have targets := [Interfaces.ExtractionTarget.subject, Interfaces.ExtractionTarget.directObject, Interfaces.ExtractionTarget.indirectObject, Interfaces.ExtractionTarget.oblique, Interfaces.ExtractionTarget.possessor]; (targets.all fun (t : Interfaces.ExtractionTarget) => ahToExtractionTarget (extractionTargetToAH t) == some t) = true

      Round-tripping ExtractionTarget → AH → ExtractionTarget is the identity for all 5 extraction targets.

      source
      theorem Core.ah_extraction_roundtrip :
      have positions := [AHPosition.subject, AHPosition.directObject, AHPosition.indirectObject, AHPosition.oblique, AHPosition.genitive]; (positions.all fun (p : AHPosition) => match ahToExtractionTarget p with | some t => extractionTargetToAH t == p | none => false) = true

      Round-tripping AH → ExtractionTarget → AH is the identity for all positions except .objComparison (which has no ExtractionTarget).

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

      .objComparison is the only AH position without an ExtractionTarget.

      source
      theorem Core.non_ocomp_have_extraction_target :
      have positions := [AHPosition.subject, AHPosition.directObject, AHPosition.indirectObject, AHPosition.oblique, AHPosition.genitive]; (positions.all fun (p : AHPosition) => (ahToExtractionTarget p).isSome) = true

      All other AH positions have ExtractionTarget equivalents.