Applicative Heads

@cite{cuervo-2003} @cite{pylkknen-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{pylkknen-2008} Table 1.1.

Semantic Denotations (@cite{pylkknen-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{pylkknen-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{pylkknen-2008}.

inductive Minimalism.ApplType : Type

High vs low applicatives (@cite{pylkknen-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

instance Minimalism.instDecidableEqApplType : DecidableEq ApplType

Equations

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

instance Minimalism.instBEqApplType : BEq ApplType

Equations

• Minimalism.instBEqApplType = { beq := Minimalism.instBEqApplType.beq }

def Minimalism.instBEqApplType.beq : ApplType → ApplType → Bool

Equations

• Minimalism.instBEqApplType.beq x✝ y✝ = (x✝.ctorIdx == y✝.ctorIdx)

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

Equations

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

instance Minimalism.instReprApplType : Repr ApplType

Equations

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

def Minimalism.ApplType.isLow : ApplType → Bool

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

Equations

• Minimalism.ApplType.lowRecipient.isLow = true
• Minimalism.ApplType.lowSource.isLow = true
• Minimalism.ApplType.high.isLow = false

inductive Minimalism.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

instance Minimalism.instDecidableEqApplSemantics : DecidableEq ApplSemantics

Equations

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

def Minimalism.instBEqApplSemantics.beq : ApplSemantics → ApplSemantics → Bool

Equations

• Minimalism.instBEqApplSemantics.beq x✝ y✝ = (x✝.ctorIdx == y✝.ctorIdx)

instance Minimalism.instBEqApplSemantics : BEq ApplSemantics

Equations

• Minimalism.instBEqApplSemantics = { beq := Minimalism.instBEqApplSemantics.beq }

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

Equations

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

instance Minimalism.instReprApplSemantics : Repr ApplSemantics

Equations

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

def Minimalism.ApplType.semantics : ApplType → ApplSemantics

Map each applicative type to its semantic contribution.

Equations

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

def Minimalism.ApplType.requiresEventSemantics : ApplType → Bool

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

• Minimalism.ApplType.high.requiresEventSemantics = true
• Minimalism.ApplType.lowRecipient.requiresEventSemantics = false
• Minimalism.ApplType.lowSource.requiresEventSemantics = false

structure Minimalism.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?

instance Minimalism.instDecidableEqApplHead : DecidableEq ApplHead

Equations

• Minimalism.instDecidableEqApplHead = Minimalism.instDecidableEqApplHead.decEq

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

Equations

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

instance Minimalism.instBEqApplHead : BEq ApplHead

Equations

• Minimalism.instBEqApplHead = { beq := Minimalism.instBEqApplHead.beq }

def Minimalism.instBEqApplHead.beq : ApplHead → ApplHead → Bool

Equations

• Minimalism.instBEqApplHead.beq { applType := a, assignsDative := a_1 } { applType := b, assignsDative := b_1 } = (a == b && a_1 == b_1)
• Minimalism.instBEqApplHead.beq x✝¹ x✝ = false

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

Equations

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

instance Minimalism.instReprApplHead : Repr ApplHead

Equations

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

def Minimalism.applHigh : ApplHead

Canonical high applicative (ethical dative).

Equations

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

def Minimalism.applLowRecipient : ApplHead

Canonical low recipient applicative (DOC, possessive dative).

Equations

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

def Minimalism.applLowSource : ApplHead

Canonical low source applicative.

Equations

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

def Minimalism.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{pylkknen-2008}).

Equations

• appl.licensedWith voice = if appl.applType.requiresEventSemantics = true then voice.hasSemantics else true

theorem Minimalism.high_requires_event : ApplType.high.requiresEventSemantics = true

High applicatives require event semantics.

theorem Minimalism.low_no_event_requirement : ApplType.lowRecipient.requiresEventSemantics = false ∧ ApplType.lowSource.requiresEventSemantics = false

Low applicatives do not require event semantics.

theorem Minimalism.ethical_dative_with_agent : applHigh.licensedWith voiceAgent = true

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

theorem Minimalism.ethical_dative_blocked_in_middle : applHigh.licensedWith voiceMiddle = false

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

theorem Minimalism.possessive_dative_survives_middle : applLowRecipient.licensedWith voiceMiddle = true

Possessive datives (low Appl) survive in middles.

theorem Minimalism.possessive_dative_survives_anticausative : applLowRecipient.licensedWith voiceAnticausative = true

Possessive datives survive in anticausatives.

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

The asymmetry: ethical blocked but possessive survives in middles.

def Minimalism.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 Minimalism.caseless_blocked_in_specAppl : applLowRecipient.specCanBearCase false = false

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

theorem Minimalism.caseful_ok_in_specAppl : applLowRecipient.specCanBearCase true = true

A case-bearing DP CAN merge in SpecApplP.