Documentation

Linglib.Core.Relativization.Hierarchy

Accessibility Hierarchy: Ordering and Contiguity #

@cite{keenan-comrie-1977}

Defines the rank function and contiguity predicate for the Accessibility Hierarchy. Mirrors Core.Case.Hierarchy for Blake's case hierarchy.

source
def Core.AHPosition.rank :
AHPosition → Nat

Numeric rank of a position on the Accessibility Hierarchy. Higher rank = more accessible = more languages can relativize it.

Equations
Instances For
    source
    def Core.AHPosition.atLeastAsAccessible (p1 p2 : AHPosition) :
    Bool

    Position p1 is at least as accessible as p2 on the hierarchy.

    Equations
    Instances For
      source
      def Core.AHPosition.moreAccessible (p1 p2 : AHPosition) :
      Bool

      Position p1 is strictly more accessible than p2.

      Equations
      Instances For
        source
        def Core.AHPosition.all :
        List AHPosition

        All AH positions in descending order of accessibility.

        Equations
        Instances For
          source
          def Core.contiguousOnAH (positions : List AHPosition) :
          Bool

          A set of AH positions forms a contiguous segment on the hierarchy: for every pair of positions in the set, all intermediate ranks are also represented.

          Mirrors Core.validInventory for the case hierarchy (@cite{blake-1994}).

          This formalizes HC₂ of @cite{keenan-comrie-1977}: "Any RC-forming strategy must apply to a continuous segment of the AH."

          Equations
          • One or more equations did not get rendered due to their size.
          Instances For
            source
            def Core.RelClauseMarker.isContinuous (m : RelClauseMarker) :
            Bool

            A marker's positions form a contiguous segment of the AH.

            Equations
            Instances For
              source
              theorem Core.ah_strictly_ordered :
              AHPosition.subject.moreAccessible AHPosition.directObject = true ∧ AHPosition.directObject.moreAccessible AHPosition.indirectObject = true ∧ AHPosition.indirectObject.moreAccessible AHPosition.oblique = true ∧ AHPosition.oblique.moreAccessible AHPosition.genitive = true ∧ AHPosition.genitive.moreAccessible AHPosition.objComparison = true

              The hierarchy is strictly ordered: each position is more accessible than the one below it.

              source
              theorem Core.subject_most_accessible :
              AHPosition.subject.rank = 6

              Subject is the most accessible position (rank 6).

              source
              theorem Core.objComparison_least_accessible :
              AHPosition.objComparison.rank = 1

              Object of comparison is the least accessible position (rank 1).

              source
              theorem Core.ah_reflexive :
              (AHPosition.all.all fun (p : AHPosition) => p.atLeastAsAccessible p) = true

              Accessibility is reflexive.

              source
              theorem Core.ah_transitive :
              (AHPosition.all.all fun (p1 : AHPosition) => AHPosition.all.all fun (p2 : AHPosition) => AHPosition.all.all fun (p3 : AHPosition) => if (p1.atLeastAsAccessible p2 && p2.atLeastAsAccessible p3) = true then p1.atLeastAsAccessible p3 else true) = true

              Accessibility is transitive.

              source
              theorem Core.full_ah_contiguous :
              contiguousOnAH AHPosition.all = true

              The full hierarchy [SU, DO, IO, OBL, GEN, OCOMP] is contiguous.

              source
              theorem Core.singleton_contiguous :
              contiguousOnAH [AHPosition.subject] = true

              A single position is trivially contiguous.

              source
              theorem Core.su_do_contiguous :
              contiguousOnAH [AHPosition.subject, AHPosition.directObject] = true

              [SU, DO] is contiguous.

              source
              theorem Core.io_obl_gen_contiguous :
              contiguousOnAH [AHPosition.indirectObject, AHPosition.oblique, AHPosition.genitive] = true

              [IO, OBL, GEN] is contiguous (a non-primary segment).

              source
              theorem Core.su_do_obl_not_contiguous :
              contiguousOnAH [AHPosition.subject, AHPosition.directObject, AHPosition.oblique] = false

              [SU, DO, OBL] is NOT contiguous (skips IO at rank 4).

              source
              theorem Core.prc_from_hc2 (positions : List AHPosition) (h_contig : contiguousOnAH positions = true) (h_su : (positions.any fun (x : AHPosition) => x == AHPosition.subject) = true) (p above : AHPosition) (hp : (positions.any fun (x : AHPosition) => x == p) = true) (habove : above.rank > p.rank) :
              (positions.any fun (x : AHPosition) => x == above) = true

              Primary Relativization Constraint (general proof).

              If a list of AH positions is contiguous (HC₂) and contains .subject (i.e., the strategy is primary), then the list is upward-closed: for any covered position p, all positions above p on the AH are also covered.

              This proves that the PRC is a logical consequence of HC₂ + being primary, not an independent constraint — the paper's core derivation.

              source
              theorem Core.prc_all_primary_segments :
              have segs := [[AHPosition.subject], [AHPosition.subject, AHPosition.directObject], [AHPosition.subject, AHPosition.directObject, AHPosition.indirectObject], [AHPosition.subject, AHPosition.directObject, AHPosition.indirectObject, AHPosition.oblique], [AHPosition.subject, AHPosition.directObject, AHPosition.indirectObject, AHPosition.oblique, AHPosition.genitive], [AHPosition.subject, AHPosition.directObject, AHPosition.indirectObject, AHPosition.oblique, AHPosition.genitive, AHPosition.objComparison]]; (segs.all fun (seg : List AHPosition) => (contiguousOnAH seg && seg.any fun (x : AHPosition) => x == AHPosition.subject) && seg.all fun (p : AHPosition) => AHPosition.all.all fun (above : AHPosition) => if above.rank > p.rank then seg.any fun (x : AHPosition) => x == above else true) = true

              All 6 canonical primary strategy segments are upward-closed. These are the only possible contiguous segments containing .subject.