Agreement paradigms

This file defines the descriptive agreement paradigm, the table from feature bundles to the exponents that realize them, and the person–number bundles such a table ranges over.

A paradigm records which forms realize which cells, as a reference grammar lists them, and commits to no account of how the table arises: syncretism is a non-injective table and defectiveness a partial one. The cells are the bundles of Syntax/Agreement/Bundle.lean, the feature space a pronoun or a word token already carries, so a controller's Word.phi indexes a paradigm directly ([Cor98]).

Main definitions

• Agreement.Bundle.personNumberCells — the six person–number bundles
• Agreement.Bundle.IsSAP, Agreement.Bundle.IsPlural, Agreement.Bundle.person — the speech-act-participant and plural cells, and the person a cell bears
• Agreement.Paradigm — a table from bundles to exponents, with Paradigm.realize

References

• [Cor98] — agreement paradigms and the shared feature space of pronouns and targets
• [Sco23] — Set A and Set B person–number inflection as descriptive tables

def Agreement.Bundle.person (b : Bundle) : Person

The person a cell bears, third where it bears none.

Equations

• b.person = Flat.unbotD Person.third (b Agreement.Dimension.person)

@[simp]

theorem Agreement.Bundle.person_personNumber (p : Person) (n : Number) : (personNumber p n).person = p

def Agreement.Bundle.IsSAP (b : Bundle) : Prop

A cell is a speech-act participant's when the person it bears is.

Equations

• b.IsSAP = b.person.IsSAP

@[instance_reducible]

instance Agreement.Bundle.instDecidableIsSAP (b : Bundle) : Decidable b.IsSAP

Equations

• b.instDecidableIsSAP = Agreement.Bundle.instDecidableIsSAP._aux_1 b

def Agreement.Bundle.IsPlural (b : Bundle) : Prop

A cell is plural when its number is.

Equations

• b.IsPlural = (b Agreement.Dimension.number = ↑Number.plural)

@[instance_reducible]

instance Agreement.Bundle.instDecidableIsPlural (b : Bundle) : Decidable b.IsPlural

Equations

• b.instDecidableIsPlural = Agreement.Bundle.instDecidableIsPlural._aux_1 b

def Agreement.Bundle.personNumberCells : List Bundle

The six person–number cells a person–number paradigm ranges over.

Equations

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

@[reducible, inline]

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

An agreement paradigm, the descriptive table of cells and their exponents.

Equations

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

def Agreement.Paradigm.realize {Exp : Type u_1} (p : Paradigm Exp) (c : Bundle) : Option Exp

The exponent realizing a cell, that of the first entry whose cell it is.

Equations

• p.realize c = List.lookup c p

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

The cells the paradigm distinguishes, in declaration order.

Equations

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