Documentation

Studies.HaninkKoontzGarboden2025

Hanink and Koontz-Garboden (2025): Variation in the Lexical Semantics of Property Concept Roots #

Hanink and Koontz-Garboden argue from Washo that property concept roots vary in meaning within a language, against Menon and Pancheva's universal quality-denoting root. Washo property concepts are verbs of three shapes (Table 1): a bare root inflected like any intransitive, a bound root with the suffix -iʔ, and a reduplicated bound root flanked by ʔil- and -iʔ, Washo.Shape. The paper reads the morphology at face value: -iʔ is the possessive light verb of ordinary possession (31), true of the possessors of something satisfying its argument, vHave, which takes a predicate of states (34); so a root that needs it denotes a quality, a predicate of states (33), while a bare root denotes a relation between individuals and states (27). The reduplicated roots denote relations too, since they alone serve as bare finals of resultative bipartite verbs (38), whose change-of-state head takes a relation (43a); being bound, they reach -iʔ through ʔil-, which returns the range of a relation (57), nabla, a Duke-of-York derivation that gives back the root's own predication when possessing a state is holding it, vHave_nabla_self. One assignment of types to shapes, RootType.ofShape, then derives the morphology of each shape as its shortest well-typed verbalization, derivation_minimal, and the bipartite gap for the suffixed roots (49), wellTyped_become_iff. The change-of-state head is Beavers and Koontz-Garboden's inchoative operator, and the resultative entails the result state of its theme (46). The seventy stems of the appendix are the rows of Washo.propertyConcepts, on which Dixon's categories predict the shape only for color; the examples are the rows of Data.Examples.HaninkKoontzGarboden2025.

Implementation notes #

Types are the substrate's Ty with .s for the paper's state sort, and the composability claims are stated at the type level, since Lean's own typing enforces them in the semantic definitions. Possession relates a possessor to a possessum of any type, so ordinary possession (67) and the possession of a state (35) are one operator. Causation and change are interpreted by the substrate's EventStructure.Interpretation, whose heads vBecome and vCause are the paper's (43) and whose effector stands for the paper's AGENT.

References #

The two root meanings, section 4 #

inductive HaninkKoontzGarboden2025.RootType :

A property concept root means either a relation between individuals and states or a predicate of states alone, a quality.

relation : RootType
quality : RootType

Instances For

@[instance_reducible]

instance HaninkKoontzGarboden2025.instDecidableEqRootType :

DecidableEq RootType

Equations

HaninkKoontzGarboden2025.instDecidableEqRootType x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

@[instance_reducible]

instance HaninkKoontzGarboden2025.instReprRootType :

Equations

HaninkKoontzGarboden2025.instReprRootType = { reprPrec := HaninkKoontzGarboden2025.instReprRootType.repr }

def HaninkKoontzGarboden2025.instReprRootType.repr :

RootType → ℕ → Std.Format

Equations

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

Instances For

def HaninkKoontzGarboden2025.RootType.ty :

RootType → Montague.Ty

The semantic type of each meaning.

Equations

Instances For

def HaninkKoontzGarboden2025.RootType.ofShape :

Washo.Shape → RootType

On the analysis bare and prefixed roots denote relations and suffixed roots qualities.

Equations

Instances For

theorem HaninkKoontzGarboden2025.exists_rootType_ne :

∃ e₁ ∈ Washo.propertyConcepts, ∃ e₂ ∈ Washo.propertyConcepts, RootType.ofShape e₁.shape ≠ RootType.ofShape e₂.shape

The two meanings are distinguished within Washo, the existence proof against a universal root meaning.

The verbalizing heads and their types #

inductive HaninkKoontzGarboden2025.Head :

The heads that build a verb from a root are zero categorization, which keeps a relation, the possessive light verb -iʔ, which takes a predicate of states, the prefix ʔil-, which takes a relation to a predicate of states, and the change-of-state head of a bipartite verb, which takes a relation.

zero : Head
possess : Head
attr : Head
become : Head

Instances For

@[instance_reducible]

instance HaninkKoontzGarboden2025.instDecidableEqHead :

DecidableEq Head

Equations

HaninkKoontzGarboden2025.instDecidableEqHead x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

def HaninkKoontzGarboden2025.instReprHead.repr :

Head → ℕ → Std.Format

Equations

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

Instances For

@[instance_reducible]

instance HaninkKoontzGarboden2025.instReprHead :

Repr Head

Equations

HaninkKoontzGarboden2025.instReprHead = { reprPrec := HaninkKoontzGarboden2025.instReprHead.repr }

def HaninkKoontzGarboden2025.Head.input :

Head → Montague.Ty

The type a head takes.

Equations

Instances For

def HaninkKoontzGarboden2025.Head.output :

Head → Montague.Ty

The type a head returns is a predicate of individuals and states for the verbalizers, a predicate of states for ʔil-, and a relation to events of change for the bipartite head.

Equations

Instances For

def HaninkKoontzGarboden2025.WellTyped :

Montague.Ty → List Head → Prop

A sequence of heads composes with a type when each takes what the last returns.

Equations

HaninkKoontzGarboden2025.WellTyped x✝ [] = True
HaninkKoontzGarboden2025.WellTyped x✝ (h :: hs) = (h.input = x✝ ∧ HaninkKoontzGarboden2025.WellTyped h.output hs)

Instances For

@[instance_reducible]

instance HaninkKoontzGarboden2025.decWellTyped (τ : Montague.Ty) (hs : List Head) :

Decidable (WellTyped τ hs)

Equations

HaninkKoontzGarboden2025.decWellTyped x✝ [] = isTrue trivial
HaninkKoontzGarboden2025.decWellTyped x✝ (h :: hs) = { decide := decide (h.input = x✝) && decide (HaninkKoontzGarboden2025.WellTyped h.output hs), reflects_decide := ⋯ }

def HaninkKoontzGarboden2025.output (τ : Montague.Ty) :

List Head → Montague.Ty

The type a sequence of heads returns.

Equations

HaninkKoontzGarboden2025.output τ [] = τ
HaninkKoontzGarboden2025.output τ (h :: hs) = HaninkKoontzGarboden2025.output h.output hs

Instances For

def HaninkKoontzGarboden2025.Verbalizes (sh : Washo.Shape) (hs : List Head) :

A verbalization of a root is a sequence of at least one head that is well-typed and returns a stative predicate, with zero categorization open only to a free root.

Equations

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

Instances For

@[instance_reducible]

instance HaninkKoontzGarboden2025.instDecidableVerbalizes (sh : Washo.Shape) (hs : List Head) :

Decidable (Verbalizes sh hs)

Equations

HaninkKoontzGarboden2025.instDecidableVerbalizes sh hs = id inferInstance

def HaninkKoontzGarboden2025.derivation :

Washo.Shape → List Head

The morphology of each shape is the bare root, the root with -iʔ, or the root with ʔil- and then -iʔ.

Equations

Instances For

theorem HaninkKoontzGarboden2025.derivation_verbalizes (sh : Washo.Shape) :

Verbalizes sh (derivation sh)

theorem HaninkKoontzGarboden2025.wellTyped_possess_iff (sh : Washo.Shape) :

WellTyped (RootType.ofShape sh).ty [Head.possess] ↔ sh = Washo.Shape.suffixed

-iʔ composes directly with a root only if the root is a suffixed one, whose meaning is a quality.

theorem HaninkKoontzGarboden2025.wellTyped_become_iff (sh : Washo.Shape) :

WellTyped (RootType.ofShape sh).ty [Head.become] ↔ sh ≠ Washo.Shape.suffixed

The change-of-state head of a bipartite verb composes with a root iff the root is not a suffixed one, the gap in the resultative bipartite verbs.

theorem HaninkKoontzGarboden2025.derivation_minimal (sh : Washo.Shape) (hs : List Head) (h : Verbalizes sh hs) :

(derivation sh).length ≤ hs.length

Each shape's morphology is a shortest verbalization of its root. The prefixed roots need two heads, being bound relations that neither zero categorization nor -iʔ alone can take.

The operators #

def HaninkKoontzGarboden2025.vHave {E : Type u_1} {Y : Type u_2} (P : Y → Prop) (R : E → Y → Prop) :

E → Prop

The possessive light verb -iʔ (34) holds of the possessors of a P, which is ordinary possession when the possessum is an entity and the possession of a state when it is a quality.

Equations

HaninkKoontzGarboden2025.vHave P R = Possession.dom P R

Instances For

def HaninkKoontzGarboden2025.nabla {E : Type u_1} {St : Type u_3} (P : E → St → Prop) :

St → Prop

The prefix ʔil- (57) takes the range of a relation, the states some individual bears it to.

Equations

HaninkKoontzGarboden2025.nabla P = ⨆ (x : E), P x

Instances For

theorem HaninkKoontzGarboden2025.vHave_nabla_self {E : Type u_1} {St : Type u_3} (P : E → St → Prop) (x : E) :

vHave (nabla P) P x ↔ ∃ (s : St), P x s

The Duke-of-York derivation of section 5.2: when possessing a state of the root is bearing the root's relation to it, the prefixed root under ʔil- and -iʔ predicates what the bare relation does (28), the meaning its bipartite uses show it to have.

Resultative bipartite verbs, section 5.1 #

theorem HaninkKoontzGarboden2025.exists_state_of_vCause {E : Type u_1} {St : Type u_3} {Event : Type u_4} (M : ArgumentStructure.EventStructure.Interpretation E St Event) {P : E → St → Prop} {manner : Event → Prop} {x y : E} {v : Event} (h : M.vCause (fun (e : Event) => manner e ∧ M.vBecome P x e) y v) :

∃ (s : St), P x s

A resultative bipartite verb, the causative head over the initial's manner and the change-of-state head over the final's root, entails the result state of its theme, the bare predication of the final's root.

The stems of the appendix #

def HaninkKoontzGarboden2025.toRoot (e : Washo.PropertyConcept) :

The semantic root of a stem has one state atom, no core arguments and the type of its meaning, so every Washo property concept is a property-concept root of the typology of Beavers and Koontz-Garboden.

Equations

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

Instances For

theorem HaninkKoontzGarboden2025.toRoot_kinds (e : Washo.PropertyConcept) :

(toRoot e).kinds = Semantics.Root.Kinds.propertyConcept

theorem HaninkKoontzGarboden2025.color_prefixed (e : Washo.PropertyConcept) :

e ∈ Washo.propertyConcepts → e.category = Semantics.PropertyConcept.Class.color → e.shape = Washo.Shape.prefixed

The only category whose members share a shape is color, all of whose stems are prefixed (appendix).

theorem HaninkKoontzGarboden2025.category_not_predictive :

∃ e₁ ∈ Washo.propertyConcepts, ∃ e₂ ∈ Washo.propertyConcepts, e₁.category = e₂.category ∧ e₁.shape ≠ e₂.shape

[Dix82]'s categories do not predict the shape: the antonyms MiLe 'old' and ešlut’ 'young' differ.