Documentation

Linglib.Studies.Creissels2024

Creissels's typology of transitivity, valency and voice #

The nominal terms of a clause bear transitivity-related roles defined by coding rather than by meaning: A and P are the two terms coded like the agent and the patient of a prototypical transitive verb; S is the term of an intransitive clause coded like the sole argument of monovalent verbs; every other nominal term is an oblique, a dative oblique where recipients are coded apart from patients. A construction of a verb assigns each of the verb's potential participants a nominal term with one of these roles, leaves it implied but unexpressed, or has it outside participant structure altogether, and a valency alternation is a relation between two constructions of the same verb. Where verbal morphology marks the alternation it is a voice alternation and the morphologically simpler, or semantically unmarked, construction is the initial one; where nothing marks it the verb is flexivalent, and a change of transitivity without marking is ambitransitivity. Two operations characterise oriented alternations: nucleativization, a participant that is not a core term of the initial construction becomes one, and denucleativization, a core term of the initial construction is not one of the derived construction, whether it remains implied or is suppressed from participant structure. The main types are defined from them. Passivization, its impersonal variant, antipassivization and S-denucleativization denucleativize one core term without suppressing it and nucleativize nothing; decausativization suppresses the initial A; an A-nucleativization makes a new participant the A or S and codes the initial A or S as P or denucleativizes it, whether the new participant is a causer, causativization in the narrow sense, an instrument, or a concernee; reflexivization and reciprocalization cumulate two participant roles in one S; applicativization keeps the initial A or S and adds an applied phrase, as P, as a dative or as an ordinary oblique, for a participant the initial construction could not code that way; portative derivation makes the initial S the A of a transitive construction whose P is a carried entity. Nucleativization is not valency increase, since a participant may be nucleativized while another is denucleativized. One marker commonly codes several types, and markers may stack compositionally, the composite alternation being the composition of its parts, subject to language-particular restrictions and non-compositional readings. Symmetrical voices, the pivot-prominent systems of Western Austronesian and of a few languages elsewhere, select a participant as pivot without nucleativizing or denucleativizing anything and so fall outside the typology. Transitive and intransitive constructions align in coding, S coded like A or like P, and the Obligatory Coding Principle, one coding assigned by every verb to one of its participants, reformulates the accusative and ergative types as obligatory A-coding and obligatory P-coding, which split-S languages violate. The book's examples are the rows of Data/Examples/Creissels2024.json.

Implementation notes #

TODO #

References #

What a construction does with a potential participant of the verb: expresses it as a nominal term with a transitivity-related role, as a dative oblique, leaves it implied but unexpressed, or has it outside participant structure.

Instances For
    def Creissels2024.instDecidableEqStatus.decEq (x✝ x✝¹ : Status) :
    Decidable (x✝ = x✝¹)
    Equations
    Instances For
      def Creissels2024.instReprStatus.repr :
      StatusStd.Format
      Equations
      • One or more equations did not get rendered due to their size.
      Instances For

        The role of the nominal term, datives counting as obliques.

        Equations
        Instances For

          A nuclear participant: one expressed as a core term.

          Equations
          Instances For

            In participant structure.

            Equations
            Instances For

              Expressed by a nominal term.

              Equations
              Instances For
                @[instance_reducible]
                Equations
                • One or more equations did not get rendered due to their size.
                @[instance_reducible]
                Equations
                @[instance_reducible]
                Equations
                @[reducible, inline]
                abbrev Creissels2024.Construction (ι : Type u_1) :
                Type u_1

                A construction of a verb over its potential participants.

                Equations
                Instances For

                  A transitive construction has an A term and a P term.

                  Equations
                  Instances For

                    An impersonal construction has neither an A term nor an S term.

                    Equations
                    Instances For
                      def Creissels2024.Construction.valency {ι : Type u_1} [Fintype ι] (c : Construction ι) :

                      The valency of a construction: its number of nuclear participants.

                      Equations
                      Instances For
                        @[instance_reducible]
                        instance Creissels2024.Construction.instDecidableTransitive {ι : Type u_1} [Fintype ι] (c : Construction ι) :
                        Decidable c.Transitive
                        Equations
                        @[instance_reducible]
                        instance Creissels2024.Construction.instDecidableImpersonal {ι : Type u_1} [Fintype ι] (c : Construction ι) :
                        Decidable c.Impersonal
                        Equations

                        Nucleativization and denucleativization (§8.1.3) #

                        def Creissels2024.Nucleativized {ι : Type u_1} (c d : Construction ι) (i : ι) :

                        A participant that is not a core term of the initial construction is one of the derived construction.

                        Equations
                        Instances For
                          def Creissels2024.Denucleativized {ι : Type u_1} (c d : Construction ι) (i : ι) :

                          A core term of the initial construction is not one of the derived construction.

                          Equations
                          Instances For
                            def Creissels2024.Suppressed {ι : Type u_1} (c d : Construction ι) (i : ι) :

                            A core term of the initial construction is removed from participant structure.

                            Equations
                            Instances For
                              def Creissels2024.Introduced {ι : Type u_1} (c d : Construction ι) (i : ι) :

                              A participant the initial construction does not express as a core term is expressed, and differently, by the derived construction.

                              Equations
                              Instances For

                                Some participant is nucleativized.

                                Equations
                                Instances For

                                  Some participant is denucleativized.

                                  Equations
                                  Instances For

                                    The two constructions imply the same participant roles.

                                    Equations
                                    Instances For
                                      @[instance_reducible]
                                      instance Creissels2024.instDecidableNucleativized {ι : Type u_1} (c d : Construction ι) (i : ι) :
                                      Decidable (Nucleativized c d i)
                                      Equations
                                      @[instance_reducible]
                                      instance Creissels2024.instDecidableDenucleativized {ι : Type u_1} (c d : Construction ι) (i : ι) :
                                      Decidable (Denucleativized c d i)
                                      Equations
                                      @[instance_reducible]
                                      instance Creissels2024.instDecidableSuppressed {ι : Type u_1} (c d : Construction ι) (i : ι) :
                                      Decidable (Suppressed c d i)
                                      Equations
                                      @[instance_reducible]
                                      instance Creissels2024.instDecidableIntroduced {ι : Type u_1} (c d : Construction ι) (i : ι) :
                                      Decidable (Introduced c d i)
                                      Equations
                                      @[instance_reducible]
                                      instance Creissels2024.instDecidableNucleativization {ι : Type u_1} [Fintype ι] (c d : Construction ι) :
                                      Decidable (Nucleativization c d)
                                      Equations
                                      @[instance_reducible]
                                      instance Creissels2024.instDecidableDenucleativization {ι : Type u_1} [Fintype ι] (c d : Construction ι) :
                                      Decidable (Denucleativization c d)
                                      Equations
                                      @[instance_reducible]
                                      instance Creissels2024.instDecidablePreservesStructure {ι : Type u_1} [Fintype ι] (c d : Construction ι) :
                                      Decidable (PreservesStructure c d)
                                      Equations
                                      theorem Creissels2024.valency_eq_of_nucleativized_denucleativized {ι : Type u_1} [Fintype ι] [DecidableEq ι] {c d : Construction ι} {i j : ι} (hi : Nucleativized c d i) (hj : Denucleativized c d j) (h : ∀ (k : ι), k ik j((c k).Nuclear (d k).Nuclear)) :

                                      Nucleativization is not valency increase: a construction may nucleativize one participant and denucleativize another, keeping its valency, as a causative that codes the initial A as P and denucleativizes the initial P does.

                                      theorem Creissels2024.not_nucleativized_self {ι : Type u_1} (c : Construction ι) (i : ι) :

                                      A construction nucleativizes none of its own participants.

                                      theorem Creissels2024.not_denucleativized_self {ι : Type u_1} (c : Construction ι) (i : ι) :

                                      A construction denucleativizes none of its own participants.

                                      The main types of voice alternation (§8.3) #

                                      def Creissels2024.Demoted {ι : Type u_1} (c d : Construction ι) (i : ι) :

                                      The common core of §8.3.2: a nuclear participant of the initial construction is denucleativized without being deleted from participant structure, and no participant is nucleativized.

                                      Equations
                                      Instances For

                                        Passivization: the initial construction is transitive, its A is demoted but maintained in participant structure, and its P remains a core term, as S in the canonical case and as the P of a transitive construction after a double-P construction.

                                        Equations
                                        • One or more equations did not get rendered due to their size.
                                        Instances For

                                          The impersonal variant of passivization: the initial P keeps its coding, so the derived construction has neither A nor S.

                                          Equations
                                          Instances For

                                            Antipassivization: the initial construction is transitive, participant structure is unchanged, a P is demoted, and the initial A becomes the S of an intransitive construction, or keeps the role of A after a double-P construction.

                                            Equations
                                            • One or more equations did not get rendered due to their size.
                                            Instances For

                                              S-denucleativization: the initial construction is intransitive and its S is demoted.

                                              Equations
                                              • One or more equations did not get rendered due to their size.
                                              Instances For

                                                Decausativization: the initial construction is transitive, its A is suppressed from participant structure, its P becomes the S of an intransitive construction, and nothing is nucleativized.

                                                Equations
                                                • One or more equations did not get rendered due to their size.
                                                Instances For
                                                  def Creissels2024.ANucleativization {ι : Type u_1} (c d : Construction ι) (i : ι) :

                                                  A-nucleativization: a participant is nucleativized and takes over the role of A or S, and the participant coded as A or S in the initial construction is coded as P or denucleativized. Causativization in the narrow sense of chapter 12, where the new participant instigates or controls the event, the A-nucleativization of an instrumental oblique, and concernativization, where the new participant is a concernee of the initial S or P, share this structure and differ in the new participant's semantic relation to the event, which is not modelled.

                                                  Equations
                                                  • One or more equations did not get rendered due to their size.
                                                  Instances For
                                                    def Creissels2024.Cumulation {ι : Type u_1} (c d : Construction ι) :

                                                    Reflexivization and reciprocalization: two participant roles expressed as A and P, or as S and a dative oblique, in the initial construction are cumulated by the S term of the derived construction. Whether the S refers to an individual or to a group is not modelled.

                                                    Equations
                                                    • One or more equations did not get rendered due to their size.
                                                    Instances For
                                                      def Creissels2024.Applicativization {ι : Type u_1} (c d : Construction ι) (applied : ι) :

                                                      Applicativization: the participant coded as A or S in the initial construction keeps the role of A or S, and the derived construction expresses, in a role other than A or S, an applied participant that the initial construction did not express that way.

                                                      Equations
                                                      • One or more equations did not get rendered due to their size.
                                                      Instances For
                                                        def Creissels2024.PApplicativization {ι : Type u_1} (c d : Construction ι) (applied : ι) :

                                                        P-applicativization: the applied phrase is a P, so the initial A or S is the A of the derived transitive construction.

                                                        Equations
                                                        • One or more equations did not get rendered due to their size.
                                                        Instances For
                                                          def Creissels2024.DApplicativization {ι : Type u_1} (c d : Construction ι) (applied : ι) :

                                                          D-applicativization: the applied phrase is a dative oblique.

                                                          Equations
                                                          Instances For
                                                            def Creissels2024.XApplicativization {ι : Type u_1} (c d : Construction ι) (applied : ι) :

                                                            X-applicativization: the applied phrase is an ordinary oblique.

                                                            Equations
                                                            Instances For
                                                              def Creissels2024.Portative {ι : Type u_1} (c d : Construction ι) (carried : ι) :

                                                              Portative derivation: an intransitive verb of motion becomes transitive, its S the A of the derived construction and a carried entity its P.

                                                              Equations
                                                              • One or more equations did not get rendered due to their size.
                                                              Instances For
                                                                def Creissels2024.Symmetrical {ι : Type u_1} (c d : Construction ι) :

                                                                A symmetrical voice alternation selects a pivot without changing which participants are core terms.

                                                                Equations
                                                                Instances For
                                                                  @[instance_reducible]
                                                                  instance Creissels2024.instDecidableDemoted {ι : Type u_1} [Fintype ι] (c d : Construction ι) (i : ι) :
                                                                  Decidable (Demoted c d i)
                                                                  Equations
                                                                  @[instance_reducible]
                                                                  instance Creissels2024.instDecidablePassivization {ι : Type u_1} [Fintype ι] (c d : Construction ι) :
                                                                  Decidable (Passivization c d)
                                                                  Equations
                                                                  @[instance_reducible]
                                                                  instance Creissels2024.instDecidableIPassivization {ι : Type u_1} [Fintype ι] (c d : Construction ι) :
                                                                  Decidable (IPassivization c d)
                                                                  Equations
                                                                  @[instance_reducible]
                                                                  instance Creissels2024.instDecidableAntipassivization {ι : Type u_1} [Fintype ι] (c d : Construction ι) :
                                                                  Decidable (Antipassivization c d)
                                                                  Equations
                                                                  @[instance_reducible]
                                                                  instance Creissels2024.instDecidableSDenucleativization {ι : Type u_1} [Fintype ι] (c d : Construction ι) :
                                                                  Decidable (SDenucleativization c d)
                                                                  Equations
                                                                  @[instance_reducible]
                                                                  instance Creissels2024.instDecidableDecausativization {ι : Type u_1} [Fintype ι] (c d : Construction ι) :
                                                                  Decidable (Decausativization c d)
                                                                  Equations
                                                                  @[instance_reducible]
                                                                  instance Creissels2024.instDecidableANucleativization {ι : Type u_1} [Fintype ι] (c d : Construction ι) (i : ι) :
                                                                  Decidable (ANucleativization c d i)
                                                                  Equations
                                                                  @[instance_reducible]
                                                                  instance Creissels2024.instDecidableCumulation {ι : Type u_1} [Fintype ι] [DecidableEq ι] (c d : Construction ι) :
                                                                  Decidable (Cumulation c d)
                                                                  Equations
                                                                  @[instance_reducible]
                                                                  instance Creissels2024.instDecidableApplicativization {ι : Type u_1} [Fintype ι] (c d : Construction ι) (i : ι) :
                                                                  Decidable (Applicativization c d i)
                                                                  Equations
                                                                  @[instance_reducible]
                                                                  instance Creissels2024.instDecidablePApplicativization {ι : Type u_1} [Fintype ι] (c d : Construction ι) (i : ι) :
                                                                  Decidable (PApplicativization c d i)
                                                                  Equations
                                                                  @[instance_reducible]
                                                                  instance Creissels2024.instDecidableDApplicativization {ι : Type u_1} [Fintype ι] (c d : Construction ι) (i : ι) :
                                                                  Decidable (DApplicativization c d i)
                                                                  Equations
                                                                  @[instance_reducible]
                                                                  instance Creissels2024.instDecidableXApplicativization {ι : Type u_1} [Fintype ι] (c d : Construction ι) (i : ι) :
                                                                  Decidable (XApplicativization c d i)
                                                                  Equations
                                                                  @[instance_reducible]
                                                                  instance Creissels2024.instDecidablePortative {ι : Type u_1} [Fintype ι] (c d : Construction ι) (i : ι) :
                                                                  Decidable (Portative c d i)
                                                                  Equations
                                                                  @[instance_reducible]
                                                                  instance Creissels2024.instDecidableSymmetrical {ι : Type u_1} [Fintype ι] (c d : Construction ι) :
                                                                  Decidable (Symmetrical c d)
                                                                  Equations

                                                                  Decausativization modifies participant structure: the initial A leaves it.

                                                                  The maintenance of the initial A in participant structure separates passivization from decausativization.

                                                                  theorem Creissels2024.SDenucleativization.not_nuclear {ι : Type u_1} {c d : Construction ι} (h : SDenucleativization c d) (hc : ∀ (i : ι), (c i).Nuclearc i = Status.term Voice.TermRole.S) (i : ι) :
                                                                  ¬(d i).Nuclear

                                                                  S-denucleativization leaves no core term when the initial construction has no core term but its S.

                                                                  theorem Creissels2024.Portative.not_aNucleativization {ι : Type u_1} {c d : Construction ι} {i : ι} (h : Portative c d i) (hS : ∃ (s : ι), c s = Status.term Voice.TermRole.S) (j : ι) :

                                                                  Portative derivation is not causativization in the narrow sense: the initial S is the A of the one and the P of the other.

                                                                  A symmetrical voice nucleativizes nothing.

                                                                  A symmetrical voice denucleativizes nothing.

                                                                  A symmetrical voice is not a passivization, nor any type defined by denucleativization.

                                                                  theorem Creissels2024.Symmetrical.not_aNucleativization {ι : Type u_1} {c d : Construction ι} (h : Symmetrical c d) (i : ι) :

                                                                  A symmetrical voice is not an A-nucleativization, nor any type defined by nucleativization.

                                                                  The substrate's summary records #

                                                                  def Creissels2024.fate {ι : Type u_1} [Fintype ι] [DecidableEq ι] (c d : Construction ι) (i : ι) :

                                                                  The fate of an initial core term, read off the two constructions: suppressed when it leaves participant structure, cumulated when it shares its derived core term with another initial core term, maintained when it remains a core term, denucleativized otherwise.

                                                                  Equations
                                                                  • One or more equations did not get rendered due to their size.
                                                                  Instances For
                                                                    def Creissels2024.Describes {ι : Type u_1} [Fintype ι] [DecidableEq ι] (va : Voice.ValencyAlternation) (c d : Construction ι) :

                                                                    A summary record of the substrate describes a pair of constructions when the fates it records are those of the initial A, P and S, a role it records as absent is absent, the participant it introduces is the one the derived construction introduces, and the transitivity it fixes is the constructions'.

                                                                    Equations
                                                                    • One or more equations did not get rendered due to their size.
                                                                    Instances For
                                                                      @[instance_reducible]
                                                                      instance Creissels2024.instDecidableDescribes {ι : Type u_1} [Fintype ι] [DecidableEq ι] (va : Voice.ValencyAlternation) (c d : Construction ι) :
                                                                      Decidable (Describes va c d)
                                                                      Equations
                                                                      • One or more equations did not get rendered due to their size.

                                                                      Alignment and the Obligatory Coding Principle (§1.3.4) #

                                                                      The flagging of a core term: the zero case, an accusative or an ergative.

                                                                      Instances For
                                                                        @[instance_reducible]
                                                                        Equations
                                                                        def Creissels2024.instReprFlag.repr :
                                                                        FlagStd.Format
                                                                        Equations
                                                                        Instances For
                                                                          @[instance_reducible]
                                                                          Equations

                                                                          The flags of A and of P in an A/P-prominent transitive construction, which contrast.

                                                                          • a : Flag

                                                                            The flag of A.

                                                                          • p : Flag

                                                                            The flag of P.

                                                                          • ne : self.a self.p

                                                                            A and P are flagged apart.

                                                                          Instances For
                                                                            def Creissels2024.instDecidableEqCoding.decEq (x✝ x✝¹ : Coding) :
                                                                            Decidable (x✝ = x✝¹)
                                                                            Equations
                                                                            • One or more equations did not get rendered due to their size.
                                                                            Instances For
                                                                              def Creissels2024.instReprCoding.repr :
                                                                              CodingStd.Format
                                                                              Equations
                                                                              • One or more equations did not get rendered due to their size.
                                                                              Instances For

                                                                                The alignment of an intransitive construction whose S carries a flag: with A, with P, or neither.

                                                                                Equations
                                                                                Instances For
                                                                                  @[simp]

                                                                                  A flag aligns with A exactly when it is the A flag.

                                                                                  @[simp]

                                                                                  A flag aligns with P exactly when it is the P flag.

                                                                                  def Creissels2024.ObligatoryCoding (t : Coding) (ss : List Flag) (k : Flag) :

                                                                                  The Obligatory Coding Principle, over the intransitive constructions of the examples: a flag of the transitive construction that every verb assigns to one of its participants, here every intransitive verb through its S.

                                                                                  Equations
                                                                                  Instances For

                                                                                    An obligatory A-coding language, the consistently accusative type.

                                                                                    Equations
                                                                                    Instances For

                                                                                      An obligatory P-coding language, the consistently ergative type.

                                                                                      Equations
                                                                                      Instances For
                                                                                        def Creissels2024.SplitS (t : Coding) (ss : List Flag) :

                                                                                        A split-S language: some intransitive constructions align with A and some with P.

                                                                                        Equations
                                                                                        Instances For
                                                                                          @[instance_reducible]
                                                                                          instance Creissels2024.instDecidableObligatoryCoding (t : Coding) (ss : List Flag) (k : Flag) :
                                                                                          Decidable (ObligatoryCoding t ss k)
                                                                                          Equations
                                                                                          @[instance_reducible]
                                                                                          instance Creissels2024.instDecidableObligatoryACoding (t : Coding) (ss : List Flag) :
                                                                                          Decidable (ObligatoryACoding t ss)
                                                                                          Equations
                                                                                          @[instance_reducible]
                                                                                          instance Creissels2024.instDecidableObligatoryPCoding (t : Coding) (ss : List Flag) :
                                                                                          Decidable (ObligatoryPCoding t ss)
                                                                                          Equations
                                                                                          @[instance_reducible]
                                                                                          instance Creissels2024.instDecidableSplitS (t : Coding) (ss : List Flag) :
                                                                                          Decidable (SplitS t ss)
                                                                                          Equations
                                                                                          theorem Creissels2024.obligatoryACoding_iff {t : Coding} {ss : List Flag} :
                                                                                          ObligatoryACoding t ss sss, t.alignment s = some Voice.Alignment.A_alignment

                                                                                          Over the S flags alone, obligatory A-coding is A-alignment throughout.

                                                                                          theorem Creissels2024.obligatoryPCoding_iff {t : Coding} {ss : List Flag} :
                                                                                          ObligatoryPCoding t ss sss, t.alignment s = some Voice.Alignment.P_alignment

                                                                                          Over the S flags alone, obligatory P-coding is P-alignment throughout.

                                                                                          A split-S language is not obligatory A-coding.

                                                                                          A split-S language is not obligatory P-coding.

                                                                                          The book's examples #

                                                                                          The types of voice alternation the book names, symmetrical voices included.

                                                                                          • passivization : Kind
                                                                                          • iPassivization : Kind
                                                                                          • antipassivization : Kind
                                                                                          • sDenucleativization : Kind
                                                                                          • decausativization : Kind
                                                                                          • causativization : Kind
                                                                                          • concernativization : Kind
                                                                                          • aNucleativization : Kind
                                                                                          • reflexivization : Kind
                                                                                          • reciprocalization : Kind
                                                                                          • pApplicativization : Kind
                                                                                          • dApplicativization : Kind
                                                                                          • xApplicativization : Kind
                                                                                          • portative : Kind
                                                                                          • symmetrical : Kind
                                                                                          Instances For
                                                                                            @[instance_reducible]
                                                                                            Equations
                                                                                            def Creissels2024.instReprKind.repr :
                                                                                            KindStd.Format
                                                                                            Equations
                                                                                            • One or more equations did not get rendered due to their size.
                                                                                            Instances For
                                                                                              @[instance_reducible]
                                                                                              Equations
                                                                                              def Creissels2024.Kind.Realize {ι : Type u_1} (c d : Construction ι) :
                                                                                              KindOption ιProp

                                                                                              Whether a pair of constructions realizes a type, given the participant the type singles out; the three A-nucleativizations and the two cumulations share their structure.

                                                                                              Equations
                                                                                              Instances For
                                                                                                @[instance_reducible]
                                                                                                instance Creissels2024.instDecidableRealizeOfFintypeOfDecidableEq {ι : Type u_1} [Fintype ι] [DecidableEq ι] (c d : Construction ι) (k : Kind) (o : Option ι) :
                                                                                                Decidable (Kind.Realize c d k o)
                                                                                                Equations
                                                                                                • One or more equations did not get rendered due to their size.

                                                                                                The share of the languages in Bahrt's sample with synthetic marking of each type, in percent; Bahrt's applicativization pools the three applicativizations with non-causative A/S-nucleativization, and the book's symmetrical voices are outside his survey.

                                                                                                Equations
                                                                                                Instances For
                                                                                                  theorem Creissels2024.bahrtShare_extremes (k : Kind) (x : ) :
                                                                                                  x k.bahrtShare(∀ yKind.causativization.bahrtShare, x y) yKind.antipassivization.bahrtShare, y x

                                                                                                  Causativization is the most widely marked type and antipassivization the least.

                                                                                                  def Creissels2024.kindNames :
                                                                                                  List (String × Kind)

                                                                                                  The types by name.

                                                                                                  Equations
                                                                                                  • One or more equations did not get rendered due to their size.
                                                                                                  Instances For
                                                                                                    def Creissels2024.statusNames :
                                                                                                    List (String × Status)

                                                                                                    The statuses by name.

                                                                                                    Equations
                                                                                                    • One or more equations did not get rendered due to their size.
                                                                                                    Instances For
                                                                                                      def Creissels2024.slotNames :
                                                                                                      List (String × Fin 5)

                                                                                                      The participant slots of a row by name.

                                                                                                      Equations
                                                                                                      Instances For
                                                                                                        def Creissels2024.flagNames :
                                                                                                        List (String × Flag)

                                                                                                        The flags by name.

                                                                                                        Equations
                                                                                                        Instances For

                                                                                                          The markings by name.

                                                                                                          Equations
                                                                                                          • One or more equations did not get rendered due to their size.
                                                                                                          Instances For

                                                                                                            The construction a row describes over its five participant slots, absent where unlisted.

                                                                                                            Equations
                                                                                                            • One or more equations did not get rendered due to their size.
                                                                                                            Instances For

                                                                                                              The rows of the same example whose variant the row names under a key: its initial construction, or the transitive use of a flexivalent verb.

                                                                                                              Equations
                                                                                                              • One or more equations did not get rendered due to their size.
                                                                                                              Instances For
                                                                                                                def Creissels2024.Examples.sFlags (language : String) :
                                                                                                                List Flag

                                                                                                                The S flags of a language's intransitive examples.

                                                                                                                Equations
                                                                                                                • One or more equations did not get rendered due to their size.
                                                                                                                Instances For
                                                                                                                  def Creissels2024.Examples.coding (language : String) :
                                                                                                                  Option Coding

                                                                                                                  The A and P flags of a language's transitive example.

                                                                                                                  Equations
                                                                                                                  • One or more equations did not get rendered due to their size.
                                                                                                                  Instances For
                                                                                                                    def Creissels2024.Examples.coExpressed (language marker : String) :
                                                                                                                    List Kind

                                                                                                                    The types a marker of a language codes across the book's examples.

                                                                                                                    Equations
                                                                                                                    • One or more equations did not get rendered due to their size.
                                                                                                                    Instances For
                                                                                                                      theorem Creissels2024.alternation_parses (row : Data.Examples.LinguisticExample) :
                                                                                                                      row Examples.all(row.feature? "alternation").isSome = true(row.parse? "alternation" kindNames).isSome = true

                                                                                                                      Every label the rows carry parses to a type.

                                                                                                                      theorem Creissels2024.paired_resolves (row : Data.Examples.LinguisticExample) :
                                                                                                                      row Examples.allkey["initial", "transitive"], (row.feature? key).isSome = trueExamples.paired key row []

                                                                                                                      Every initial construction or transitive use a row names is a row of the same example.

                                                                                                                      theorem Creissels2024.rows_classified (row : Data.Examples.LinguisticExample) :
                                                                                                                      row Examples.allkrow.parse? "alternation" kindNames, initExamples.paired "initial" row, Kind.Realize (Examples.construction init) (Examples.construction row) k (row.parse? "new" slotNames)

                                                                                                                      Every derived construction of the book's examples realizes the type the book assigns it, relative to its initial construction.

                                                                                                                      theorem Creissels2024.symmetrical_rows (row : Data.Examples.LinguisticExample) :
                                                                                                                      row Examples.allrow.parse? "alternation" kindNames = some Kind.symmetricalinitExamples.paired "initial" row, prow.parse? "pivot" slotNames, qinit.parse? "pivot" slotNames, p q (Examples.construction row p).Expressed

                                                                                                                      A symmetrical voice selects a different, expressed participant as pivot.

                                                                                                                      Each substrate record with the book's initial and derived example of its type.

                                                                                                                      Equations
                                                                                                                      • One or more equations did not get rendered due to their size.
                                                                                                                      Instances For

                                                                                                                        The book's defining example of each type is described by the substrate's record of it.

                                                                                                                        Mandinka (13) of chapter 1: 'repair' takes A and P, 'forget' takes S and a postpositional oblique.

                                                                                                                        theorem Creissels2024.alignment_rows :
                                                                                                                        (∃ tExamples.coding "russ1263", Examples.sFlags "russ1263" [] ObligatoryACoding t (Examples.sFlags "russ1263")) (∃ tExamples.coding "avar1256", Examples.sFlags "avar1256" [] ObligatoryPCoding t (Examples.sFlags "avar1256")) tExamples.coding "basq1248", SplitS t (Examples.sFlags "basq1248")

                                                                                                                        Russian (23) is obligatory A-coding, Avar (24) obligatory P-coding, and Basque (22), with an ergative S beside a zero-flagged one, split-S and neither.

                                                                                                                        The uncoded alternations of Bambara (2), (3) and Basque (4), which the book calls P-ambitransitivity for Basque and describes in the same terms as the Tswana passive for Bambara, are P-ambitransitivity: the initial P is the S of an intransitive construction and the initial A is not a core term; Bambara's preserves participant structure, with the agent an optional oblique, and Basque's does not.

                                                                                                                        Tswana -w codes passivization, its impersonal variant and S-denucleativization; Tswana -ɛl codes P-applicativization, X-applicativization and the A-nucleativization of an oblique; Tswana -is codes causativization and, in chapter 12, portative derivation; Diré Songhay -ndi codes causativization and passivization.

                                                                                                                        theorem Creissels2024.stacking_tswana :
                                                                                                                        Relation.Comp (Relation.Comp (fun (x1 x2 : Construction (Fin 5)) => ANucleativization x1 x2 2) fun (x1 x2 : Construction (Fin 5)) => PApplicativization x1 x2 3) Passivization (Examples.construction Examples.ex_8_38a) (Examples.construction Examples.ex_8_38h)

                                                                                                                        Tswana (38): passivizing the applicative of the causative is the composite of the three alternations, through (38d) and (38e).

                                                                                                                        Classical Nahuatl (39): the passive of the antipassive of the causative, through (39b) and (39c).

                                                                                                                        Passivization need not yield an intransitive construction: the passive (38f) of the double-P applicative (38c) is transitive, the applied P taking A coding.

                                                                                                                        Portative derivation in Tswana (3) of chapter 12: the woman who brought the food came, and the food, which cannot come, is not the initial S.

                                                                                                                        Symmetrical voice systems (§8.5) #

                                                                                                                        Balinese (47): a binary symmetrical system, agent voice and patient voice.

                                                                                                                        Equations
                                                                                                                        Instances For

                                                                                                                          Tagalog (48): a multiple symmetrical system whose locative, conveyance and instrumental voices select an oblique as pivot; the substrate has no conveyance pivot, so the conveyance voice, whose pivot is a beneficiary or a displaced theme, is entered as benefactive.

                                                                                                                          Equations
                                                                                                                          • One or more equations did not get rendered due to their size.
                                                                                                                          Instances For