Documentation

Studies.Song1996

Song (1996): Causatives and causation #

[Son96] classifies causative constructions by what joins the expression of cause to the expression of effect. In the COMPACT type [Vcause] and [Veffect] share one clause, fused (English kill), bound (Turkish öl-dür) or free (French faire lire); in the AND type a clause of cause and a clause of effect are coordinated, in that order (Vata le); in the PURP type the clause of effect is a clause of purpose (Korean -ke) (chapter 2). The traditional typology, lexical, morphological and syntactic, splits the COMPACT type and lumps the other two together (§1.2). The COMPACT type being the diachronic residue of the other two, what distinguishes those is implicativity: the AND type expresses the EVENT and RESULT stages of the cognitive structure of causation GOAL → EVENT → RESULT and entails its effect, the PURP type expresses GOAL and EVENT and does not, except through the inference that people realize the goals they act for (chapter 5). The grammatical relation of the causee follows no hierarchy of its own: a language caps the core NPs of a simplex clause, causative or not, and its causatives keep within the cap (chapter 6).

Form.type computes the type of a form and Form.traditional its traditional class, and on Song's examples neither classification refines the other (not_factorsThrough_type, not_factorsThrough_traditional). A biclausal type entails its effect in every model exactly when it expresses RESULT (forall_meaning_subset_iff), so the AND type is implicative and the PURP type is not (and_meaning_subset, purp_not_implicative), as the example (7) bears out (effectNegated_rows), while COMPACT causatives go either way (compact_implicativity_varies); the success assumption restores implicativity (meaning_subset_of_success). The paradigm causative of [Com89]'s case hierarchy never has more than three core NPs (paradigmCoreNPs_le_three), so a language capped at two refutes the hierarchy for transitive bases (paradigmCoreNPs_two).

Implementation notes #

TODO #

References #

Forms and types (chapter 2) #

How [Vcause] is realized in a one-clause causative (§2.3): fused with [Veffect] beyond morphological analysis (English kill), bound to it (Turkish -dür), or a free verb beside it (French faire).

Instances For
    @[instance_reducible]
    Equations
    def Song1996.instReprVcause.repr :
    Vcause → ℕ → Std.Format
    Equations
    Instances For
      @[instance_reducible]
      Equations
      @[instance_reducible]
      Equations
      def Song1996.instReprLink.repr :
      Link → ℕ → Std.Format
      Equations
      Instances For

        The order of the clause of cause and the clause of effect.

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

            A causative construction's form in Song's operating terms (§2.2): [Vcause] and [Veffect] in one clause, or a clause of cause and a clause of effect joined by a link.

            Instances For
              def Song1996.instDecidableEqForm.decEq (x✝ x✝¹ : Form) :
              Decidable (x✝ = x✝¹)
              Equations
              Instances For
                @[instance_reducible]
                Equations
                def Song1996.instReprForm.repr :
                Form → ℕ → Std.Format
                Equations
                • One or more equations did not get rendered due to their size.
                Instances For

                  The three types of causative construction; the names are mnemonic (p. 9).

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

                      The type of a form, by the schemas (3), (29) and (60): one clause is COMPACT whatever the order of [Vcause] and [Veffect]; a clause of purpose makes PURP in either order of the clauses; coordinated clauses make AND only with the clause of cause first, their order being fixed (p. 35).

                      Equations
                      Instances For

                        The COMPACT type is the traditional lexical and morphological types together (p. 9).

                        def Song1996.Form.ofRow (e : Datum) :
                        Option Form

                        The form of an example, as Song describes it.

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

                          Song's typology does not refine the traditional one: English kill (1.b) and Turkish öl-dür (2.b) are both COMPACT, the one lexical and the other morphological (pp. 3, 9).

                          The traditional typology does not refine Song's: Vata le (5) and Korean -ke (3.b) are both syntactic, the one AND and the other PURP (p. 10).

                          Implicativity and the cognitive structure of causation (chapter 5) #

                          inductive Song1996.Stage :

                          The stages of the cognitive structure of causation, in their temporal order (10): the perception of a desire or wish (GOAL), the deliberate attempt to realize it (EVENT), and its accomplishment (RESULT).

                          Instances For
                            @[instance_reducible]
                            instance Song1996.instDecidableEqStage :
                            DecidableEq Stage
                            Equations
                            def Song1996.instReprStage.repr :
                            Stage → ℕ → Std.Format
                            Equations
                            Instances For
                              @[instance_reducible]
                              Equations
                              @[instance_reducible]
                              Equations
                              def Song1996.Stage.prop {W : Type u_1} (goal event effect : Set W) :
                              Stage → Set W

                              The proposition a stage contributes, given the causer's goal that the effect come about, the causing event, and the effect.

                              Equations
                              Instances For

                                The semantic structure of the type a link forms (11): EVENT and RESULT for the AND type, GOAL and EVENT for the PURP type.

                                Equations
                                Instances For
                                  def Song1996.Link.meaning {W : Type u_1} (l : Link) (goal event effect : Set W) :
                                  Set W

                                  What a biclausal causative asserts: every stage its semantic structure expresses.

                                  Equations
                                  Instances For

                                    Both types express the causer's attempt, without which there is no causation (pp. 142–143).

                                    theorem Song1996.forall_meaning_subset_iff (l : Link) :
                                    (∀ (W : Type) (goal event effect : Set W), l.meaning goal event effect ⊆ effect) ↔ Stage.result ∈ l.stages

                                    A biclausal type entails its effect in every model exactly when it expresses RESULT: the AND type's clause of effect is factual, the PURP type's only a goal (p. 142).

                                    theorem Song1996.and_meaning_subset {W : Type u_1} (goal event effect : Set W) :
                                    Link.and_.meaning goal event effect ⊆ effect

                                    The AND type is fully implicative (p. 136).

                                    theorem Song1996.purp_not_implicative :
                                    ¬∀ (W : Type) (goal event effect : Set W), Link.purp.meaning goal event effect ⊆ effect

                                    The prototypical PURP type is nonimplicative (p. 136).

                                    theorem Song1996.meaning_subset_of_success {W : Type u_1} (l : Link) {goal event effect : Set W} (h : goal ∩ event ⊆ effect) :
                                    l.meaning goal event effect ⊆ effect

                                    Implicativity restored (§5.4): under the assumption (19) that people generally succeed in realizing the goals they act for, a causative of either type entails its effect, the PURP type by the inference from (20) to (21).

                                    theorem Song1996.effectNegated_rows (e : Datum) :
                                    e ∈ Examples.all → e.feature? "effect" = some "negated" → ∀ (l : Link) (o : ClauseOrder), Form.ofRow e = some (Form.twoClauses l o) → (e.judgment = Judgment.acceptable ↔ Stage.result ∉ l.stages)

                                    Song's diagnostic on his biclausal examples: denying the effect is acceptable exactly when the link's semantic structure lacks RESULT, as for the PURP causative (7) (pp. 12–13).

                                    theorem Song1996.compact_implicativity_varies :
                                    ∃ e₁ ∈ Examples.all, ∃ e₂ ∈ Examples.all, e₁.feature? "effect" = some "negated" ∧ e₂.feature? "effect" = some "negated" ∧ (Form.ofRow e₁).bind Form.type = some CausativeType.compact ∧ (Form.ofRow e₂).bind Form.type = some CausativeType.compact ∧ e₁.judgment = Judgment.ungrammatical ∧ e₂.judgment = Judgment.acceptable

                                    Compactness does not settle implicativity (§2.6; Figure 5.2, points A and B): denying the effect of a COMPACT causative is contradictory for English kill (6) and acceptable for the Kammu p- causative (104).

                                    NP density control and the case hierarchy (chapter 6) #

                                    def Song1996.paradigmCoreNPs (v : ℕ) :
                                    ℕ

                                    The core NPs of the paradigm causative of [Com89]'s case hierarchy on a base of valency v: the causer, the base's other arguments keeping their relations, and the causee unless the hierarchy makes it an oblique, which is no core NP (p. 178).

                                    Equations
                                    Instances For
                                      theorem Song1996.paradigmCoreNPs_le_three {v : ℕ} (hv : v ∈ Set.Icc 1 3) :

                                      The paradigm causative of an intransitive, transitive or ditransitive base never has more than three core NPs: it keeps within the cap of three that Song finds in languages causativizing transitive bases (p. 175).

                                      In a language capped at two core NPs, such as Lamang, Uradhi or Urubu-Kaapor, the paradigm causative of a transitive base, with its causee an indirect object, exceeds the cap: such a language has no morphological causative of transitives (§6.4, p. 174).

                                      theorem Song1996.isLowerSet_setOf_add_one_le (n : ℕ) :
                                      IsLowerSet {v : ℕ | v + 1 ≤ n}

                                      Under a cap of n core NPs, the bases whose morphological causative stays within it form a lower set of valencies: productivity declines from intransitive to transitive to ditransitive bases (p. 172).