Documentation

Linglib.Syntax.Minimalist.Category.FunctionalSequence

The functional sequence #

This file defines the height of a category in the functional sequence and the families of extended projections. Grimshaw takes a clause or a noun phrase to be one extended projection, a lexical head together with the functional heads above it, all of one category family and with a functional level, the F-value, that does not decrease going up. The F-value of each category is a natural number, with the lexical heads at 0, and the four families, verbal, nominal, adjectival and adpositional, carry Chomsky's [±V, ±N] features, so that two categories share those features exactly when they are of one family. A category extends to another when the two are of one family and the second is at least as high; the extended projections are the chains of this relation.

Main definitions #

Main results #

Implementation notes #

The F-values place the families on one scale, n with v, Q with T, Num with Fin and D with Foc. Rizzi's order Fin < Foc < Top < Force fixes the verbal left periphery, Borer's individuation before counting puts Q below Num, the Say layer of embedded speech reports sits between Foc and C as in Egressy, and Speas and Tenny's speech-act head closes the verbal sequence. Prepositions form their own family, with den Dikken's Place and Path above them, following Chomsky's [−V, −N], whereas Grimshaw places P in the nominal extended projection.

References #

source
inductive Minimalist.CatFamily :
Type

The four families of extended projections, each anchored by a lexical category.

Instances For
    source
    @[instance_reducible]
    instance Minimalist.instDecidableEqCatFamily :
    DecidableEq CatFamily
    Equations
    source
    def Minimalist.instReprCatFamily.repr :
    CatFamily → ℕ → Std.Format
    Equations
    • One or more equations did not get rendered due to their size.
    Instances For
      source
      @[instance_reducible]
      instance Minimalist.instReprCatFamily :
      Repr CatFamily
      Equations
      source
      def Minimalist.Cat.family :
      Cat → CatFamily

      The family of a category, the extended projection it belongs to.

      Equations
      Instances For
        source
        structure Minimalist.CatFeatures :
        Type

        Chomsky's categorial features [±V, ±N], which cross-classify the four lexical categories: V is [+V, −N], N is [−V, +N], A is [+V, +N] and P is [−V, −N].

        • plusV : Bool
        • plusN : Bool
        Instances For
          source
          @[instance_reducible]
          instance Minimalist.instDecidableEqCatFeatures :
          DecidableEq CatFeatures
          Equations
          source
          def Minimalist.instDecidableEqCatFeatures.decEq (x✝ x✝¹ : CatFeatures) :
          Decidable (x✝ = x✝¹)
          Equations
          Instances For
            source
            def Minimalist.instReprCatFeatures.repr :
            CatFeatures → ℕ → Std.Format
            Equations
            • One or more equations did not get rendered due to their size.
            Instances For
              source
              @[instance_reducible]
              instance Minimalist.instReprCatFeatures :
              Repr CatFeatures
              Equations
              source
              def Minimalist.CatFamily.features :
              CatFamily → CatFeatures

              The features of a family are those of its lexical anchor.

              Equations
              Instances For
                source
                theorem Minimalist.CatFamily.features_injective :
                Function.Injective features
                source
                def Minimalist.Cat.features (c : Cat) :
                CatFeatures

                The features of a category are those of its family, so that every functional head inherits the features of its lexical anchor.

                Equations
                Instances For
                  source
                  theorem Minimalist.Cat.features_eq_iff {c d : Cat} :
                  c.features = d.features ↔ c.family = d.family
                  source
                  def Minimalist.Cat.fValue :
                  Cat → ℕ

                  The F-value of a category is its level in the functional sequence: lexical heads are at 0, categorizers at 1, the inflectional domain at 2 and the left periphery from 3 up, with the nominal and adpositional levels aligned to the verbal ones.

                  levelverbalnominaladjectivaladpositional
                  0VNAP
                  1v, Voice, ApplnaPlace
                  2T, Neg, Mod, Pol, Asp, EvidQPath
                  3Fin, NmlzNum
                  4FocD, Dem
                  5Top, Rel, SayK
                  6C, Force
                  7SA
                  Equations
                  Instances For
                    source
                    def Minimalist.Cat.ExtendsTo (c d : Cat) :
                    Prop

                    c.ExtendsTo d holds when d extends the projection of c, the two categories being of one family and d at least as high, so that the extended projections are the chains of this relation.

                    Equations
                    Instances For
                      source
                      @[instance_reducible]
                      instance Minimalist.instDecidableRelCatExtendsTo :
                      DecidableRel Cat.ExtendsTo
                      Equations
                      source
                      instance Minimalist.instIsPreorderCatExtendsTo :
                      IsPreorder Cat Cat.ExtendsTo