Documentation

Studies.Audring2019

Audring (2019): Mothers or sisters? The encoding of morphological knowledge #

This file formalizes Audring's division of labour between mother schemas and sister links in a full-entry lexicon. A generalization over stored words can be encoded by a mother schema dominating them or by sister links, coindices between the words themselves. A sister link is a subscripting through which the pair of words factors, so it captures relations of sameness: boyish and childish are sisters at the affix (ish_affix_sisters) but cannot be coindexed at the base, where their fillers differ (not_base_sisters). The mother [N -ish]A of (8) relates every member of the family through one variable (ishSchema_relates), which is what states that different bases serve the same function. The mother also carries productivity: it generates Trumpish over an empty lexicon (ishSchema_generates_trumpish), whereas a fully specified word generates nothing but itself (word_generates_iff).

The second-order schema [N -ful]A ≈ [N -less]A of (14) is a sister link between mother schemas, one description over a shared base variable read through two subscriptings. The coindexed base pairs careful with careless and not with clueless (careful_careless_pairs, not_careful_clueless_pairs). A mother of the two schemas would be the meet of their descriptions, which over these slots is empty (fulLess_mother_eq_bot) and so is instantiated by every word (fulLess_mother_instantiates): it states nothing the sisters do not, and cannot state the pairing they do.

Implementation notes #

References #

source
def Audring2019.word (b a : String) :
Fin 2 → Flat String

A word with base b and affix a over the two slots base and affix.

Equations
Instances For
    source
    def Audring2019.ishSchema :
    ConstructionMorphology.Schema (Fin 2) (Flat String)

    The mother schema [N -ish]A of (8) has its affix pinned and its base an open variable.

    Equations
    Instances For
      source
      def Audring2019.ishFamily :
      Set (Fin 2 → Flat String)

      The stored family of (8).

      Equations
      Instances For
        source
        theorem Audring2019.ishSchema_instantiates {w : Fin 2 → Flat String} (h : w 1 = ↑"ish") :
        ishSchema.Instantiates w

        Any word whose affix is -ish instantiates the mother.

        source
        theorem Audring2019.ish_affix_sisters :
        Function.FactorsThrough (Sum.elim Forms.boyish.slots Forms.childish.slots) affixLink

        boyish and childish are sisters at the affix, since the pair factors through the link.

        source
        theorem Audring2019.not_base_sisters :
        ¬Function.FactorsThrough (Sum.elim Forms.boyish.slots Forms.childish.slots) baseLink

        boyish and childish cannot be coindexed at the base. The relation between boy and child is equivalence of function, not sameness, and no sister link states it.

        source
        theorem Audring2019.ishSchema_relates {w : Fin 2 → Flat String} (hw : w ∈ ishFamily) :
        ishSchema.Relates ishFamily w

        The mother relates every member of the family through its one variable.

        source
        theorem Audring2019.ishSchema_isProductive :
        ishSchema.IsProductive

        The mother is productive, since its one variable is open.

        source
        theorem Audring2019.ishSchema_generates_trumpish :
        ishSchema.Generates ∅ Forms.trumpish.slots

        The mother generates the novel Trumpish with nothing stored.

        source
        theorem Audring2019.word_generates_iff (b a : String) {Λ : Set (Fin 2 → Flat String)} {w : Fin 2 → Flat String} :
        { body := word b a, opens := ∅ }.Generates Λ w ↔ w = word b a

        A fully specified word, taken as a schema, generates nothing but itself. A sister link between stored words therefore licenses no novel word, and productivity needs a mother's variable.

        The second-order schema [N -ful]A ≈ [N -less]A #

        source
        inductive Audring2019.FulLessVar :
        Type

        The variables of (14) are the base shared by the two schemas and the two affixes.

        Instances For
          source
          @[instance_reducible]
          instance Audring2019.instDecidableEqFulLessVar :
          DecidableEq FulLessVar
          Equations
          source
          def Audring2019.fulLess :
          ConstructionMorphology.Schema FulLessVar (Flat String)

          The second-order schema (14) is the two schemas with their coindexed base as one description.

          Equations
          • One or more equations did not get rendered due to their size.
          Instances For
            source
            def Audring2019.fulSub :
            Fin 2 → FulLessVar

            The subscripting of the slots of [N -ful]A by the variables of (14).

            Equations
            Instances For
              source
              def Audring2019.lessSub :
              Fin 2 → FulLessVar

              The subscripting of the slots of [N -less]A by the variables of (14).

              Equations
              Instances For
                source
                def Audring2019.fulSchema :
                ConstructionMorphology.Schema (Fin 2) (Flat String)

                The schema [N -ful]A is the description of (14) read at its own slots.

                Equations
                Instances For
                  source
                  def Audring2019.lessSchema :
                  ConstructionMorphology.Schema (Fin 2) (Flat String)

                  The schema [N -less]A is the description of (14) read at its own slots.

                  Equations
                  Instances For
                    source
                    def Audring2019.fulLessWord (b : String) :
                    FulLessVar → Flat String

                    The variables of (14) filled by base b.

                    Equations
                    Instances For
                      source
                      theorem Audring2019.careful_careless_pairs :
                      fulLess.InstantiatesAt (Sum.elim fulSub lessSub) (Sum.elim Forms.careful.slots Forms.careless.slots)

                      careful and careless are a paired instantiation of (14), with the same base and sister affixes.

                      source
                      theorem Audring2019.not_careful_clueless_pairs :
                      ¬fulLess.InstantiatesAt (Sum.elim fulSub lessSub) (Sum.elim Forms.careful.slots Forms.clueless.slots)

                      careful and clueless are not a paired instantiation, since the coindexed base is filled differently.

                      source
                      theorem Audring2019.fulLess_mother_eq_bot :
                      fulSchema.body ⊓ lessSchema.body = ⊥

                      A mother of the two schemas would be the meet of their descriptions, which over these slots is empty. It holds nothing but the categories, which the slots do not record.

                      source
                      theorem Audring2019.fulLess_mother_instantiates (w : Fin 2 → Flat String) :
                      { body := fulSchema.body ⊓ lessSchema.body, opens := ∅ }.Instantiates w

                      The mother is instantiated by every word, so it states nothing the sisters do not.