Documentation

Linglib.Core.Lexical.PersonCategory

Person Categories #

@cite{cysouw-2009}

The 8 referential person categories from Cysouw's paradigmatic framework, extracted to Core/ for use by both Phenomena/ (typological data) and Fragments/ (person feature decomposition).

This module contains just the type and its basic predicates. The full paradigmatic structure machinery (morpheme classes, homophony types, language data) remains in Phenomena/Agreement/PersonMarkingTypology.lean.

source
inductive Core.PersonCategory.PersonCategory :
Type

The 8 referential person categories (@cite{cysouw-2009}, Fig 10.1).

Three singular categories (individual speech act roles) and five group categories (attested combinations of participants).

Instances For
    source
    instance Core.PersonCategory.instDecidableEqPersonCategory :
    DecidableEq PersonCategory
    Equations
    source
    instance Core.PersonCategory.instBEqPersonCategory :
    BEq PersonCategory
    Equations
    source
    def Core.PersonCategory.instBEqPersonCategory.beq :
    PersonCategory → PersonCategory → Bool
    Equations
    Instances For
      source
      def Core.PersonCategory.instReprPersonCategory.repr :
      PersonCategory → Nat → Std.Format
      Equations
      • One or more equations did not get rendered due to their size.
      Instances For
        source
        instance Core.PersonCategory.instReprPersonCategory :
        Repr PersonCategory
        Equations
        source
        instance Core.PersonCategory.instInhabitedPersonCategory :
        Inhabited PersonCategory
        Equations
        source
        def Core.PersonCategory.instInhabitedPersonCategory.default :
        PersonCategory
        Equations
        Instances For
          source
          def Core.PersonCategory.PersonCategory.all :
          List PersonCategory

          All 8 categories in canonical order (singular, then group).

          Equations
          • One or more equations did not get rendered due to their size.
          Instances For
            source
            theorem Core.PersonCategory.PersonCategory.all_length :
            all.length = 8
            source
            def Core.PersonCategory.PersonCategory.isSingular :
            PersonCategory → Bool

            Is this a singular (individual) category?

            Equations
            Instances For
              source
              def Core.PersonCategory.PersonCategory.isGroup :
              PersonCategory → Bool

              Is this a group (non-singular) category?

              Equations
              Instances For
                source
                def Core.PersonCategory.PersonCategory.isFirstPersonComplex :
                PersonCategory → Bool

                Is this part of the first person complex (contains speaker)?

                Equations
                Instances For
                  source
                  def Core.PersonCategory.PersonCategory.isInclusive :
                  PersonCategory → Bool

                  Is this an inclusive category (contains both speaker and addressee)?

                  Equations
                  Instances For
                    source
                    def Core.PersonCategory.PersonCategory.includesSpeaker :
                    PersonCategory → Bool

                    Does this category include the speaker?

                    Equations
                    Instances For
                      source
                      def Core.PersonCategory.PersonCategory.includesAddressee :
                      PersonCategory → Bool

                      Does this category include the addressee?

                      Equations
                      Instances For
                        source
                        def Core.PersonCategory.PersonCategory.toUDPerson :
                        PersonCategory → Option UD.Person

                        Map singular PersonCategory to UD.Person.

                        Equations
                        Instances For
                          source
                          def Core.PersonCategory.PersonCategory.fromUDPerson :
                          UD.Person → Option PersonCategory

                          Map UD.Person to singular PersonCategory.

                          Equations
                          Instances For
                            source
                            theorem Core.PersonCategory.ud_person_roundtrip :
                            (PersonCategory.fromUDPerson UD.Person.first).bind PersonCategory.toUDPerson = some UD.Person.first ∧ (PersonCategory.fromUDPerson UD.Person.second).bind PersonCategory.toUDPerson = some UD.Person.second ∧ (PersonCategory.fromUDPerson UD.Person.third).bind PersonCategory.toUDPerson = some UD.Person.third

                            Round-trip: UD.Person → PersonCategory → UD.Person is identity.

                            source
                            def Core.PersonCategory.PersonCategory.toUDPersonNumber :
                            PersonCategory → Option (UD.Person × UD.Number)

                            Map PersonCategory to traditional person × number pair.

                            Equations
                            Instances For
                              source
                              theorem Core.PersonCategory.ud_conflates_incl_excl :
                              PersonCategory.augIncl.toUDPersonNumber = PersonCategory.excl.toUDPersonNumber

                              UD conflates inclusive and exclusive under first person plural.

                              source
                              def Core.PersonCategory.PersonCategory.toPersonLevel :
                              PersonCategory → Option Prominence.PersonLevel

                              Map singular PersonCategory to PersonLevel (the canonical three-way person distinction used by PersonGeometry, DifferentialIndexing, etc.). Group categories map to none — they encode number distinctions that PersonLevel does not capture.

                              Equations
                              Instances For
                                source
                                def Core.PersonCategory.PersonCategory.fromPersonLevel :
                                Prominence.PersonLevel → PersonCategory

                                Map PersonLevel to singular PersonCategory.

                                Equations
                                Instances For
                                  source
                                  theorem Core.PersonCategory.personLevel_roundtrip (p : Prominence.PersonLevel) :
                                  (PersonCategory.fromPersonLevel p).toPersonLevel = some p

                                  Round-trip: PersonLevel → PersonCategory → PersonLevel is identity.

                                  source
                                  theorem Core.PersonCategory.includesSpeaker_iff_author :
                                  PersonCategory.s1.includesSpeaker = true ∧ PersonCategory.s2.includesSpeaker = false ∧ PersonCategory.s3.includesSpeaker = false

                                  includesSpeaker on PersonCategory = hasParticipant ∧ hasAuthor on PersonLevel for singular categories: speaker (s1) = [+participant, +author], addressee (s2) = [+participant, −author], other (s3) = [−participant, −author]. This unifies the PersonCategory decomposition in Spanish/PersonFeatures.lean with PersonGeometry.decomposePerson.

                                  source
                                  theorem Core.PersonCategory.includesAddressee_iff_participant_not_author :
                                  PersonCategory.s1.includesAddressee = false ∧ PersonCategory.s2.includesAddressee = true ∧ PersonCategory.s3.includesAddressee = false
                                  source
                                  theorem Core.PersonCategory.singular_sap_match :
                                  (PersonCategory.s1.includesSpeaker || PersonCategory.s1.includesAddressee) = true ∧ (PersonCategory.s2.includesSpeaker || PersonCategory.s2.includesAddressee) = true ∧ (PersonCategory.s3.includesSpeaker || PersonCategory.s3.includesAddressee) = false

                                  SAP (speech-act participant) = includesSpeaker ∨ includesAddressee for singular categories. This matches PersonLevel.isSAP.