Documentation

Linglib.Syntax.Adposition.Order

Adposition typology: shared substrate type #

[Dry13] [Gre63] [Dry92]

Framework-agnostic enum for storing per-language adposition order (WALS Ch 85). The adposition-order facet of the bare-root Adposition namespace (sibling of Syntax/Adposition/Basic.lean's PP structure); both Fragments/ (per-language profiles) and Studies/ (cross-linguistic generalisations) import it.

Sister substrate to WordOrder — same shape (enum with WALS-attested cases plus epistemic-distinction cases, namespaced AdpositionOrder.ofWALS{85A,} converters, classification predicates, head-direction projection).

Epistemic distinction: noDominant vs notInWALS #

AdpositionOrder.noDominant is the WALS-attested mixed-system code (language has both pre- and postpositions, neither dominates — itself a finding). AdpositionOrder.notInWALS is absence from Ch 85 — the language was not coded. A consumer that filtered on ≠ .noDominant would otherwise silently include unencoded languages as "genuinely nondominant". The two cases are kept distinct, mirroring WordOrder's post-refactor design.

noAdpositions as a category #

WALS codes ~30 languages as .noAdpositions (case-marking alone, no adposition morphology). This is distinct from noDominant (language has both) and from notInWALS (uncoded). All three are framework- neutral.

Greenbergian vs Dryerian primacy #

The substrate is neutral on which classification is theoretically primary. [Gre63]'s Universals 3 and 4 treat adposition as the correlate of basic constituent order (VSO → Prep, SOV → Postp). [Dry92] explicitly demoted SOV/SVO/VSO in favour of OV/VO + correlation pairs (Branching Direction Theory), making adposition a co-primary head-direction phenomenon. Consumers downstream choose which projection to read; the substrate provides both IsPrepositional/IsPostpositional (Greenberg-style predicates) and headDirection (Dryer-style projection).

source
inductive Adposition.AdpositionOrder :
Type

WALS Ch 85 plus the absence-from-WALS case.

  • prepositional : AdpositionOrder

    Adposition precedes complement NP (head-initial PP).

  • postpositional : AdpositionOrder

    Adposition follows complement NP (head-final PP).

  • inpositional : AdpositionOrder

    Adposition appears medially in a complex NP (rare; WALS lists ~8 Australian Aboriginal + Cariban + PNG languages).

  • noAdpositions : AdpositionOrder

    Language has no adpositions (case-marking alone; ~30 WALS languages). Distinct from notInWALS.

  • noDominant : AdpositionOrder

    WALS-attested mixed system (both pre- and postpositions, neither dominates).

  • notInWALS : AdpositionOrder

    Language not coded in WALS Ch 85 (no information). Distinct from noAdpositions (which is a substantive WALS finding).

Instances For
    source
    @[implicit_reducible]
    instance Adposition.instDecidableEqAdpositionOrder :
    DecidableEq AdpositionOrder
    Equations
    source
    def Adposition.instReprAdpositionOrder.repr :
    AdpositionOrder → ℕ → Std.Format
    Equations
    • One or more equations did not get rendered due to their size.
    Instances For
      source
      @[implicit_reducible]
      instance Adposition.instReprAdpositionOrder :
      Repr AdpositionOrder
      Equations
      source
      def Adposition.AdpositionOrder.ofWALS85A :
      Data.WALS.F85A.AdpositionNPOrder → AdpositionOrder

      Convert WALS F85A's AdpositionNPOrder to a local AdpositionOrder.

      Equations
      Instances For
        source
        def Adposition.AdpositionOrder.ofWALS (iso : String) :
        AdpositionOrder

        Look up Ch 85 adposition order for an ISO 639-3 code. Returns .notInWALS when the language is absent from the chapter.

        Equations
        • One or more equations did not get rendered due to their size.
        Instances For
          source
          @[reducible, inline]
          abbrev Adposition.AdpositionOrder.IsPrepositional (a : AdpositionOrder) :
          Prop

          a is prepositional.

          Equations
          Instances For
            source
            @[reducible, inline]
            abbrev Adposition.AdpositionOrder.IsPostpositional (a : AdpositionOrder) :
            Prop

            a is postpositional.

            Equations
            Instances For
              source
              def Adposition.AdpositionOrder.headDirection :
              AdpositionOrder → Option HeadDirection

              Project an AdpositionOrder to a HeadDirection. Theory-neutral: prepositional ⇒ head-initial PP, postpositional ⇒ head-final PP. Returns none for the categories that do not commit to a single direction (.inpositional, .noAdpositions, .noDominant, .notInWALS). Sister of OVOrder.verbPosition; consumers needing BDT-style head-direction unification can iterate over both projections.

              Equations
              Instances For