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.

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}

@[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