Pylkkänen (2008): Introducing Arguments

Pylkkänen's inventory of argument-introducing heads underlies two typologies. Applicative heads are high or low: a high applicative relates the applied argument to the event and combines with the verb phrase by Event Identification, and a low applicative relates it to the verb's theme by a transfer of possession and takes the verb as its argument. Causative heads share one meaning, Cause, which relates a causing event to a caused one and introduces no individual; they vary in whether Cause is bundled with Voice and in whether it selects a root, a verb or a phase. The diagnostics that separate the heads, such as the restriction of low applicatives to structures with a direct object, are facts about semantic types, derived here by the type-driven composition engine.

Main definitions

• lowAppl: the low applicative.
• cause: Cause, the meaning shared by every causative head.
• CauseHead.Embeds: the layers a causative head's complement may contain.

Main results

• composes_unergative_iff: only high applicatives combine with unergatives.
• lowAppl_agent_eq_bot: a low applicative over an unergative makes the object agent and theme.
• cause_voice_order: Cause applies before Voice.
• hasCauseePosition_iff: a root-selecting, Voice-bundling causative leaves no causee position.

Implementation notes

Semantic types are those of Montague.Ty, in which events share the type e with individuals, as in the composition engine: the book's ⟨s,t⟩ is Ty.et and ⟨e,⟨s,t⟩⟩ is Ty.eet. A constituent fails to compose with another exactly when tyBinary returns none.

The third applicative diagnostic, the availability of the applied argument for depictive modification, is also a typing fact in the book: a depictive phrase is of type ⟨e,⟨s,t⟩⟩ and combines by Predicate Modification with constituents of that type, which a high Appl' is and a low Appl' is not. The engine's predicate modification is at ⟨e,t⟩ only, so that diagnostic is recorded in the data rows only.

The Voice-bundling status of the Bemba, Luganda, and Venda causatives is unknown (Table 3.1, note a), so only the English, Japanese, and Finnish heads are given as CauseHead values.

TODO

The second applicative diagnostic (18), that low applicatives are nonsensical with completely static verbs such as hold, is a fact about the plausibility of the transfer of possession (15) asserts, not a typing fact: the low ApplP composes with a static transitive verb (lowApplP_composes_transitive). Since the transfer relation of (15) is not relativized to the event, the clash with a static event does not follow from the denotation; the study records the book's correlation of the two tests across Table 2.1 (table21_static_iff_unergative).

References

• [Pyl08]
• [Kra96]
• [Mar93]
• [Mar97]
• [Cue03]

Applicatives: high relates to the event, low to the theme

def Pylkkanen2008.lowAppl {Entity : Type u_1} {E : Type u_2} (theme : Entity → E → Prop) (poss : Entity → Entity → Prop) (x y : Entity) (f : Entity → E → Prop) : E → Prop

The low applicative (15) relates the direct object x to the indirect object y by the transfer relation poss, to-the-possession for a recipient applicative and from-the-possession for a source applicative, and asserts that x is the theme of the verb f.

Equations

• Pylkkanen2008.lowAppl theme poss x y f e = (f x e ∧ theme x e ∧ poss x y)

@[reducible, inline]

abbrev Pylkkanen2008.lowApplTy : Montague.Ty

lowApplTy is the type of the low applicative head (15), ⟨e,⟨e,⟨⟨e,⟨s,t⟩⟩,⟨s,t⟩⟩⟩⟩.

Equations

• Pylkkanen2008.lowApplTy = (Montague.Ty.e ⇒ Montague.Ty.e ⇒ Montague.Ty.eet ⇒ Montague.Ty.et)

def Pylkkanen2008.sisterTy : Minimalist.ApplType → Option Montague.Ty

sisterTy a is the type of the applicative constituent that is the verb's sister, the high applicative head (13) of type ⟨e,⟨s,t⟩⟩, which the verb phrase combines with by Event Identification, or the low ApplP of type ⟨⟨e,⟨s,t⟩⟩,⟨s,t⟩⟩, which takes the verb as its argument. The affected applicative of [Cue03] is outside the book's inventory and has no type here.

Equations

• Pylkkanen2008.sisterTy Minimalist.ApplType.high = some Montague.Ty.eet
• Pylkkanen2008.sisterTy (Minimalist.ApplType.low relation) = some (Montague.Ty.eet ⇒ Montague.Ty.et)
• Pylkkanen2008.sisterTy Minimalist.ApplType.affected = none

theorem Pylkkanen2008.composes_unergative_iff (a : Minimalist.ApplType) : (∃ τ ∈ sisterTy a, (HeimKratzer.Tree.tyBinary τ Montague.Ty.et).isSome = true) ↔ a = Minimalist.ApplType.high

An applicative composes with an unergative verb phrase, of type ⟨s,t⟩, exactly when it is high, Diagnostic 1 (17).

theorem Pylkkanen2008.lowAppl_not_composes_unergative (τ : Montague.Ty) : τ ∈ [lowApplTy, Montague.Ty.e ⇒ Montague.Ty.eet ⇒ Montague.Ty.et, Montague.Ty.eet ⇒ Montague.Ty.et] → HeimKratzer.Tree.tyBinary τ Montague.Ty.et = none ∧ HeimKratzer.Tree.tyBinary Montague.Ty.et τ = none

A low applicative cannot appear in a structure that lacks a direct object (17), since at no stage of its saturation does it compose with an unergative verb phrase, in either order.

theorem Pylkkanen2008.lowApplP_composes_transitive : HeimKratzer.Tree.tyBinary (Montague.Ty.eet ⇒ Montague.Ty.et) Montague.Ty.eet = some Montague.Ty.et

The low ApplP composes with a transitive verb, static or not, so the second diagnostic (18) is not a typing fact.

theorem Pylkkanen2008.voiceP_lowAppl {Entity : Type u_1} {E : Type u_2} (agent theme : Entity → E → Prop) (poss : Entity → Entity → Prop) (buying : E → Prop) (mary john book : Entity) (e : E) : ArgumentStructure.eventIdentification agent (lowAppl theme poss book john (ArgumentStructure.eventIdentification theme buying)) mary e ↔ buying e ∧ agent mary e ∧ theme book e ∧ poss book john

In the derivation (16) of Mary bought John the book, the low ApplP takes the verb, whose denotation relates its theme to a buying event, and Voice adds the agent by Event Identification.

theorem Pylkkanen2008.lowAppl_agent_eq_bot {Entity : Type u_1} {E : Type u_2} {agent theme : Entity → E → Prop} (h : Disjoint agent theme) (poss : Entity → Entity → Prop) (run : E → Prop) (x y : Entity) : lowAppl theme poss x y (ArgumentStructure.eventIdentification agent run) = ⊥

Over an unergative the constituent of type ⟨e,⟨s,t⟩⟩ is the Voice' whose open argument is the agent, and the low ApplP composed with it holds of no event when no participant is both agent and theme, the contradiction of (103b).

inductive Pylkkanen2008.Construction : Type

A Construction is one of the applicative constructions the book analyzes, with the head it assigns (Table 1.1, together with the Korean and Albanian applicatives of Chapter 2).

• chagaBenefactive : Construction
• lugandaBenefactive : Construction
• vendaBenefactive : Construction
• albanianBenefactive : Construction
• japaneseGaplessAdversity : Construction
• englishDOC : Construction
• japaneseDOC : Construction
• koreanDOC : Construction
• hebrewPossessorDative : Construction
• japaneseAdversityCausative : Construction
• japaneseGappedAdversity : Construction

@[instance_reducible]

instance Pylkkanen2008.instDecidableEqConstruction : DecidableEq Construction

Equations

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

def Pylkkanen2008.instReprConstruction.repr : Construction → ℕ → Std.Format

Equations

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

@[instance_reducible]

instance Pylkkanen2008.instReprConstruction : Repr Construction

Equations

• Pylkkanen2008.instReprConstruction = { reprPrec := Pylkkanen2008.instReprConstruction.repr }

def Pylkkanen2008.Construction.head : Construction → Minimalist.ApplType

c.head is the head the book assigns to the construction c.

Equations

• Pylkkanen2008.Construction.chagaBenefactive.head = Minimalist.ApplType.high
• Pylkkanen2008.Construction.lugandaBenefactive.head = Minimalist.ApplType.high
• Pylkkanen2008.Construction.vendaBenefactive.head = Minimalist.ApplType.high
• Pylkkanen2008.Construction.albanianBenefactive.head = Minimalist.ApplType.high
• Pylkkanen2008.Construction.japaneseGaplessAdversity.head = Minimalist.ApplType.high
• Pylkkanen2008.Construction.englishDOC.head = Minimalist.ApplType.low Minimalist.LowRelation.recipient
• Pylkkanen2008.Construction.japaneseDOC.head = Minimalist.ApplType.low Minimalist.LowRelation.recipient
• Pylkkanen2008.Construction.koreanDOC.head = Minimalist.ApplType.low Minimalist.LowRelation.recipient
• Pylkkanen2008.Construction.hebrewPossessorDative.head = Minimalist.ApplType.low Minimalist.LowRelation.source
• Pylkkanen2008.Construction.japaneseAdversityCausative.head = Minimalist.ApplType.low Minimalist.LowRelation.source
• Pylkkanen2008.Construction.japaneseGappedAdversity.head = Minimalist.ApplType.low Minimalist.LowRelation.source

def Pylkkanen2008.Construction.ComposesUnergative (c : Construction) : Prop

A construction composes with an unergative verb phrase when its head's applicative constituent does.

Equations

• c.ComposesUnergative = ∃ τ ∈ Pylkkanen2008.sisterTy c.head, (HeimKratzer.Tree.tyBinary τ Montague.Ty.et).isSome = true

@[instance_reducible]

instance Pylkkanen2008.instDecidablePredConstructionComposesUnergative : DecidablePred Construction.ComposesUnergative

Equations

• Pylkkanen2008.instDecidablePredConstructionComposesUnergative c = Pylkkanen2008.instDecidablePredConstructionComposesUnergative._aux_1 c

def Pylkkanen2008.table21 : List (Construction × Datum × Datum)

Table 2.1 lists each of the six languages with the construction tested, its unergative test, and its static-verb test.

Equations

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

theorem Pylkkanen2008.table21_unergative (t : Construction × Datum × Datum) : t ∈ table21 → (t.2.1.judgment = Judgment.acceptable ↔ t.1.ComposesUnergative)

In Table 2.1, test 1, the applicative attaches to an unergative in exactly the languages whose head composes with one.

theorem Pylkkanen2008.table21_static_iff_unergative (t : Construction × Datum × Datum) : t ∈ table21 → (t.2.2.judgment = Judgment.acceptable ↔ t.2.1.judgment = Judgment.acceptable)

Across the six languages of Table 2.1 the static-verb test patterns with the unergative test, the correlation of §2.1.2.

theorem Pylkkanen2008.adversity_passives : Construction.japaneseGaplessAdversity.ComposesUnergative ∧ ¬Construction.japaneseGappedAdversity.ComposesUnergative

The gapless Japanese adversity passive, a high applicative, composes with unergatives, while the gapped one, a low source applicative, does not (Table 2.5).

theorem Pylkkanen2008.possessor_dative_transitivity : ¬Construction.hebrewPossessorDative.ComposesUnergative

The transitivity restriction on Hebrew possessor datives (102), Table 2.2, follows from their low source analysis.

Cause introduces a causing event, not a causer

def Pylkkanen2008.cause {E : Type u_2} (CAUSE : E → E → Prop) (f : E → Prop) : E → Prop

Cause (9), the meaning shared by every causative head, relates the event it describes to a caused event of which the predicate f holds, and introduces no individual.

Equations

• Pylkkanen2008.cause CAUSE f e = ∃ (e' : E), f e' ∧ CAUSE e e'

theorem Pylkkanen2008.melted_readings {Entity : Type u_1} {E : Type u_2} (CAUSE : E → E → Prop) (agent causer : Entity → E → Prop) (melt : E → Prop) (john : Entity) (e : E) : (ArgumentStructure.eventIdentification agent (cause CAUSE melt) john e ↔ agent john e ∧ ∃ (e' : E), melt e' ∧ CAUSE e e') ∧ (ArgumentStructure.eventIdentification causer melt john e ↔ causer john e ∧ melt e)

On the bieventive analysis (14) of John melted the ice, Voice relates John to an event that causes a melting, the reading (13b); on the θ-role analysis (16), a causer head relates John to the melting itself, the reading (15b).

@[reducible, inline]

abbrev Pylkkanen2008.causeTy : Montague.Ty

causeTy is the type of Cause (9), ⟨⟨s,t⟩,⟨s,t⟩⟩.

Equations

• Pylkkanen2008.causeTy = (Montague.Ty.et ⇒ Montague.Ty.et)

theorem Pylkkanen2008.unaccusative_causative : HeimKratzer.Tree.tyBinary causeTy Montague.Ty.et = some Montague.Ty.et ∧ HeimKratzer.Tree.tyBinary Montague.Ty.eet Montague.Ty.et = some Montague.Ty.eet

Cause applied to a verb phrase yields a predicate of events, the unaccusative causative (18), while the θ-role analysis's causer head (16a), of type ⟨e,⟨s,t⟩⟩, yields a relation that still awaits an individual (§3.2).

theorem Pylkkanen2008.cause_voice_order : HeimKratzer.Tree.tyBinary causeTy Montague.Ty.eet = none ∧ HeimKratzer.Tree.tyBinary Montague.Ty.eet causeTy = none ∧ (HeimKratzer.Tree.tyBinary causeTy Montague.Ty.et).bind (HeimKratzer.Tree.tyBinary Montague.Ty.eet) = some Montague.Ty.eet ∧ (HeimKratzer.Tree.tyBinary Montague.Ty.eet Montague.Ty.et).bind (HeimKratzer.Tree.tyBinary causeTy) = none

The two heads of the Voice-bundling Cause (42) cannot combine with each other, in either order, so they apply to the verb phrase one at a time, and only Cause first, since after Voice nothing Cause can take remains (§3.3).

Selection: Cause takes a root, a verb, or a phase

inductive Pylkkanen2008.Layer : Type

The layers of the Kratzer/Marantz verbal architecture (12) are the category-neutral root, the verb a category-defining head makes of it, and the phase closed by an external-argument introducer, Voice or a high applicative.

• root : Layer
• verb : Layer
• phase : Layer

@[instance_reducible]

instance Pylkkanen2008.instDecidableEqLayer : DecidableEq Layer

Equations

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

def Pylkkanen2008.instReprLayer.repr : Layer → ℕ → Std.Format

Equations

• Pylkkanen2008.instReprLayer.repr Pylkkanen2008.Layer.root prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Pylkkanen2008.Layer.root")).group prec✝
• Pylkkanen2008.instReprLayer.repr Pylkkanen2008.Layer.verb prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Pylkkanen2008.Layer.verb")).group prec✝
• Pylkkanen2008.instReprLayer.repr Pylkkanen2008.Layer.phase prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Pylkkanen2008.Layer.phase")).group prec✝

@[instance_reducible]

instance Pylkkanen2008.instReprLayer : Repr Layer

Equations

• Pylkkanen2008.instReprLayer = { reprPrec := Pylkkanen2008.instReprLayer.repr }

@[instance_reducible]

instance Pylkkanen2008.instFintypeLayer : Fintype Layer

Equations

• Pylkkanen2008.instFintypeLayer = { elems := { val := ↑Pylkkanen2008.Layer.enumList, nodup := Pylkkanen2008.Layer.enumList_nodup }, complete := Pylkkanen2008.instFintypeLayer._proof_1 }

def Pylkkanen2008.Layer.rank : Layer → ℕ

Layers are ordered by containment.

Equations

• Pylkkanen2008.Layer.root.rank = 0
• Pylkkanen2008.Layer.verb.rank = 1
• Pylkkanen2008.Layer.phase.rank = 2

@[instance_reducible]

instance Pylkkanen2008.instLinearOrderLayer : LinearOrder Layer

Equations

• Pylkkanen2008.instLinearOrderLayer = LinearOrder.lift' Pylkkanen2008.Layer.rank Pylkkanen2008.instLinearOrderLayer._proof_1

structure Pylkkanen2008.CauseHead : Type

A causative head is given by the largest layer its complement may contain (11) and whether Cause is bundled with Voice (10).

• selects : Layer
• bundled : Bool

@[instance_reducible]

instance Pylkkanen2008.instDecidableEqCauseHead : DecidableEq CauseHead

Equations

• Pylkkanen2008.instDecidableEqCauseHead = Pylkkanen2008.instDecidableEqCauseHead.decEq

def Pylkkanen2008.instDecidableEqCauseHead.decEq (x✝ x✝¹ : CauseHead) : Decidable (x✝ = x✝¹)

Equations

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

def Pylkkanen2008.instReprCauseHead.repr : CauseHead → ℕ → Std.Format

Equations

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

@[instance_reducible]

instance Pylkkanen2008.instReprCauseHead : Repr CauseHead

Equations

• Pylkkanen2008.instReprCauseHead = { reprPrec := Pylkkanen2008.instReprCauseHead.repr }

def Pylkkanen2008.CauseHead.Embeds (c : CauseHead) (l : Layer) : Prop

c.Embeds l holds when a constituent of layer l can occur between the root and Cause.

Equations

• c.Embeds l = (l ≤ c.selects)

@[instance_reducible]

instance Pylkkanen2008.instDecidableEmbeds (c : CauseHead) (l : Layer) : Decidable (c.Embeds l)

Equations

• Pylkkanen2008.instDecidableEmbeds c l = { decide := l.rank.ble c.selects.rank, reflects_decide := ⋯ }

theorem Pylkkanen2008.embeds_verb_iff (c : CauseHead) : c.Embeds Layer.verb ↔ c.selects ≠ Layer.root

VP modifiers take scope below Cause, and verbal morphology intervenes between the root and Cause, exactly when Cause selects at least a verb (Table 3.2, rows 1 and 2). The two rows correlate because both are this one fact.

theorem Pylkkanen2008.embeds_phase_iff (c : CauseHead) : c.Embeds Layer.phase ↔ c.selects = Layer.phase

Agent-oriented modifiers take scope below Cause, and high applicative morphology intervenes between the root and Cause, exactly when Cause selects a phase (Table 3.2, rows 3 and 4).

def Pylkkanen2008.CauseHead.HasCauseePosition (c : CauseHead) : Prop

A causee position (94) exists inside Cause's complement when that complement is at least a verb, or between Cause and Voice when Cause is not bundled with Voice.

Equations

• c.HasCauseePosition = (c.Embeds Pylkkanen2008.Layer.verb ∨ c.bundled = false)

@[instance_reducible]

instance Pylkkanen2008.instDecidableHasCauseePosition (c : CauseHead) : Decidable c.HasCauseePosition

Equations

• Pylkkanen2008.instDecidableHasCauseePosition c = { decide := decide (c.Embeds Pylkkanen2008.Layer.verb) || decide (c.bundled = false), reflects_decide := ⋯ }

theorem Pylkkanen2008.hasCauseePosition_iff (c : CauseHead) : c.HasCauseePosition ↔ ¬(c.selects = Layer.root ∧ c.bundled = true)

Causatives of unergatives and transitives are impossible exactly for a root-selecting, Voice-bundling head (Table 3.1, second row).

def Pylkkanen2008.englishZero : CauseHead

The English zero-causative is root-selecting and Voice-bundling.

Equations

• Pylkkanen2008.englishZero = { selects := Pylkkanen2008.Layer.root, bundled := true }

def Pylkkanen2008.japaneseLexical : CauseHead

The Japanese lexical causative is root-selecting, with Cause independent of Voice.

Equations

• Pylkkanen2008.japaneseLexical = { selects := Pylkkanen2008.Layer.root, bundled := false }

def Pylkkanen2008.finnishTta : CauseHead

The Finnish -tta causative is verb-selecting, with Cause independent of Voice.

Equations

• Pylkkanen2008.finnishTta = { selects := Pylkkanen2008.Layer.verb, bundled := false }

theorem Pylkkanen2008.root_causativized_unergative : (Examples.ex95.judgment = Judgment.acceptable ↔ englishZero.HasCauseePosition) ∧ (Examples.ex96.judgment = Judgment.acceptable ↔ japaneseLexical.HasCauseePosition)

The English and Japanese root-selecting causatives differ on unergative bases, (95) and (96), exactly as hasCauseePosition_iff predicts.