Documentation

Studies.Just2024

Just (2024): A structural and functional comparison of differential A and P indexing #

This file formalizes Just's claim that differential A indexing and differential P indexing, the variable occurrence of a verbal index for reasons other than the referent's argument role, are one phenomenon: a referent is indexed when it reaches a language-specific level of referential prominence in Haspelmath's sense, whatever its role. The two look like mirror images because the roles differ in default prominence: A referents are typically prominent, so a non-prominent or focused A loses an otherwise present index, while P referents typically are not, so a topical, definite, or animate P gains one. The principle is Indexed, prominence at or above the threshold, whose coding length is the cutoff split Haspelmath2021.atLeast, and deviation_coding derives the mirror image and its consequence for coding asymmetries: a referent that deviates from its role's default receives longer coding exactly when the default is unindexed, so Haspelmath's generalization that deviations from role-reference associations are coded by longer forms holds of differential P indexing and fails of differential A indexing, where the deviating configuration loses the index. The examples of the paper's survey are rows, and indexed_iff_prominent reads each as the paper does, the index present exactly where the referent has the prominence the language demands, for A and P alike.

Co-argument sensitivity is the paper's other case: in Reyesano which of A and P is indexed depends on the persons of both, its table being rows of Clause.Scenario Person, and no_ranking_fits shows that no ranking of the persons predicts the table by indexing the argument the scenario's kind under that ranking favours, as the paper argues after Witzlack-Makarevich and colleagues that hierarchies are not needed to describe such systems.

Implementation notes #

References #

Indexing and referential prominence #

source
def Just2024.Indexed {Prominence : Type u_1} [LinearOrder Prominence] (θ p : Prominence) :
Prop

By the principle, a referent is indexed when its prominence reaches the language's threshold.

Equations
Instances For
    source
    @[instance_reducible]
    instance Just2024.instDecidableIndexed {Prominence : Type u_1} [LinearOrder Prominence] (θ p : Prominence) :
    Decidable (Indexed θ p)
    Equations
    source
    def Just2024.Deviates {Prominence : Type u_1} [LinearOrder Prominence] (θ : Prominence) {ρ : Type u_2} (dflt : ρ → Prominence) (r : ρ) (p : Prominence) :
    Prop

    A referent deviates from its role when it lies on the other side of the threshold from the role's default prominence.

    Equations
    Instances For
      source
      @[instance_reducible]
      instance Just2024.instDecidableDeviates {Prominence : Type u_1} [LinearOrder Prominence] (θ : Prominence) {ρ : Type u_2} (dflt : ρ → Prominence) (r : ρ) (p : Prominence) :
      Decidable (Deviates θ dflt r p)
      Equations
      source
      theorem Just2024.deviation_coding {Prominence : Type u_1} [LinearOrder Prominence] (θ : Prominence) {ρ : Type u_2} (dflt : ρ → Prominence) {r : ρ} {p : Prominence} (h : Deviates θ dflt r p) :
      Haspelmath2021.atLeast θ (dflt r) < Haspelmath2021.atLeast θ p ↔ ¬Indexed θ (dflt r)

      The mirror image yields the coding asymmetry, a deviating referent being coded longer than its role's default exactly when the default is unindexed. Differential P indexing, with a default below the threshold, codes the deviation by adding an index; differential A indexing, with a default above it, codes the deviation by dropping one.

      source
      theorem Just2024.deviation_shorter {Prominence : Type u_1} [LinearOrder Prominence] (θ : Prominence) {ρ : Type u_2} (dflt : ρ → Prominence) {r : ρ} {p : Prominence} (h : Deviates θ dflt r p) (hr : Indexed θ (dflt r)) :
      Haspelmath2021.atLeast θ p < Haspelmath2021.atLeast θ (dflt r)

      The deviating referent of a role indexed by default is coded shorter.

      source
      def Just2024.transitiveDefault (r : ArgumentRole) :
      Bool

      The default prominence of the transitive roles puts A above the threshold and P below it, the role-reference associations of [Has21c].

      Equations
      Instances For
        source
        theorem Just2024.transitive_mirror :
        Haspelmath2021.atLeast true false < Haspelmath2021.atLeast true (transitiveDefault ArgumentRole.A) ∧ Haspelmath2021.atLeast true (transitiveDefault ArgumentRole.P) < Haspelmath2021.atLeast true true

        A non-prominent A and a prominent P both deviate from their defaults; the A is coded shorter than a default A and the P longer than a default P.

        The survey #

        source
        inductive Just2024.Condition :
        Type

        The condition under which the paper reports a referent indexed or not, the factor named for the example. focus is focus on the referent, otherFocus focus on another constituent of a language whose index requires predicate focus.

        Instances For
          source
          @[instance_reducible]
          instance Just2024.instDecidableEqCondition :
          DecidableEq Condition
          Equations
          source
          @[instance_reducible]
          instance Just2024.instReprCondition :
          Repr Condition
          Equations
          source
          def Just2024.instReprCondition.repr :
          Condition → ℕ → Std.Format
          Equations
          Instances For
            source
            def Just2024.Condition.Prominent :
            Condition → Prop

            Whether a condition puts the referent at the prominence the language demands. Topical, animate, definite, and pronominal referents do, and so does predicate focus, which leaves the arguments unfocused; a focused, inanimate, indefinite, or lexical referent falls short, as does an argument in a clause whose focus lies elsewhere than the predicate.

            Equations
            Instances For
              source
              @[instance_reducible]
              instance Just2024.instDecidablePredConditionProminent :
              DecidablePred Condition.Prominent
              Equations
              source
              def Just2024.datum (r : Datum) :
              Option (ArgumentRole × Bool × Condition)

              A grammatical row of the survey gives the role, whether it is indexed, and the paper's condition.

              Equations
              • One or more equations did not get rendered due to their size.
              Instances For
                source
                def Just2024.data :
                List (ArgumentRole × Bool × Condition)

                The examples of the survey for which the paper names the conditioning factor.

                Equations
                Instances For
                  source
                  theorem Just2024.indexed_iff_prominent (d : ArgumentRole × Bool × Condition) :
                  d ∈ data → (d.2.1 = true ↔ d.2.2.Prominent)

                  Across the survey the index is present exactly where the referent is prominent under the named condition, for A and for P.

                  source
                  theorem Just2024.both_roles_both_ways (role : ArgumentRole) :
                  role ∈ [ArgumentRole.A, ArgumentRole.P] → ∀ b ∈ [true, false], ∃ d ∈ data, d.1 = role ∧ d.2.1 = b

                  Both roles are attested in both directions, with an indexed and an unindexed A and an indexed and an unindexed P.

                  Co-argument sensitivity: Reyesano #

                  source
                  inductive Just2024.IndexedArgs :
                  Type

                  The arguments indexed in a scenario.

                  Instances For
                    source
                    @[instance_reducible]
                    instance Just2024.instDecidableEqIndexedArgs :
                    DecidableEq IndexedArgs
                    Equations
                    source
                    @[instance_reducible]
                    instance Just2024.instReprIndexedArgs :
                    Repr IndexedArgs
                    Equations
                    source
                    def Just2024.instReprIndexedArgs.repr :
                    IndexedArgs → ℕ → Std.Format
                    Equations
                    Instances For
                      source
                      def Just2024.scenario (r : Datum) :
                      Option (Clause.Scenario Person × IndexedArgs)

                      A scenario of the paper's table, the persons of A and P, with the arguments indexed.

                      Equations
                      • One or more equations did not get rendered due to their size.
                      Instances For
                        source
                        def Just2024.reyesano :
                        List (Clause.Scenario Person × IndexedArgs)

                        The Reyesano table.

                        Equations
                        Instances For
                          source
                          def Just2024.byRanking (rank : Person → Fin 3) (s : Clause.Scenario Person) :
                          IndexedArgs

                          Indexing by a ranking of persons indexes the higher-ranked argument, the A in a downstream scenario and the P in an upstream one, and both when balanced.

                          Equations
                          • One or more equations did not get rendered due to their size.
                          Instances For
                            source
                            theorem Just2024.coargument_sensitive :
                            ∃ s ∈ reyesano, ∃ s' ∈ reyesano, s.1.high = s'.1.high ∧ s.2 ≠ s'.2

                            Whether an A of a given person is indexed depends on the person of its co-argument.

                            source
                            theorem Just2024.no_ranking_fits :
                            ¬∃ (rank : Person → Fin 3), ∀ s ∈ reyesano, s.2 = byRanking rank s.1

                            No ranking of the tripartition predicts the table by indexing the higher-ranked argument, since a first-person A outranks a third-person P but a third-person A ties with a first-person P.