Lucy (1994): The Role of Semantic Value in Lexical Comparison

This file formalizes the morpho-distributional diagnostic of [Luc94]: the lexical classes of a language are to be identified by their morphology rather than by notional content, and the notional class of motion verbs, assembled from English intuition, coincides with no morphologically defined class of Yucatec. The diagnostic is the derivation a root requires to form a transitive stem, the affective suffix =t for agent-salient roots, no derivation for agent-patient-salient roots, and the causative suffix =s for patient-salient roots (affectiveT, zeroDeriv, causativeS), salience being a set of default semantic values in a root that influence case marking. Roots are encoded by their entailment signature and their valency after [BKG20] and [Coo19], the classifier is the substrate's ArgumentStructure.SalienceClass.ofKinds, and the derivations predicted from the encoding reproduce every derivation the paper attests (predicted_matches_attested), the attestations being the form relations of Data/Forms/Lucy1994. Notional motion roots land in the patient-salient class, each classified as kíim 'die' is (motion_roots_not_separate_class); at best the roots lacking the -Vl imperfective form a formal class of motion verbs, a distinction invisible to the entailment grid (hash_not_signature_definable). Positional roots, which take the positional derivation =lah, cross-cut the transitiviser classes, čin 'bend' also zero-deriving a transitive (positional_crosscuts_transitiviser_classes), and each class's derivation adds the complement of its underived stem's valency (transitiviser_adds_compl).

Implementation notes

The agent-patient class is carried by valency rather than by a signature, since its roots share none: p'is 'measure' is manner-only and k'os 'cut' manner and result. The affective class is inflated by denominal and loanword verbalization, so =t is a weaker signal of manner entailments than the other two derivations are of theirs. Root spellings are the paper's, read from the form rows; the class sizes and the two-way split of intransitives the paper aligns with the unaccusativity tradition are described in prose.

References

• [Luc94]
• [BKG20]
• [Coo19]

def Lucy1994.ofForm (f : Data.Forms.Form Forms.Cell) (entailments : Finset Semantics.Root.Entailment) : Semantics.Root

The root of the sample that a form spells, with its entailment signature.

Equations

• Lucy1994.ofForm f entailments = { name := f.form, entailments := entailments }

Agent-salient roots ((1a), p. 629)

def Lucy1994.siit : Semantics.Root

síit' 'jump' (1a).

Equations

• Lucy1994.siit = Lucy1994.ofForm Lucy1994.Forms.siit {Semantics.Root.Entailment.manner "jumping"}

def Lucy1994.tziib : Semantics.Root

¢'iib' 'write' (p. 629).

Equations

• Lucy1994.tziib = Lucy1994.ofForm Lucy1994.Forms.tziib {Semantics.Root.Entailment.manner "writing"}

def Lucy1994.miis : Semantics.Root

mìis 'sweep' (p. 629), denominal from 'broom'.

Equations

• Lucy1994.miis = Lucy1994.ofForm Lucy1994.Forms.miis {Semantics.Root.Entailment.manner "sweeping"}

def Lucy1994.cheh : Semantics.Root

čé'eh 'smile' (p. 629).

Equations

• Lucy1994.cheh = Lucy1994.ofForm Lucy1994.Forms.cheh {Semantics.Root.Entailment.manner "smiling"}

def Lucy1994.paak : Semantics.Root

páak 'weed' (p. 629).

Equations

• Lucy1994.paak = Lucy1994.ofForm Lucy1994.Forms.paak {Semantics.Root.Entailment.manner "weeding"}

Agent-patient-salient roots ((1b), p. 629)

Root transitives, carrying no uniform signature: kuč, p'is, ha¢ and loš are manner-only, surface contact without an entailed result, while k'os 'cut' is manner and result.

def Lucy1994.kuc : Semantics.Root

kuč 'carry' (1b).

Equations

• Lucy1994.kuc = Lucy1994.ofForm Lucy1994.Forms.kuc {Semantics.Root.Entailment.manner "carrying"}

def Lucy1994.kos : Semantics.Root

k'os 'cut' (p. 629), manner and result.

Equations

• Lucy1994.kos = Lucy1994.ofForm Lucy1994.Forms.kos {Semantics.Root.Entailment.manner "cutting", Semantics.Root.Entailment.result "cut"}

def Lucy1994.pis : Semantics.Root

p'is 'measure' (p. 629), no entailed change of state.

Equations

• Lucy1994.pis = Lucy1994.ofForm Lucy1994.Forms.pis {Semantics.Root.Entailment.manner "measuring"}

def Lucy1994.hats : Semantics.Root

ha¢ 'whip' (p. 629).

Equations

• Lucy1994.hats = Lucy1994.ofForm Lucy1994.Forms.hats {Semantics.Root.Entailment.manner "whipping"}

def Lucy1994.los : Semantics.Root

loš 'punch' (p. 629), surface contact without an entailed result.

Equations

• Lucy1994.los = Lucy1994.ofForm Lucy1994.Forms.los {Semantics.Root.Entailment.manner "striking"}

Patient-salient roots ((2), pp. 629–630)

List (2) is arranged in antonym pairs listed in vertical adjacency: 'ah wen, siih kíim, tú'ub' k'a'ah, ču'un č'en, hó'op' ~ háaw. The order below is the list's.

def Lucy1994.ah : Semantics.Root

'ah '(a)wake(n)', 'ah=s 'wake (someone)'.

Equations

• Lucy1994.ah = Lucy1994.ofForm Lucy1994.Forms.ah {Semantics.Root.Entailment.result "awake"}

def Lucy1994.wen : Semantics.Root

wen '(fall a)sleep', ween=s 'put to sleep'; fn. 7 flags it as also denoting continuation in the state.

Equations

• Lucy1994.wen = Lucy1994.ofForm Lucy1994.Forms.wen {Semantics.Root.Entailment.result "asleep"}

def Lucy1994.siih : Semantics.Root

siih 'be born', siih=s 'give birth, bear'.

Equations

• Lucy1994.siih = Lucy1994.ofForm Lucy1994.Forms.siih {Semantics.Root.Entailment.result "born"}

def Lucy1994.kiim : Semantics.Root

kíim 'die' (1c), kíim=s 'kill'.

Equations

• Lucy1994.kiim = Lucy1994.ofForm Lucy1994.Forms.kiim {Semantics.Root.Entailment.result "dead"}

def Lucy1994.tuub : Semantics.Root

tú'ub' 'forget', tú'ub'=s 'distract, cause to forget'.

Equations

• Lucy1994.tuub = Lucy1994.ofForm Lucy1994.Forms.tuub {Semantics.Root.Entailment.result "forgotten"}

def Lucy1994.kaah : Semantics.Root

k'a'ah 'remember', k'á'ah=s 'remind, mention, invoke'.

Equations

• Lucy1994.kaah = Lucy1994.ofForm Lucy1994.Forms.kaah {Semantics.Root.Entailment.result "remembered"}

def Lucy1994.chuun : Semantics.Root

ču'un 'begin activity', ču'un=s 'cause to begin'.

Equations

• Lucy1994.chuun = Lucy1994.ofForm Lucy1994.Forms.chuun {Semantics.Root.Entailment.result "begun"}

def Lucy1994.chen : Semantics.Root

č'en 'stop, cease', č'en=s 'cause to stop, suspend'.

Equations

• Lucy1994.chen = Lucy1994.ofForm Lucy1994.Forms.chen {Semantics.Root.Entailment.result "ceased"}

def Lucy1994.hoop : Semantics.Root

hó'op' 'begin, start', hó'op'=s 'cause to begin'.

Equations

• Lucy1994.hoop = Lucy1994.ofForm Lucy1994.Forms.hoop {Semantics.Root.Entailment.result "started"}

def Lucy1994.haaw : Semantics.Root

háaw 'stop, cease, heal', háaw=s 'stop, revoke, medicate'.

Equations

• Lucy1994.haaw = Lucy1994.ofForm Lucy1994.Forms.haaw {Semantics.Root.Entailment.result "stopped"}

def Lucy1994.heel : Semantics.Root

hé'el 'rest, stop at', hé'e(l)=s 'rest'.

Equations

• Lucy1994.heel = Lucy1994.ofForm Lucy1994.Forms.heel {Semantics.Root.Entailment.result "rested"}

def Lucy1994.paat : Semantics.Root

p'át 'remain', p'át=s 'abandon'.

Equations

• Lucy1994.paat = Lucy1994.ofForm Lucy1994.Forms.paat {Semantics.Root.Entailment.result "remaining"}

Motion roots ((4), p. 640)

Locational-spatial state-change predicates: notionally motion, formally plain members of the patient-salient class. The five roots marked # do not, and cannot, take the -Vl suffix in the imperfective; fn. 17 adds that péek and 'ú'ul are also irregular in their agent-focused perfective forms, where they pattern like agent-salient roots.

def Lucy1994.maan : Semantics.Root

máan 'pass by' (#), maan=s 'pass, transfer, transport'.

Equations

• Lucy1994.maan = Lucy1994.ofForm Lucy1994.Forms.maan {Semantics.Root.Entailment.result "past"}

def Lucy1994.peek : Semantics.Root

péek 'move, vibrate' (#), pek=s 'cause to move, vibrate'.

Equations

• Lucy1994.peek = Lucy1994.ofForm Lucy1994.Forms.peek {Semantics.Root.Entailment.result "in-motion"}

def Lucy1994.bin : Semantics.Root

b'in 'go' (#), bi(n)=s 'take'.

Equations

• Lucy1994.bin = Lucy1994.ofForm Lucy1994.Forms.bin {Semantics.Root.Entailment.result "gone"}

def Lucy1994.taal : Semantics.Root

tàal 'come (here)' (#), taa(l)=s 'bring'.

Equations

• Lucy1994.taal = Lucy1994.ofForm Lucy1994.Forms.taal {Semantics.Root.Entailment.result "come"}

def Lucy1994.uul : Semantics.Root

'ú'ul 'arrive (here)' (#), 'u'uh=s 'bring it to here'.

Equations

• Lucy1994.uul = Lucy1994.ofForm Lucy1994.Forms.uul {Semantics.Root.Entailment.result "arrived"}

def Lucy1994.ok : Semantics.Root

'ok 'enter, intrude', 'ook=s 'move it in(to)'.

Equations

• Lucy1994.ok = Lucy1994.ofForm Lucy1994.Forms.ok {Semantics.Root.Entailment.result "inside"}

def Lucy1994.luub : Semantics.Root

lúub' 'fall', luub'=s 'fell'.

Equations

• Lucy1994.luub = Lucy1994.ofForm Lucy1994.Forms.luub {Semantics.Root.Entailment.result "fallen"}

def Lucy1994.liik : Semantics.Root

líik' '(a)rise, ascend', lii(k)'=s 'raise, lift, put away'.

Equations

• Lucy1994.liik = Lucy1994.ofForm Lucy1994.Forms.liik {Semantics.Root.Entailment.result "risen"}

def Lucy1994.naak : Semantics.Root

ná'ak '(a)rise, ascend', na'ak=s 'raise'; distinct from náak 'arrive, reach, hit', not sampled here.

Equations

• Lucy1994.naak = Lucy1994.ofForm Lucy1994.Forms.naak {Semantics.Root.Entailment.result "ascended"}

Positional roots ((5) to (7), pp. 642–644)

def Lucy1994.cin : Semantics.Root

čin 'bow, bend down, bend over' ((5) to (7)); zero-derives a transitive, (6) 'I bent it'.

Equations

• Lucy1994.cin = Lucy1994.ofForm Lucy1994.Forms.cin {Semantics.Root.Entailment.state "bent"}

def Lucy1994.cil : Semantics.Root

čil 'lie down, lying down' (7).

Equations

• Lucy1994.cil = Lucy1994.ofForm Lucy1994.Forms.cil {Semantics.Root.Entailment.state "lying"}

Valency and class lists

def Lucy1994.rootTransitives : List Semantics.Root

The roots attested forming a transitive stem by zero derivation, the sampled =∅ predicate roots (p. 629) and the positional čin (6).

Equations

• Lucy1994.rootTransitives = [Lucy1994.kuc, Lucy1994.kos, Lucy1994.pis, Lucy1994.hats, Lucy1994.los, Lucy1994.cin]

def Lucy1994.valency (r : Semantics.Root) : ArgumentStructure.Valency

Root valency for the sample, [Coo19]'s √TV as {.internal}: zero-derivers introduce their internal argument, every other sampled root none.

Equations

• Lucy1994.valency r = if r ∈ Lucy1994.rootTransitives then {ArgumentStructure.ArgPosition.internal} else ∅

def Lucy1994.agentSalientRoots : List Semantics.Root

The sampled agent-salient roots.

Equations

• Lucy1994.agentSalientRoots = [Lucy1994.siit, Lucy1994.tziib, Lucy1994.miis, Lucy1994.cheh, Lucy1994.paak]

def Lucy1994.agentPatientSalientRoots : List Semantics.Root

The sampled agent-patient-salient roots.

Equations

• Lucy1994.agentPatientSalientRoots = [Lucy1994.kuc, Lucy1994.kos, Lucy1994.pis, Lucy1994.hats, Lucy1994.los]

def Lucy1994.patientSalientRoots : List Semantics.Root

The sampled patient-salient roots of list (2), in the list's order.

Equations

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

def Lucy1994.motionRoots : List Semantics.Root

The sampled motion roots of (4).

Equations

• Lucy1994.motionRoots = [Lucy1994.maan, Lucy1994.peek, Lucy1994.bin, Lucy1994.taal, Lucy1994.uul, Lucy1994.ok, Lucy1994.luub, Lucy1994.liik, Lucy1994.naak]

def Lucy1994.hashMarked : List Semantics.Root

The #-marked subset of (4), the roots lacking the -Vl imperfective: for the paper, the only candidate formal class of motion verbs (p. 641).

Equations

• Lucy1994.hashMarked = [Lucy1994.maan, Lucy1994.peek, Lucy1994.bin, Lucy1994.taal, Lucy1994.uul]

def Lucy1994.positionalRoots : List Semantics.Root

The sampled positional roots.

Equations

• Lucy1994.positionalRoots = [Lucy1994.cin, Lucy1994.cil]

def Lucy1994.sampledRoots : List Semantics.Root

Every sampled root.

Equations

• Lucy1994.sampledRoots = Lucy1994.agentSalientRoots ++ Lucy1994.agentPatientSalientRoots ++ Lucy1994.patientSalientRoots ++ Lucy1994.motionRoots ++ Lucy1994.positionalRoots

Diagnostic operators

structure Lucy1994.DiagOp : Type

A diagnostic derivational operator is given by its exponent, the core-argument positions it adds, and its structural applicability condition with bundled decidability, since the inventory holds heterogeneous conditions. Selection comes from the Morphology.Exponence.Rule instance.

• exponent : String

  The suffix, in the paper's orthography.

• adds : ArgumentStructure.Valency

  The core-argument positions the derivation adds (transitiviser_adds_compl).

• Applies : Semantics.Root → Prop

  The structural condition on the root.

• decApplies : DecidablePred self.Applies

  Bundled decidability of the condition.

@[instance_reducible]

instance Lucy1994.instRuleDiagOpRootString : Morphology.Exponence.Rule DiagOp Semantics.Root String

Equations

• Lucy1994.instRuleDiagOpRootString = { exponent := Lucy1994.DiagOp.exponent, Applies := Lucy1994.DiagOp.Applies }

@[instance_reducible]

instance Lucy1994.instDecidableRelDiagOpRootAppliesString : DecidableRel Morphology.Exponence.Applies

Equations

• Lucy1994.instDecidableRelDiagOpRootAppliesString op r = op.decApplies r

@[simp]

theorem Lucy1994.applies_iff (op : DiagOp) (r : Semantics.Root) : Morphology.Exponence.Applies op r ↔ op.Applies r

def Lucy1994.affectiveT : DiagOp

Affective =t transitivises an agent-salient root by adding a patient argument.

Equations

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

def Lucy1994.zeroDeriv : DiagOp

Under zero derivation =∅ the root alone supports a transitive stem.

Equations

• Lucy1994.zeroDeriv = { exponent := "=∅", adds := ∅, Applies := fun (r : Semantics.Root) => ArgumentStructure.ArgPosition.internal ∈ Lucy1994.valency r, decApplies := inferInstance }

def Lucy1994.causativeS : DiagOp

Causative =s transitivises a patient-salient root by adding an agent argument.

Equations

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

def Lucy1994.positionalLah : DiagOp

The positional derivation, realized =lah ~ =tal by status, the =tal incompletive apparently compounding with tàal 'come' (p. 643).

Equations

• Lucy1994.positionalLah = { exponent := "=lah", adds := ∅, Applies := fun (r : Semantics.Root) => ArgumentStructure.IsPositional r.kinds, decApplies := inferInstance }

def Lucy1994.inventory : Morphology.Exponence.RuleSet DiagOp

The diagnostic inventory in the paper's order, the three transitivisers of (1) and then the positional derivation.

Equations

• Lucy1994.inventory = [Lucy1994.affectiveT, Lucy1994.zeroDeriv, Lucy1994.causativeS, Lucy1994.positionalLah]

def Lucy1994.predictedExponents (r : Semantics.Root) : List String

The exponents of the inventory's applicable operators at r, in inventory order, which are the root's predicted derivational behaviour.

Equations

• Lucy1994.predictedExponents r = List.map Lucy1994.DiagOp.exponent (Lucy1994.inventory.applicable r)

Predicted against attested derivations

def Lucy1994.attested (r : Semantics.Root) : List String

The derivations the paper attests for a root. Each is the final segment of a form that the root's row is related to, a derived stem or the bare derivational morpheme.

Equations

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

theorem Lucy1994.predicted_matches_attested (r : Semantics.Root) : r ∈ sampledRoots → predictedExponents r = attested r

The derivations predicted from signature and valency reproduce every derivation the paper attests.

The derived classification

def Lucy1994.predictedClass (r : Semantics.Root) : Option ArgumentStructure.SalienceClass

A root's predicted salience class.

Equations

• Lucy1994.predictedClass r = ArgumentStructure.SalienceClass.ofKinds r.kinds (Lucy1994.valency r)

def Lucy1994.exponentOf : ArgumentStructure.SalienceClass → String

The transitiviser each salience class requires.

Equations

• Lucy1994.exponentOf ArgumentStructure.SalienceClass.agent = "=t"
• Lucy1994.exponentOf ArgumentStructure.SalienceClass.agentPatient = "=∅"
• Lucy1994.exponentOf ArgumentStructure.SalienceClass.patient = "=s"

theorem Lucy1994.predictedExponents_eq (r : Semantics.Root) : predictedExponents r = List.map exponentOf (predictedClass r).toList ++ if ArgumentStructure.IsPositional r.kinds then ["=lah"] else []

Predicted derivational behaviour decomposes as the class's transitiviser followed by the positional derivation when the signature licenses it: the applicability profile is the classification, plus the cross-cutting positional diagnostic.

theorem Lucy1994.agentSalient_class (r : Semantics.Root) : r ∈ agentSalientRoots → predictedClass r = some ArgumentStructure.SalienceClass.agent

theorem Lucy1994.agentPatientSalient_class (r : Semantics.Root) : r ∈ agentPatientSalientRoots → predictedClass r = some ArgumentStructure.SalienceClass.agentPatient

theorem Lucy1994.patientSalient_class (r : Semantics.Root) : r ∈ patientSalientRoots → predictedClass r = some ArgumentStructure.SalienceClass.patient

theorem Lucy1994.rootTransitives_not_signature_uniform : ∃ r ∈ agentPatientSalientRoots, ∃ r' ∈ agentPatientSalientRoots, r.kinds ≠ r'.kinds

The =∅ class is not signature-homogeneous, p'is manner-only against k'os manner and result: root transitivity is carried by valency, not by any feature configuration.

The motion-verb non-class

theorem Lucy1994.motion_roots_not_separate_class (r : Semantics.Root) : r ∈ motionRoots → predictedClass r = predictedClass kiim

Notional motion roots form no salience class of their own, the paper's central typological point: each is classified exactly as the plain state-change root kíim 'die'.

theorem Lucy1994.hash_not_signature_definable : ∃ r ∈ hashMarked, ∃ r' ∈ motionRoots, r' ∉ hashMarked ∧ r.kinds = r'.kinds ∧ valency r = valency r'

The # subclass, the paper's only candidate formal motion class, is not a function of the entailment grid: péek (#) and lúub' (plain) agree in signature and valency. The class is carried by a morphological gap, not by lexical semantics.

theorem Lucy1994.transitiviser_adds_compl : affectiveT.adds = ArgumentStructure.SalienceClass.agent.stemValencyᶜ ∧ zeroDeriv.adds = ArgumentStructure.SalienceClass.agentPatient.stemValencyᶜ ∧ causativeS.adds = ArgumentStructure.SalienceClass.patient.stemValencyᶜ

The transitiviser system is complementation in the valency lattice: each class's required derivation adds the Boolean complement of its underived stem's valency, =t the patient the agent stem lacks, =s the agent the patient stem lacks, =∅ nothing.

Positional interstitiality

theorem Lucy1994.positional_crosscuts_transitiviser_classes : ArgumentStructure.IsPositional cin.kinds ∧ predictedClass cin = some ArgumentStructure.SalienceClass.agentPatient ∧ ArgumentStructure.IsPositional cil.kinds ∧ predictedClass cil = none

The positional diagnostic cross-cuts the transitiviser cut: čin is positional yet zero-derives a transitive, while čil is positional and outside the cut altogether. The paper's classes are diagnostics, not a partition.

Closure robustness

theorem Lucy1994.predictedClass_closure_invariant (r : Semantics.Root) (h : Semantics.Root.Kind.cause ∉ r.kinds) : ArgumentStructure.SalienceClass.ofKinds r.closedKinds (valency r) = predictedClass r

For cause-free roots, every root in this sample, collocational closure does not change the predicted class.