Documentation

Studies.DeHaan2013

de Haan (2013): Semantic Distinctions of Evidentiality #

This file formalizes de Haan's WALS map of the semantic distinctions of evidentiality, which codes a language as having no grammatical evidentials, indirect evidentials only, or direct and indirect ones. A direct evidential marks sensory evidence, an indirect one inference or report. Only grammaticalized evidentials count, modal verbs, auxiliaries and particles among them, and no language in the sample has direct evidentials without indirect ones.

The value of an inventory is read off what its evidentials cover (value?), and an inventory of direct evidentials alone has none. On the Fragment languages the map never records fewer distinctions than the inventory (exists_mem_lookup_walsCode). Where the two differ, the inventory has no evidentials, or no direct one, because the Fragments follow Aikhenvald, who counts modal and mood forms and the Georgian perfect as evidentiality strategies and reads the Turkish and Bulgarian unmarked pasts as evidentiality-neutral. Taking the Turkish witnessed past as a direct evidential, as the chapter glosses it, gives the map's value and turns Aikhenvald's A2 system into an A1 (turkish_di). An inventory realizing one of Aikhenvald's kinds is off the map exactly when the kind is A5, auditory against everything else (value?_eq_none_iff); its one language, Euchee, is on the map without evidentials, coded after Wagner's grammar, which takes the auditory -ke for a locative (euchee).

Implementation notes #

The map codes Georgian with direct and indirect evidentials, although the companion chapter on coding says that the Georgian aorist, unlike the perfect, has not been formalized as a direct evidential. Kashaya is placed on the map by the paradigm of a spontaneous remark.

References #

The map's values #

source
def DeHaan2013.ofCovers (cs : List (Finset Evidential.Parameter)) :
Option Data.WALS.F77A.EvidentialityDistinctions

The value on the map of the coverages of a language's evidentials. Some indirect evidential covers inference or report, a parameter outside attested evidence, and a direct one covers attested evidence alone; coverages that are all direct have no value.

Equations
  • One or more equations did not get rendered due to their size.
Instances For
    source
    def DeHaan2013.value? (es : List Evidential) :
    Option Data.WALS.F77A.EvidentialityDistinctions

    The value of an inventory on the map.

    Equations
    Instances For
      source
      theorem DeHaan2013.ofCovers_perm {cs cs' : List (Finset Evidential.Parameter)} (h : cs.Perm cs') :
      ofCovers cs = ofCovers cs'
      source
      theorem DeHaan2013.ofCovers_rows_eq_none_iff (k : Aikhenvald2004.Kind) (r : List (Aikhenvald2004.Term × Finset Evidential.Parameter)) :
      r ∈ k.rows → (ofCovers (List.map Prod.snd r) = none ↔ k = Aikhenvald2004.Kind.A5)

      Among Aikhenvald's kinds of system, A5 alone has direct terms only.

      source
      theorem DeHaan2013.value?_eq_none_iff {es : List Evidential} {k : Aikhenvald2004.Kind} (h : Aikhenvald2004.Realizes es k) :
      value? es = none ↔ k = Aikhenvald2004.Kind.A5

      An inventory realizing one of Aikhenvald's kinds is off the map exactly when the kind is A5, auditory against everything else.

      The Fragment languages #

      source
      inductive DeHaan2013.Language :
      Type

      The Fragment languages on the map.

      Instances For
        source
        @[instance_reducible]
        instance DeHaan2013.instDecidableEqLanguage :
        DecidableEq Language
        Equations
        source
        @[instance_reducible]
        instance DeHaan2013.instReprLanguage :
        Repr Language
        Equations
        source
        def DeHaan2013.instReprLanguage.repr :
        Language → ℕ → Std.Format
        Equations
        Instances For
          source
          @[instance_reducible]
          instance DeHaan2013.instFintypeLanguage :
          Fintype Language
          Equations
          source
          def DeHaan2013.Language.walsCode :
          Language → String

          The WALS code of a language.

          Equations
          Instances For
            source
            def DeHaan2013.Language.evidentials :
            Language → List Evidential

            A language's evidentials, from its Fragment; for Kashaya, those of a spontaneous remark.

            Equations
            Instances For
              source
              theorem DeHaan2013.value?_isSome (l : Language) :
              (value? l.evidentials).isSome = true

              No Fragment language has direct evidentials without indirect ones, as no language of the chapter's sample does.

              source
              theorem DeHaan2013.exists_mem_lookup_walsCode (l : Language) :
              ∃ v ∈ List.lookup l.walsCode Data.WALS.F77A.allData, value? l.evidentials = some v ∨ l.evidentials = [] ∧ v ≠ Data.WALS.F77A.EvidentialityDistinctions.noGrammaticalEvidentials ∨ value? l.evidentials = some Data.WALS.F77A.EvidentialityDistinctions.indirectOnly ∧ v = Data.WALS.F77A.EvidentialityDistinctions.directAndIndirect

              The map has a value for every Fragment language, which is the inventory's value unless the Fragment has no evidentials where the map has some, or no direct evidential where the map has one.

              source
              theorem DeHaan2013.westGreenlandic :
              value? WestGreenlandic.Evidentiality.evidentials = List.lookup "grw" Data.WALS.F77A.allData

              West Greenlandic's reported evidentials give it the map's value.

              source
              def DeHaan2013.di :
              Evidential

              The Turkish witnessed past -dI, which the chapter glosses as a direct evidential and Aikhenvald reads as evidentiality-neutral, taken as a firsthand term for what the speaker saw.

              Equations
              Instances For
                source
                theorem DeHaan2013.turkish_di :
                value? (di :: Turkish.Evidentiality.evidentials) = List.lookup "tur" Data.WALS.F77A.allData ∧ Aikhenvald2004.Realizes (di :: Turkish.Evidentiality.evidentials) Aikhenvald2004.Kind.A1

                With the witnessed past as a direct evidential, Turkish takes the map's value, and its system is Aikhenvald's A1 rather than the A2 she gives it.

                source
                theorem DeHaan2013.euchee :
                value? [Aikhenvald2004.eucheeKe] = none ∧ List.lookup "yuc" Data.WALS.F77A.allData = some Data.WALS.F77A.EvidentialityDistinctions.noGrammaticalEvidentials

                Euchee's auditory evidential, an A5 system, is off the map, which codes the language as having no evidentials after Wagner's grammar.