Documentation

Linglib.Syntax.Minimalist.Feature.Basic

Features for Minimalist Agree #

A feature dimension is a kind of feature that Agree checks: an agreement dimension (Agreement.Dimension), one of Harbour's person or number features (Person.Feature, Number.Feature), or a Minimalist feature such as [±wh]. Each takes its values from the type that already owns it, so the person dimension here is the person of an agreement bundle, and Harbour's features are bivalent. A feature value is a dimension with a value in it, and two values share a dimension when their first components agree. A feature bundle assigns each dimension a three-state checking slot: absent, unvalued (a probe), or valued.

Interpretability is orthogonal to valuation. Chomsky's interpretable features contribute to LF (the φ-features of a noun, categorial features), and uninterpretable ones must be checked and deleted before it (the φ-features of T and v, the case of a noun); which a feature is depends on its host as well as its dimension.

Main definitions #

References #

source
inductive Minimalist.Infl :
Type

The inflectional feature [Infl] ([Bjo11]) is valued on the verb by the higher temporal or aspectual head that selects it, perf for a participle under Perf/Asp and impf under imperfective Asp.

Instances For
    source
    @[instance_reducible]
    instance Minimalist.instReprInfl :
    Repr Infl
    Equations
    source
    def Minimalist.instReprInfl.repr :
    Infl → ℕ → Std.Format
    Equations
    Instances For
      source
      @[instance_reducible]
      instance Minimalist.instDecidableEqInfl :
      DecidableEq Infl
      Equations

      Dimensions and values #

      source
      inductive Minimalist.FeatureType :
      Type

      The feature dimensions Agree checks are the agreement dimensions, Harbour's person and number features, and the Minimalist [±wh], [±tense], [Infl] and [obl].

      Instances For
        source
        def Minimalist.instReprFeatureType.repr :
        FeatureType → ℕ → Std.Format
        Equations
        • One or more equations did not get rendered due to their size.
        Instances For
          source
          @[instance_reducible]
          instance Minimalist.instReprFeatureType :
          Repr FeatureType
          Equations
          source
          def Minimalist.instDecidableEqFeatureType.decEq (x✝ x✝¹ : FeatureType) :
          Decidable (x✝ = x✝¹)
          Equations
          Instances For
            source
            @[instance_reducible]
            instance Minimalist.instDecidableEqFeatureType :
            DecidableEq FeatureType
            Equations
            source
            @[instance_reducible]
            instance Minimalist.instFintypeFeatureType :
            Fintype FeatureType
            Equations
            source
            @[reducible, match_pattern, inline]
            abbrev Minimalist.FeatureType.person :
            FeatureType

            person is the agreement dimension of person.

            Equations
            Instances For
              source
              @[reducible, match_pattern, inline]
              abbrev Minimalist.FeatureType.number :
              FeatureType

              number is the agreement dimension of number.

              Equations
              Instances For
                source
                @[reducible, match_pattern, inline]
                abbrev Minimalist.FeatureType.gender :
                FeatureType

                gender is the agreement dimension of gender.

                Equations
                Instances For
                  source
                  @[reducible, match_pattern, inline]
                  abbrev Minimalist.FeatureType.case :
                  FeatureType

                  case is the agreement dimension of case.

                  Equations
                  Instances For
                    source
                    @[reducible, match_pattern, inline]
                    abbrev Minimalist.FeatureType.participant :
                    FeatureType

                    participant is Harbour's [±participant].

                    Equations
                    Instances For
                      source
                      @[reducible, match_pattern, inline]
                      abbrev Minimalist.FeatureType.author :
                      FeatureType

                      author is Harbour's [±author].

                      Equations
                      Instances For
                        source
                        @[reducible, match_pattern, inline]
                        abbrev Minimalist.FeatureType.atomic :
                        FeatureType

                        atomic is Harbour's [±atomic].

                        Equations
                        Instances For
                          source
                          @[reducible, match_pattern, inline]
                          abbrev Minimalist.FeatureType.minimal :
                          FeatureType

                          minimal is Harbour's [±minimal].

                          Equations
                          Instances For
                            source
                            def Minimalist.FeatureType.all :
                            List FeatureType

                            All feature dimensions, for computable enumeration (Finset.univ.toList is noncomputable).

                            Equations
                            • One or more equations did not get rendered due to their size.
                            Instances For
                              source
                              theorem Minimalist.FeatureType.mem_all (t : FeatureType) :
                              t ∈ all

                              Every dimension is listed in all.

                              source
                              @[reducible]
                              def Minimalist.FeatureType.ValueOf :
                              FeatureType → Type

                              The value type of a dimension is that of the agreement dimension it is, [Infl]'s values, or Bool for the bivalent features.

                              Equations
                              Instances For
                                source
                                @[instance_reducible]
                                instance Minimalist.FeatureType.instDecidableEqValueOf (t : FeatureType) :
                                DecidableEq t.ValueOf
                                Equations
                                • One or more equations did not get rendered due to their size.
                                source
                                @[instance_reducible]
                                instance Minimalist.FeatureType.instReprValueOf (t : FeatureType) :
                                Repr t.ValueOf
                                Equations
                                • One or more equations did not get rendered due to their size.
                                source
                                @[reducible, inline]
                                abbrev Minimalist.FeatureVal :
                                Type

                                A feature value is a dimension with a value in it, written ⟨.person, .first⟩.

                                Equations
                                Instances For

                                  Feature bundles #

                                  A feature bundle is a total assignment from the dimensions to three-state checking slots (Minimalist.FeatureSlot), absent, unvalued or valued, after [MCB25], whose free-Merge core keeps the features of a syntactic object atomic, so the slots are an Agree-layer structure decoupled from the SyntacticObject carrier.

                                  source
                                  @[reducible, inline]
                                  abbrev Minimalist.FeatureBundle :
                                  Type

                                  A feature bundle assigns each dimension a checking slot.

                                  Equations
                                  Instances For
                                    source
                                    def Minimalist.FeatureBundle.hasValuedFeature (a : FeatureBundle) (t : FeatureType) :
                                    Bool

                                    The bundle has a valued feature of the given dimension.

                                    Equations
                                    Instances For
                                      source
                                      def Minimalist.FeatureBundle.hasUnvaluedFeature (a : FeatureBundle) (t : FeatureType) :
                                      Bool

                                      The bundle has an unvalued (probe) feature of the given dimension.

                                      Equations
                                      Instances For
                                        source
                                        def Minimalist.FeatureBundle.getValuedFeature (a : FeatureBundle) (t : FeatureType) :
                                        Option t.ValueOf

                                        The value at the given dimension, when valued.

                                        Equations
                                        Instances For
                                          source
                                          def Minimalist.FeatureBundle.single (t : FeatureType) (v : t.ValueOf) :
                                          FeatureBundle

                                          The assignment specifying exactly one valued dimension, all others absent.

                                          Equations
                                          Instances For
                                            source
                                            @[simp]
                                            theorem Minimalist.FeatureBundle.single_self (t : FeatureType) (v : t.ValueOf) :
                                            single t v t = FeatureSlot.valued v
                                            source
                                            def Minimalist.FeatureBundle.ofList (l : List ((t : FeatureType) × FeatureSlot t.ValueOf)) :
                                            FeatureBundle

                                            The bundle read off a list of slots, the list head winning on a repeated dimension.

                                            Equations
                                            • One or more equations did not get rendered due to their size.
                                            Instances For
                                              source
                                              @[simp]
                                              theorem Minimalist.FeatureBundle.ofList_nil :
                                              ofList [] = ⊥
                                              source
                                              def Minimalist.FeatureBundle.toList (b : FeatureBundle) :
                                              List ((t : FeatureType) × FeatureSlot t.ValueOf)

                                              The specified slots of a bundle, in FeatureType.all order.

                                              Equations
                                              Instances For
                                                source
                                                def Minimalist.FeatureBundle.valued (b : FeatureBundle) :
                                                List FeatureVal

                                                The valued features of a bundle, in FeatureType.all order.

                                                Equations
                                                Instances For
                                                  source
                                                  @[instance_reducible]
                                                  instance Minimalist.FeatureBundle.instInhabited :
                                                  Inhabited FeatureBundle

                                                  The everywhere-absent bundle is the default.

                                                  Equations
                                                  source
                                                  @[instance_reducible]
                                                  instance Minimalist.FeatureBundle.instDecidableEq :
                                                  DecidableEq FeatureBundle
                                                  Equations
                                                  source
                                                  @[instance_reducible]
                                                  instance Minimalist.FeatureBundle.instRepr :
                                                  Repr FeatureBundle

                                                  A bundle is rendered by its specified (non-absent) dimensions. The function carrier has no structural Repr, so containing structures that deriving Repr rely on this.

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

                                                  Interpretability #

                                                  source
                                                  inductive Minimalist.Interpretability :
                                                  Type

                                                  A feature is interpretable when it contributes to LF and uninterpretable when it must be checked and deleted before LF ([Cho95b]). The distinction is orthogonal to valuation: the φ-features of a noun are interpretable and valued, those of T and v uninterpretable and unvalued.

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