Wood (2023): Icelandic Nominalizations and Allosemy

This file formalizes Wood's account of Icelandic deverbal nominalizations as complex heads: a root categorized by v and then by n, with no verb phrase and no Voice, whose ambiguity between complex event, simple event, and referring readings is allosemy of v and n (Derivation). A complex event nominal has eventive v and zero n, so the noun inherits the verb's meaning; the simple readings have zero v and a contentful n. Borer's Generalization, that a complex event reading entails a morphologically related verb with that meaning, follows from two facts: only v introduces the event variable, and n is not in the root's domain, so it cannot condition root suppletion past v (borers_generalization). The nominal's external argument is introduced by i*, the head that is Voice in the verbal domain, interpreted as an agent in the context of an eventive nP and as a possessor otherwise (IStar.alloseme).

The form side is contextual allomorphy on the same complex head. The nominalizers -un, -ing, -sla, -stur and the rest are exponents of one n, each listed for a set of roots or for an overt verbalizer, with no elsewhere item (Allomorphy.vocab); Vocabulary Insertion runs from the inside out over the concatenated neighbors, null exponents pruned (ComplexHead.insertAll). Two of the book's descriptive generalizations are then theorems: the nominalizer is chosen by the verbalizer whenever that is overt, since it hides the root, and by the root otherwise (Allomorphy.nominalizer_of_ne_zero, Allomorphy.nominalizer_of_eq_zero), so that -k takes -un and -er takes -ing whatever the root; and a root that no item lists has no nominalization at all, the book's borða 'eat' (Allomorphy.nominalizer_eq_none). Every segmentation in Fragments.Icelandic.Nouns is derived this way (Allomorphy.fragment_realize).

Special meaning is subject to phase locality: a dependency may cross at most one categorizer (Local). A preposition heading the PP complement of a nominal is separated from the root by v and n, so a preposition that conditions the root's meaning must adjoin to the complex n head as a prefix, while one with its own meaning heads a PP, and one that does both is doubled (nominal_complement_not_local). The same bound lets n condition an idiosyncratic root meaning across v (nominal_n_local) and forbids it in -væðing nominals, where -væða is a compound head attaching to a categorized word, so that two categorizers separate the root from the outer n (vaeda_n_not_local). The prefixes marg- and endur- are event modifiers: marg- adjoins to v, endur- to v or to n, and each needs an event variable at its host, which licenses marg- exactly on nominals whose v is eventive and endur- also on simple event and result nominals but not on simple entities (Licensed); the book's judgments on the prefixed readings of þvottur and prentun are the rows of Data.Examples.Wood2023, checked one by one (rows_licensed). Allosemy is contextual as allomorphy is: aðdáun and viðvörun share the nominalizer -un, and only the second has a concrete entity reading (reading_not_by_nominalizer).

Implementation notes

The exponents of the roots and affixes are the surface morphs of the fragment, so the u-umlaut of söfn-un and vönt-un is not undone and the theme vowel -a of the verb is absent, as the book's own segmentation has it. The roots are identified by their forms. The prefixed preposition of við-ger-ð adjoins to n and is not inserted by the vocabulary; the derivation covers the root, v, and n. Wood's bound for allosemy, one intervening categorizer, is one phase looser than ComplexHead.RootLocal, the bound the book keeps for root suppletion; the study states the strict one through the substrate. A preposition adjoined to a complex head has no spine position, since a head does not c-command its own adjunct, so the heads between a preposition and the root are read off its attachment. The event-modifier account licenses marg- on a result nominal built on eventive v, a case the book does not test.

References

• [Woo23]
• [Emb10]
• [Emb15]
• [Mar13]
• [WM17]
• [Myl16]

Vocabulary Insertion at v and n

inductive Wood2023.Allomorphy.Feature : Type

A Vocabulary Item of v or n may mention the category of its own head, or the exponent of a concatenated neighbor, a root or an affix.

• cat (c : DistributedMorphology.Categorizer) : Feature
• exp (m : Morphology.Morph) : Feature

@[instance_reducible]

instance Wood2023.Allomorphy.instDecidableEqFeature : DecidableEq Feature

Equations

• Wood2023.Allomorphy.instDecidableEqFeature = Wood2023.Allomorphy.instDecidableEqFeature.decEq

def Wood2023.Allomorphy.instDecidableEqFeature.decEq (x✝ x✝¹ : Feature) : Decidable (x✝ = x✝¹)

Equations

• Wood2023.Allomorphy.instDecidableEqFeature.decEq (Wood2023.Allomorphy.Feature.cat a) (Wood2023.Allomorphy.Feature.cat b) = if h : a = b then h ▸ isTrue ⋯ else isFalse ⋯
• Wood2023.Allomorphy.instDecidableEqFeature.decEq (Wood2023.Allomorphy.Feature.cat c) (Wood2023.Allomorphy.Feature.exp m) = isFalse ⋯
• Wood2023.Allomorphy.instDecidableEqFeature.decEq (Wood2023.Allomorphy.Feature.exp m) (Wood2023.Allomorphy.Feature.cat c) = isFalse ⋯
• Wood2023.Allomorphy.instDecidableEqFeature.decEq (Wood2023.Allomorphy.Feature.exp a) (Wood2023.Allomorphy.Feature.exp b) = if h : a = b then h ▸ isTrue ⋯ else isFalse ⋯

def Wood2023.Allomorphy.instReprFeature.repr : Feature → ℕ → Std.Format

Equations

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

@[instance_reducible]

instance Wood2023.Allomorphy.instReprFeature : Repr Feature

Equations

• Wood2023.Allomorphy.instReprFeature = { reprPrec := Wood2023.Allomorphy.instReprFeature.repr }

def Wood2023.Allomorphy.zero : Morphology.Morph

The zero exponent.

Equations

• Wood2023.Allomorphy.zero = Morphology.Morph.suff ""

def Wood2023.Allomorphy.expFeatures (m : Morphology.Morph) : List Feature

A realized exponent presents itself as context.

Equations

• Wood2023.Allomorphy.expFeatures m = [Wood2023.Allomorphy.Feature.exp m]

def Wood2023.Allomorphy.nAfter (m : Morphology.Morph) (e : String) : DistributedMorphology.VocabularyItem Feature Morphology.Morph

The item spelling out n as e after the exponent m.

Equations

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

def Wood2023.Allomorphy.vocab : Morphology.Exponence.RuleSet (DistributedMorphology.VocabularyItem Feature Morphology.Morph)

The Vocabulary Items of v and n. v is -k after sein and, in a nominal only, after not, -er after analýs, and zero elsewhere; n is -ing after -er, -un after -k and after the roots the fragment shows with -un, -n, -ttur and -ð after their roots, and has no elsewhere item, as the rule (2.8) of the book has it.

Equations

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

def Wood2023.Allomorphy.listed : List String

The roots the items of n list.

Equations

• Wood2023.Allomorphy.listed = ["opn", "söfn", "vönt", "prent", "vör", "dá", "önn", "misheyr", "þvo", "ger"]

def Wood2023.Allomorphy.word (r : String) (v : Option Morphology.Morph) : DistributedMorphology.ComplexHead (DistributedMorphology.Morpheme Feature Morphology.Morph) (DistributedMorphology.Morpheme Feature Morphology.Morph)

The root categorized by v and then by n, with the exponent of v if already inserted.

Equations

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

@[reducible, inline]

abbrev Wood2023.Allomorphy.insertAt (w : DistributedMorphology.ComplexHead (DistributedMorphology.Morpheme Feature Morphology.Morph) (DistributedMorphology.Morpheme Feature Morphology.Morph)) (i : ℕ) : DistributedMorphology.ComplexHead (DistributedMorphology.Morpheme Feature Morphology.Morph) (DistributedMorphology.Morpheme Feature Morphology.Morph)

Vocabulary Insertion at head i, over the concatenated neighbors with zero exponents pruned.

Equations

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

def Wood2023.Allomorphy.realize (w : DistributedMorphology.ComplexHead (DistributedMorphology.Morpheme Feature Morphology.Morph) (DistributedMorphology.Morpheme Feature Morphology.Morph)) : List Morphology.Morph

The morphs of a complex head after insertion from the inside out.

Equations

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

theorem Wood2023.Allomorphy.fragment_realize (w : Icelandic.Nouns.Deverbal) : w ∈ Icelandic.Nouns.deverbals → (Option.map Morphology.Morph.pref w.preposition).toList ++ realize (word w.root none) = w.morphs

Every nominal of the fragment is the root's spell-out, with its preposition prefixed.

def Wood2023.Allomorphy.vContext (r : String) : DistributedMorphology.Neighborhood (List Feature)

In the context v presents, the root is inside and the bare n outside.

Equations

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

def Wood2023.Allomorphy.nContext (r : String) (e : Morphology.Morph) : DistributedMorphology.Neighborhood (List Feature)

In the context n presents after the exponent e of v, the inner neighbor is v when it is overt, and the root past a pruned zero v.

Equations

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

theorem Wood2023.Allomorphy.contextAt_word_zero (r : String) : (word r none).contextAt (fun (x : Morphology.Morph) => x = zero) DistributedMorphology.ComplexHead.Locality.concatenation expFeatures 0 = vContext r

theorem Wood2023.Allomorphy.contextAt_word_one (r : String) (e : Morphology.Morph) : (word r (some e)).contextAt (fun (x : Morphology.Morph) => x = zero) DistributedMorphology.ComplexHead.Locality.concatenation expFeatures 1 = nContext r e

theorem Wood2023.Allomorphy.insertAt_word_zero (r : String) : insertAt (word r none) 0 = word r (DistributedMorphology.subsetPrinciple vocab (vContext r))

theorem Wood2023.Allomorphy.insertAt_word_one (r : String) (e : Morphology.Morph) : (do let x ← (insertAt (word r (some e)) 1).heads[1]? x.exp) = DistributedMorphology.subsetPrinciple vocab (nContext r e)

theorem Wood2023.Allomorphy.subsetPrinciple_vContext_isSome (r : String) : (DistributedMorphology.subsetPrinciple vocab (vContext r)).isSome = true

v always receives an exponent, since zero is its elsewhere item.

def Wood2023.Allomorphy.verbalizer (r : String) : Morphology.Morph

The exponent of v in the nominal of the root r.

Equations

• Wood2023.Allomorphy.verbalizer r = (DistributedMorphology.subsetPrinciple Wood2023.Allomorphy.vocab (Wood2023.Allomorphy.vContext r)).getD Wood2023.Allomorphy.zero

def Wood2023.Allomorphy.nominalizer (r : String) : Option Morphology.Morph

The exponent of n in the nominal of the root r, if it has one.

Equations

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

theorem Wood2023.Allomorphy.nominalizer_eq (r : String) : nominalizer r = DistributedMorphology.subsetPrinciple vocab (nContext r (verbalizer r))

The nominalizer is selected in the context v presents once realized.

theorem Wood2023.Allomorphy.nominalizer_of_ne_zero (r : String) (h : verbalizer r ≠ zero) : nominalizer r = DistributedMorphology.subsetPrinciple vocab { focus := [Feature.cat DistributedMorphology.Categorizer.n], leftCtx := [[Feature.cat DistributedMorphology.Categorizer.v, Feature.exp (verbalizer r)]] }

An overt verbalizer hides the root, so the nominalizer is chosen by the verbalizer alone.

theorem Wood2023.Allomorphy.nominalizer_of_eq_zero (r : String) (h : verbalizer r = zero) : nominalizer r = DistributedMorphology.subsetPrinciple vocab { focus := [Feature.cat DistributedMorphology.Categorizer.n], leftCtx := [[Feature.exp (Morphology.Morph.root r)]] }

A zero verbalizer is pruned, so the nominalizer is chosen by the root.

theorem Wood2023.Allomorphy.nominalizer_of_k (r : String) (h : verbalizer r = Morphology.Morph.suff "k") : nominalizer r = some (Morphology.Morph.suff "un")

After -k the nominalizer is -un, whatever the root.

theorem Wood2023.Allomorphy.nominalizer_of_er (r : String) (h : verbalizer r = Morphology.Morph.suff "er") : nominalizer r = some (Morphology.Morph.suff "ing")

After -er the nominalizer is -ing, whatever the root.

theorem Wood2023.Allomorphy.nominalizer_eq_none (r : String) (h : verbalizer r = zero) (hr : r ∉ listed) : nominalizer r = none

With no elsewhere item for n, a root with a zero verbalizer that no item lists has no nominalization.

theorem Wood2023.Allomorphy.borda : nominalizer "borð" = none

borða 'eat' has no nominalization (*borð-un).

The complex head and its readings

inductive Wood2023.Head : Type

A head of the complex head is a categorizer with its alloseme.

• v (a : DistributedMorphology.Allosemy.Verbalizer.Alloseme) : Head
• n (a : DistributedMorphology.Allosemy.Nominalizer.Alloseme) : Head

@[instance_reducible]

instance Wood2023.instDecidableEqHead : DecidableEq Head

Equations

• Wood2023.instDecidableEqHead = Wood2023.instDecidableEqHead.decEq

def Wood2023.instDecidableEqHead.decEq (x✝ x✝¹ : Head) : Decidable (x✝ = x✝¹)

Equations

• Wood2023.instDecidableEqHead.decEq (Wood2023.Head.v a) (Wood2023.Head.v b) = if h : a = b then h ▸ isTrue ⋯ else isFalse ⋯
• Wood2023.instDecidableEqHead.decEq (Wood2023.Head.v a) (Wood2023.Head.n a_1) = isFalse ⋯
• Wood2023.instDecidableEqHead.decEq (Wood2023.Head.n a) (Wood2023.Head.v a_1) = isFalse ⋯
• Wood2023.instDecidableEqHead.decEq (Wood2023.Head.n a) (Wood2023.Head.n b) = if h : a = b then h ▸ isTrue ⋯ else isFalse ⋯

def Wood2023.instReprHead.repr : Head → ℕ → Std.Format

Equations

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

@[instance_reducible]

instance Wood2023.instReprHead : Repr Head

Equations

• Wood2023.instReprHead = { reprPrec := Wood2023.instReprHead.repr }

def Wood2023.Head.Cyclic : Head → Prop

Every head of the complex head is a categorizer, hence a phase head.

Equations

• x✝.Cyclic = True

@[instance_reducible]

instance Wood2023.instDecidablePredHeadCyclic : DecidablePred Head.Cyclic

Equations

• Wood2023.instDecidablePredHeadCyclic x✝ = { decide := true, reflects_decide := ⋯ }

structure Wood2023.Derivation : Type

A choice of allosemes for the v and n of a nominalization.

• v : DistributedMorphology.Allosemy.Verbalizer.Alloseme
• n : DistributedMorphology.Allosemy.Nominalizer.Alloseme

def Wood2023.instDecidableEqDerivation.decEq (x✝ x✝¹ : Derivation) : Decidable (x✝ = x✝¹)

Equations

• Wood2023.instDecidableEqDerivation.decEq { v := a, n := a_1 } { v := b, n := b_1 } = if h : a = b then h ▸ if h : a_1 = b_1 then h ▸ isTrue ⋯ else isFalse ⋯ else isFalse ⋯

@[instance_reducible]

instance Wood2023.instDecidableEqDerivation : DecidableEq Derivation

Equations

• Wood2023.instDecidableEqDerivation = Wood2023.instDecidableEqDerivation.decEq

@[instance_reducible]

instance Wood2023.instFintypeDerivation : Fintype Derivation

Equations

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

def Wood2023.Derivation.reading (d : Derivation) : Option DistributedMorphology.Allosemy.NominalizationReading

The reading the allosemes yield.

Equations

• d.reading = DistributedMorphology.Allosemy.readingFromAllosemes d.v d.n

def Wood2023.Derivation.heads (d : Derivation) : List Head

The heads of the nominalization, innermost first.

Equations

• d.heads = [Wood2023.Head.v d.v, Wood2023.Head.n d.n]

def Wood2023.Derivation.cen : Derivation

The complex event derivation has eventive v and zero n.

Equations

• Wood2023.Derivation.cen = { v := DistributedMorphology.Allosemy.Verbalizer.Alloseme.eventive, n := DistributedMorphology.Allosemy.Nominalizer.Alloseme.zero }

def Wood2023.Derivation.sen : Derivation

The simple event derivation has zero v and the simple event alloseme of n.

Equations

• Wood2023.Derivation.sen = { v := DistributedMorphology.Allosemy.Verbalizer.Alloseme.zero, n := DistributedMorphology.Allosemy.Nominalizer.Alloseme.simpleEvent }

def Wood2023.Derivation.simpleEntity : Derivation

The simple entity derivation has zero v and the entity alloseme of n.

Equations

• Wood2023.Derivation.simpleEntity = { v := DistributedMorphology.Allosemy.Verbalizer.Alloseme.zero, n := DistributedMorphology.Allosemy.Nominalizer.Alloseme.entity }

def Wood2023.Derivation.result : Derivation

The result derivation has eventive v and the result alloseme of n.

Equations

• Wood2023.Derivation.result = { v := DistributedMorphology.Allosemy.Verbalizer.Alloseme.eventive, n := DistributedMorphology.Allosemy.Nominalizer.Alloseme.result }

theorem Wood2023.Derivation.reading_cen : cen.reading = some DistributedMorphology.Allosemy.NominalizationReading.complexEvent

theorem Wood2023.Derivation.reading_sen : sen.reading = some DistributedMorphology.Allosemy.NominalizationReading.simpleEvent

theorem Wood2023.Derivation.reading_simpleEntity : simpleEntity.reading = some DistributedMorphology.Allosemy.NominalizationReading.simpleEntity

theorem Wood2023.Derivation.reading_result : result.reading = some DistributedMorphology.Allosemy.NominalizationReading.result

def Wood2023.Derivation.Eventive (d : Derivation) : Prop

The nP denotes an event when v is eventive and n passes its meaning up unchanged.

Equations

• d.Eventive = (d.v = DistributedMorphology.Allosemy.Verbalizer.Alloseme.eventive ∧ d.n = DistributedMorphology.Allosemy.Nominalizer.Alloseme.zero)

@[instance_reducible]

instance Wood2023.Derivation.instDecidablePredEventive : DecidablePred Eventive

Equations

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

theorem Wood2023.Derivation.eventive_iff (d : Derivation) : d.Eventive ↔ d.reading = some DistributedMorphology.Allosemy.NominalizationReading.complexEvent

The complex event reading is exactly the eventive nP.

theorem Wood2023.Derivation.exists_reading (rd : DistributedMorphology.Allosemy.NominalizationReading) : ∃ (d : Derivation), d.reading = some rd

Every reading is derived by some choice of allosemes.

Complex heads

def Wood2023.verb (r : DistributedMorphology.Root) : DistributedMorphology.ComplexHead DistributedMorphology.Root Head

The verb is the root categorized by eventive v.

Equations

• Wood2023.verb r = { root := r, heads := [Wood2023.Head.v DistributedMorphology.Allosemy.Verbalizer.Alloseme.eventive] }

def Wood2023.nominal (r : DistributedMorphology.Root) (d : Derivation) : DistributedMorphology.ComplexHead DistributedMorphology.Root Head

The nominalization is the root categorized by v and then by n.

Equations

• Wood2023.nominal r d = { root := r, heads := d.heads }

def Wood2023.vaedaVerb (r : DistributedMorphology.Root) (a : DistributedMorphology.Allosemy.Nominalizer.Alloseme) : DistributedMorphology.ComplexHead DistributedMorphology.Root Head

A -væða verb is the root categorized by n, compounded with the v of -væða.

Equations

• Wood2023.vaedaVerb r a = { root := r, heads := [Wood2023.Head.n a, Wood2023.Head.v DistributedMorphology.Allosemy.Verbalizer.Alloseme.eventive] }

def Wood2023.vaedaNominal (r : DistributedMorphology.Root) (a c : DistributedMorphology.Allosemy.Nominalizer.Alloseme) : DistributedMorphology.ComplexHead DistributedMorphology.Root Head

A -væðing nominal is the -væða verb categorized by n.

Equations

• Wood2023.vaedaNominal r a c = { root := r, heads := (Wood2023.vaedaVerb r a).heads ++ [Wood2023.Head.n c] }

Borer's Generalization

theorem Wood2023.nominal_n_not_rootLocal (r : DistributedMorphology.Root) (d : Derivation) : ¬(nominal r d).RootLocal Head.Cyclic ⟨1, Nat.one_lt_two⟩

The n of a nominalization is not in the root's domain, since category change closes it.

theorem Wood2023.borers_generalization (r : DistributedMorphology.Root) {d : Derivation} (h : d.reading = some DistributedMorphology.Allosemy.NominalizationReading.complexEvent) : d.v = DistributedMorphology.Allosemy.Verbalizer.Alloseme.eventive ∧ ¬(nominal r d).RootLocal Head.Cyclic ⟨1, Nat.one_lt_two⟩

By Borer's Generalization a complex event nominal contains the eventive v of the verb and its n cannot condition suppletion of the root, so the nominal is built on a verb with the same root exponent and the same meaning.

The external argument

inductive Wood2023.IStar.Contentful : Type

The contentful allosemes of i*, the external-argument head that is Voice in the verbal domain and Poss in the nominal domain.

• agent : Contentful
• possessor : Contentful

@[instance_reducible]

instance Wood2023.IStar.instDecidableEqContentful : DecidableEq Contentful

Equations

• Wood2023.IStar.instDecidableEqContentful x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

@[instance_reducible]

instance Wood2023.IStar.instReprContentful : Repr Contentful

Equations

• Wood2023.IStar.instReprContentful = { reprPrec := Wood2023.IStar.instReprContentful.repr }

def Wood2023.IStar.instReprContentful.repr : Contentful → ℕ → Std.Format

Equations

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

@[instance_reducible]

instance Wood2023.IStar.instFintypeContentful : Fintype Contentful

Equations

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

@[reducible, inline]

abbrev Wood2023.IStar.Alloseme : Type

The allosemes of i*.

Equations

• Wood2023.IStar.Alloseme = DistributedMorphology.Allosemy.Alloseme Wood2023.IStar.Contentful

@[match_pattern]

def Wood2023.IStar.Alloseme.agent : Alloseme

Equations

• Wood2023.IStar.Alloseme.agent = DistributedMorphology.Allosemy.Alloseme.of Wood2023.IStar.Contentful.agent

@[match_pattern]

def Wood2023.IStar.Alloseme.possessor : Alloseme

Equations

• Wood2023.IStar.Alloseme.possessor = DistributedMorphology.Allosemy.Alloseme.of Wood2023.IStar.Contentful.possessor

def Wood2023.IStar.vocabulary : Morphology.Exponence.RuleSet (DistributedMorphology.VocabularyItem DistributedMorphology.Allosemy.Feature Alloseme)

i* is an agent in the context of an eventive complement and a possessor elsewhere.

Equations

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

def Wood2023.IStar.alloseme (fs : List DistributedMorphology.Allosemy.Feature) : Alloseme

The alloseme of i* selected by its complement's features.

Equations

• Wood2023.IStar.alloseme fs = (DistributedMorphology.subsetPrinciple Wood2023.IStar.vocabulary (DistributedMorphology.Allosemy.complement fs)).getD Wood2023.IStar.Alloseme.possessor

def Wood2023.Derivation.features (d : Derivation) : List DistributedMorphology.Allosemy.Feature

An nP presents its category to i*, and eventivity when it denotes an event.

Equations

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

theorem Wood2023.iStar_agent_iff (d : Derivation) : IStar.alloseme d.features = IStar.Alloseme.agent ↔ d.reading = some DistributedMorphology.Allosemy.NominalizationReading.complexEvent

The possessor of a nominal is its agent exactly on the complex event reading.

Phase locality of special meaning

def Wood2023.Local (between : List Head) : Prop

Wood's phase locality lets a dependency conditioning special meaning cross at most one categorizer.

Equations

• Wood2023.Local between = (between.length ≤ 1)

inductive Wood2023.Attachment : Type

A preposition attaches to a complex head either adjoined to it or heading its complement PP.

• adjunct : Attachment
• complement : Attachment

@[instance_reducible]

instance Wood2023.instDecidableEqAttachment : DecidableEq Attachment

Equations

• Wood2023.instDecidableEqAttachment x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

def Wood2023.instReprAttachment.repr : Attachment → ℕ → Std.Format

Equations

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

@[instance_reducible]

instance Wood2023.instReprAttachment : Repr Attachment

Equations

• Wood2023.instReprAttachment = { reprPrec := Wood2023.instReprAttachment.repr }

def Wood2023.interveners (s : DistributedMorphology.ComplexHead DistributedMorphology.Root Head) : Attachment → List Head

The heads between a preposition and the root are every head of the complex head when the preposition heads its complement, and all but the outermost when it adjoins to the complex head, since a head does not c-command its own adjunct.

Equations

• Wood2023.interveners s Wood2023.Attachment.complement = s.heads
• Wood2023.interveners s Wood2023.Attachment.adjunct = s.heads.dropLast

theorem Wood2023.Local.adjunct_of_complement {s : DistributedMorphology.ComplexHead DistributedMorphology.Root Head} (h : Local (interveners s Attachment.complement)) : Local (interveners s Attachment.adjunct)

Adjunction is at least as local as complementation.

theorem Wood2023.verb_local (r : DistributedMorphology.Root) (a : Attachment) : Local (interveners (verb r) a)

A preposition may condition the root of a verb whether adjoined or in its complement.

theorem Wood2023.nominal_complement_not_local (r : DistributedMorphology.Root) (d : Derivation) : ¬Local (interveners (nominal r d) Attachment.complement)

A preposition heading the complement of a nominal cannot condition its root, since v and n intervene. A preposition that conditions the root's meaning must therefore be prefixed.

theorem Wood2023.nominal_adjunct_local (r : DistributedMorphology.Root) (d : Derivation) : Local (interveners (nominal r d) Attachment.adjunct)

A preposition adjoined to the complex n head may condition the root, since only v intervenes.

theorem Wood2023.nominal_n_local (r : DistributedMorphology.Root) (d : Derivation) : Local (List.take 1 (nominal r d).heads)

The n of a nominalization may condition an idiosyncratic meaning of the root across v.

theorem Wood2023.vaeda_n_not_local (r : DistributedMorphology.Root) (a c : DistributedMorphology.Allosemy.Nominalizer.Alloseme) : ¬Local (List.take 2 (vaedaNominal r a c).heads)

The outer n of a -væðing nominal cannot condition the root, since the inner n and v intervene, so the nominal has no idiosyncratic referring reading.

theorem Wood2023.vaeda_complement_not_local (r : DistributedMorphology.Root) (a : DistributedMorphology.Allosemy.Nominalizer.Alloseme) : ¬Local (interveners (vaedaVerb r a) Attachment.complement)

A PP complement of a -væða verb cannot condition its root, so its interpretation is compositional.

The prefixes marg- and endur-

inductive Wood2023.Prefix : Type

The event-modifying prefixes are iterative marg- 'many' and endur- 're-'.

• marg : Prefix
• endur : Prefix

@[instance_reducible]

instance Wood2023.instDecidableEqPrefix : DecidableEq Prefix

Equations

• Wood2023.instDecidableEqPrefix x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

def Wood2023.instReprPrefix.repr : Prefix → ℕ → Std.Format

Equations

• Wood2023.instReprPrefix.repr Wood2023.Prefix.marg prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Wood2023.Prefix.marg")).group prec✝
• Wood2023.instReprPrefix.repr Wood2023.Prefix.endur prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Wood2023.Prefix.endur")).group prec✝

@[instance_reducible]

instance Wood2023.instReprPrefix : Repr Prefix

Equations

• Wood2023.instReprPrefix = { reprPrec := Wood2023.instReprPrefix.repr }

def Wood2023.Prefix.AdjoinsTo : Prefix → Head → Prop

At the complex head marg- adjoins to v, and endur- to v or n.

Equations

• Wood2023.Prefix.marg.AdjoinsTo (Wood2023.Head.v a) = True
• Wood2023.Prefix.marg.AdjoinsTo (Wood2023.Head.n a) = False
• Wood2023.Prefix.endur.AdjoinsTo x✝ = True

def Wood2023.Head.HasEvent : Head → Prop

A head's alloseme carries an event variable for eventive v and for the simple event and result allosemes of n.

Equations

• (Wood2023.Head.v a).HasEvent = (a = DistributedMorphology.Allosemy.Verbalizer.Alloseme.eventive)
• (Wood2023.Head.n a).HasEvent = (a = DistributedMorphology.Allosemy.Nominalizer.Alloseme.simpleEvent ∨ a = DistributedMorphology.Allosemy.Nominalizer.Alloseme.result)

def Wood2023.Licensed (p : Prefix) (d : Derivation) : Prop

A prefix is licensed on a nominalization when some head it adjoins to there carries an event variable.

Equations

• Wood2023.Licensed p d = ∃ h ∈ d.heads, p.AdjoinsTo h ∧ h.HasEvent

theorem Wood2023.licensed_marg_iff (d : Derivation) : Licensed Prefix.marg d ↔ d.v = DistributedMorphology.Allosemy.Verbalizer.Alloseme.eventive

marg- is licensed exactly when v is eventive.

theorem Wood2023.licensed_endur_iff (d : Derivation) : Licensed Prefix.endur d ↔ d.v = DistributedMorphology.Allosemy.Verbalizer.Alloseme.eventive ∨ d.n = DistributedMorphology.Allosemy.Nominalizer.Alloseme.simpleEvent ∨ d.n = DistributedMorphology.Allosemy.Nominalizer.Alloseme.result

endur- is licensed exactly when v or n carries an event variable.

theorem Wood2023.Licensed.endur {d : Derivation} (h : Licensed Prefix.marg d) : Licensed Prefix.endur d

marg- is stricter than endur-.

@[instance_reducible]

instance Wood2023.instDecidableLicensed (p : Prefix) (d : Derivation) : Decidable (Licensed p d)

Equations

• One or more equations did not get rendered due to their size.
• Wood2023.instDecidableLicensed Wood2023.Prefix.marg d = decidable_of_iff (d.v = DistributedMorphology.Allosemy.Verbalizer.Alloseme.eventive) ⋯

def Wood2023.prefixTable : List (String × Prefix)

The prefixes as the rows name them.

Equations

• Wood2023.prefixTable = [("marg-", Wood2023.Prefix.marg), ("endur-", Wood2023.Prefix.endur)]

def Wood2023.readingTable : List (String × Derivation)

The readings as the rows name them, where the referring reading of þvottur is the simple entity one and that of endurprentun the result.

Equations

• Wood2023.readingTable = [("CEN", Wood2023.Derivation.cen), ("SEN", Wood2023.Derivation.sen), ("RN", Wood2023.Derivation.simpleEntity), ("result RN", Wood2023.Derivation.result)]

def Wood2023.ofRow (ex : Datum) : Option (Prefix × Derivation)

A row of a prefixed nominal on a reading, as the prefix and the derivation.

Equations

• Wood2023.ofRow ex = do let p ← ex.parse? "prefix" Wood2023.prefixTable let d ← ex.parse? "reading" Wood2023.readingTable pure (p, d)

theorem Wood2023.rows_licensed (ex : Datum) : ex ∈ Examples.all → ∀ pd ∈ ofRow ex, ex.judgment = Judgment.acceptable ↔ Licensed pd.1 pd.2

By the book's judgments on marg- and endur-, a prefixed nominal is acceptable on a reading exactly when the prefix is licensed on that reading's derivation.

Allosemy conditioned by the root

def Wood2023.judgments (w : Icelandic.Nouns.Deverbal) (reading : String) : List Judgment

The judgments of the rows on a nominal of the fragment under a reading.

Equations

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

theorem Wood2023.reading_not_by_nominalizer : Icelandic.Nouns.addaun.nominalizer = Icelandic.Nouns.vidvorun.nominalizer ∧ judgments Icelandic.Nouns.addaun "RN" = [Judgment.ungrammatical] ∧ judgments Icelandic.Nouns.vidvorun "RN" = [Judgment.acceptable]

The reading is not a function of the nominalizer, since aðdáun and viðvörun share -un and only viðvörun is a concrete entity.