Gender resolution

[Cor91] [WG23] [MNB15] [AA25] [BW13] [NW19]

Resolution of gender with coordinated nominals, over a language's own controller-gender carrier. Unlike Number.resolve — which derives from the join-semilattice of individuals — gender resolution has no lattice-theoretic ground: the attested mechanisms are an inventory of strategies ([NW19] for the survey), and which one applies is language- and configuration-particular data.

Main declarations

• Gender.Strategy — the strategy inventory: language-particular resolution rules (res, [Cor91]; computed by feature intersection in [AA25]), default value insertion (dvi, no-peeking/percolation-failure, [MNB15]), and the single-conjunct strategies (closest/highest, [MNB15]'s three coexisting grammars).
• Gender.System.resolve — per-strategy resolution, Option-valued: ineffability is a predicted outcome ([AA25] derive resolution without all-purpose default insertion; [BW13]'s bidirectional-agreement matching effects are a second ineffability source).
• Gender.System.resolveIn — the value set produced by a set of active strategies: within-speaker optionality is parallel grammars ([WG23] Fig. 1), not nondeterminism inside a strategy ([BW13]: Hindi-Urdu F+F subjects resolve F, or M only when animate — a choice between strategies).
• Gender.Locus — where resolution applies: on the ConjP goal (early) or on the probe after copying (late), [WG23]'s experimental contrast. [BW13]'s syntactic-resolved vs post-syntactic-CCA split is the same axis from the theory side; both are implementable as the timing of Agree-Copy ([Smi21]).

Implementation notes

• Strategies are arguments, not System fields: one language can use different strategies in different agreement configurations ([BW13]: Hindi-Urdu T resolves subjects but takes closest-conjunct agreement with case-licensed objects, LCA preverbally and FCA postverbally).
• The res table is language-particular data; its derivation from feature intersection over interpretable features is [AA25]'s mechanism, formalized in Studies/AdamsonAnagnostopoulou2025.lean (resolve/resolveN).
• Binary resolution only; n-ary conjunctions fold once consumers need them (cf. AdamsonAnagnostopoulou2025.resolveN).
• The strategy layer (closest/highest/resolved/default) is φ-generic — [BW13]'s CCA is one mechanism across number and gender — and hoists to shared substrate when a second feature module consumes it.
• For closest/highest the convention is: the first argument is the structurally higher / linearly first conjunct.

inductive Gender.Strategy (G : Type u_2) : Type u_2

A gender-resolution strategy ([NW19]). The res table is the language's resolution rules ([Cor91]); dvi inserts the system default; closest/highest are single-conjunct agreement.

• res {G : Type u_2} (table : G → G → Option G) : Strategy G

  Resolution rules: equal contribution of both conjuncts, computed by a language-particular table; none = ineffable conflict.

• dvi {G : Type u_2} : Strategy G

  Default value insertion: the system default regardless of conjunct values (no-peeking / percolation failure).

• closest {G : Type u_2} : Strategy G

  Closest conjunct agreement (second argument).

• highest {G : Type u_2} : Strategy G

  Highest conjunct agreement (first argument).

def Gender.Strategy.Congruent {G : Type u_1} (table : G → G → Option G) : Prop

A resolution table treats congruent conjuncts trivially: shared gender resolves to itself ([WG23]'s congruent-conjunct baseline).

Equations

• Gender.Strategy.Congruent table = ∀ (g : G), table g g = some g

def Gender.System.resolve {G : Type u_1} (S : System G) : Strategy G → G → G → Option G

Resolve the gender of two coordinated conjuncts by a strategy. none = ineffability (no grammatical output).

Equations

• S.resolve (Gender.Strategy.res t) x✝¹ x✝ = t x✝¹ x✝
• S.resolve Gender.Strategy.dvi x✝¹ x✝ = some S.default
• S.resolve Gender.Strategy.closest x✝¹ x✝ = some x✝
• S.resolve Gender.Strategy.highest x✝¹ x✝ = some x✝¹

@[simp]

theorem Gender.System.resolve_res {G : Type u_1} (S : System G) (t : G → G → Option G) (a b : G) : S.resolve (Strategy.res t) a b = t a b

@[simp]

theorem Gender.System.resolve_dvi {G : Type u_1} (S : System G) (a b : G) : S.resolve Strategy.dvi a b = some S.default

@[simp]

theorem Gender.System.resolve_closest {G : Type u_1} (S : System G) (a b : G) : S.resolve Strategy.closest a b = some b

@[simp]

theorem Gender.System.resolve_highest {G : Type u_1} (S : System G) (a b : G) : S.resolve Strategy.highest a b = some a

theorem Gender.System.resolve_closest_swap {G : Type u_1} (S : System G) (a b : G) : S.resolve Strategy.closest a b = S.resolve Strategy.highest b a

Closest- and highest-conjunct agreement are order duals.

theorem Gender.System.resolve_res_self {G : Type u_1} (S : System G) {t : G → G → Option G} (h : Strategy.Congruent t) (g : G) : S.resolve (Strategy.res t) g g = some g

A congruent table resolves shared gender to itself.

def Gender.System.resolveIn {G : Type u_1} (S : System G) (strats : Set (Strategy G)) (a b : G) : Set G

The values produced by a set of active strategies — within-speaker and cross-configuration variation as parallel grammars ([WG23]; [BW13]).

Equations

• S.resolveIn strats a b = {g : G | ∃ st ∈ strats, S.resolve st a b = some g}

theorem Gender.System.resolveIn_mono {G : Type u_1} (S : System G) {s₁ s₂ : Set (Strategy G)} (h : s₁ ⊆ s₂) (a b : G) : S.resolveIn s₁ a b ⊆ S.resolveIn s₂ a b

More active strategies produce more values.

theorem Gender.System.resolveIn_singleton {G : Type u_1} (S : System G) (st : Strategy G) (a b g : G) : g ∈ S.resolveIn {st} a b ↔ S.resolve st a b = some g

A single active strategy produces exactly its output.

inductive Gender.Locus : Type

Where resolution applies ([WG23]): on the ConjP goal (early — the value is present before the probe agrees) or on the probe (late — after copying from both conjuncts). Implementable as the timing of Agree-Copy ([Smi21]); [BW13]'s syntactic vs post-syntactic split is the same axis.

• goal : Locus

  Goal resolution: ConjP valued before probing.

• probe : Locus

  Probe resolution: valuation on the probe after Multiple Agree.

@[implicit_reducible]

instance Gender.instDecidableEqLocus : DecidableEq Locus

Equations

• Gender.instDecidableEqLocus x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

@[implicit_reducible]

instance Gender.instReprLocus : Repr Locus

Equations

• Gender.instReprLocus = { reprPrec := Gender.instReprLocus.repr }

def Gender.instReprLocus.repr : Locus → ℕ → Std.Format

Equations

• Gender.instReprLocus.repr Gender.Locus.goal prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Gender.Locus.goal")).group prec✝
• Gender.instReprLocus.repr Gender.Locus.probe prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Gender.Locus.probe")).group prec✝

@[implicit_reducible]

instance Gender.instFintypeLocus : Fintype Locus

Equations

• Gender.instFintypeLocus = { elems := { val := ↑Gender.Locus.enumList, nodup := Gender.Locus.enumList_nodup }, complete := Gender.instFintypeLocus._proof_1 }