Documentation

Linglib.Studies.Lucy1994

Lucy 1994: The role of semantic value in lexical comparison #

[Luc94] argues that the right way to identify lexical classes is morpho-distributional, not denotational. Yucatek's "spatial" verbs are his test case: a notional set assembled by English intuition fails to coincide with any morphologically defined Yucatek class. What the morphology does deliver is a different, three-way classification of roots by salience profile, derivable from which transitiviser the root requires:

Required transitiviser	Salience class	Examples
`=t` (affective)	agent-salient	síit' "jump", ¢'iib "write"
`=∅` (zero)	agent-patient salient	kuč "carry", p'is "measure", lo'š "punch"
`=s` (causative)	patient-salient	kíim "die", háan "cease", lúub' "fall", 'ok "enter"

Crucially, Lucy's "motion" roots (luub, ok, etc.) do not form a unified class — they pattern with other state-change verbs as patient-salient. What does form a unified class is the positional roots (čin "bend", kul "sit", etc.), distinguished by their derivation via -tal (allomorph -lah) for the positional inchoative.

Here we recast the salience cut as a derived equivalence on roots under the operator inventory in Fragments/Mayan/Yukatek/Operators.lean: two roots have the same salience class iff the same operator(s) apply to them. The classification then falls out of (B&K-G feature signature × Coon root arity) × (operator applicability conditions) — it is not stipulated. Arity carries the agent-patient class (Lucy's =∅ roots "require two arguments"; p'is 'measure' and lo'š 'punch' entail no change of state, so no feature configuration could carry it); the signature separates the two intransitive classes.

The structural theorem class_depends_only_on_signature_and_arity makes this precise: salience class depends only on the pair, not on the specific root identity. The per-root checks then degenerate to finite lookups.

Salience classes (re-exported from theory) #

SalienceClass and classOf live in Semantics/Lexical/Roots/SalienceClass.lean. This file provides the full [Luc94] analysis on top of them: operator-applicability characterizations and per-root sanity checks.

@[reducible, inline]

abbrev Lucy1994.predictedClass (r : Verb.Root) :

Option Verb.SalienceClass

A root's predicted salience class: the substrate classifier applied to its signature and the fragment's arity assignment.

Equations

Lucy1994.predictedClass r = Verb.classOf r.kinds (Yukatek.Roots.arity r)

Instances For

theorem Lucy1994.class_depends_only_on_signature_and_arity (r₁ r₂ : Verb.Root) (h : r₁.kinds = r₂.kinds) (h' : Yukatek.Roots.arity r₁ = Yukatek.Roots.arity r₂) :

predictedClass r₁ = predictedClass r₂

Predicted class agrees with operator applicability #

Both predictedClass and the inventory's applicability profile factor through the pair (kind signature × arity), drawn from a 32-element fintype. Each characterisation therefore reduces — after rewriting the profile to pair level (applicableNames_eq_profile) and generalising the pair — to a statement over all pairs that decide checks. The local macro lucy_applicable packages the reduction.

theorem Lucy1994.agent_iff_applicable_t (r : Verb.Root) :

predictedClass r = some Verb.SalienceClass.agent ↔ Yukatek.Operators.inventory.applicableNames r = ["=t"]

The =t-only applicability profile characterises agent-salient roots.

theorem Lucy1994.agentPatient_iff_applicable_zero (r : Verb.Root) :

predictedClass r = some Verb.SalienceClass.agentPatient ↔ Yukatek.Operators.inventory.applicableNames r = ["=∅"]

The =∅-only applicability profile characterises agent-patient salient roots.

theorem Lucy1994.patient_iff_applicable_s (r : Verb.Root) :

predictedClass r = some Verb.SalienceClass.patient ↔ Yukatek.Operators.inventory.applicableNames r = ["=s"]

The =s-only applicability profile characterises patient-salient roots.

theorem Lucy1994.positional_iff_applicable_tal (r : Verb.Root) :

predictedClass r = some Verb.SalienceClass.positional ↔ Yukatek.Operators.inventory.applicableNames r = ["-tal"]

The -tal-only applicability profile characterises positional roots.

theorem Lucy1994.none_iff_applicable_empty (r : Verb.Root) :

predictedClass r = none ↔ Yukatek.Operators.inventory.applicableNames r = []

An empty applicability profile characterises roots in [Luc94]'s diagnostic gap (the no-manner, no-result signatures other than the pure positional configuration {.state}).

theorem Lucy1994.applicableNames_eq_iff_predictedClass_eq (r₁ r₂ : Verb.Root) :

Yukatek.Operators.inventory.applicableNames r₁ = Yukatek.Operators.inventory.applicableNames r₂ ↔ predictedClass r₁ = predictedClass r₂

Applicability-as-classifier. Two roots have the same applicability profile under [Luc94]'s diagnostic inventory iff they have the same predicted salience class. The 4 named-class iff-theorems are special cases.

Per-root sanity checks #

Agent-salient.

theorem Lucy1994.siit_agent :

predictedClass Yukatek.Roots.siit = some Verb.SalienceClass.agent

theorem Lucy1994.tziib_agent :

predictedClass Yukatek.Roots.tziib = some Verb.SalienceClass.agent

theorem Lucy1994.miis_agent :

predictedClass Yukatek.Roots.miis = some Verb.SalienceClass.agent

theorem Lucy1994.cheh_agent :

predictedClass Yukatek.Roots.cheh = some Verb.SalienceClass.agent

theorem Lucy1994.paak_agent :

predictedClass Yukatek.Roots.paak = some Verb.SalienceClass.agent

Agent-patient salient.

theorem Lucy1994.kuc_agentPatient :

predictedClass Yukatek.Roots.kuc = some Verb.SalienceClass.agentPatient

theorem Lucy1994.pis_agentPatient :

predictedClass Yukatek.Roots.pis = some Verb.SalienceClass.agentPatient

theorem Lucy1994.los_agentPatient :

predictedClass Yukatek.Roots.los = some Verb.SalienceClass.agentPatient

Patient-salient.

theorem Lucy1994.kiim_patient :

predictedClass Yukatek.Roots.kiim = some Verb.SalienceClass.patient

theorem Lucy1994.haanCease_patient :

predictedClass Yukatek.Roots.haanCease = some Verb.SalienceClass.patient

theorem Lucy1994.luub_patient :

predictedClass Yukatek.Roots.luub = some Verb.SalienceClass.patient

theorem Lucy1994.ok_patient :

predictedClass Yukatek.Roots.ok = some Verb.SalienceClass.patient

theorem Lucy1994.ah_patient :

predictedClass Yukatek.Roots.ah = some Verb.SalienceClass.patient

theorem Lucy1994.wen_patient :

predictedClass Yukatek.Roots.wen = some Verb.SalienceClass.patient

theorem Lucy1994.siih_patient :

predictedClass Yukatek.Roots.siih = some Verb.SalienceClass.patient

theorem Lucy1994.tuub_patient :

predictedClass Yukatek.Roots.tuub = some Verb.SalienceClass.patient

theorem Lucy1994.kaah_patient :

predictedClass Yukatek.Roots.kaah = some Verb.SalienceClass.patient

theorem Lucy1994.chuun_patient :

predictedClass Yukatek.Roots.chuun = some Verb.SalienceClass.patient

theorem Lucy1994.chenCease_patient :

predictedClass Yukatek.Roots.chenCease = some Verb.SalienceClass.patient

theorem Lucy1994.hoop_patient :

predictedClass Yukatek.Roots.hoop = some Verb.SalienceClass.patient

theorem Lucy1994.heel_patient :

predictedClass Yukatek.Roots.heel = some Verb.SalienceClass.patient

theorem Lucy1994.paat_patient :

predictedClass Yukatek.Roots.paat = some Verb.SalienceClass.patient

Motion roots — pattern as patient-salient (Lucy's central point).

theorem Lucy1994.maan_patient :

predictedClass Yukatek.Roots.maan = some Verb.SalienceClass.patient

theorem Lucy1994.taal_patient :

predictedClass Yukatek.Roots.taal = some Verb.SalienceClass.patient

theorem Lucy1994.bin_patient :

predictedClass Yukatek.Roots.bin = some Verb.SalienceClass.patient

theorem Lucy1994.naak_patient :

predictedClass Yukatek.Roots.naak = some Verb.SalienceClass.patient

theorem Lucy1994.liik_patient :

predictedClass Yukatek.Roots.liik = some Verb.SalienceClass.patient

Positional.

theorem Lucy1994.cin_positional :

predictedClass Yukatek.Roots.cin = some Verb.SalienceClass.positional

theorem Lucy1994.kul_positional :

predictedClass Yukatek.Roots.kul = some Verb.SalienceClass.positional

The "motion verbs" non-class #

theorem Lucy1994.motion_roots_not_separate_class :

predictedClass Yukatek.Roots.luub = predictedClass Yukatek.Roots.kiim ∧ predictedClass Yukatek.Roots.ok = predictedClass Yukatek.Roots.kiim

[Luc94]'s central typological point: "motion" verbs (luub "fall", ok "enter") are not in their own salience class — they pattern with other patient-salient state-change roots. Concretely: their predicted class is the same as kiim "die".

theorem Lucy1994.positional_distinct_from_motion :

predictedClass Yukatek.Roots.cin ≠ predictedClass Yukatek.Roots.luub

Conversely, positional roots do form a unified class distinguishable from any "motion" or state-change root: their predicted class differs from every patient-salient root's.

Root transitivity is not MRC violation #

theorem Lucy1994.rootTransitives_respect_mrc (r : Verb.Root) :

r ∈ Yukatek.Roots.rootTransitives → r.RespectsMannerResultComplementarity

Lucy's root transitives are manner-only roots in B&K-G terms — lexical transitivity does not entail a result. Under the previous schema (agent-patient salience as manner + result) every Yukatek root transitive came out violating Manner/Result Complementarity, contradicting [BKG20]'s finding that manner+result roots are a restricted, special class; hit-type surface-contact roots like lo'š 'punch' are their parade manner-without-result examples.

Closure robustness #

def Lucy1994.closedPredictedClass (r : Verb.Root) :

Option Verb.SalienceClass

The class predicted from a root's closed kind signature (the collocational closure Root.Kinds.close of the derived signature). Arity is closure-invariant.

Equations

Lucy1994.closedPredictedClass r = Verb.classOf r.closedKinds (Yukatek.Roots.arity r)

Instances For

theorem Lucy1994.predictedClass_closure_invariant (r : Verb.Root) (h : ¬r.HasCause) :

closedPredictedClass r = predictedClass r

For cause-free roots, collocational closure does not change the Lucy 1994 salience classification: arity is untouched, the only closure edge that can fire is result→state, the agent / patient arms ignore .state membership, and a base that gains .state from closure carries .result and so is already excluded from the positional arm. The hypothesis is necessary: an intransitive root carrying .cause but not .result is unclassified at base yet patient-salient after closure, since the cause→result closure edge introduces .result.

Bridge to Bohnemeyer's 5-way verb stem classes #

[Boh04] refines [Luc94]'s 4-way salience cut into a 5-way stem classification (active, inactive, inchoative, positional, transitiveActive). The mapping is VerbStemClass.toSalienceClass in VerbClasses.lean. The agent / patient / agent-patient classes correspond one-to-one; Lucy's positional covers both Bohnemeyer's inchoative and positional.

The per-root theorems below check that for each Yukatek root in
`Roots.lean`, Lucy's predicted class agrees with the Bohnemeyer
stem-class label converted via `toSalienceClass`.

theorem Lucy1994.siit_lucy_agrees_active :

predictedClass Yukatek.Roots.siit = some Yukatek.VerbStemClass.active.toSalienceClass

Agent-salient Lucy roots map to Bohnemeyer's active stem class.

theorem Lucy1994.tziib_lucy_agrees_active :

predictedClass Yukatek.Roots.tziib = some Yukatek.VerbStemClass.active.toSalienceClass

theorem Lucy1994.kuc_lucy_agrees_transitiveActive :

predictedClass Yukatek.Roots.kuc = some Yukatek.VerbStemClass.transitiveActive.toSalienceClass

Agent-patient salient Lucy roots map to Bohnemeyer's transitiveActive.

theorem Lucy1994.pis_lucy_agrees_transitiveActive :

predictedClass Yukatek.Roots.pis = some Yukatek.VerbStemClass.transitiveActive.toSalienceClass

theorem Lucy1994.los_lucy_agrees_transitiveActive :

predictedClass Yukatek.Roots.los = some Yukatek.VerbStemClass.transitiveActive.toSalienceClass

theorem Lucy1994.kiim_lucy_agrees_inactive :

predictedClass Yukatek.Roots.kiim = some Yukatek.VerbStemClass.inactive.toSalienceClass

Patient-salient Lucy roots map to Bohnemeyer's inactive.

theorem Lucy1994.haanCease_lucy_agrees_inactive :

predictedClass Yukatek.Roots.haanCease = some Yukatek.VerbStemClass.inactive.toSalienceClass

theorem Lucy1994.luub_lucy_agrees_inactive :

predictedClass Yukatek.Roots.luub = some Yukatek.VerbStemClass.inactive.toSalienceClass

theorem Lucy1994.ok_lucy_agrees_inactive :

predictedClass Yukatek.Roots.ok = some Yukatek.VerbStemClass.inactive.toSalienceClass

theorem Lucy1994.cin_lucy_agrees_positional :

predictedClass Yukatek.Roots.cin = some Yukatek.VerbStemClass.positional.toSalienceClass

Positional Lucy roots map to Bohnemeyer's positional (and would equally map to inchoative per inchoative_positional_collapse_under_lucy).

theorem Lucy1994.kul_lucy_agrees_positional :

predictedClass Yukatek.Roots.kul = some Yukatek.VerbStemClass.positional.toSalienceClass