Comparative argument roles

import Linglib.Syntax.Clause.ArgumentRole

The comparative concepts S, A, P, T and R of alignment typology, in the sense Haspelmath calls Comrie's. A and P are the arguments of a language's major two-argument construction that represent the agent and the patient when it expresses an action, S is the argument of an intransitive clause coded like the single argument of a one-argument predicate, and T and R are the theme and the recipient of a physical-transfer verb such as 'give', together with whatever arguments are coded like them. Transitivity is defined from the roles, a transitive clause being one with an A and a P. Dixon's O is P.

Role rank puts A above P and R above T, and Haspelmath's role-reference associations say that a role's usual referential prominence follows its rank.

Main definitions

ArgumentRole: the five roles.
ArgumentRole.core: S, A and P, the roles monotransitive alignment compares.
ArgumentRole.Outranks, ArgumentRole.IsHigherRanked, ArgumentRole.IsLowerRanked: role rank.
ArgumentRole.MoreUsualFor: the order of prominence values by how usual they are for a role.

Implementation notes

The roles are coding slots, not semantic roles (ArgumentStructure.ThetaRole): the A of a language's transitive construction need not be an agent. The library's classifiers, ArgumentStructure.Valency.role and ArgumentFrame.argumentRole, read the roles off the number of core arguments, taking transitivity as given. Haspelmath calls this procedure Dixon's and argues against it; on the major two-argument construction it agrees with the definitions above. It departs from them on transfer verbs: ArgumentFrame.argumentRole names the objects of a double-object frame R and T in English order, and makes the sole object of an NP + PP frame P, so the theme of give a book to her is P rather than T.

References

Comrie 1978, Ergativity
Dixon 1994, Ergativity formalized
Haspelmath 2011, On S, A, P, T, and R as Comparative Concepts for Alignment Typology
Haspelmath 2021, Role-Reference Associations and the Explanation of Argument Coding Splits formalized

Declarations

The comparative argument roles of Haspelmath 2011: the sole argument of an intransitive clause, the two arguments of a transitive one, and the two objects of a ditransitive one.

inductive ArgumentRole L50–66

Type

S : ArgumentRole
The argument of an intransitive clause coded like the single argument of a one-argument predicate.
A : ArgumentRole
The argument of the major two-argument construction that represents the agent when the construction expresses an action.
P : ArgumentRole
The argument of the major two-argument construction that represents the patient when the construction expresses an action.
R : ArgumentRole
The recipient of a physical-transfer verb, or an argument coded like it.
T : ArgumentRole
The theme of a physical-transfer verb, or an argument coded like it.

Derives DecidableEq, Repr, Fintype.

Used by ArgumentRole.core, ArgumentRole.mem_core, ArgumentRole.Outranks, ArgumentRole.outranks_iff, ArgumentRole.IsHigherRanked, ArgumentRole.IsLowerRanked, ArgumentRole.instDecidablePredIsLowerRanked, ArgumentRole.IsHigherRanked.not_isLowerRanked, ArgumentRole.IsLowerRanked.not_isHigherRanked, ArgumentRole.MoreUsualFor, ArgumentRole.instDecidableMoreUsualForOfDecidableLT

Used in Fragments/Dargwa/Tanti/Agreement, Fragments/Dargwa/Tanti/Case, Fragments/Mayan/Agreement, Fragments/Mayan/Chol/Agreement, Fragments/Mayan/Chuj/Extraction and 34 more

The roles S, A and P, whose coding monotransitive alignment compares.

def ArgumentRole.core L70–71

Finset ArgumentRole

ArgumentRole.core = {ArgumentRole.S, ArgumentRole.A, ArgumentRole.P}

Built from

Used by ArgumentRole.mem_core

Used in CoonMateoPedroPreminger2014, Dixon1994, Imanishi2014

L73–74

Role rank

Role rank, Haspelmath 2021's (7): in a monotransitive construction A ranks above P, and in a ditransitive one R ranks above T. The sole argument S is unranked.

inductive ArgumentRole.Outranks L78–82

ArgumentRole → ArgumentRole → Prop

monotransitive : A.Outranks P
ditransitive : R.Outranks T

Built from

Used by ArgumentRole.outranks_iff, ArgumentRole.instDecidableRelOutranks, ArgumentRole.IsHigherRanked, ArgumentRole.IsLowerRanked, ArgumentRole.instDecidablePredIsHigherRanked, ArgumentRole.instDecidablePredIsLowerRanked

L84–85

L87

The role is the higher-ranked argument of its construction, A or R.

def ArgumentRole.IsHigherRanked L89–90

(r : ArgumentRole) :

Prop

r.IsHigherRanked = ∃ (s : ArgumentRole), r.Outranks s

Built from ,

Used by ArgumentRole.instDecidablePredIsHigherRanked, ArgumentRole.IsHigherRanked.not_isLowerRanked, ArgumentRole.IsLowerRanked.not_isHigherRanked, ArgumentRole.MoreUsualFor, ArgumentRole.instDecidableMoreUsualForOfDecidableLT

Used in Haspelmath2021, Just2024

The role is the lower-ranked argument of its construction, P or T.

def ArgumentRole.IsLowerRanked L92–93

(r : ArgumentRole) :

Prop

r.IsLowerRanked = ∃ (s : ArgumentRole), s.Outranks r

Built from ,

Used by ArgumentRole.instDecidablePredIsLowerRanked, ArgumentRole.IsHigherRanked.not_isLowerRanked, ArgumentRole.IsLowerRanked.not_isHigherRanked, ArgumentRole.MoreUsualFor, ArgumentRole.instDecidableMoreUsualForOfDecidableLT

Used in Haspelmath2021

Prominence x is a more usual association than y for role r, Haspelmath 2021's (9): a higher-ranked role tends to be referentially prominent and a lower-ranked one non-prominent, so nothing is more usual for S.

def ArgumentRole.MoreUsualFor L107–111

{α : Type u_1} [LT α] (r : ArgumentRole) (x y : α) :

Prop

r.MoreUsualFor x y = (r.IsHigherRanked ∧ y < x ∨ r.IsLowerRanked ∧ x < y)

Built from , ,

Used by ArgumentRole.instDecidableMoreUsualForOfDecidableLT

Used in Haspelmath2021

L113–115