Documentation

Linglib.Fragments.Romance.Clitics

Romance Clitic Paradigm Schema #

[MP26]

The shared schema for Romance object-clitic paradigms: the three-way ACC/DAT/REFL paradigm contrast, the clitic entry record with its capability instances, and the paradigm-derived syncretism predicates. Italian (Fragments/Italian/Pronouns.lean) and Spanish (Fragments/Spanish/Clitics.lean) instantiate it with their paradigm data; the syncretism predicates drive [MP26]'s stylistic applicatives.

REFL is a paradigm cell, not a case value. In the languages instantiated here (Italian, Spanish) the third-person reflexive (si/se) is a single form that does not determine the accusative/dative contrast — at first/second person the contrast is syncretic throughout — so CliticCase.toCase sends REFL to none while ACC/DAT project to the analytical inventory. This is a commitment scoped to those languages: Romanian contrasts reflexive accusative se with reflexive dative își, so a Romanian instantiation must split the REFL cell (or make the projection person-sensitive) rather than reuse this toCase.

The clitic is its own bespoke struct — capabilities (Proform, Bound, HasPerson, HasNumber, HasCase) abstract over it without merging it into Pronoun (the FunLike-over-many-hom-types pattern). Deficiency is deliberately not a capability: it is per-series (a whole clitic paradigm is .clitic), modelled by the per-language cliticStrength and the Strength order, not by a per-element accessor.

source
inductive Romance.Clitics.CliticCase :
Type

The three-way paradigm contrast for Romance object clitics.

Instances For
    source
    @[implicit_reducible]
    instance Romance.Clitics.instDecidableEqCliticCase :
    DecidableEq CliticCase
    Equations
    source
    @[implicit_reducible]
    instance Romance.Clitics.instReprCliticCase :
    Repr CliticCase
    Equations
    source
    def Romance.Clitics.instReprCliticCase.repr :
    CliticCase → ℕ → Std.Format
    Equations
    • One or more equations did not get rendered due to their size.
    Instances For
      source
      def Romance.Clitics.CliticCase.toCase :
      CliticCase → Option Case

      Project a paradigm cell to the analytical case inventory. REFL projects to none: in Italian/Spanish the reflexive does not determine the accusative/dative contrast. (Romanian, contrasting reflexive se/își, needs a split REFL cell instead.)

      Equations
      Instances For
        source
        structure Romance.Clitics.CliticEntry :
        Type

        A single clitic form in a paradigm.

        Instances For
          source
          @[implicit_reducible]
          instance Romance.Clitics.instReprCliticEntry :
          Repr CliticEntry
          Equations
          source
          def Romance.Clitics.instReprCliticEntry.repr :
          CliticEntry → ℕ → Std.Format
          Equations
          • One or more equations did not get rendered due to their size.
          Instances For
            source
            @[implicit_reducible]
            instance Romance.Clitics.instBEqCliticEntry :
            BEq CliticEntry
            Equations
            source
            def Romance.Clitics.instBEqCliticEntry.beq :
            CliticEntry → CliticEntry → Bool
            Equations
            Instances For
              source
              @[implicit_reducible]
              instance Romance.Clitics.instHasNumberCliticEntry :
              HasNumber CliticEntry

              A clitic bears its φ-slot's number (HasNumber).

              Equations
              source
              @[implicit_reducible]
              instance Romance.Clitics.instHasPersonCliticEntry :
              HasPerson CliticEntry
              Equations
              source
              @[implicit_reducible]
              instance Romance.Clitics.instHasCaseCliticEntry :
              HasCase CliticEntry

              A clitic bears the analytical case its paradigm cell projects to; reflexives, neutralizing the contrast, bear none.

              Equations
              source
              @[implicit_reducible]
              instance Romance.Clitics.instProformCliticEntry :
              Proform CliticEntry

              A clitic's surface form + φ-features (person/number).

              Equations
              source
              @[implicit_reducible]
              instance Romance.Clitics.instBoundCliticEntry :
              Bound CliticEntry

              Binding class from the clitic's paradigm cell: a reflexive clitic is a Principle-A anaphor; an accusative/dative object clitic is a Principle-B pronominal.

              Equations
              • One or more equations did not get rendered due to their size.
              source
              def Romance.Clitics.lookupForm (paradigm : List CliticEntry) (p : UD.Person) (n : UD.Number) (c : CliticCase) :
              Option String

              Look up the form for a given person, number, and paradigm cell.

              Equations
              • One or more equations did not get rendered due to their size.
              Instances For
                source
                def Romance.Clitics.isSyncretic (paradigm : List CliticEntry) (p : UD.Person) (n : UD.Number) (c1 c2 : CliticCase) :
                Bool

                Are two paradigm cells syncretic for a given person/number combination? Derived from the paradigm data: syncretism holds iff the looked-up forms are identical (and both exist).

                Equations
                • One or more equations did not get rendered due to their size.
                Instances For
                  source
                  def Romance.Clitics.datReflSyncretic (paradigm : List CliticEntry) (p : UD.Person) (n : UD.Number) :
                  Bool

                  DAT/REFL syncretism for a given person/number — the key condition for SE-optionality ([MP26]).

                  Equations
                  Instances For