Valency

The two core-argument positions of a verbal clause — the internal argument (complement of the lexical core) and the external argument (specifier of Voice, [Kra96]) — and valency: the set of positions an argument-introducing locus (root, functional head, derivational operator) contributes. Valencies form the Boolean lattice Finset ArgPosition; introducers compose by ∪, and valency-changing operations ([Cre25]) are maps on the lattice.

[Coo19]'s division of labor is stated as predicates over valencies (IsRootValency, IsVoiceValency), not baked into a type: roots introduce at most the internal argument, v Voice at most the external. The former two-case enum Root.Arity (selectsTheme valency {.internal}, noTheme ~ valency ∅) was this lattice restricted by the thesis.

label maps a valency to the comparative core-term labels of Features.Prominence.ArgumentRole: a lone position — internal or external alike — surfaces as S, both together as A and P. The labels are relational, so label is deliberately not monotone (label_not_monotone): adding a co-argument relabels S, which is why alignment typology needs S as its own comparative concept.

Main declarations

• ArgPosition, Valency
• Valency.IsRootValency, IsVoiceValency, IsTransitive
• Valency.label — valencies to comparative core-term labels

inductive ArgumentStructure.ArgPosition : Type

A core-argument position of the verbal clause: the internal argument (complement of the lexical core) or the external argument (specifier of Voice, [Kra96]).

• internal : ArgPosition
• external : ArgPosition

@[instance_reducible]

instance ArgumentStructure.instDecidableEqArgPosition : DecidableEq ArgPosition

Equations

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

@[instance_reducible]

instance ArgumentStructure.instFintypeArgPosition : Fintype ArgPosition

Equations

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

@[instance_reducible]

instance ArgumentStructure.instReprArgPosition : Repr ArgPosition

Equations

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

def ArgumentStructure.instReprArgPosition.repr : ArgPosition → ℕ → Std.Format

Equations

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

@[reducible, inline]

abbrev ArgumentStructure.Valency : Type

The set of core-argument positions an argument-introducing locus contributes; inherits the Boolean lattice of finite sets, and introducers compose by ∪.

Equations

• ArgumentStructure.Valency = Finset ArgumentStructure.ArgPosition

@[instance_reducible]

instance ArgumentStructure.instReprValency : Repr Valency

Finset carries no Repr; over the two-element position universe the four valencies render literally.

Equations

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

def ArgumentStructure.Valency.IsRootValency (v : Valency) : Prop

[Coo19]'s division of labor, root half: roots introduce at most the internal argument. A thesis about the lexicon, stated as a predicate rather than a type restriction.

Equations

• v.IsRootValency = (v ⊆ {ArgumentStructure.ArgPosition.internal})

@[instance_reducible]

instance ArgumentStructure.Valency.instDecidableIsRootValency (v : Valency) : Decidable v.IsRootValency

Equations

• v.instDecidableIsRootValency = ArgumentStructure.Valency.instDecidableIsRootValency._aux_1 v

def ArgumentStructure.Valency.IsVoiceValency (v : Valency) : Prop

[Coo19]'s division of labor, functional half: v ~ Voice heads introduce at most the external argument.

Equations

• v.IsVoiceValency = (v ⊆ {ArgumentStructure.ArgPosition.external})

@[instance_reducible]

instance ArgumentStructure.Valency.instDecidableIsVoiceValency (v : Valency) : Decidable v.IsVoiceValency

Equations

• v.instDecidableIsVoiceValency = ArgumentStructure.Valency.instDecidableIsVoiceValency._aux_1 v

def ArgumentStructure.Valency.IsTransitive (v : Valency) : Prop

A transitive clause realizes both core positions.

Equations

• v.IsTransitive = (v = {ArgumentStructure.ArgPosition.internal, ArgumentStructure.ArgPosition.external})

@[instance_reducible]

instance ArgumentStructure.Valency.instDecidableIsTransitive (v : Valency) : Decidable v.IsTransitive

Equations

• v.instDecidableIsTransitive = ArgumentStructure.Valency.instDecidableIsTransitive._aux_1 v

theorem ArgumentStructure.Valency.isRootValency_inter_isVoiceValency (v v' : Valency) : v.IsRootValency → v'.IsVoiceValency → v ∩ v' = ∅

Root and Voice valencies are disjoint, so under the division of labor the two loci partition a transitive clause's core positions.

theorem ArgumentStructure.Valency.isTransitive_union_iff (v v' : Valency) : v.IsRootValency → v'.IsVoiceValency → ((v ∪ v').IsTransitive ↔ v = {ArgPosition.internal} ∧ v' = {ArgPosition.external})

A root valency and a Voice valency compose to a transitive clause iff each introduces its position.

Comparative core-term labels

def ArgumentStructure.Valency.label (v : Valency) : Finset Features.Prominence.ArgumentRole

The comparative core-term labels a valency's arguments surface with (S A P, Features.Prominence.ArgumentRole): a lone position — internal or external alike — is the S of an intransitive clause; both together are A and P.

Equations

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

theorem ArgumentStructure.Valency.s_mem_label_iff (v : Valency) : Features.Prominence.ArgumentRole.S ∈ v.label ↔ v = {ArgPosition.internal} ∨ v = {ArgPosition.external}

S surfaces exactly for the two singleton valencies — the unaccusative (internal) and unergative (external) S, which split-intransitive systems mark differently.

theorem ArgumentStructure.Valency.label_not_monotone : ¬Monotone label

Labels are relational, not positional: adding a co-argument relabels S to A or P, so label is not monotone in the lattice.