Categorizer Semantics @cite{adamson-2024} @cite{barker-2011}

Semantic denotations for categorizing heads (n) in Distributed Morphology, bridging the morphosyntactic structure of DM categorizers to compositional semantics via @cite{barker-2011}'s type-shifting framework.

@cite{adamson-2024} proposes three denotation types for n heads in Teop:

• n_{body-part{D}} (36): λy.λx. ROOT(x) ∧ body-part-of(x,y) Introduces a body-part-of relation, yielding a relational predicate (type ⟨e,⟨e,t⟩⟩). Equivalent to @cite{barker-2011}'s π (relationalizer).

• n_{sortal} (37): λx. ROOT(x) Bare sortal predicate (type ⟨e,t⟩). Equivalent to @cite{barker-2011}'s bare semantics.

• n_{alienator} (43): λQ.λx. ∃y. Q(y)(x) Existentially closes the possessor argument of a relational noun, yielding a property (type ⟨e,t⟩). Structurally parallel to @cite{barker-2011}'s Ex (existential closure).

Key structural correspondence

The morphosyntactic features on n determine the semantic type:

• n with {D} (selectsD = true) → relational denotation (π)
• n without {D}, combining with a non-relational root → sortal (bare)
• n without {D}, mediating aPossession → existential closure (Ex)

This means the DM categorizer head is simultaneously:

1. A morphosyntactic object (bearing gender features, licensing possession)
2. A compositional semantic operator (determining the noun's semantic type)

inductive Morphology.DM.CategorizerSemantics.NSemanticType : Type

The semantic type contributed by a categorizing head n. This determines how the root's content is composed into the noun's denotation (@cite{adamson-2024} §3.1).

• relational : NSemanticType

  Relational: n introduces a relation (body-part-of, part-of, etc.). Result type: ⟨e,⟨e,t⟩⟩ = Pred2.

• sortal : NSemanticType

  Sortal: n simply categorizes. Result type: ⟨e,t⟩ = Pred1.

• alienator : NSemanticType

  Alienator: n existentially closes a relational root. Input type: ⟨e,⟨e,t⟩⟩; result type: ⟨e,t⟩.

instance Morphology.DM.CategorizerSemantics.instDecidableEqNSemanticType : DecidableEq NSemanticType

Equations

• Morphology.DM.CategorizerSemantics.instDecidableEqNSemanticType x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

def Morphology.DM.CategorizerSemantics.instBEqNSemanticType.beq : NSemanticType → NSemanticType → Bool

Equations

• Morphology.DM.CategorizerSemantics.instBEqNSemanticType.beq x✝ y✝ = (x✝.ctorIdx == y✝.ctorIdx)

instance Morphology.DM.CategorizerSemantics.instBEqNSemanticType : BEq NSemanticType

Equations

• Morphology.DM.CategorizerSemantics.instBEqNSemanticType = { beq := Morphology.DM.CategorizerSemantics.instBEqNSemanticType.beq }

def Morphology.DM.CategorizerSemantics.instReprNSemanticType.repr : NSemanticType → ℕ → Std.Format

Equations

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

instance Morphology.DM.CategorizerSemantics.instReprNSemanticType : Repr NSemanticType

Equations

• Morphology.DM.CategorizerSemantics.instReprNSemanticType = { reprPrec := Morphology.DM.CategorizerSemantics.instReprNSemanticType.repr }

def Morphology.DM.CategorizerSemantics.catHeadSemanticType (ch : CatHead) (mediatesAPossession : Bool := false) : NSemanticType

Map n-head features to the semantic type they contribute.

Equations

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

def Morphology.DM.CategorizerSemantics.nBodyPartDenot {E S : Type} (rootPred : Semantics.Lexical.Noun.Relational.Barker2011.Pred1 E S) (bodyPartOf : Semantics.Lexical.Noun.Relational.Barker2011.Pred2 E S) : Semantics.Lexical.Noun.Relational.Barker2011.Pred2 E S

Denotation of n_{body-part{D}}: combines a root predicate with a body-part-of relation to yield a relational noun.

@cite{adamson-2024} (36): ⟦nP⟧ = λy.λx. ROOT(x) ∧ body-part-of(x,y)

This is @cite{barker-2011}'s π (relationalizer): π(P, R) = λx.λy. P(y) ∧ R(x,y)

In π's convention: first arg = possessor, second arg = possessee.

Equations

• Morphology.DM.CategorizerSemantics.nBodyPartDenot rootPred bodyPartOf = Semantics.Lexical.Noun.Relational.Barker2011.π rootPred bodyPartOf

def Morphology.DM.CategorizerSemantics.nSortalDenot {E S : Type} (rootPred : Semantics.Lexical.Noun.Relational.Barker2011.Pred1 E S) : Semantics.Lexical.Noun.Relational.Barker2011.Pred1 E S

Denotation of n_{sortal}: the root predicate, unchanged.

@cite{adamson-2024} (37): ⟦nP⟧ = λx. ROOT(x)

Equations

• Morphology.DM.CategorizerSemantics.nSortalDenot rootPred = Semantics.Lexical.Noun.Relational.Barker2011.bareSemantics rootPred

def Morphology.DM.CategorizerSemantics.nAlienatorDenot {E S : Type} (relation : Semantics.Lexical.Noun.Relational.Barker2011.Pred2 E S) (x : E) (s : S) : Prop

Denotation of n_{alienator}: existentially closes the possessor argument of a relational noun.

@cite{adamson-2024} (43): ⟦n_{alienator}⟧ = λQ.λx. ∃y. Q(y)(x)

The first argument of the input relation (the possessor) is existentially closed, yielding a one-place property of the possessee.

Equations

• Morphology.DM.CategorizerSemantics.nAlienatorDenot relation x s = ∃ (y : E), relation y x s = true

theorem Morphology.DM.CategorizerSemantics.nBodyPartDenot_eq_pi {E S : Type} (rootPred : Semantics.Lexical.Noun.Relational.Barker2011.Pred1 E S) (bodyPartOf : Semantics.Lexical.Noun.Relational.Barker2011.Pred2 E S) : nBodyPartDenot rootPred bodyPartOf = Semantics.Lexical.Noun.Relational.Barker2011.π rootPred bodyPartOf

n_{body-part{D}} IS Barker's π: the relationalizer.

theorem Morphology.DM.CategorizerSemantics.nSortalDenot_eq_bare {E S : Type} (rootPred : Semantics.Lexical.Noun.Relational.Barker2011.Pred1 E S) : nSortalDenot rootPred = Semantics.Lexical.Noun.Relational.Barker2011.bareSemantics rootPred

n_{sortal} IS Barker's bare semantics: identity on the root predicate.

theorem Morphology.DM.CategorizerSemantics.nAlienatorDenot_is_ex_flipped {E S : Type} (R : Semantics.Lexical.Noun.Relational.Barker2011.Pred2 E S) (x : E) (s : S) : nAlienatorDenot R x s ↔ Semantics.Lexical.Noun.Relational.Barker2011.ExProp (fun (a b : E) (t : S) => R b a t) x s

n_{alienator} is the argument-flipped version of Barker's Ex.

Barker's Ex closes the second argument of R(x,y): ExProp(R)(x)(s) = ∃y. R(x,y,s)

The alienator closes the first argument (the possessor): nAlienatorDenot(R)(x)(s) = ∃y. R(y,x,s)

Both perform existential closure; the difference is which argument of the relation represents the possessor vs possessee.

theorem Morphology.DM.CategorizerSemantics.selectsD_iff_relational (ch : CatHead) : ch.selectsD = true ↔ catHeadSemanticType ch = NSemanticType.relational

n with {D} produces a relational denotation; n without {D} does not.

def Morphology.DM.CategorizerSemantics.teopSpleenIPossessed {E S : Type} (isSpleen : Semantics.Lexical.Noun.Relational.Barker2011.Pred1 E S) (bodyPartOf : Semantics.Lexical.Noun.Relational.Barker2011.Pred2 E S) : Semantics.Lexical.Noun.Relational.Barker2011.Pred2 E S

iPossession: √BINA + n_{body-part{D}} → relational noun.

⟦bina⟧ = λposs.λx. isSpleen(x) ∧ bodyPartOf(poss, x) 'spleen of poss'

Equations

• Morphology.DM.CategorizerSemantics.teopSpleenIPossessed isSpleen bodyPartOf = Morphology.DM.CategorizerSemantics.nBodyPartDenot isSpleen bodyPartOf

def Morphology.DM.CategorizerSemantics.teopSpleenAPossessed {E S : Type} (isSpleen : Semantics.Lexical.Noun.Relational.Barker2011.Pred1 E S) (bodyPartOf : Semantics.Lexical.Noun.Relational.Barker2011.Pred2 E S) (x : E) (s : S) : Prop

aPossession: √BINA + n_{alienator} → existentially closed.

⟦bina⟧ = λx. ∃y. isSpleen(x) ∧ bodyPartOf(y, x) 'a spleen (of some unspecified possessor)'

Equations

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

def Morphology.DM.CategorizerSemantics.teopHouseSortal {E S : Type} (isHouse : Semantics.Lexical.Noun.Relational.Barker2011.Pred1 E S) : Semantics.Lexical.Noun.Relational.Barker2011.Pred1 E S

Sortal noun: √TARA + n_{sortal} → bare predicate.

⟦house⟧ = λx. isHouse(x) No possessor slot available.

Equations

• Morphology.DM.CategorizerSemantics.teopHouseSortal isHouse = Morphology.DM.CategorizerSemantics.nSortalDenot isHouse

theorem Morphology.DM.CategorizerSemantics.ipossessed_with_possessor {E S : Type} (isSpleen : Semantics.Lexical.Noun.Relational.Barker2011.Pred1 E S) (bodyPartOf : Semantics.Lexical.Noun.Relational.Barker2011.Pred2 E S) (john x : E) (s : S) : teopSpleenIPossessed isSpleen bodyPartOf john x s = Semantics.Lexical.Noun.Relational.Barker2011.possessiveRelational john (Semantics.Lexical.Noun.Relational.Barker2011.π isSpleen bodyPartOf) x s

With a specific possessor, the iPossessed body part reduces to a property (Barker's possessiveRelational).

theorem Morphology.DM.CategorizerSemantics.sortal_is_pred1 {E S : Type} (isHouse : Semantics.Lexical.Noun.Relational.Barker2011.Pred1 E S) : teopHouseSortal isHouse = isHouse

The sortal noun has no relatum slot — it cannot directly take a possessor without π.

theorem Morphology.DM.CategorizerSemantics.same_root_different_types {E S : Type} (isSpleen : Semantics.Lexical.Noun.Relational.Barker2011.Pred1 E S) (bodyPartOf : Semantics.Lexical.Noun.Relational.Barker2011.Pred2 E S) (x y : E) (s : S) : teopSpleenIPossessed isSpleen bodyPartOf y x s = (isSpleen x s && bodyPartOf y x s)

Key insight: the SAME root (√BINA) yields different semantic types depending on which n head it combines with. The gender alternation in Teop (gender I vs gender II) corresponds to this semantic type alternation (relational vs sortal/alienated).

theorem Morphology.DM.CategorizerSemantics.alienated_closes_possessor {E S : Type} (isSpleen : Semantics.Lexical.Noun.Relational.Barker2011.Pred1 E S) (bodyPartOf : Semantics.Lexical.Noun.Relational.Barker2011.Pred2 E S) (x : E) (s : S) : teopSpleenAPossessed isSpleen bodyPartOf x s ↔ ∃ (z : E), isSpleen x s = true ∧ bodyPartOf z x s = true

The alienator existentially closes the possessor slot.

The Barker–Adamson correspondence:

CatHead feature	Semantic type	Barker operation
selectsD = true	relational	π
selectsD = false (regular)	sortal	bare
selectsD = false (aPoss)	alienator	Ex

The genuine correspondence theorem is selectsD_iff_relational above: selectsD on n ↔ relational semantic type. The sortal/alienator distinction is secondary (determined by whether aPossession is mediated).

theorem Morphology.DM.CategorizerSemantics.alienator_retraction {E S : Type} (P : Semantics.Lexical.Noun.Relational.Barker2011.Pred1 E S) (R : Semantics.Lexical.Noun.Relational.Barker2011.Pred2 E S) (x : E) (s : S) : nAlienatorDenot (Semantics.Lexical.Noun.Relational.Barker2011.π P R) x s ↔ ∃ (y : E), P x s = true ∧ R y x s = true

The retraction property: applying the alienator to a π-relational noun recovers the root predicate (up to existential closure).

nAlienatorDenot(π(P, R), x, s) ↔ ∃y. P(x,s) ∧ R(y,x,s)

This is why "free" uses of iPossessable nouns in Jarawara are feminine: the root combines with n_{alienator}, existentially closing the possessor slot. The result is a property, which is the same type as n_{sortal}. Since the alienator n is plain (no gender feature), the noun is feminine (unmarked).

def Morphology.DM.CategorizerSemantics.NSemanticType.toBarker : NSemanticType → Semantics.Lexical.Noun.Relational.Barker2011.NominalInterpType

NominalInterpType from Barker 2011 corresponds to NSemanticType.

Equations

• Morphology.DM.CategorizerSemantics.NSemanticType.relational.toBarker = Semantics.Lexical.Noun.Relational.Barker2011.NominalInterpType.pred2
• Morphology.DM.CategorizerSemantics.NSemanticType.sortal.toBarker = Semantics.Lexical.Noun.Relational.Barker2011.NominalInterpType.pred1
• Morphology.DM.CategorizerSemantics.NSemanticType.alienator.toBarker = Semantics.Lexical.Noun.Relational.Barker2011.NominalInterpType.pred1

theorem Morphology.DM.CategorizerSemantics.possessor_requires_relational (t : NSemanticType) : t.toBarker.canTakePossessor = true ↔ t = NSemanticType.relational

Only relational nouns (n with {D}) can directly take a possessor. Sortal and alienated nouns cannot — they need Barker's π first.