Documentation

Studies.BobaljikHarley2017

Bobaljik and Harley (2017): Suppletion is local: Evidence from Hiaki #

A trigger may condition the suppletion of a head only if no phrasal boundary separates them. In the first formulation the boundary is a maximal projection, and in the refined one any projection above the head level, so that a specifier is not local to its head either. Hiaki verbs supplete for the number of an argument, of the object of a transitive verb and of the subject of an intransitive one. Since an internal argument is base-generated as the sister of its Root, the object is local to the Root, while an external argument, in the specifier of VoiceP, is separated from it by the Root's own projection. The subjects that condition suppletion are therefore those of unaccusative verbs, which the applicative -ria, impossible without an agentive verb, confirms. The locality is structural rather than word-internal: within a complex head and with a sister phrase alike, conditioning is local exactly where no phrase intervenes.

The refined condition also decides between the configurations in which the internal argument is introduced. As the Root's sister it may condition the Root under both formulations. In the specifier of the categorizer that takes the Root as its complement, as in Embick's resultative participles, it may do so only under the first. Adjoined to a low functional projection above the Root, as van Craenenbroeck suggests, it may do so under neither, since the lower segment of that projection is already a maximal one.

Main statements #

Implementation notes #

TODO #

The typological survey of number-conditioned suppletion and the subject-conditioned transitive suppletives of Seri and Hiw, which the chapter leaves to further investigation, are not formalized.

References #

The configurations of the chapter #

source
inductive BobaljikHarley2017.Cat :
Type

The categories are two abstract ones for the schematic trees, the Root's own, Voice, the verbalizer, a low functional head, and determiner phrases.

Instances For
    source
    @[instance_reducible]
    instance BobaljikHarley2017.instDecidableEqCat :
    DecidableEq Cat
    Equations
    source
    @[instance_reducible]
    instance BobaljikHarley2017.instReprCat :
    Repr Cat
    Equations
    source
    def BobaljikHarley2017.instReprCat.repr :
    Cat → ℕ → Std.Format
    Equations
    Instances For
      source
      inductive BobaljikHarley2017.Word :
      Type

      The terminals are heads, phrases, Roots, DPs with their number, and the heads Voice, v and F.

      Instances For
        source
        def BobaljikHarley2017.instDecidableEqWord.decEq (x✝ x✝¹ : Word) :
        Decidable (x✝ = x✝¹)
        Equations
        Instances For
          source
          @[instance_reducible]
          instance BobaljikHarley2017.instDecidableEqWord :
          DecidableEq Word
          Equations
          source
          @[instance_reducible]
          instance BobaljikHarley2017.instReprWord :
          Repr Word
          Equations
          source
          def BobaljikHarley2017.instReprWord.repr :
          Word → ℕ → Std.Format
          Equations
          • One or more equations did not get rendered due to their size.
          Instances For
            source
            @[reducible, inline]
            abbrev BobaljikHarley2017.T :
            Type

            Trees over the chapter's categories.

            Equations
            Instances For
              source
              def BobaljikHarley2017.tree19 :
              T

              The schematic tree (19), a head with a specifier and a complement.

              Equations
              • One or more equations did not get rendered due to their size.
              Instances For
                source
                theorem BobaljikHarley2017.mayCondition_mayCondition'_tree19 :
                DistributedMorphology.MayCondition tree19 { toList := [1, 0] } { toList := [0] } ∧ DistributedMorphology.MayCondition tree19 { toList := [1, 0] } { toList := [1, 1] } ∧ ¬DistributedMorphology.MayCondition' tree19 { toList := [1, 0] } { toList := [0] } ∧ DistributedMorphology.MayCondition' tree19 { toList := [1, 0] } { toList := [1, 1] }

                Both arguments of a head are local to it under (1), only its complement under (1′) (19).

                source
                def BobaljikHarley2017.tree20 :
                T

                The schematic tree (20), a head with a specifier over a phrase whose head has a specifier and a complement.

                Equations
                • One or more equations did not get rendered due to their size.
                Instances For
                  source
                  theorem BobaljikHarley2017.mayCondition'_tree20 :
                  DistributedMorphology.MayCondition' tree20 { toList := [1, 1, 1, 0] } { toList := [1, 1, 1, 1] } ∧ ¬DistributedMorphology.MayCondition' tree20 { toList := [1, 1, 1, 0] } { toList := [1, 1, 0] } ∧ ¬DistributedMorphology.MayCondition' tree20 { toList := [1, 1, 1, 0] } { toList := [0] } ∧ ¬DistributedMorphology.MayCondition' tree20 { toList := [1, 1, 1, 0] } { toList := [1, 0] }

                  Of the phrases of (20) only the complement of Y⁰ may condition it under (1′), and the higher head X⁰ may not either.

                  Hiaki clauses #

                  source
                  def BobaljikHarley2017.rootP (c : Clause.Arguments Number) :
                  T

                  The Root's projection, the internal argument base-generated as the Root's sister (13).

                  Equations
                  • One or more equations did not get rendered due to their size.
                  Instances For
                    source
                    def BobaljikHarley2017.clause (c : Clause.Arguments Number) :
                    T

                    The clause, VoiceP over the Root's projection, the external argument in its specifier (14).

                    Equations
                    • One or more equations did not get rendered due to their size.
                    Instances For
                      source
                      def BobaljikHarley2017.rootPos (c : Clause.Arguments Number) :
                      Core.Order.TreePath

                      The position of the Root in the clause.

                      Equations
                      • One or more equations did not get rendered due to their size.
                      Instances For
                        source
                        def BobaljikHarley2017.localNumbers (t : T) (α : Core.Order.TreePath) :
                        List Number

                        The numbers of the DPs that may condition the head at α under (1′).

                        Equations
                        • One or more equations did not get rendered due to their size.
                        Instances For
                          source
                          theorem BobaljikHarley2017.localNumbers_clause (c : Clause.Arguments Number) :
                          localNumbers (clause c) (rootPos c) = (c ArgumentStructure.ArgPosition.internal).toList

                          Only the internal argument is local to the Root. Whatever arguments a Hiaki clause has, the numbers that may condition its Root are exactly that of its internal argument.

                          source
                          def BobaljikHarley2017.structuralSite (c : Clause.Arguments Number) (r : DistributedMorphology.Root) :
                          DistributedMorphology.Neighborhood (List Harley2014.SiteFeature)

                          The context that locality gives a Root's Vocabulary Items, its index and the numbers local to it.

                          Equations
                          • One or more equations did not get rendered due to their size.
                          Instances For
                            source
                            theorem BobaljikHarley2017.structuralSite_eq_site (c : Clause.Arguments Number) (r : DistributedMorphology.Root) :
                            structuralSite c r = Harley2014.site c r

                            The context locality gives a Root is the one Harley's site stipulates, so Hiaki suppletion is spelled out over the context that (1′) delivers.

                            source
                            theorem BobaljikHarley2017.spellout_eq (c : Clause.Arguments Number) (r : DistributedMorphology.Root) :
                            Harley2014.spellout c r = DistributedMorphology.subsetPrinciple Harley2014.vocabulary (structuralSite c r)
                            source
                            def BobaljikHarley2017.moveToVoice (c : Clause.Arguments Number) :
                            T

                            Head movement of the Root to Voice adjoins the Root to Voice, leaving a trace.

                            Equations
                            • One or more equations did not get rendered due to their size.
                            Instances For
                              source
                              theorem BobaljikHarley2017.mayCondition_moveToVoice (e : Number) :
                              DistributedMorphology.MayCondition (moveToVoice (Clause.Arguments.unergative e)) { toList := [1, 1, 0] } { toList := [0] } ∧ ¬DistributedMorphology.MayCondition' (moveToVoice (Clause.Arguments.unergative e)) { toList := [1, 1, 0] } { toList := [0] }

                              Moved to Voice, the Root is separated from the external argument by no maximal projection, so (1) would let an external argument condition it; (1′) does not, since Voice′ is phrasal.

                              The applicative diagnostic #

                              source
                              inductive BobaljikHarley2017.VerbClass :
                              Type

                              The classes of the applicative examples.

                              Instances For
                                source
                                @[instance_reducible]
                                instance BobaljikHarley2017.instDecidableEqVerbClass :
                                DecidableEq VerbClass
                                Equations
                                source
                                def BobaljikHarley2017.instReprVerbClass.repr :
                                VerbClass → ℕ → Std.Format
                                Equations
                                • One or more equations did not get rendered due to their size.
                                Instances For
                                  source
                                  @[instance_reducible]
                                  instance BobaljikHarley2017.instReprVerbClass :
                                  Repr VerbClass
                                  Equations
                                  source
                                  def BobaljikHarley2017.ApplicativeLicensed (c : Clause.Arguments Number) :
                                  Prop

                                  The applicative -ria needs an agentive verb, a clause with an external argument.

                                  Equations
                                  Instances For
                                    source
                                    @[instance_reducible]
                                    instance BobaljikHarley2017.instDecidableApplicativeLicensed (c : Clause.Arguments Number) :
                                    Decidable (ApplicativeLicensed c)
                                    Equations
                                    source
                                    def BobaljikHarley2017.VerbClass.frame (s : Clause.Arguments Number) :
                                    VerbClass → Clause.Arguments Number

                                    The argument frame of each class, given the frame of the suppletive intransitives.

                                    Equations
                                    Instances For
                                      source
                                      def BobaljikHarley2017.classTable :
                                      List (String × VerbClass)

                                      The classes as named in the rows.

                                      Equations
                                      • One or more equations did not get rendered due to their size.
                                      Instances For
                                        source
                                        def BobaljikHarley2017.applicativeRows :
                                        List (VerbClass × Judgment)

                                        The applicative examples with a suffixed -ria, by their verb class and judgment.

                                        Equations
                                        • One or more equations did not get rendered due to their size.
                                        Instances For
                                          source
                                          def BobaljikHarley2017.Fits (s : Clause.Arguments Number) :
                                          Prop

                                          A frame for the suppletive intransitives fits the rows when every suffixed applicative is acceptable exactly where its frame is agentive.

                                          Equations
                                          Instances For
                                            source
                                            @[instance_reducible]
                                            instance BobaljikHarley2017.instDecidableFits (s : Clause.Arguments Number) :
                                            Decidable (Fits s)
                                            Equations
                                            • One or more equations did not get rendered due to their size.
                                            source
                                            theorem BobaljikHarley2017.length_applicativeRows :
                                            applicativeRows.length = 5
                                            source
                                            theorem BobaljikHarley2017.frame_eq_unaccusative (n : Number) :
                                            Fits (Clause.Arguments.unaccusative n) ∧ ¬Fits (Clause.Arguments.unergative n)

                                            Of the single-argument frames only the unaccusative one fits the applicative rows, so the suppletive intransitives are unaccusative and their subjects internal arguments, local to the Root (16).

                                            The configurations of an internal argument #

                                            source
                                            inductive BobaljikHarley2017.Configuration :
                                            Type

                                            An internal argument is introduced as the Root's sister, in the specifier of the categorizer that takes the Root as its complement, or adjoined to a low functional projection over the Root.

                                            Instances For
                                              source
                                              @[instance_reducible]
                                              instance BobaljikHarley2017.instDecidableEqConfiguration :
                                              DecidableEq Configuration
                                              Equations
                                              source
                                              def BobaljikHarley2017.instReprConfiguration.repr :
                                              Configuration → ℕ → Std.Format
                                              Equations
                                              • One or more equations did not get rendered due to their size.
                                              Instances For
                                                source
                                                @[instance_reducible]
                                                instance BobaljikHarley2017.instReprConfiguration :
                                                Repr Configuration
                                                Equations
                                                source
                                                def BobaljikHarley2017.Configuration.tree (n : Number) :
                                                Configuration → T

                                                The tree of a configuration with the internal argument of number n, the Root at position [1, 1] in the last two and [1] in the first.

                                                Equations
                                                • One or more equations did not get rendered due to their size.
                                                Instances For
                                                  source
                                                  def BobaljikHarley2017.Configuration.rootPos :
                                                  Configuration → Core.Order.TreePath

                                                  The position of the Root in a configuration.

                                                  Equations
                                                  Instances For
                                                    source
                                                    theorem BobaljikHarley2017.mayCondition'_iff_configuration (n : Number) (k : Configuration) :
                                                    DistributedMorphology.MayCondition' (Configuration.tree n k) k.rootPos { toList := [0] } ↔ k = Configuration.sister

                                                    Under (1′) the internal argument may condition the Root only as its sister.

                                                    source
                                                    theorem BobaljikHarley2017.mayCondition_iff_configuration (n : Number) (k : Configuration) :
                                                    DistributedMorphology.MayCondition (Configuration.tree n k) k.rootPos { toList := [0] } ↔ k ≠ Configuration.lowAdjunct

                                                    Under (1) the internal argument may condition the Root as its sister and as the specifier of the categorizer, but not adjoined to a low projection, whose lower segment is maximal.