Gender assignment systems

This file defines an assignment system, the rules by which a language assigns its nouns to genders, and its semantic core.

An assignment system reads a noun's meaning through semantic rules and its form through formal rules, morphological or phonological; the semantic rules take precedence, the formal rules sort the semantic residue, and the residue gender catches what neither covers. No attested system is formal alone: every system assigns by meaning on some nonempty set of nouns, its semantic core, which here is the set of nouns the semantic rules cover, so that the core determines gender by meaning as a theorem rather than a stipulation.

Main definitions

• Gender.AssignmentSystem: semantic rules, formal rules and a residue gender.
• Gender.AssignmentSystem.assign: the gender of a noun under the rules, in order.
• Gender.AssignmentSystem.IsStrictSemantic: a system with no formal rules.
• Gender.AssignmentSystem.semanticCore: the nouns the semantic rules cover.

Main results

• Gender.AssignmentSystem.assign_of_formal: a formal rule decides only in the semantic residue.
• Gender.AssignmentSystem.factorsThrough_semanticCore: on the semantic core, gender is a function of meaning.
• Gender.AssignmentSystem.factorsThrough_of_isStrictSemantic: in a strict semantic system, gender is a function of meaning everywhere.

Implementation notes

The system is typed by the meaning σ its semantic rules read and the form φ its formal rules read; a language's fragment supplies the maps from nouns to both. The rules are total functions to an optional gender, so their order of application is fixed by construction.

References

• [Cor91] — chapters 2 and 3: semantic and formal assignment, and the semantic core
• [Dah00] — the animacy refinement of the semantic core
• [Kra15] — the semantic core generalization restated

structure Gender.AssignmentSystem (σ : Type u_1) (φ : Type u_2) (G : Type u_3) : Type (max (max u_1 u_2) u_3)

An assignment system consists of semantic rules reading a noun's meaning, formal rules reading its form, and the residue gender.

• semantic : σ → Option G

  The semantic rules, as a partial function of the meaning.

• formal : φ → Option G

  The formal rules, morphological or phonological, as a partial function of the form.

• residue : G

  The gender of nouns no rule covers.

def Gender.AssignmentSystem.assign {N : Type u_1} {σ : Type u_2} {φ : Type u_3} {G : Type u_4} (A : AssignmentSystem σ φ G) (sem : N → σ) (form : N → φ) (n : N) : G

The gender of a noun is decided by the semantic rules first, then by the formal rules on the semantic residue, and by the residue gender last.

Equations

• A.assign sem form n = ((A.semantic (sem n)).or (A.formal (form n))).getD A.residue

theorem Gender.AssignmentSystem.assign_of_semantic {N : Type u_1} {σ : Type u_2} {φ : Type u_3} {G : Type u_4} (A : AssignmentSystem σ φ G) (sem : N → σ) (form : N → φ) {n : N} {g : G} (h : A.semantic (sem n) = some g) : A.assign sem form n = g

theorem Gender.AssignmentSystem.assign_of_formal {N : Type u_1} {σ : Type u_2} {φ : Type u_3} {G : Type u_4} (A : AssignmentSystem σ φ G) (sem : N → σ) (form : N → φ) {n : N} {g : G} (h₁ : A.semantic (sem n) = none) (h₂ : A.formal (form n) = some g) : A.assign sem form n = g

Semantic rules take precedence, so a formal rule decides only in the semantic residue.

theorem Gender.AssignmentSystem.assign_of_residue {N : Type u_1} {σ : Type u_2} {φ : Type u_3} {G : Type u_4} (A : AssignmentSystem σ φ G) (sem : N → σ) (form : N → φ) {n : N} (h₁ : A.semantic (sem n) = none) (h₂ : A.formal (form n) = none) : A.assign sem form n = A.residue

def Gender.AssignmentSystem.IsStrictSemantic {σ : Type u_2} {φ : Type u_3} {G : Type u_4} (A : AssignmentSystem σ φ G) : Prop

A strict semantic system has no formal rules.

Equations

• A.IsStrictSemantic = ∀ (x : φ), A.formal x = none

theorem Gender.AssignmentSystem.factorsThrough_of_isStrictSemantic {N : Type u_1} {σ : Type u_2} {φ : Type u_3} {G : Type u_4} (A : AssignmentSystem σ φ G) (sem : N → σ) (form : N → φ) (h : A.IsStrictSemantic) : Function.FactorsThrough (A.assign sem form) sem

In a strict semantic system the gender is a function of the meaning.

def Gender.AssignmentSystem.semanticCore {N : Type u_1} {σ : Type u_2} {φ : Type u_3} {G : Type u_4} (A : AssignmentSystem σ φ G) (sem : N → σ) : Set N

The semantic core is the set of nouns the semantic rules cover.

Equations

• A.semanticCore sem = {n : N | (A.semantic (sem n)).isSome = true}

theorem Gender.AssignmentSystem.factorsThrough_semanticCore {N : Type u_1} {σ : Type u_2} {φ : Type u_3} {G : Type u_4} (A : AssignmentSystem σ φ G) (sem : N → σ) (form : N → φ) : Function.FactorsThrough ((A.semanticCore sem).domRestrict (A.assign sem form)) ((A.semanticCore sem).domRestrict sem)

On the semantic core, gender is a function of meaning.