Documentation

Studies.SarvasyAikhenvald2025

Sarvasy & Aikhenvald (2025): Clause Chaining in the Languages of the World #

This file formalizes the typological generalizations of the volume's introduction over the clause-chaining systems of four of its languages. A clause chain is a sequence of medial clauses, formally dependent and underspecified for inflectional categories, closed by one independent clause, and the introduction surveys the parameters along which chaining varies: the switch-reference marking of many medial-final languages, the categories medial verbs retain, the relations medial forms encode, the two bridging constructions and the non-canonical uses of medial clauses. The sample (Language) is Nungon and Manambu, whose chapters describe switch-reference systems, and Korean and Turkish, which chain without switch-reference; each language's medial forms are its fragment's carrier (Language.Forms), and its retention profile (Language.medialMorph), bridging constructions (Language.bridging) and stand-alone medial clauses (Language.MedialStandsAlone) are read off the forms where the forms decide them and are the chapters' reports otherwise. The generalizations proved are that same-subject medial forms leave the subject unindexed while different-subject forms index it (ss_forms_lack_subject_marking), that Manambu's switch-reference markers each encode a temporal or logical relation whereas Nungon's mark subject continuity alone, the temporal relation coming from a switch-reference-neutral construction (relations_fused_with_sr), that the chain's tense comes from the final verb in the two Papuan languages while Korean admits tense before some medial suffixes (tense_from_final_verb), that Turkish negates medial clauses individually (negated_individually), that the medial verbs of both are converbs (converb_form), and that in the sample switch-reference goes with the loss or reduction of medial tense (sr_and_tense).

Implementation notes #

The Korean and Turkish inventories come from reference grammars rather than the volume, whose introduction discusses both languages; the volume's Turkish suffix list adds the two converbial subordinators on a doubled verb, which the fragment records outside its carrier. Nungon's medial polarity is the earlier formalization's value, which chapter 7 does not settle. Ku Waru and Korowai, formerly in the sample, are dropped: the former has no chapter in the volume and the latter's switch-reference system was misrecorded as tracking several arguments.

References #

The sample #

source
inductive SarvasyAikhenvald2025.Language :
Type

The four languages.

Instances For
    source
    @[instance_reducible]
    instance SarvasyAikhenvald2025.instDecidableEqLanguage :
    DecidableEq Language
    Equations
    source
    def SarvasyAikhenvald2025.instReprLanguage.repr :
    Language → ℕ → Std.Format
    Equations
    • One or more equations did not get rendered due to their size.
    Instances For
      source
      @[instance_reducible]
      instance SarvasyAikhenvald2025.instReprLanguage :
      Repr Language
      Equations
      source
      @[instance_reducible]
      instance SarvasyAikhenvald2025.instFintypeLanguage :
      Fintype Language
      Equations
      • One or more equations did not get rendered due to their size.
      source
      def SarvasyAikhenvald2025.Language.Forms :
      Language → Type

      The medial forms of a language, its fragment's carrier.

      Equations
      Instances For
        source
        @[instance_reducible]
        instance SarvasyAikhenvald2025.Language.instFintypeForms (L : Language) :
        Fintype L.Forms
        Equations
        • One or more equations did not get rendered due to their size.
        source
        @[instance_reducible]
        instance SarvasyAikhenvald2025.Language.instMedialFormForms (L : Language) :
        Clause.Chaining.MedialForm L.Forms
        Equations
        • One or more equations did not get rendered due to their size.
        source
        def SarvasyAikhenvald2025.Language.tense :
        Language → Clause.Chaining.CategoryRetention

        The tense medial verbs retain, which is none in Nungon, relative tense fused with the marking in Manambu, and tense before the converbs that admit it in Korean and in Turkish.

        Equations
        Instances For
          source
          def SarvasyAikhenvald2025.Language.mood :
          Language → Clause.Chaining.CategoryRetention

          The mood medial verbs retain, which is none in the two Papuan languages, in Korean the modal before the suffixes that admit it, and in Turkish the modality markers before the converbs on a tensed stem.

          Equations
          Instances For
            source
            def SarvasyAikhenvald2025.Language.polarity :
            Language → Clause.Chaining.CategoryRetention

            Independent negation of the medial clause, which in Manambu and Turkish is as far as the forms admit it, in Korean the negative adverbs and negative verb of a medial clause, and in Nungon the earlier formalization's value.

            Equations
            Instances For
              source
              def SarvasyAikhenvald2025.Language.aspect :
              Language → Clause.Chaining.CategoryRetention

              The aspect medial verbs retain, which is none in Nungon, in Manambu aspect only before the causal marker, which takes the tensed cross-referencing of a main verb, in Korean the perfect before the suffixes that admit it, and in Turkish the aspect markers before the converbs on a tensed stem.

              Equations
              Instances For
                source
                def SarvasyAikhenvald2025.Language.medialMorph (L : Language) :
                Clause.Chaining.MedialMorphProfile

                The retention profile of a language's medial verbs, agreement read off its forms.

                Equations
                Instances For
                  source
                  def SarvasyAikhenvald2025.Language.bridging :
                  Language → Finset Clause.Chaining.BridgingType

                  The bridging constructions attested, both in the two Papuan languages and neither in Korean and Turkish.

                  Equations
                  Instances For
                    source
                    def SarvasyAikhenvald2025.Language.MedialStandsAlone :
                    Language → Prop

                    Medial clauses occur on their own in Nungon and Korean, in Manambu with the forms that do, and not in Turkish.

                    Equations
                    Instances For

                      The generalizations #

                      source
                      theorem SarvasyAikhenvald2025.ss_forms_lack_subject_marking :
                      Clause.Chaining.MedialForm.SSUnmarked Nungon.Medial ∧ Clause.Chaining.MedialForm.SSUnmarked Manambu.MedialMarker ∧ Clause.Chaining.MedialForm.agreement Nungon.Medial = Clause.Chaining.CategoryRetention.restricted ∧ Clause.Chaining.MedialForm.agreement Manambu.MedialMarker = Clause.Chaining.CategoryRetention.restricted

                      Same-subject medial forms leave the subject unindexed and different-subject forms index it: Nungon's same-subject verb is the bare dependent stem with the medial suffix while its different-subject verb carries a subject desinence, and no Manambu same-subject marker follows subject cross-referencing while both different-subject markers do, so agreement on medial verbs is restricted in both.

                      source
                      theorem SarvasyAikhenvald2025.relations_fused_with_sr :
                      (∀ (m : Manambu.MedialMarker), m.sr ≠ none → m.relations.Nonempty) ∧ (∃ r ∈ Clause.Chaining.MedialForm.relationsMarked Manambu.MedialMarker, ¬r.Temporal) ∧ (∀ (m : Nungon.Medial), m.sr ≠ none → m.relations = ∅) ∧ ∃ (m : Nungon.Medial), m.sr = none ∧ m.relations.Nonempty

                      Manambu's switch-reference markers each encode a temporal or logical relation, and some of the relations lie beyond the temporal ones; Nungon's switch-reference forms encode no relation, and completion before the next event is marked by the perfect, which is neutral to switch-reference.

                      source
                      theorem SarvasyAikhenvald2025.tense_from_final_verb :
                      Language.nungon.tense = Clause.Chaining.CategoryRetention.absent ∧ Language.manambu.tense = Clause.Chaining.CategoryRetention.restricted ∧ Language.korean.tense = Clause.Chaining.CategoryRetention.restricted

                      The chain's tense comes from the final verb in Nungon, whose medial verbs bear no tense, and Manambu's medial tense is relative; Korean admits tense before some but not all of its medial suffixes.

                      source
                      theorem SarvasyAikhenvald2025.negated_individually :
                      Language.turkish.polarity = Clause.Chaining.CategoryRetention.full

                      Turkish negates medial clauses individually, since every converb admits the negative before it or is negative itself.

                      source
                      theorem SarvasyAikhenvald2025.converb_form :
                      Language.korean.medialMorph.udVerbForm = UD.VerbForm.Conv ∧ Language.turkish.medialMorph.udVerbForm = UD.VerbForm.Conv ∧ (∀ (c : Korean.Converb), c.verbForm = Language.korean.medialMorph.udVerbForm) ∧ ∀ (c : Turkish.Converb), c.verbForm = Language.turkish.medialMorph.udVerbForm

                      The medial verbs of the languages without switch-reference are converbs, as their fragments record them.

                      source
                      theorem SarvasyAikhenvald2025.sr_and_tense (L : Language) :
                      Clause.Chaining.MedialForm.HasSR L.Forms → L.tense ≠ Clause.Chaining.CategoryRetention.full

                      Switch-reference goes with the Papuan systems of the sample and its absence with the converbal ones, and the systems with switch-reference are the ones whose medial verbs lose tense or reduce it to relative tense.