Building and interpreting possession sentences

[Myl16] treats every have and be as one meaningless copula v, whose meaning is the identity function and whose form is fixed by its syntactic surroundings: have under a transitive Voice — one that bears the specifier feature {D} and φ-features — and be otherwise. The possession relation comes from inside the DP complement, and Voice adds a θ-role only when the complement is a predicate of eventualities. Icelandic's two have verbs divide the transitive context by what lies below v: hafa over a PredP, eiga elsewhere.

Main definitions

• Context, englishItems, icelandicItems: what v's insertion sees and the Vocabulary Items of English and Icelandic.
• Attributive: the two DP-internal possession structures, a PP possessor under Pred or a possessor in Spec,PossP.
• voiceAlloseme: the Voice alloseme a complement selects, the substrate's Voice.Alloseme.fromComplement.

Main results

• have_iff_transitive: have is be in a transitive Voice context.
• hafa_iff_predP, eiga_only_if_no_pp, hafa_only_if_pp: the Icelandic items and the two generalizations that follow from the structures.
• clausal_rows, attributive_rows: the items reproduce the Icelandic data pool, clausal and attributive.
• expletive_voice_passes_complement: with a relational complement Voice is the identity, so the sentence means what its complement means.

Implementation notes

Example numbers are the book's: chapter 1 for the copula and Voice rules, chapter 4 for have and the Icelandic section. The Minimalist Voice.Head flavors are not used for the insertion context: Myler's condition is syntactic ({D} and φ, the transitive configuration of (24)), and relational have has an expletive Voice at LF while still surfacing as have.

The copula's context and form

inductive Myler2016.Feature : Type

What the insertion of v sees: the specifier feature {D} and the φ-features on the Voice above, and a PredP complement below.

• d : Feature
• phi : Feature
• pred : Feature

@[instance_reducible]

instance Myler2016.instDecidableEqFeature : DecidableEq Feature

Equations

• Myler2016.instDecidableEqFeature x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

@[instance_reducible]

instance Myler2016.instReprFeature : Repr Feature

Equations

• Myler2016.instReprFeature = { reprPrec := Myler2016.instReprFeature.repr }

def Myler2016.instReprFeature.repr : Feature → ℕ → Std.Format

Equations

• Myler2016.instReprFeature.repr Myler2016.Feature.d prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Myler2016.Feature.d")).group prec✝
• Myler2016.instReprFeature.repr Myler2016.Feature.phi prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Myler2016.Feature.phi")).group prec✝
• Myler2016.instReprFeature.repr Myler2016.Feature.pred prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Myler2016.Feature.pred")).group prec✝

structure Myler2016.Context : Type

A clause's context for v.

• voiceD : Bool
• voicePhi : Bool
• predComplement : Bool

def Myler2016.instDecidableEqContext.decEq (x✝ x✝¹ : Context) : Decidable (x✝ = x✝¹)

Equations

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

@[instance_reducible]

instance Myler2016.instDecidableEqContext : DecidableEq Context

Equations

• Myler2016.instDecidableEqContext = Myler2016.instDecidableEqContext.decEq

def Myler2016.instReprContext.repr : Context → ℕ → Std.Format

Equations

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

@[instance_reducible]

instance Myler2016.instReprContext : Repr Context

Equations

• Myler2016.instReprContext = { reprPrec := Myler2016.instReprContext.repr }

@[instance_reducible]

instance Myler2016.instFintypeContext : Fintype Context

Equations

• Myler2016.instFintypeContext = Fintype.ofEquiv ((_ : Bool) × (_ : Bool) × Bool) Myler2016.Context.proxyTypeEquiv

def Myler2016.Context.features (c : Context) : List Feature

The features a context exposes.

Equations

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

def Myler2016.Context.Transitive (c : Context) : Prop

A transitive context: Voice introduces an external argument and bears φ-features that license v's complement.

Equations

• c.Transitive = (c.voiceD = true ∧ c.voicePhi = true)

@[instance_reducible]

instance Myler2016.instDecidableTransitive (c : Context) : Decidable c.Transitive

Equations

• Myler2016.instDecidableTransitive c = Myler2016.instDecidableTransitive._aux_1 c

def Myler2016.englishItems : List (DistributedMorphology.VocabularyItem Feature String)

English ((89) of chapter 1): have in a transitive context, be elsewhere.

Equations

• Myler2016.englishItems = [DistributedMorphology.VocabularyItem.ofFeatures [Myler2016.Feature.d, Myler2016.Feature.phi] "have", DistributedMorphology.VocabularyItem.ofFeatures [] "be"]

def Myler2016.icelandicItems : List (DistributedMorphology.VocabularyItem Feature String)

Icelandic ((89) of chapter 4): hafa in a transitive context over a PredP, eiga in a transitive context otherwise, and the copula vera elsewhere.

Equations

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

def Myler2016.spellout (items : List (DistributedMorphology.VocabularyItem Feature String)) (c : Context) : Option String

The form of v in a context, by the Subset Principle over a language's items.

Equations

• Myler2016.spellout items c = DistributedMorphology.subsetPrinciple items (DistributedMorphology.Neighborhood.ofBundle c.features)

theorem Myler2016.have_iff_transitive (c : Context) : spellout englishItems c = some "have" ↔ c.Transitive

have is be plus transitivity.

theorem Myler2016.hafa_iff_predP (c : Context) : spellout icelandicItems c = some "hafa" ↔ c.Transitive ∧ c.predComplement = true

hafa is the transitive spell-out over a PredP; the rule is conditioned from both sides of v.

Attributive possession and the two generalizations (§4.3)

inductive Myler2016.Attributive : Type

The two DP-internal possession structures ((93), (94)): the possessor in a PP under Pred, or in Spec,PossP.

• predP : Attributive
• possP : Attributive

@[instance_reducible]

instance Myler2016.instDecidableEqAttributive : DecidableEq Attributive

Equations

• Myler2016.instDecidableEqAttributive x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

def Myler2016.instReprAttributive.repr : Attributive → ℕ → Std.Format

Equations

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

@[instance_reducible]

instance Myler2016.instReprAttributive : Repr Attributive

Equations

• Myler2016.instReprAttributive = { reprPrec := Myler2016.instReprAttributive.repr }

@[instance_reducible]

instance Myler2016.instFintypeAttributive : Fintype Attributive

Equations

• Myler2016.instFintypeAttributive = { elems := { val := ↑Myler2016.Attributive.enumList, nodup := Myler2016.Attributive.enumList_nodup }, complete := Myler2016.instFintypeAttributive._proof_1 }

def Myler2016.Attributive.AllowsPP : Attributive → Prop

A PP possessor is available exactly under the PredP structure ((92), column C).

Equations

• Myler2016.Attributive.predP.AllowsPP = True
• Myler2016.Attributive.possP.AllowsPP = False

@[instance_reducible]

instance Myler2016.instDecidablePredAttributiveAllowsPP : DecidablePred Attributive.AllowsPP

Equations

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

def Myler2016.Attributive.context (a : Attributive) : Context

Clausal possession embeds the attributive structure under v in a transitive context.

Equations

• a.context = { voiceD := true, voicePhi := true, predComplement := decide (a = Myler2016.Attributive.predP) }

theorem Myler2016.eiga_only_if_no_pp (a : Attributive) (h : spellout icelandicItems a.context = some "eiga") : ¬a.AllowsPP

Generalization 1 ((90a)): clausal possession with eiga only if DP-internal possession cannot use a PP.

theorem Myler2016.hafa_only_if_pp (a : Attributive) (h : spellout icelandicItems a.context = some "hafa") : a.AllowsPP

Generalization 2 ((90b)): clausal possession with hafa only if DP-internal possession can use a PP.

The Icelandic data pool

inductive Myler2016.Relation : Type

The possession relations of (91) and (92).

• concrete : Relation
• kinship : Relation
• bodyPart : Relation
• abstract : Relation

@[instance_reducible]

instance Myler2016.instDecidableEqRelation : DecidableEq Relation

Equations

• Myler2016.instDecidableEqRelation x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

@[instance_reducible]

instance Myler2016.instReprRelation : Repr Relation

Equations

• Myler2016.instReprRelation = { reprPrec := Myler2016.instReprRelation.repr }

def Myler2016.instReprRelation.repr : Relation → ℕ → Std.Format

Equations

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

@[instance_reducible]

instance Myler2016.instFintypeRelation : Fintype Relation

Equations

• Myler2016.instFintypeRelation = { elems := { val := ↑Myler2016.Relation.enumList, nodup := Myler2016.Relation.enumList_nodup }, complete := Myler2016.instFintypeRelation._proof_1 }

def Myler2016.Relation.ofString : String → Option Relation

Equations

• Myler2016.Relation.ofString "concrete" = some Myler2016.Relation.concrete
• Myler2016.Relation.ofString "kinship" = some Myler2016.Relation.kinship
• Myler2016.Relation.ofString "bodyPart" = some Myler2016.Relation.bodyPart
• Myler2016.Relation.ofString "abstract" = some Myler2016.Relation.abstract
• Myler2016.Relation.ofString x✝ = none

def Myler2016.Relation.attributive : Relation → Attributive

The structure each relation is built with: body parts and abstract relations under Pred with a PP possessor, concrete and kinship relations under Poss ((92)–(94)).

Equations

• Myler2016.Relation.concrete.attributive = Myler2016.Attributive.possP
• Myler2016.Relation.kinship.attributive = Myler2016.Attributive.possP
• Myler2016.Relation.bodyPart.attributive = Myler2016.Attributive.predP
• Myler2016.Relation.abstract.attributive = Myler2016.Attributive.predP

structure Myler2016.ClausalRow : Type

A clausal row of (91): the relation, the verb, and whether it is accepted.

• relation : Relation
• verb : String
• accepted : Bool

@[instance_reducible]

instance Myler2016.instDecidableEqClausalRow : DecidableEq ClausalRow

Equations

• Myler2016.instDecidableEqClausalRow = Myler2016.instDecidableEqClausalRow.decEq

def Myler2016.instDecidableEqClausalRow.decEq (x✝ x✝¹ : ClausalRow) : Decidable (x✝ = x✝¹)

Equations

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

@[instance_reducible]

instance Myler2016.instReprClausalRow : Repr ClausalRow

Equations

• Myler2016.instReprClausalRow = { reprPrec := Myler2016.instReprClausalRow.repr }

def Myler2016.instReprClausalRow.repr : ClausalRow → ℕ → Std.Format

Equations

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

def Myler2016.ClausalRow.ofExample (ex : Data.Examples.LinguisticExample) : Option ClausalRow

Equations

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

structure Myler2016.PPRow : Type

A column-C row of (92): the relation and whether the PP possessor is accepted.

• relation : Relation
• accepted : Bool

def Myler2016.instDecidableEqPPRow.decEq (x✝ x✝¹ : PPRow) : Decidable (x✝ = x✝¹)

Equations

• Myler2016.instDecidableEqPPRow.decEq { relation := a, accepted := a_1 } { relation := b, accepted := b_1 } = if h : a = b then h ▸ if h : a_1 = b_1 then h ▸ isTrue ⋯ else isFalse ⋯ else isFalse ⋯

@[instance_reducible]

instance Myler2016.instDecidableEqPPRow : DecidableEq PPRow

Equations

• Myler2016.instDecidableEqPPRow = Myler2016.instDecidableEqPPRow.decEq

def Myler2016.instReprPPRow.repr : PPRow → ℕ → Std.Format

Equations

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

@[instance_reducible]

instance Myler2016.instReprPPRow : Repr PPRow

Equations

• Myler2016.instReprPPRow = { reprPrec := Myler2016.instReprPPRow.repr }

def Myler2016.PPRow.ofExample (ex : Data.Examples.LinguisticExample) : Option PPRow

Equations

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

def Myler2016.clausalRows : List ClausalRow

Equations

• Myler2016.clausalRows = List.filterMap Myler2016.ClausalRow.ofExample Myler2016.Examples.all

def Myler2016.ppRows : List PPRow

Equations

• Myler2016.ppRows = List.filterMap Myler2016.PPRow.ofExample Myler2016.Examples.all

theorem Myler2016.rows_cover (ex : Data.Examples.LinguisticExample) : ex ∈ Examples.all → (ClausalRow.ofExample ex).isSome = true ∨ List.lookup "construction" ex.paperFeatures ≠ some "clausal"

Every example is a clausal row or an attributive row.

theorem Myler2016.clausal_rows (r : ClausalRow) : r ∈ clausalRows → (spellout icelandicItems r.relation.attributive.context = some r.verb) = (r.accepted = true)

Clausal possession ((91)): each relation's structure spells out as exactly the accepted verb.

theorem Myler2016.attributive_rows (r : PPRow) : r ∈ ppRows → decide r.relation.attributive.AllowsPP = r.accepted

Attributive possession ((92), column C): a PP possessor is accepted exactly for the relations built under Pred.

The meaning of a have sentence

def Myler2016.voiceAlloseme (eventiveVoiceP stative : Bool) : DistributedMorphology.Allosemy.Voice.Alloseme

The Voice alloseme a have sentence's complement selects ((62)): the substrate's competition over Voice.vocabulary.

Equations

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

theorem Myler2016.expletive_voice_passes_complement : voiceAlloseme false false = DistributedMorphology.Allosemy.Voice.Alloseme.expletive

⟦v⟧ = λx.x ((61)) and, over a relational complement — neither an eventive VoiceP nor a state — Voice is the expletive identity: the sentence means what its complement means — (7a), the have of §4.1.1: relational, locative, and experiencer have.

theorem Myler2016.contentful_voice_adds_theta : (voiceAlloseme false true).AssignsTheta ∧ (voiceAlloseme true false).AssignsTheta

Over an eventuality predicate Voice adds a θ-role — the holder of a state, the engineer of an eventive VoiceP — so light-verb and ECM have mean more than their complement — (7b), §4.1.2.