Documentation

Linglib.Morphology.Word.UD

Universal Dependencies annotation of tokens #

The bridge between the analytical inventories of person, number, gender and case and the tags treebanks annotate. Each inventory realizes as a tag where one exists and each tag ingests as a value: person's clusivity has no tag and collapses to the first person, so ingestion after realization is coarsening; number's minimal, augmented and general values have no tag, and the inverse, collective and count tags no value; the animacy genders have no tag. A token's features realize as an annotation record and an annotation ingests as features, and an annotation ingests as an agreement bundle.

Main declarations #

References #

Person #

source
def Person.toUD :
Person → UD.Person

Realize as an annotation: clusivity collapses to the first person.

Equations
Instances For
    source
    def Person.fromUD :
    UD.Person → Option Person

    Ingest an annotation; the impersonal Person=0 is the absence of a person.

    Equations
    Instances For
      source
      theorem Person.fromUD_toUD (p : Person) :
      fromUD p.toUD = some p.coarsen

      Realization is a partial inverse of ingestion up to clusivity, which has no tag.

      source
      @[simp]
      theorem Person.toUD_fromUD {u : UD.Person} {p : Person} (h : fromUD u = some p) :
      p.toUD = u
      source
      theorem Person.ud_conflates_clusivity :
      firstInclusive.toUD = firstExclusive.toUD

      The annotation conflates the clusivity values.

      Number #

      source
      def Number.toUD :
      Number → Option UD.Number

      Realize as an annotation; general, minimal, augmented, unit augmented and global plural have no tag.

      Equations
      Instances For
        source
        def Number.fromUD :
        UD.Number → Option Number

        Ingest an annotation; the inverse, collective and count tags have no value.

        Equations
        Instances For
          source
          theorem Number.roundtrip_fromUD_toUD (v : Number) :
          v ∈ [singular, dual, trial, paucal, plural, greaterPaucal, greaterPlural] → v.toUD.bind fromUD = some v

          The values with a tag round-trip.

          Gender #

          source
          def Gender.toUD :
          Gender → Option UD.Gender

          Realize as an annotation; the animacy labels have no tag.

          Equations
          Instances For
            source
            def Gender.fromUD :
            UD.Gender → Gender

            Ingest an annotation.

            Equations
            Instances For
              source
              theorem Gender.isPartialInv_fromUD_toUD :
              Function.IsPartialInv fromUD toUD

              Realization is a partial inverse of ingestion.

              source
              @[simp]
              theorem Gender.toUD_fromUD (u : UD.Gender) :
              (fromUD u).toUD = some u
              source
              theorem Gender.fromUD_of_toUD_eq_some {g : Gender} {u : UD.Gender} (h : g.toUD = some u) :
              fromUD u = g

              The labels with a tag round-trip.

              Case #

              source
              def Case.toUD :
              Case → UD.Case

              Realize as an annotation.

              Equations
              Instances For
                source
                def Case.fromUD :
                UD.Case → Case

                Ingest an annotation.

                Equations
                Instances For
                  source
                  theorem Case.fromUD_toUD (c : Case) :
                  fromUD c.toUD = if c = obl then acc else c

                  Ingestion after realization is the identity but on the oblique, which realizes as Acc, the tag UD's guidelines give the oblique of a language with a direct and an oblique case only, and ingests as the accusative.

                  source
                  theorem Case.toUD_fromUD (u : UD.Case) :
                  (fromUD u).toUD = u

                  Tokens #

                  source
                  def Morphology.Features.toUD (f : Features) :
                  UD.MorphFeatures

                  The annotation of a token's features.

                  Equations
                  • One or more equations did not get rendered due to their size.
                  Instances For
                    source
                    def Morphology.Features.ofUD (m : UD.MorphFeatures) :
                    Features

                    The features an annotation ingests as.

                    Equations
                    Instances For
                      source
                      def Agreement.Bundle.ofUD (m : UD.MorphFeatures) :
                      Bundle

                      The agreement bundle an annotation ingests as.

                      Equations
                      Instances For