Documentation

Studies.MaslovaNedjalkov2013

Maslova and Nedjalkov (2013): Reciprocal Constructions #

[MN13] classify languages by the polysemy of their non-iconic reciprocal constructions (§2). A reciprocal construction either can also express the reflexive meaning or cannot, so a language has reflexive reciprocal constructions, non-reflexive ones, both (the mixed type), or no non-iconic reciprocal construction at all. This file computes that value from a marker inventory (ofInventory) and characterizes each value by the kinds of marker the inventory contains (ofInventory_eq_mixed_iff and its siblings). The chapter's own examples come out as it states, English with only non-reflexive reciprocals and German of the mixed type (ofInventory_english, ofInventory_german, §2.2), and every language of the chapter's sample whose reciprocal markers a fragment records has the value the chapter codes (ofInventory_eq_wals).

Implementation notes #

A marker's polysemy is its Reciprocal.Marker.readings; the value reads only whether each reciprocal marker also covers the reflexive reading. Mandarin, coded non-reflexive, is left out of Language: its fragment's one marker, the compound dǎ-lái-dǎ-qù, repeats its verb, the iconic encoding the chapter sets aside (§2.1).

TODO #

ofInventory reads every marker of an inventory, while the chapter counts only the non-iconic constructions; Reciprocal.Strategy would need to record iconicity for the value to be exact.

References #

Reflexive and non-reflexive reciprocals #

source
def MaslovaNedjalkov2013.IsReflexiveReciprocal (m : Reciprocal.Marker) :
Prop

The marker expresses the reciprocal and also the reflexive meaning: a reflexive reciprocal construction.

Equations
Instances For
    source
    def MaslovaNedjalkov2013.IsNonreflexiveReciprocal (m : Reciprocal.Marker) :
    Prop

    The marker expresses the reciprocal meaning but not the reflexive one: a non-reflexive reciprocal construction.

    Equations
    Instances For
      source
      @[instance_reducible]
      instance MaslovaNedjalkov2013.instDecidableIsReflexiveReciprocal (m : Reciprocal.Marker) :
      Decidable (IsReflexiveReciprocal m)
      Equations
      source
      @[instance_reducible]
      instance MaslovaNedjalkov2013.instDecidableIsNonreflexiveReciprocal (m : Reciprocal.Marker) :
      Decidable (IsNonreflexiveReciprocal m)
      Equations
      source
      def MaslovaNedjalkov2013.ofInventory (inv : Finset Reciprocal.Marker) :
      Data.WALS.F106A.ReciprocalType

      The value of an inventory: reflexive reciprocal markers, non-reflexive ones, both (the mixed type), or neither.

      Equations
      • One or more equations did not get rendered due to their size.
      Instances For
        source
        @[simp]
        theorem MaslovaNedjalkov2013.ofInventory_eq_mixed_iff {inv : Finset Reciprocal.Marker} :
        ofInventory inv = Data.WALS.F106A.ReciprocalType.mixed ↔ (∃ m ∈ inv, IsReflexiveReciprocal m) ∧ ∃ m ∈ inv, IsNonreflexiveReciprocal m
        source
        @[simp]
        theorem MaslovaNedjalkov2013.ofInventory_eq_identicalToReflexive_iff {inv : Finset Reciprocal.Marker} :
        ofInventory inv = Data.WALS.F106A.ReciprocalType.identicalToReflexive ↔ (∃ m ∈ inv, IsReflexiveReciprocal m) ∧ ∀ m ∈ inv, ¬IsNonreflexiveReciprocal m
        source
        @[simp]
        theorem MaslovaNedjalkov2013.ofInventory_eq_distinctFromReflexive_iff {inv : Finset Reciprocal.Marker} :
        ofInventory inv = Data.WALS.F106A.ReciprocalType.distinctFromReflexive ↔ (∀ m ∈ inv, ¬IsReflexiveReciprocal m) ∧ ∃ m ∈ inv, IsNonreflexiveReciprocal m
        source
        @[simp]
        theorem MaslovaNedjalkov2013.ofInventory_eq_noReciprocalConstruction_iff {inv : Finset Reciprocal.Marker} :
        ofInventory inv = Data.WALS.F106A.ReciprocalType.noReciprocalConstruction ↔ ∀ m ∈ inv, Reciprocal.Reading.reciprocal ∉ m.readings

        An inventory has no reciprocal construction when none of its markers is reciprocal.

        The chapter's examples (§2.2) #

        source
        theorem MaslovaNedjalkov2013.ofInventory_english :
        ofInventory English.Reciprocals.markers = Data.WALS.F106A.ReciprocalType.distinctFromReflexive

        English has only non-reflexive reciprocals, each other and one another.

        source
        theorem MaslovaNedjalkov2013.ofInventory_german :
        ofInventory German.Reciprocals.markers = Data.WALS.F106A.ReciprocalType.mixed

        German is of the mixed type: sich is also reflexive, einander is not.

        The sample #

        source
        inductive MaslovaNedjalkov2013.Language :
        Type

        The languages of the chapter's sample whose reciprocal markers a fragment records.

        Instances For
          source
          @[instance_reducible]
          instance MaslovaNedjalkov2013.instDecidableEqLanguage :
          DecidableEq Language
          Equations
          source
          def MaslovaNedjalkov2013.Language.walsCode :
          Language → String

          The WALS code under which the chapter's data lists the language.

          Equations
          Instances For
            source
            def MaslovaNedjalkov2013.Language.markers :
            Language → Finset Reciprocal.Marker

            The language's reciprocal markers, from its fragment.

            Equations
            Instances For
              source
              theorem MaslovaNedjalkov2013.ofInventory_eq_wals (l : Language) :
              List.lookup l.walsCode Data.WALS.F106A.allData = some (ofInventory l.markers)

              Each language's inventory has the value the chapter codes for it.