Core arguments of a clause token

What each core-argument position of a clause (ArgumentStructure.ArgPosition) bears — a DP, its φ-features, its number — with none at an unfilled position. The filled positions are the clause's valency.

Main definitions

• Clause.Arguments α — the assignment of an α to each filled position.
• Clause.Arguments.unaccusative, unergative, transitive, empty — the clause shapes by which positions are filled.
• Clause.Arguments.valency — the filled positions.
• Clause.Arguments.codingRole — the comparative S/A/P classification of a filled position; the clause, not the predicate, takes the classification.

Main results

• Clause.Arguments.unaccusative_isRootValency, transitive_isTransitive — the shapes land in the valency classes of [Coo19]'s division of labor.

@[reducible, inline]

abbrev Clause.Arguments (α : Type u_1) : Type u_1

What each core-argument position of a clause token bears, none where the position is unfilled.

Equations

• Clause.Arguments α = (ArgumentStructure.ArgPosition → Option α)

def Clause.Arguments.unaccusative {α : Type u_1} (x : α) : Arguments α

An intransitive clause whose sole argument is internal.

Equations

• Clause.Arguments.unaccusative x ArgumentStructure.ArgPosition.internal = some x
• Clause.Arguments.unaccusative x ArgumentStructure.ArgPosition.external = none

def Clause.Arguments.unergative {α : Type u_1} (x : α) : Arguments α

An intransitive clause whose sole argument is external.

Equations

• Clause.Arguments.unergative x ArgumentStructure.ArgPosition.internal = none
• Clause.Arguments.unergative x ArgumentStructure.ArgPosition.external = some x

def Clause.Arguments.transitive {α : Type u_1} (obj subj : α) : Arguments α

A transitive clause: an internal argument obj and an external one subj.

Equations

• Clause.Arguments.transitive obj subj ArgumentStructure.ArgPosition.internal = some obj
• Clause.Arguments.transitive obj subj ArgumentStructure.ArgPosition.external = some subj

def Clause.Arguments.empty {α : Type u_1} : Arguments α

A clause with no core argument filled.

Equations

• Clause.Arguments.empty x✝ = none

def Clause.Arguments.valency {α : Type u_1} (c : Arguments α) : ArgumentStructure.Valency

The filled positions.

Equations

• c.valency = {p : ArgumentStructure.ArgPosition | (c p).isSome = true}

def Clause.Arguments.codingRole {α : Type u_1} (c : Arguments α) : ArgumentStructure.ArgPosition → Option ArgumentRole

The comparative classification of a filled position — the clause takes the classification: the sole argument of a one-place clause is S; in a two-place clause the external argument is A and the internal P. ArgumentFrame.argumentRole classifies the slots of an argument frame by their coding.

Equations

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

@[simp]

theorem Clause.Arguments.codingRole_unaccusative {α : Type u_1} (x : α) : (unaccusative x).codingRole ArgumentStructure.ArgPosition.internal = some ArgumentRole.S

@[simp]

theorem Clause.Arguments.codingRole_unergative {α : Type u_1} (x : α) : (unergative x).codingRole ArgumentStructure.ArgPosition.external = some ArgumentRole.S

@[simp]

theorem Clause.Arguments.codingRole_transitive {α : Type u_1} (obj subj : α) : (transitive obj subj).codingRole ArgumentStructure.ArgPosition.external = some ArgumentRole.A ∧ (transitive obj subj).codingRole ArgumentStructure.ArgPosition.internal = some ArgumentRole.P

@[simp]

theorem Clause.Arguments.valency_unaccusative {α : Type u_1} (x : α) : (unaccusative x).valency = {ArgumentStructure.ArgPosition.internal}

@[simp]

theorem Clause.Arguments.valency_unergative {α : Type u_1} (x : α) : (unergative x).valency = {ArgumentStructure.ArgPosition.external}

@[simp]

theorem Clause.Arguments.valency_transitive {α : Type u_1} (obj subj : α) : (transitive obj subj).valency = {ArgumentStructure.ArgPosition.internal, ArgumentStructure.ArgPosition.external}

@[simp]

theorem Clause.Arguments.valency_empty {α : Type u_1} : empty.valency = ∅

theorem Clause.Arguments.unaccusative_isRootValency {α : Type u_1} (x : α) : (unaccusative x).valency.IsRootValency

An unaccusative clause's sole argument occupies the root's valency.

theorem Clause.Arguments.unergative_isVoiceValency {α : Type u_1} (x : α) : (unergative x).valency.IsVoiceValency

An unergative clause's sole argument occupies Voice's valency.

theorem Clause.Arguments.transitive_isTransitive {α : Type u_1} (obj subj : α) : (transitive obj subj).valency.IsTransitive