Comparative argument roles

ArgumentRole: the S/A/P/R/T comparative concepts for argument coding, neutral between case and agreement. The clause takes the classification — a passive clause's sole argument is S whatever the predicate calls it — so the label set lives with the clause vocabulary; Clause.Arguments.codingRole classifies clause tokens and Verb.codingRoles the citation clause. ArgumentRole.core is the monotransitive core that alignment partitions quantify over; IsHighDefault/IsLowDefault classify the roles by their usual referential prominence (the role-reference association).

Distinct from the semantic tier (ArgumentStructure.ThetaRole, the Dowty proto-role profiles): S/A/P/R/T are construction-relative coding slots — the A of a transitive clause may be an instrument or experiencer, and S spans unergative agents and unaccusative patients, which is what lets alignment statements like "S groups with P" be expressed at all. The linking theories relating the two tiers live in Semantics/ArgumentStructure/Linking.lean and its studies.

References

• [Com78]
• [haspelmath-2021]

inductive ArgumentRole : Type

Argument roles spanning monotransitive and ditransitive clauses, following [Com78] and [haspelmath-2021] in using S/A/P/R/T (not subject/object) to avoid theory-dependent constituency assumptions.

• S : ArgumentRole

  S: sole argument of an intransitive verb

• A : ArgumentRole

  A: the more agent-like argument of a transitive verb

• P : ArgumentRole

  P: the more patient-like argument of a transitive verb

• R : ArgumentRole

  R: the recipient-like argument of a ditransitive verb

• T : ArgumentRole

  T: the theme-like argument of a ditransitive verb

@[instance_reducible]

instance instDecidableEqArgumentRole : DecidableEq ArgumentRole

Equations

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

def instReprArgumentRole.repr : ArgumentRole → Nat → Std.Format

Equations

• instReprArgumentRole.repr ArgumentRole.S prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "ArgumentRole.S")).group prec✝
• instReprArgumentRole.repr ArgumentRole.A prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "ArgumentRole.A")).group prec✝
• instReprArgumentRole.repr ArgumentRole.P prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "ArgumentRole.P")).group prec✝
• instReprArgumentRole.repr ArgumentRole.R prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "ArgumentRole.R")).group prec✝
• instReprArgumentRole.repr ArgumentRole.T prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "ArgumentRole.T")).group prec✝

@[instance_reducible]

instance instReprArgumentRole : Repr ArgumentRole

Equations

• instReprArgumentRole = { reprPrec := instReprArgumentRole.repr }

def ArgumentRole.core : List ArgumentRole

The monotransitive core roles: A, P, and S (omits the ditransitive scaffolding roles R/T). The domain over which alignment partitions and per-language case/agreement coverage theorems quantify.

Equations

• ArgumentRole.core = [ArgumentRole.A, ArgumentRole.P, ArgumentRole.S]

def ArgumentRole.IsHighDefault (r : ArgumentRole) : Prop

The role defaults to high referential prominence (A and R, which are usually human, definite, topical) — so differential marking targets its non-prominent end ([haspelmath-2021]'s (6)).

Equations

• r.IsHighDefault = (r = ArgumentRole.A ∨ r = ArgumentRole.R)

@[instance_reducible]

instance instDecidableIsHighDefault (r : ArgumentRole) : Decidable r.IsHighDefault

Equations

• instDecidableIsHighDefault r = instDecidableIsHighDefault._aux_1 r

def ArgumentRole.IsLowDefault (r : ArgumentRole) : Prop

The role defaults to low referential prominence (P and T) — so differential marking targets its prominent end. S is the alignment reference point and is neither.

Equations

• r.IsLowDefault = (r = ArgumentRole.P ∨ r = ArgumentRole.T)

@[instance_reducible]

instance instDecidableIsLowDefault (r : ArgumentRole) : Decidable r.IsLowDefault

Equations

• instDecidableIsLowDefault r = instDecidableIsLowDefault._aux_1 r