Salience classes

[Luc94]'s classification of verbal roots by required transitiviser — "salience" is his term for the default semantic values in a root that influence overt case marking, which is why the classifier lives in the argument-realization layer. Stated over the (kind signature × arity) coordinates: agent salient (intransitive manner roots), agent-patient salient (root transitives), patient salient (intransitive change-of-state roots). The positional diagnostic (IsPositional) is deliberately separate and arity-free — positional roots cross-cut the transitiviser classes rather than forming a fourth case.

Originates with [Luc94] (Yucatec =t, =∅, =s); the Yucatec instantiation with attested derivations is Studies/Lucy1994.lean.

Main declarations

• SalienceClass
• IsAgentSalient, IsPatientSalient, IsPositional
• SalienceClass.ofKinds — the pair-level classifier
• SalienceClass.ofRoot — the classifier on an annotated root, agreeing with ofKinds on manner-free signatures (ofRoot_eq_ofKinds)
• SalienceClass.ofKinds_close — closure invariance on cause-free signatures

inductive ArgumentStructure.SalienceClass : Type

Lucy's "three large predicate root classes", named for the argument(s) the underived root makes salient. Positional roots are deliberately not a case: they fall outside the transitiviser cut (IsPositional).

• agent : SalienceClass
• agentPatient : SalienceClass
• patient : SalienceClass

@[instance_reducible]

instance ArgumentStructure.instDecidableEqSalienceClass : DecidableEq SalienceClass

Equations

• ArgumentStructure.instDecidableEqSalienceClass x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

@[instance_reducible]

instance ArgumentStructure.instFintypeSalienceClass : Fintype SalienceClass

Equations

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

@[instance_reducible]

instance ArgumentStructure.instReprSalienceClass : Repr SalienceClass

Equations

• ArgumentStructure.instReprSalienceClass = { reprPrec := ArgumentStructure.instReprSalienceClass.repr }

def ArgumentStructure.instReprSalienceClass.repr : SalienceClass → ℕ → Std.Format

Equations

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

@[reducible, inline]

abbrev ArgumentStructure.IsAgentSalient (s : Semantics.Root.Kinds) (v : Valency) : Prop

Agent salient: intransitive manner-of-action root ("actions or activities that some entity undertakes").

Equations

• ArgumentStructure.IsAgentSalient s v = (ArgumentStructure.ArgPosition.internal ∉ v ∧ Semantics.Root.Kind.manner ∈ s ∧ Semantics.Root.Kind.result ∉ s)

@[reducible, inline]

abbrev ArgumentStructure.IsPatientSalient (s : Semantics.Root.Kinds) (v : Valency) : Prop

Patient salient: intransitive change-of-state root ("state changes that some entity undergoes more or less spontaneously").

Equations

• ArgumentStructure.IsPatientSalient s v = (ArgumentStructure.ArgPosition.internal ∉ v ∧ Semantics.Root.Kind.manner ∉ s ∧ Semantics.Root.Kind.result ∈ s)

@[reducible, inline]

abbrev ArgumentStructure.IsPositional (s : Semantics.Root.Kinds) : Prop

Positional: pure stative configurational signature. Deliberately valency-free — a positional root may also zero-derive a transitive ([Luc94]'s čin 'bend'), so the positional class cross-cuts the transitiviser cut.

Equations

• ArgumentStructure.IsPositional s = (s = {Semantics.Root.Kind.state})

def ArgumentStructure.SalienceClass.ofKinds (s : Semantics.Root.Kinds) (v : Valency) : Option SalienceClass

The transitiviser cut, over (kind signature × root valency). Agent-patient salience is root transitivity (the root introduces the internal argument), not a feature configuration; the two intransitive classes split by signature; intransitive signatures with neither manner nor result — pure statives included — are outside the cut.

Equations

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

theorem ArgumentStructure.SalienceClass.ofKinds_close (s : Semantics.Root.Kinds) (v : Valency) (h : Semantics.Root.Kind.cause ∉ s) : ofKinds s.close v = ofKinds s v

Collocational closure does not move the transitiviser cut on cause-free signatures: the only available closure edge is result→state, which no arm of the classifier consults.

theorem ArgumentStructure.SalienceClass.ofKinds_close_cause : ofKinds {Semantics.Root.Kind.cause} ∅ = none ∧ ofKinds {Semantics.Root.Kind.cause}.close ∅ = some patient

The cause-free hypothesis of ofKinds_close is necessary: a lone cause atom is outside the cut at base but patient salient after closure.

def ArgumentStructure.SalienceClass.ofRoot (r : Semantics.Root) : Option SalienceClass

The salience class of a root from its annotation, agent-patient for a root licensing transitive Voice and patient for any other root carrying result ([Luc94]; [Coo19] §3.3). A root with neither is left undetermined, since without atoms a manner root and a stative one look alike.

Equations

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

theorem ArgumentStructure.SalienceClass.ofRoot_eq_ofKinds (v : Valency) {r : Semantics.Root} (h : Semantics.Root.Kind.manner ∉ r.kinds) (hl : r.licensesTransitiveVoice = decide (ArgPosition.internal ∈ v)) : ofRoot r = ofKinds r.kinds v

On manner-free signatures the annotation-level classifier agrees with the signature-level one, when the root is annotated as licensing transitive Voice exactly when its valency has the internal position.

Stem valencies

def ArgumentStructure.SalienceClass.stemValency : SalienceClass → Valency

The underived stem's valency per salience class: the unergative agent stem realizes only Voice's external S, the unaccusative patient stem only the internal S, and the root-transitive stem both positions.

Equations

• ArgumentStructure.SalienceClass.agent.stemValency = {ArgumentStructure.ArgPosition.external}
• ArgumentStructure.SalienceClass.agentPatient.stemValency = {ArgumentStructure.ArgPosition.internal, ArgumentStructure.ArgPosition.external}
• ArgumentStructure.SalienceClass.patient.stemValency = {ArgumentStructure.ArgPosition.internal}

theorem ArgumentStructure.SalienceClass.label_stemValency (c : SalienceClass) : c.stemValency.label = if c = agentPatient then {ArgumentRole.A, ArgumentRole.P} else {ArgumentRole.S}

Both intransitive classes surface a lone S; the agent-patient class surfaces A and P (Valency.label's relational relabeling).