Applicative Heads

@cite{cuervo-2003} @cite{pylkkanen-2008} @cite{wood-2015}

Applicative heads introduce applied arguments (benefactives, goals, sources) into the verbal structure. The high/low distinction determines whether the applied argument relates to the event as a whole (high) or to the theme (low).

Low applicatives further split into recipient (transfer to) and source (transfer from), following @cite{pylkkanen-2008} Table 1.1.

Semantic Denotations (@cite{pylkkanen-2008})

• High Appl: λx.λe. Appl(e, x) — relates individual to event (ethical datives: "he ate food on-me")
• Low Appl (recipient): λx.λy. HAVE(x, y) — transfer TO (English DOC: "I sent him a letter")
• Low Appl (source): λx.λy. HAVE-FROM(y, x) — transfer FROM (possessive datives: "they broke his arm")

High/Low Asymmetry (@cite{pylkkanen-2008}, @cite{schaefer-2008})

High applicatives require Voice with event semantics; low applicatives are independent of Voice. This predicts high Appl is blocked when Voice is semantically null (middles, anticausatives).

Note: @cite{wood-2015} Ch. 5 argues that Icelandic lacks true high applicatives entirely. The high/low interaction modeled here follows the cross-linguistic typology of @cite{pylkkanen-2008}.

inductive Minimalist.ApplType : Type

High vs low applicatives (@cite{pylkkanen-2008}, Table 1.1).

• High: Above VP, relates applied argument to the event (benefactive: Chaga "he ate food for wife")
• Low recipient: Below VP, transfer-of-possession to the applied argument (English DOC: "I sent him a letter")
• Low source: Below VP, transfer-of-possession from the applied argument (Korean, Hebrew possessor datives, Japanese adversity passives)

• high : ApplType
• lowRecipient : ApplType
• lowSource : ApplType

@[implicit_reducible]

instance Minimalist.instDecidableEqApplType : DecidableEq ApplType

Equations

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

@[implicit_reducible]

instance Minimalist.instReprApplType : Repr ApplType

Equations

• Minimalist.instReprApplType = { reprPrec := Minimalist.instReprApplType.repr }

def Minimalist.instReprApplType.repr : ApplType → ℕ → Std.Format

Equations

• One or more equations did not get rendered due to their size.
• Minimalist.instReprApplType.repr Minimalist.ApplType.high prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Minimalist.ApplType.high")).group prec✝

def Minimalist.ApplType.IsLow (a : ApplType) : Prop

Is this a low applicative (either recipient or source)?

Equations

• a.IsLow = (a = Minimalist.ApplType.lowRecipient ∨ a = Minimalist.ApplType.lowSource)

@[implicit_reducible]

instance Minimalist.instDecidablePredApplTypeIsLow : DecidablePred ApplType.IsLow

Equations

• Minimalist.instDecidablePredApplTypeIsLow x✝ = Minimalist.instDecidablePredApplTypeIsLow._aux_1 x✝

inductive Minimalist.ApplSemantics : Type

The semantic relation an applicative head contributes.

• eventRelation: λx.λe. R(e, x) — relates individual to event (high Appl)
• possessionTo: λx.λy. HAVE(x, y) — transfer-to (low recipient)
• possessionFrom: λx.λy. HAVE-FROM(y, x) — transfer-from (low source)

• eventRelation : ApplSemantics
• possessionTo : ApplSemantics
• possessionFrom : ApplSemantics

@[implicit_reducible]

instance Minimalist.instDecidableEqApplSemantics : DecidableEq ApplSemantics

Equations

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

def Minimalist.instReprApplSemantics.repr : ApplSemantics → ℕ → Std.Format

Equations

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

@[implicit_reducible]

instance Minimalist.instReprApplSemantics : Repr ApplSemantics

Equations

• Minimalist.instReprApplSemantics = { reprPrec := Minimalist.instReprApplSemantics.repr }

def Minimalist.ApplType.semantics : ApplType → ApplSemantics

Map each applicative type to its semantic contribution.

Equations

• Minimalist.ApplType.high.semantics = Minimalist.ApplSemantics.eventRelation
• Minimalist.ApplType.lowRecipient.semantics = Minimalist.ApplSemantics.possessionTo
• Minimalist.ApplType.lowSource.semantics = Minimalist.ApplSemantics.possessionFrom

def Minimalist.ApplType.RequiresEventSemantics (a : ApplType) : Prop

Does this applicative type require event-level semantics from Voice? High applicatives relate to the event, so they need Voice to contribute event semantics. Low applicatives relate to the theme and are independent of Voice.

Equations

• a.RequiresEventSemantics = (a = Minimalist.ApplType.high)

@[implicit_reducible]

instance Minimalist.instDecidablePredApplTypeRequiresEventSemantics : DecidablePred ApplType.RequiresEventSemantics

Equations

• Minimalist.instDecidablePredApplTypeRequiresEventSemantics x✝ = Minimalist.instDecidablePredApplTypeRequiresEventSemantics._aux_1 x✝

def Minimalist.ApplType.RequiresThemeInComplement (a : ApplType) : Prop

Does this applicative type require its complement to provide an unsaturated theme argument? Low applicatives do — they relate the applied argument to the theme via transfer-of-possession. High applicatives don't — they relate the applied argument to the event described by the verb, not to a theme.

This predicate is the source of @cite{pylkkanen-2008}'s transitivity restriction (Diagnostic 1, eq. 17 of book): low applicatives cannot combine with unergatives because unergative VPs lack an unsaturated theme. The semantic mismatch is shown in eq. 103 (page 55): combining low Appl with an unergative VP yields agent(e, x) ∧ theme(e, x) — a contradiction.

Equations

• a.RequiresThemeInComplement = a.IsLow

@[implicit_reducible]

instance Minimalist.instDecidablePredApplTypeRequiresThemeInComplement : DecidablePred ApplType.RequiresThemeInComplement

Equations

• Minimalist.instDecidablePredApplTypeRequiresThemeInComplement a = Minimalist.instDecidablePredApplTypeRequiresThemeInComplement._aux_1 a

structure Minimalist.ApplHead : Type

An applicative head with its type and properties.

• applType : ApplType

  High or low (recipient/source)

• assignsDative : Bool

  Does the applied argument get dative case?

def Minimalist.instDecidableEqApplHead.decEq (x✝ x✝¹ : ApplHead) : Decidable (x✝ = x✝¹)

Equations

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

@[implicit_reducible]

instance Minimalist.instDecidableEqApplHead : DecidableEq ApplHead

Equations

• Minimalist.instDecidableEqApplHead = Minimalist.instDecidableEqApplHead.decEq

def Minimalist.instReprApplHead.repr : ApplHead → ℕ → Std.Format

Equations

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

@[implicit_reducible]

instance Minimalist.instReprApplHead : Repr ApplHead

Equations

• Minimalist.instReprApplHead = { reprPrec := Minimalist.instReprApplHead.repr }

def Minimalist.applHigh : ApplHead

Canonical high applicative (ethical dative).

Equations

• Minimalist.applHigh = { applType := Minimalist.ApplType.high }

def Minimalist.applLowRecipient : ApplHead

Canonical low recipient applicative (DOC, possessive dative).

Equations

• Minimalist.applLowRecipient = { applType := Minimalist.ApplType.lowRecipient }

def Minimalist.applLowSource : ApplHead

Canonical low source applicative.

Equations

• Minimalist.applLowSource = { applType := Minimalist.ApplType.lowSource }

def Minimalist.ApplHead.licensedWith (appl : ApplHead) (voice : VoiceHead) : Bool

Is this applicative licensed in the context of a given Voice head?

High applicatives require Voice with event semantics; when Voice is semantically null (middles, anticausatives), high Appl is blocked. Low applicatives relate to the theme and are always licensed (@cite{pylkkanen-2008}).

Equations

• appl.licensedWith voice = if appl.applType.RequiresEventSemantics then decide voice.HasSemantics else true

theorem Minimalist.high_requires_event : ApplType.high.RequiresEventSemantics

High applicatives require event semantics.

theorem Minimalist.low_no_event_requirement : ¬ApplType.lowRecipient.RequiresEventSemantics ∧ ¬ApplType.lowSource.RequiresEventSemantics

Low applicatives do not require event semantics.

theorem Minimalist.ethical_dative_with_agent : applHigh.licensedWith voiceAgent = true

Ethical datives (high Appl) are licensed with agentive Voice.

theorem Minimalist.ethical_dative_blocked_in_middle : applHigh.licensedWith voiceMiddle = false

High Appl is BLOCKED with middle Voice (no event semantics) (@cite{pylkkanen-2008}).

theorem Minimalist.possessive_dative_survives_middle : applLowRecipient.licensedWith voiceMiddle = true

Possessive datives (low Appl) survive in middles.

theorem Minimalist.possessive_dative_survives_anticausative : applLowRecipient.licensedWith voiceAnticausative = true

Possessive datives survive in anticausatives.

theorem Minimalist.ethical_possessive_middle_asymmetry : applHigh.licensedWith voiceMiddle = false ∧ applLowRecipient.licensedWith voiceMiddle = true

The asymmetry: ethical blocked but possessive survives in middles.

def Minimalist.ApplHead.specCanBearCase (appl : ApplHead) (bearerHasCase : Bool) : Bool

Can a given element merge in SpecApplP?

@cite{wood-2015} Ch. 5 (§5.3.2): Appl assigns dative case to its specifier. Therefore only elements that can bear case can merge in SpecApplP. The Icelandic clitic -st lacks case features and is thus blocked from SpecApplP, even though it can merge in SpecVoiceP and SpecpP (where no case is assigned to the specifier).

Equations

• appl.specCanBearCase bearerHasCase = if appl.assignsDative = true then bearerHasCase else true

theorem Minimalist.caseless_blocked_in_specAppl : applLowRecipient.specCanBearCase false = false

-st (caseless) cannot merge in SpecApplP (@cite{wood-2015} §5.3.2).

theorem Minimalist.caseful_ok_in_specAppl : applLowRecipient.specCanBearCase true = true

A case-bearing DP CAN merge in SpecApplP.