Documentation

Linglib.Semantics.ArgumentStructure.AuxiliarySelection

Perfect-auxiliary selection (be/have) #

[Bur86] [Sor00]

The be/have perfect-auxiliary selection typology: many European languages select between be and have as the perfect auxiliary by the transitivity/ unaccusativity class of the lexical verb (the Auxiliary Selection Hierarchy): unaccusatives → be (Italian è arrivato, French est arrivé), unergatives/transitives → have (Italian ha mangiato). English has collapsed the split (all verbs take have). Graduated from the dissolved Typology/ drawer; the orthogonal AVC inflection typology split off to Syntax/AuxiliaryVerbs.lean.

Main definitions #

Implementation note #

selection flattens [Sor00]'s Auxiliary Selection Hierarchy (a 7-class semantic gradient with per-language cutoffs) to a 4-class enum keyed on a single reflexive parameter. A faithful graded scale, derived from Semantics/ArgumentStructure/EntailmentProfile.lean's proto-role predicates, is the documented successor (it would discharge Studies/Sorace2000's standing TODO).

source
inductive ArgumentStructure.AuxiliarySelection.PerfectAux :
Type

Perfect auxiliary choice.

Instances For
    source
    @[implicit_reducible]
    instance ArgumentStructure.AuxiliarySelection.instDecidableEqPerfectAux :
    DecidableEq PerfectAux
    Equations
    source
    @[implicit_reducible]
    instance ArgumentStructure.AuxiliarySelection.instReprPerfectAux :
    Repr PerfectAux
    Equations
    source
    def ArgumentStructure.AuxiliarySelection.instReprPerfectAux.repr :
    PerfectAux → Nat → Std.Format
    Equations
    • One or more equations did not get rendered due to their size.
    Instances For
      source
      inductive ArgumentStructure.AuxiliarySelection.TransitivityClass :
      Type

      Transitivity class relevant to auxiliary selection.

      Instances For
        source
        @[implicit_reducible]
        instance ArgumentStructure.AuxiliarySelection.instDecidableEqTransitivityClass :
        DecidableEq TransitivityClass
        Equations
        source
        def ArgumentStructure.AuxiliarySelection.instReprTransitivityClass.repr :
        TransitivityClass → Nat → Std.Format
        Equations
        • One or more equations did not get rendered due to their size.
        Instances For
          source
          @[implicit_reducible]
          instance ArgumentStructure.AuxiliarySelection.instReprTransitivityClass :
          Repr TransitivityClass
          Equations
          source
          inductive ArgumentStructure.AuxiliarySelection.SelectionRule :
          Type

          Language-level auxiliary selection rule.

          Instances For
            source
            @[implicit_reducible]
            instance ArgumentStructure.AuxiliarySelection.instDecidableEqSelectionRule :
            DecidableEq SelectionRule
            Equations
            source
            @[implicit_reducible]
            instance ArgumentStructure.AuxiliarySelection.instReprSelectionRule :
            Repr SelectionRule
            Equations
            source
            def ArgumentStructure.AuxiliarySelection.instReprSelectionRule.repr :
            SelectionRule → Nat → Std.Format
            Equations
            • One or more equations did not get rendered due to their size.
            Instances For
              source
              def ArgumentStructure.AuxiliarySelection.selection (reflexIsBe : Bool) :
              TransitivityClass → PerfectAux

              Auxiliary selection driven by a single binary parameter: does the language treat reflexives as BE-selecting (Romance pattern) or HAVE-selecting (German pattern)? In this coarse 4-class model unaccusatives select BE and unergatives/transitives select HAVE, with the reflexive row the locus of cross-linguistic variation ([Bur86] for the Italian generalization; [Sor00] for the cross-linguistic split).

              Equations
              Instances For
                source
                def ArgumentStructure.AuxiliarySelection.canonicalSelection :
                TransitivityClass → PerfectAux

                Canonical (Romance) auxiliary selection: reflexives → be.

                Equations
                Instances For
                  source
                  def ArgumentStructure.AuxiliarySelection.germanSelection :
                  TransitivityClass → PerfectAux

                  German auxiliary selection: reflexives → haben, not sein — the Romance-vs-German reflexive contrast of [Sor00].

                  Equations
                  Instances For
                    source
                    def ArgumentStructure.AuxiliarySelection.SelectionRule.selects (reflexIsBe : Bool) :
                    SelectionRule → TransitivityClass → Option PerfectAux

                    The auxiliary a selection rule assigns to each transitivity class: split follows selection, haveOnly/beOnly are constant (English has arrived), and mixed systems make no categorical assignment.

                    Equations
                    Instances For
                      source
                      def ArgumentStructure.AuxiliarySelection.SelectsBe (c : TransitivityClass) :
                      Prop

                      Does this transitivity class canonically select be? Defined off canonicalSelection so the equivalence is true by construction.

                      Equations
                      Instances For
                        source
                        @[implicit_reducible]
                        instance ArgumentStructure.AuxiliarySelection.instDecidablePredTransitivityClassSelectsBe :
                        DecidablePred SelectsBe
                        Equations