Agreement paradigms — the descriptive realization table

[Cor98] [Sco23]

A theory-neutral representation of an agreement paradigm: the descriptive table mapping agreement-feature cells to their surface exponents, in the sense of [Cor98] (Morphology and Agreement, Handbook of Morphology) and the grammar-sketch chapters of descriptive work like [Sco23] (Ch. 2: Set A / Set B person–number inflection).

Theory-neutrality

This file records what forms realize which feature cells — the paradigm table a reference grammar lists. It deliberately commits to no generative account of how the table arises. Syncretism is recorded as a plain fact (two cells, one form — a non-injective table), not explained. The competing realizational analyses — Distributed Morphology (vocabulary insertion + impoverishment; [Sco23] Ch. 4), Paradigm Function Morphology, HPSG type-hierarchy unification — are theories of this table and belong in Studies/, not here.

One φ-space with pronouns

Per [Cor98] (§1), agreement in the wider sense includes pronouns — diachronically, agreement morphology grammaticalizes from pronouns. The three indisputable agreement features (§2) are exactly person, number, gender (case is government, not agreement). So an Cell is the canonical φ-subspace a Pronoun/Word already carries: Word.agrCell projects a word's φ-features into a paradigm index, so the same feature space drives pronoun reference and agreement realization — no parallel person/number enum.

Main declarations

• Cell — an agreement-feature cell (person × number × gender), in the canonical UD feature types.
• Paradigm Exp — a descriptive table: agreement cells to exponents.
• Paradigm.realize — look up the exponent for a cell (exact match).
• Word.agrCell / Paradigm.realizeFor — index a paradigm by a word's φ.

structure Agreement.Cell : Type

An agreement-feature cell: the canonical φ-features that may be realized by agreement ([Cor98] §2 — person, number, gender; case excluded as government). Uses the same UD feature types a Pronoun/Word carries, so a controller's φ projects directly into the index (Word.agrCell). A none field is a feature the paradigm does not distinguish.

• person : Option UD.Person
• number : Option UD.Number
• gender : Option UD.Gender

def Agreement.instDecidableEqCell.decEq (x✝ x✝¹ : Cell) : Decidable (x✝ = x✝¹)

Equations

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

@[implicit_reducible]

instance Agreement.instDecidableEqCell : DecidableEq Cell

Equations

• Agreement.instDecidableEqCell = Agreement.instDecidableEqCell.decEq

def Agreement.instReprCell.repr : Cell → ℕ → Std.Format

Equations

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

@[implicit_reducible]

instance Agreement.instReprCell : Repr Cell

Equations

• Agreement.instReprCell = { reprPrec := Agreement.instReprCell.repr }

@[implicit_reducible]

instance Agreement.instBEqCell : BEq Cell

Equations

• Agreement.instBEqCell = { beq := Agreement.instBEqCell.beq }

def Agreement.instBEqCell.beq : Cell → Cell → Bool

Equations

• Agreement.instBEqCell.beq { person := a, number := a_1, gender := a_2 } { person := b, number := b_1, gender := b_2 } = (a == b && (a_1 == b_1 && a_2 == b_2))
• Agreement.instBEqCell.beq x✝¹ x✝ = false

def Agreement.Cell.pn (p : UD.Person) (n : UD.Number) : Cell

Build a person–number cell (the common case: no gender agreement).

Equations

• Agreement.Cell.pn p n = { person := some p, number := some n }

def Agreement.Cell.isSAP (c : Cell) : Bool

Is this a speech-act-participant (1st/2nd person) cell? Drives person-conditioned phenomena like differential indexing ([Cor98]).

Equations

• c.isSAP = (c.person == some UD.Person.first || c.person == some UD.Person.second)

def Agreement.Cell.toPerson (c : Cell) : Person

The person level of a cell, on the Person scale (an unspecified or 0-person cell maps to .third). Adapts a φ-cell to consumers that reason on person prominence (decomposition, indexing).

Equations

• c.toPerson = match c.person with | some UD.Person.first => Person.first | some UD.Person.second => Person.second | x => Person.third

def Agreement.Cell.isPlural (c : Cell) : Bool

Is this a plural cell?

Equations

• c.isPlural = (c.number == some UD.Number.Plur)

@[implicit_reducible]

instance Agreement.instHasNumberCell : HasNumber Cell

A cell bears the number its UD slot ingests (Number.fromUD); an undistinguished slot leaves the cell unvalued (wildcard).

Equations

• Agreement.instHasNumberCell = { numberOf := fun (c : Agreement.Cell) => c.number.bind Number.fromUD }

@[implicit_reducible]

instance Agreement.instHasPersonCell : HasPerson Cell

Equations

• Agreement.instHasPersonCell = { personOf := fun (c : Agreement.Cell) => Option.map Person.fromUD c.person }

def Agreement.Cell.pnCells : List Cell

The basic 3-person × {singular, plural} inventory of φ-cells — the cells a person/number agreement paradigm ranges over.

Equations

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

def Word.agrCell (w : Word) : Agreement.Cell

The φ-cell of a word: its person/number/gender features, as an agreement index. The bridge that lets a pronoun (or any controller) drive an agreement paradigm in the same feature space ([Cor98] §1).

Equations

• w.agrCell = { person := w.features.person, number := w.features.number, gender := w.features.gender }

@[reducible, inline]

abbrev Agreement.Paradigm (Exp : Type u_1) : Type u_1

An agreement paradigm: the descriptive table of (cell, exponent) entries. Exp is the exponent type (a surface string, a structured affix, …). A non-injective table records syncretism as a fact; a partial table (a cell with no entry) records defectiveness.

Equations

• Agreement.Paradigm Exp = List (Agreement.Cell × Exp)

def Agreement.Paradigm.realize {Exp : Type u_1} [DecidableEq Exp] (p : Paradigm Exp) (c : Cell) : Option Exp

The exponent realizing a given cell, by exact match (the first entry whose cell equals c). none if the paradigm has no entry for the cell.

Equations

• p.realize c = Option.map (fun (x : Agreement.Cell × Exp) => x.2) (List.find? (fun (x : Agreement.Cell × Exp) => x.1 == c) p)

def Agreement.Paradigm.realizeFor {Exp : Type u_1} [DecidableEq Exp] (p : Paradigm Exp) (controller : Word) : Option Exp

Realize the exponent agreeing with a controller word, via its agrCell.

Equations

• p.realizeFor controller = p.realize controller.agrCell

def Agreement.Paradigm.cells {Exp : Type u_1} (p : Paradigm Exp) : List Cell

The cells the paradigm distinguishes (in declaration order).

Equations

• p.cells = List.map (fun (x : Agreement.Cell × Exp) => x.1) p