Documentation

Studies.Bobaljik2008

Bobaljik (2008): Where's Phi? Agreement as a Postsyntactic Operation #

This file formalizes the claim that the finite verb agrees with the highest accessible noun phrase in its domain, where accessibility is a matter of morphological case. The categories of morphological case are those of Marantz's realization hierarchy, and they are ordered for agreement the other way round: unmarked case is more accessible than dependent case, and dependent case more accessible than lexical case. A language chooses how far down this order its verb can see. Since morphological case is assigned after the syntax, agreement, which feeds on it, is postsyntactic as well.

Stated over case categories, Moravcsik's hierarchy of agreement controllers holds of ergative and accusative languages alike. It also explains a gap among the splits between case and agreement. An ergative case system gives absolutive agreement when only unmarked case is accessible and subject agreement when dependent case is accessible too, as in Nepali, while an accusative case system gives subject agreement at every setting. Ergative agreement over accusative case cannot be derived.

Main declarations #

Main results #

Implementation notes #

Case is assigned by the dependent case rules of Syntax/Case/Dependent.lean. Case valued by agreement with a functional head, which those rules also provide for, counts as unmarked.

References #

source
inductive Bobaljik2008.CaseCategory :
Type

The categories of morphological case, in their order of accessibility for agreement, with lexical case the least accessible and unmarked case the most.

Instances For
    source
    @[instance_reducible]
    instance Bobaljik2008.instDecidableEqCaseCategory :
    DecidableEq CaseCategory
    Equations
    source
    @[instance_reducible]
    instance Bobaljik2008.instReprCaseCategory :
    Repr CaseCategory
    Equations
    source
    def Bobaljik2008.instReprCaseCategory.repr :
    CaseCategory → ℕ → Std.Format
    Equations
    • One or more equations did not get rendered due to their size.
    Instances For
      source
      @[instance_reducible]
      instance Bobaljik2008.instFintypeCaseCategory :
      Fintype CaseCategory
      Equations
      • One or more equations did not get rendered due to their size.
      source
      @[instance_reducible]
      instance Bobaljik2008.CaseCategory.instLinearOrder :
      LinearOrder CaseCategory
      Equations
      source
      def Bobaljik2008.CaseCategory.ofMechanism :
      Case.Mechanism → CaseCategory

      The category of a case, by what valued it.

      Equations
      Instances For
        source
        theorem Bobaljik2008.isUpperSet_accessible (t : CaseCategory) :
        IsUpperSet {c : CaseCategory | t ≤ c}

        In a language whose least accessible category is t, the categories at or above t are accessible, so the accessible categories are closed upward.

        source
        def Bobaljik2008.controller {α : Type u_1} (t : CaseCategory) (domain : Case.Valuation α (Case × Case.Mechanism)) :
        Option ℕ

        The controller of agreement is the highest noun phrase of the domain whose case is accessible. Noun phrases whose case is not accessible are invisible and do not intervene.

        Equations
        • One or more equations did not get rendered due to their size.
        Instances For
          source
          def Bobaljik2008.controls (a : Alignment.AlignmentType) (t : CaseCategory) :
          ArgumentRole → Bool

          Whether an argument controls agreement in a clause of the given alignment, in a language whose least accessible category is t.

          Equations
          Instances For

            The predicted agreement alignments #

            source
            theorem Bobaljik2008.isAccusative_controls_accusative (t : CaseCategory) :
            Alignment.IsAccusative (controls Alignment.AlignmentType.accusative t)

            An accusative case system gives subject agreement at every setting.

            source
            theorem Bobaljik2008.isErgative_controls_ergative_unmarked :
            Alignment.IsErgative (controls Alignment.AlignmentType.ergative CaseCategory.unmarked)

            An ergative case system gives absolutive agreement when only unmarked case is accessible, as in Hindi.

            source
            theorem Bobaljik2008.isAccusative_controls_ergative_dependent :
            Alignment.IsAccusative (controls Alignment.AlignmentType.ergative CaseCategory.dependent)

            An ergative case system gives subject agreement when dependent case is accessible, as in Nepali.

            source
            theorem Bobaljik2008.not_isErgative_controls_accusative (t : CaseCategory) :
            ¬Alignment.IsErgative (controls Alignment.AlignmentType.accusative t)

            No setting derives ergative agreement from accusative case.

            Case against grammatical function #

            source
            theorem Bobaljik2008.controller_quirky (c : Case) (t : CaseCategory) (ht : t ≠ CaseCategory.lexical) :
            controller t (DependentCase.assignCases Alignment.AlignmentType.accusative (fun (r : ArgumentRole) => if r = ArgumentRole.A then some c else none) [ArgumentRole.A, ArgumentRole.P]) = some 1

            Below a subject with lexical case, as the dative subjects of Icelandic, the verb agrees with the nominative object unless lexical case is itself accessible.

            source
            theorem Bobaljik2008.hindi_controller :
            controller CaseCategory.unmarked (DependentCase.assignCases (HindiUrdu.alignment Aspect.Perfectivity.perfective) (fun (x : ArgumentRole) => none) [ArgumentRole.A, ArgumentRole.P]) = some 1 ∧ controller CaseCategory.unmarked (DependentCase.assignCases (HindiUrdu.alignment Aspect.Perfectivity.imperfective) (fun (x : ArgumentRole) => none) [ArgumentRole.A, ArgumentRole.P]) = some 0

            In the Hindi perfective the verb agrees with the unmarked object past the ergative subject, and in the imperfective with the subject.