Embick (2015): The Morpheme: A Theoretical Introduction

This file formalizes [Emb15]'s procedure of Vocabulary Insertion in a complex head: insertion proceeds from the inside out (§4.5, the condition (C3) of §7.3), substitutes an exponent for the Q variable of each functional morpheme (§4.2), leaves the morpheme's synsem features in place (§4.2.2), and lets a contextual item see the concatenated neighbours of its morpheme, null exponents pruned (§7.3.2). The procedure is the substrate's ComplexHead.insertAll, and this file runs it on the book's own material. The fragment of the Latin conjugation (§4.6) derives the four tenses of laudāre in (40) from the Vocabulary Items (36), (37) and (42): the perfect-specific agreement endings are inserted only where the deleted T[−past] leaves Agr concatenated with Asp[perf], the overt tense of the pluperfect intervening (§7.3.2.1), and the first singular -m of the imperfect and pluperfect reads T[+past]. Under rewriting, where insertion deletes the synsem features of the morpheme it realizes, both conditionings are lost, and Agr would have to refer to the exponents -rā and -bā, and to each allomorph of Asp[perf], one by one; that is the book's argument for non-deletion (§4.6.3). The Hungarian plural of (7) and (8) looks outward at the possessive, and the Korean nominative of (10) and (11) looks inward at whether its host ends in a consonant or a vowel. The predictions of (C3) in (43) are that outward conditioning sees synsem features only, the possessive being bare when the plural is realized, while inward conditioning may see the phonological features of a realized exponent.

Implementation notes

• The book's rule (38) deletes T[−past] outright; here T[−past] receives a null exponent and is pruned from the concatenation statements, the alternative the book itself offers for transparent zero morphemes in §7.3.2, so that the four tenses share the one spine ROOT-v-(Asp)-T-Agr of (35).
• The theme vowel is the exponent of v, as in (36a), spelled out in the context of the root's conjugation feature [+I].
• (42) prints the number feature of the -m item as [−sg] where (39) has [−pl], and omits the third singular -t of (33a); both are restored.
• The Korean hosts are transcribed into the segments of Fragments.Korean.Phonology, so that the consonant-final or vowel-final shape an item refers to is read off the [consonantal] value of the final segment rather than listed per host.
• The examples are Data.Examples.Embick2015.

References

• [Emb15]
• [HM93]
• [Bob00]
• [Car87]

The Latin fragment

inductive Embick2015.Latin.Feature : Type

The root of laudāre with its conjugation feature [+I], and the features of v, Asp[perf], T[±past] and Agr[±1, ±2, ±pl].

• laud : Feature
• conjI : Feature
• v : Feature
• asp : Feature
• perf : Feature
• tense : Feature
• past : Feature
• agr : Feature
• first (b : Bool) : Feature
• second (b : Bool) : Feature
• pl (b : Bool) : Feature

def Embick2015.Latin.instDecidableEqFeature.decEq (x✝ x✝¹ : Feature) : Decidable (x✝ = x✝¹)

Equations

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

@[instance_reducible]

instance Embick2015.Latin.instDecidableEqFeature : DecidableEq Feature

Equations

• Embick2015.Latin.instDecidableEqFeature = Embick2015.Latin.instDecidableEqFeature.decEq

def Embick2015.Latin.instReprFeature.repr : Feature → ℕ → Std.Format

Equations

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

@[instance_reducible]

instance Embick2015.Latin.instReprFeature : Repr Feature

Equations

• Embick2015.Latin.instReprFeature = { reprPrec := Embick2015.Latin.instReprFeature.repr }

def Embick2015.Latin.vocab : List (DistributedMorphology.VocabularyItem Feature String)

The Vocabulary Items (36), (37) and (42) are the theme vowel of v in conjugation I, Asp[perf] -vi, T[+past] -rā after Asp[perf] and -bā otherwise, the null T[−past] of (38), and the agreement endings, the perfect-specific set after Asp[perf], -m after T[+past], the defaults elsewhere.

Equations

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

inductive Embick2015.Latin.Tense : Type

The four tenses of (40).

• present : Tense
• imperfect : Tense
• perfect : Tense
• pluperfect : Tense

@[instance_reducible]

instance Embick2015.Latin.instDecidableEqTense : DecidableEq Tense

Equations

• Embick2015.Latin.instDecidableEqTense x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

def Embick2015.Latin.instReprTense.repr : Tense → ℕ → Std.Format

Equations

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

@[instance_reducible]

instance Embick2015.Latin.instReprTense : Repr Tense

Equations

• Embick2015.Latin.instReprTense = { reprPrec := Embick2015.Latin.instReprTense.repr }

def Embick2015.Latin.Tense.heads : Tense → List (DistributedMorphology.Morpheme Feature String)

The Asp and T morphemes of a tense, with Asp[perf] in the perfects only (§4.6.1).

Equations

• One or more equations did not get rendered due to their size.
• Embick2015.Latin.Tense.present.heads = [{ feats := [Embick2015.Latin.Feature.tense] }]
• Embick2015.Latin.Tense.imperfect.heads = [{ feats := [Embick2015.Latin.Feature.tense, Embick2015.Latin.Feature.past] }]
• Embick2015.Latin.Tense.perfect.heads = [{ feats := [Embick2015.Latin.Feature.asp, Embick2015.Latin.Feature.perf] }, { feats := [Embick2015.Latin.Feature.tense] }]

def Embick2015.Latin.word (t : Tense) (p₁ p₂ pl : Bool) : DistributedMorphology.ComplexHead (DistributedMorphology.Morpheme Feature String) (DistributedMorphology.Morpheme Feature String)

ROOT-v-(Asp)-T-Agr, (35).

Equations

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

def Embick2015.Latin.morphs (dis : DistributedMorphology.ComplexHead.Discharge) (w : DistributedMorphology.ComplexHead (DistributedMorphology.Morpheme Feature String) (DistributedMorphology.Morpheme Feature String)) : List String

The surface morphs after inside-out insertion with the given discharge, the pruned T[−past] dropped.

Equations

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

def Embick2015.Latin.tenseTable : List (String × Tense)

The tenses as named in the rows.

Equations

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

def Embick2015.Latin.personTable : List (String × Bool × Bool)

The persons as named in the rows, as [±1, ±2].

Equations

• Embick2015.Latin.personTable = [("1", true, false), ("2", false, true), ("3", false, false)]

def Embick2015.Latin.numberTable : List (String × Bool)

The numbers as named in the rows, as [±pl].

Equations

• Embick2015.Latin.numberTable = [("sg", false), ("pl", true)]

def Embick2015.Latin.ofRow (ex : Datum) : Option (DistributedMorphology.ComplexHead (DistributedMorphology.Morpheme Feature String) (DistributedMorphology.Morpheme Feature String) × List String)

A row of (40) as its complex head and its morphs.

Equations

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

theorem Embick2015.Latin.ofRow_isSome (ex : Datum) : ex ∈ Examples.all → ex.language = "lati1261" → (ofRow ex).isSome = true

def Embick2015.Latin.rows : List (DistributedMorphology.ComplexHead (DistributedMorphology.Morpheme Feature String) (DistributedMorphology.Morpheme Feature String) × List String)

The twenty-four forms of (40).

Equations

• Embick2015.Latin.rows = List.filterMap Embick2015.Latin.ofRow (List.filter (fun (x : Datum) => decide (x.language = "lati1261")) Embick2015.Examples.all)

theorem Embick2015.Latin.rows_morphs (r : DistributedMorphology.ComplexHead (DistributedMorphology.Morpheme Feature String) (DistributedMorphology.Morpheme Feature String) × List String) : r ∈ rows → morphs DistributedMorphology.ComplexHead.Discharge.nondeletion r.1 = r.2

In (40) the four tenses derive with T[−past] pruned, so that Agr is concatenated with Asp[perf] in the perfect but with the overt T[+past] in the pluperfect (§7.3.2.1).

theorem Embick2015.Latin.rewriting_loses_conditioning : morphs DistributedMorphology.ComplexHead.Discharge.rewriting (word Tense.imperfect true false false) = ["laud", "ā", "bā", "ō"] ∧ morphs DistributedMorphology.ComplexHead.Discharge.rewriting (word Tense.perfect true false false) = ["laud", "ā", "vi", "ō"]

As §4.6.3 argues, were a morpheme's synsem features deleted at its insertion, Agr could see neither T[+past] nor Asp[perf], and the first singular of the imperfect and of the perfect would fall to the default -ō.

Outward conditioning: the Hungarian plural

inductive Embick2015.Hungarian.Feature : Type

The plural and possessive features.

• pl : Feature
• poss : Feature

@[instance_reducible]

instance Embick2015.Hungarian.instDecidableEqFeature : DecidableEq Feature

Equations

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

@[instance_reducible]

instance Embick2015.Hungarian.instReprFeature : Repr Feature

Equations

• Embick2015.Hungarian.instReprFeature = { reprPrec := Embick2015.Hungarian.instReprFeature.repr }

def Embick2015.Hungarian.instReprFeature.repr : Feature → ℕ → Std.Format

Equations

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

def Embick2015.Hungarian.vocab : List (DistributedMorphology.VocabularyItem Feature String)

In (8), with the concatenation of (28), the plural is -((j)a)i- before a possessive and -(V)k otherwise; the first singular possessive is -m.

Equations

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

def Embick2015.Hungarian.word (r : String) (possessed : Bool) : DistributedMorphology.ComplexHead (DistributedMorphology.Morpheme Feature String) (DistributedMorphology.Morpheme Feature String)

Noun-[+pl], or Noun-[+pl]-[+poss] when possessed.

Equations

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

def Embick2015.Hungarian.plural (w : DistributedMorphology.ComplexHead (DistributedMorphology.Morpheme Feature String) (DistributedMorphology.Morpheme Feature String)) : Option String

The exponent of the plural after inside-out insertion.

Equations

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

def Embick2015.Hungarian.possTable : List (String × Bool)

Possession as named in the rows.

Equations

• Embick2015.Hungarian.possTable = [("yes", true), ("no", false)]

def Embick2015.Hungarian.ofRow (ex : Datum) : Option (DistributedMorphology.ComplexHead (DistributedMorphology.Morpheme Feature String) (DistributedMorphology.Morpheme Feature String) × String)

A row of (7) as its complex head and the exponent of its plural.

Equations

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

theorem Embick2015.Hungarian.ofRow_isSome (ex : Datum) : ex ∈ Examples.all → ex.language = "hung1274" → (ofRow ex).isSome = true

def Embick2015.Hungarian.rows : List (DistributedMorphology.ComplexHead (DistributedMorphology.Morpheme Feature String) (DistributedMorphology.Morpheme Feature String) × String)

The plural and possessed plural of the three nouns of (7).

Equations

• Embick2015.Hungarian.rows = List.filterMap Embick2015.Hungarian.ofRow (List.filter (fun (x : Datum) => decide (x.language = "hung1274")) Embick2015.Examples.all)

theorem Embick2015.Hungarian.rows_plural (r : DistributedMorphology.ComplexHead (DistributedMorphology.Morpheme Feature String) (DistributedMorphology.Morpheme Feature String) × String) : r ∈ rows → plural r.1 = some r.2

The rows of (7) show outward conditioning by the possessive's feature.

theorem Embick2015.Hungarian.outward_features_only (r : DistributedMorphology.ComplexHead (DistributedMorphology.Morpheme Feature String) (DistributedMorphology.Morpheme Feature String) × String) : r ∈ rows → (r.1.contextAt (fun (x : String) => x = "") DistributedMorphology.ComplexHead.Locality.concatenation (fun (x : String) => []) 0).rightCtx = List.map (fun (x : DistributedMorphology.Morpheme Feature String) => x.feats) (List.drop 1 r.1.heads)

As (43a, b) state, when the plural is reached, what it sees outward is the features of the possessive and nothing of an exponent, the possessive being still bare.

Inward phonological conditioning: the Korean nominative

inductive Embick2015.Korean.Feature : Type

The nominative, and the shape of its host.

• nom : Feature
• cFinal : Feature
• vFinal : Feature

@[instance_reducible]

instance Embick2015.Korean.instDecidableEqFeature : DecidableEq Feature

Equations

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

@[instance_reducible]

instance Embick2015.Korean.instReprFeature : Repr Feature

Equations

• Embick2015.Korean.instReprFeature = { reprPrec := Embick2015.Korean.instReprFeature.repr }

def Embick2015.Korean.instReprFeature.repr : Feature → ℕ → Std.Format

Equations

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

def Embick2015.Korean.vocab : List (DistributedMorphology.VocabularyItem Feature String)

In (11) the nominative is -i after a consonant and -ka after a vowel.

Equations

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

def Embick2015.Korean.segments : List (String × List Phonology.Segment)

The hosts of (10), transcribed into the segments of the fragment.

Equations

• Embick2015.Korean.segments = [("pap", [Korean.p, Korean.a, Korean.p]), ("ai", [Korean.a, Korean.i])]

def Embick2015.Korean.shape (e : String) : List Feature

The phonological feature a realized exponent presents to insertion is whether its final segment is a consonant.

Equations

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

def Embick2015.Korean.word (r : String) : DistributedMorphology.ComplexHead (DistributedMorphology.Morpheme Feature String) (DistributedMorphology.Morpheme Feature String)

Noun-[nom].

Equations

• Embick2015.Korean.word r = { root := { feats := [], exp := some r }, heads := [{ feats := [Embick2015.Korean.Feature.nom] }] }

def Embick2015.Korean.nominative (w : DistributedMorphology.ComplexHead (DistributedMorphology.Morpheme Feature String) (DistributedMorphology.Morpheme Feature String)) : Option String

The exponent of the nominative after inside-out insertion.

Equations

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

def Embick2015.Korean.ofRow (ex : Datum) : Option (DistributedMorphology.ComplexHead (DistributedMorphology.Morpheme Feature String) (DistributedMorphology.Morpheme Feature String) × String)

A row of (10) as its complex head and the exponent of its nominative.

Equations

• Embick2015.Korean.ofRow ex = do let __do_lift ← ex.feature? "root" let __do_lift_1 ← ex.feature? "nomExponent" pure (Embick2015.Korean.word __do_lift, __do_lift_1)

theorem Embick2015.Korean.ofRow_isSome (ex : Datum) : ex ∈ Examples.all → ex.language = "kore1280" → (ofRow ex).isSome = true

def Embick2015.Korean.rows : List (DistributedMorphology.ComplexHead (DistributedMorphology.Morpheme Feature String) (DistributedMorphology.Morpheme Feature String) × String)

The two hosts of (10).

Equations

• Embick2015.Korean.rows = List.filterMap Embick2015.Korean.ofRow (List.filter (fun (x : Datum) => decide (x.language = "kore1280")) Embick2015.Examples.all)

theorem Embick2015.Korean.rows_nominative (r : DistributedMorphology.ComplexHead (DistributedMorphology.Morpheme Feature String) (DistributedMorphology.Morpheme Feature String) × String) : r ∈ rows → nominative r.1 = some r.2

The rows of (10) show the inward conditioning of (43d), by the host's phonology as visible through its realized exponent.