Documentation

Studies.Comrie1989

Comrie (1989): Language Universals and Linguistic Typology #

Three of the book's chapters make claims sharp enough to state. Case marking (chapter 6) serves first to discriminate the two arguments of a transitive clause: of the five ways the primitives S, A and P can share cases, only the nominative–accusative and ergative–absolutive systems keep A and P apart with two cases, which is why those two are the widespread ones, the tripartite system spending a case on a distinction it does not need and the neutral and the A/P-against-S systems failing to make the one that matters. The same function explains differential marking: the agent of a transitive clause is typically more animate and more definite than its patient, so marking is spent on the departures, a P high on the hierarchies or an A low on them, and each language's marking is monotone in prominence, Russian and Polish by animacy, Turkish and Persian by definiteness, Hindi and Spanish by both, Dyirbal marking its As downward and its Ps upward from the same cut between first and second person pronouns and the rest of the animacy hierarchy.

In causatives (chapter 8) the causee takes the highest position on the hierarchy subject > direct object > indirect object > oblique that the base verb's arguments leave free, as Turkish shows for intransitive, transitive and ditransitive bases; languages may in addition double a filled position, Sanskrit a direct object and Turkish an indirect object, or demote further than required, French by par, and the analysis of the oblique causee as a passive fails for Turkish, where passive applies to every transitive verb but the oblique causee only to ditransitive bases, and for Hungarian, which has an oblique causee and no passive expressing its agent in that case. Where a language offers two cases for the causee, the one lower on the hierarchy encodes the causee that retains more control, Hungarian instrumental over accusative, Japanese dative over accusative, Kannada instrumental over dative; and within a language the more compact a causative's form, the more direct the causation it expresses. Subject (chapter 5) is a prototype, the intersection of agent and topic, so that constructions tied to agents, such as imperative addressee deletion, group S with A even in Dyirbal, constructions tied to affected participants, such as the Nivkh resultative, group S with P, both as tendencies, and constructions tied to neither, such as coordination, vary: S with A in English, S with P in Dyirbal, neither in Chukchi.

The case systems are the equivalence relations on the three primitives, caseSystem_of_equivalence that the five are all of them and discriminates_two_case_iff that two of them are the economical discriminating ones; the book's examples are the rows, over which marking_monotone is the information-flow prediction, causee_rows and passive_analysis_fails the hierarchy against its rival, control_rows the control hierarchy, compactness_rows the directness correlation through the substrate's monotonicity, and bias_rows, coordination_rows and mixed_rows the prototype's predictions.

Implementation notes #

TODO #

References #

The discriminatory function of case (§6.1) #

The three primitives of case marking are the intransitive subject and the agent and patient of the transitive clause.

Instances For
    @[instance_reducible]
    Equations
    def Comrie1989.instReprPrimitive.repr :
    Primitive → ℕ → Std.Format
    Equations
    Instances For

      The five logically possible case systems, by which primitives share a case.

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

          Two primitives take the same case.

          Equations
          • c.Same x y = ∃ b ∈ c.blocks, x ∈ b ∧ y ∈ b
          Instances For
            @[instance_reducible]
            instance Comrie1989.instDecidableSame (c : CaseSystem) (x y : Primitive) :
            Decidable (c.Same x y)
            Equations
            • One or more equations did not get rendered due to their size.

            The number of cases.

            Equations
            Instances For

              The system discriminates the two arguments of a transitive clause.

              Equations
              Instances For
                @[instance_reducible]
                Equations
                theorem Comrie1989.caseSystem_of_equivalence (r : Primitive → Primitive → Prop) (h : Equivalence r) :
                ∃ (c : CaseSystem), ∀ (x y : Primitive), r x y ↔ c.Same x y

                Every equivalence relation on the primitives is one of the five systems.

                The systems that discriminate A from P are all but the neutral and the A/P-against-S ones.

                The systems discriminating A from P with two cases are the nominative–accusative and the ergative–absolutive ones, the widespread systems; the tripartite system marks S apart for no discriminatory gain.

                The rows #

                The rows the book accepts.

                Equations
                Instances For

                  Differential marking and the natural information flow (§6.2) #

                  The marking an argument's position takes is none, optional, or obligatory.

                  Instances For
                    @[instance_reducible]
                    Equations
                    @[instance_reducible]
                    Equations
                    def Comrie1989.instReprMarked.repr :
                    Marked → ℕ → Std.Format
                    Equations
                    Instances For

                      Optional marking sits between unmarked and marked.

                      Equations
                      Instances For
                        @[instance_reducible]
                        Equations

                        One argument's marking in a row records its role, the parameters the book invokes for the language, and the marking its position takes.

                        • role : Primitive

                          A or P; S, taking the unmarked case, has no row.

                        • person : Option Person.Class

                          Whether the argument is a speech-act participant, where the marking consults it.

                        • animacy : Option Reference.Animacy

                          The argument's animacy, where the marking consults it.

                        • definiteness : Option Reference.DefinitenessDegree

                          The argument's degree of definiteness, where the marking consults it.

                        • marked : Marked

                          The marking the position takes.

                        Instances For

                          The animacy labels of the rows, read as person and animacy apart, the parameters §9.4 separates: the speech-act participants are human, and the nouns are third person.

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

                            The markings a row records, one per argument whose marking it gives, under the key prefixes A. and P.; a row whose marking the book attributes to a parameter beside the hierarchies has none.

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

                              m₁ marks the same role as m₂ and is at most as prominent on every parameter both cite.

                              Equations
                              • One or more equations did not get rendered due to their size.
                              Instances For
                                @[instance_reducible]
                                instance Comrie1989.instDecidableAtMost (m₁ m₂ : Marking) :
                                Decidable (m₁.AtMost m₂)
                                Equations
                                • One or more equations did not get rendered due to their size.
                                theorem Comrie1989.marking_monotone (r₁ : Datum) :
                                r₁ ∈ acceptable → ∀ m₁ ∈ Marking.ofRow r₁, ∀ r₂ ∈ List.filter (fun (x : Datum) => decide (x.language = r₁.language)) acceptable, ∀ m₂ ∈ Marking.ofRow r₂, m₁.AtMost m₂ → (m₁.role = Primitive.P → m₁.marked ≤ m₂.marked) ∧ (m₁.role = Primitive.A → m₂.marked ≤ m₁.marked)

                                The information-flow prediction: within a language, the special case on P is monotone up the prominence scales and the special case on A monotone down them, (7)–(27) of chapter 6: Russian and Polish by animacy, Turkish and Persian by definiteness, Hindi and Spanish by both, and Dyirbal on both roles from the cut between first and second person pronouns and the rest of the hierarchy.

                                theorem Comrie1989.marking_contrast (role : Primitive) :
                                role ≠ Primitive.S → ∃ r₁ ∈ acceptable, ∃ r₂ ∈ acceptable, r₁.language = r₂.language ∧ ∃ m₁ ∈ Marking.ofRow r₁, ∃ m₂ ∈ Marking.ofRow r₂, m₁.role = role ∧ m₁.AtMost m₂ ∧ (role = Primitive.P → m₁.marked < m₂.marked) ∧ (role = Primitive.A → m₂.marked < m₁.marked)

                                The prediction has content in both directions, since some P is outranked by another of its language and carries less marking, and some A is outranked and carries more.

                                The causee hierarchy (§8.2) #

                                A language's departures from the paradigm case.

                                • The positions the language lets a causee double.

                                • extended : Bool

                                  Whether the causee may take a position below the paradigm one.

                                • passive : Bool

                                  Whether the language has a passive expressing its agent in the oblique case of the causee, which the rival analysis consults.

                                Instances For
                                  def Comrie1989.parameters :
                                  List (String × Parameters)

                                  Among the languages with causative rows, Turkish doubles indirect objects and never demotes further, Sanskrit doubles direct objects and demotes to the instrumental, French, Hungarian, Japanese and Kannada demote further, and Hungarian has no passive.

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

                                    A causative row's configuration is the base verb's valency, the causee's position, and the language's parameters.

                                    Instances For

                                      The configuration a causative or control row records.

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

                                        The paradigm position is the highest the base verb's arguments leave free.

                                        Equations
                                        Instances For

                                          The causee doubles a filled position the language permits.

                                          Equations
                                          Instances For
                                            @[instance_reducible]
                                            Equations

                                            The hierarchy analysis admits the causee's position in the paradigm case, in a doubled position, or in a lower one where the language demotes further.

                                            Equations
                                            Instances For
                                              @[instance_reducible]
                                              Equations

                                              The rival analysis takes the oblique causee as a passive agent, admitting the paradigm case, a doubled position, or the oblique of a transitive base wherever the language has a passive.

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

                                                The Turkish paradigm (12)–(16), the doubling of (17)–(18), the further demotion of (20) and of the control alternatives, and the exclusion of (22): the hierarchy with the language's parameters admits exactly the positions the languages accept.

                                                The passive analysis admits (22), the oblique causee of a transitive base in Turkish, which the language rejects although it passivizes every transitive verb, and excludes the instrumental causee of Hungarian (9), whose base is intransitive and whose language has no passive expressing the agent in that case.

                                                Whether a causee retains less or more control.

                                                Instances For
                                                  @[instance_reducible]
                                                  Equations
                                                  @[instance_reducible]
                                                  Equations
                                                  def Comrie1989.instReprControl.repr :
                                                  Control → ℕ → Std.Format
                                                  Equations
                                                  Instances For

                                                    A control row's configuration is the control the causee retains and its position.

                                                    Instances For

                                                      The configuration a control row records.

                                                      Equations
                                                      • One or more equations did not get rendered due to their size.
                                                      Instances For
                                                        theorem Comrie1989.control_rows :
                                                        (∀ r₁ ∈ Examples.all, ∀ c₁ ∈ Controlled.ofRow r₁, ∀ r₂ ∈ List.filter (fun (x : Datum) => decide (x.language = r₁.language)) Examples.all, ∀ c₂ ∈ Controlled.ofRow r₂, c₁.control = Control.less → c₂.control = Control.more → c₂.causee < c₁.causee) ∧ ∃ r₁ ∈ Examples.all, ∃ r₂ ∈ Examples.all, r₁.language = r₂.language ∧ ∃ c₁ ∈ Controlled.ofRow r₁, ∃ c₂ ∈ Controlled.ofRow r₂, c₁.control = Control.less ∧ c₂.control = Control.more

                                                        By the control hierarchy, (8)–(9) and (23)–(28), the causee retaining more control takes the position lower on the hierarchy within a language, and a language offers the pair.

                                                        Compactness and directness (§8.1) #

                                                        The causative construction a row records, its formal complexity and its mediation.

                                                        Equations
                                                        • One or more equations did not get rendered due to their size.
                                                        Instances For
                                                          theorem Comrie1989.compactness_rows :
                                                          (∀ r₁ ∈ Examples.all, ∀ c₁ ∈ CausativeConstruction.ofRow r₁, ∀ r₂ ∈ List.filter (fun (x : Datum) => decide (x.language = r₁.language)) Examples.all, ∀ c₂ ∈ CausativeConstruction.ofRow r₂, c₁.ComrieMonotone c₂) ∧ ∃ r₁ ∈ Examples.all, ∃ r₂ ∈ Examples.all, r₁.language = r₂.language ∧ ∃ c₁ ∈ CausativeConstruction.ofRow r₁, ∃ c₂ ∈ CausativeConstruction.ofRow r₂, c₁.complexity < c₂.complexity ∧ c₁.mediation < c₂.mediation

                                                          Within a language, the more compact causative is the more appropriate to direct causation, Nivkh (6)–(7) and the English broke ~ brought it about pair: the substrate's monotonicity on every pair of rows, and a pair strictly ordered on both scales.

                                                          Subject as a prototype (chapter 5) #

                                                          The argument of a transitive clause a construction groups with S is A, P, or neither, where either may be omitted.

                                                          Instances For
                                                            @[instance_reducible]
                                                            Equations
                                                            def Comrie1989.instReprGrouping.repr :
                                                            Grouping → ℕ → Std.Format
                                                            Equations
                                                            Instances For

                                                              The constructions tested.

                                                              Instances For
                                                                @[instance_reducible]
                                                                instance Comrie1989.instDecidableEqTest :
                                                                DecidableEq Test
                                                                Equations
                                                                def Comrie1989.instReprTest.repr :
                                                                Test → ℕ → Std.Format
                                                                Equations
                                                                Instances For
                                                                  @[instance_reducible]
                                                                  Equations
                                                                  @[instance_reducible]
                                                                  Equations

                                                                  The prototype predicts that a construction tied to agents, the deletion of an imperative's addressee or of the recipient of an indirect command, and a control complement such as the Chukchi infinitive construction, favour S with A; one tied to affected participants, the resultative, favours S with P; coordination, tied to neither, is free to vary (§5.3–§5.4).

                                                                  Equations
                                                                  Instances For

                                                                    A grouping row's configuration.

                                                                    • test : Test

                                                                      The construction.

                                                                    • grouping : Grouping

                                                                      The grouping it shows.

                                                                    Instances For

                                                                      The configuration a grouping row records.

                                                                      Equations
                                                                      • One or more equations did not get rendered due to their size.
                                                                      Instances For
                                                                        theorem Comrie1989.bias_rows :
                                                                        (∀ row ∈ Examples.all, ∀ g ∈ Grouped.ofRow row, g.test = Test.imperative → g.grouping = Grouping.withA) ∧ (∃ row ∈ Examples.all, ∃ g ∈ Grouped.ofRow row, g.test = Test.resultative ∧ g.grouping = Grouping.withP) ∧ ∀ (b : Grouping), b ≠ Grouping.neither → ∃ row ∈ Examples.all, ∃ g ∈ Grouped.ofRow row, g.test.bias = some b ∧ g.grouping ≠ b

                                                                        The imperative groups S with A in every language with rows, Dyirbal included, the Nivkh resultative groups S with P, and yet each bias is a tendency: the English resultative keeps its A, and Dyirbal's indirect commands, agent-tied like its imperatives, keep S with P.

                                                                        theorem Comrie1989.coordination_rows (gr : Grouping) :
                                                                        ∃ row ∈ Examples.all, ∃ g ∈ Grouped.ofRow row, g.test = Test.coordination ∧ g.grouping = gr

                                                                        Coordination, tied to neither prototype property, realizes every grouping, S with A in English, S with P in Dyirbal, and neither in Chukchi.

                                                                        theorem Comrie1989.mixed_rows :
                                                                        ∃ r₁ ∈ Examples.all, ∃ r₂ ∈ Examples.all, r₁.language = r₂.language ∧ ∃ g₁ ∈ Grouped.ofRow r₁, ∃ g₂ ∈ Grouped.ofRow r₂, g₁.grouping ≠ g₂.grouping

                                                                        A language can be mixed, as Chukchi's coordination restricts nothing while its infinitive construction groups S with A.