Documentation

Linglib.Studies.Embick2015

Embick 2015: Vocabulary Insertion from the inside out #

[embick-2015]'s exposition of Distributed Morphology runs Vocabulary Insertion over a complex head from the inside out, each morpheme's Q variable replaced by the most specific applicable exponent, the conditioning context being the concatenated neighbors once null exponents are pruned. This file runs that procedure on the book's own material: the Latin verb fragment for laudāre (present, imperfect, perfect, pluperfect) whose Agr exponents look inward at Asp[perf] and T[+past], the Hungarian plural whose exponent looks outward at a possessive, and the Korean nominative whose exponent looks inward at the phonology of the stem, the three directions of conditioning the book predicts, inward phonological conditioning through the stem's exponent and outward conditioning through features only.

Main results #

latin_rows: the twenty-four forms of the fragment derive with Pruning of the null T[−past].
rewriting_loses_m: if insertion deleted T's features, the first-singular -m could not be conditioned by T[+past]; non-deletion is what the fragment needs.
hungarian_rows, korean_rows: outward synsem and inward phonological conditioning.
outward_features_only: at the Hungarian plural, the possessive ahead of it is still bare.

References #

[embick-2015], [Hal97].

inductive Embick2015.Latin.Feature :

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

Instances For

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

Decidable (x✝ = x✝¹)

Equations

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

Instances For

@[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.

Instances For

@[instance_reducible]

instance Embick2015.Latin.instReprFeature :

Equations

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

def Embick2015.Latin.vocab :

List (DistributedMorphology.VocabularyItem Feature String)

The theme vowel as the exponent of v in conjugation I, Asp[perf] -vi, T[+past] -rā after the perfect and -bā otherwise, T[−past] null, and the Agr exponents: the perfect set after Asp[perf], -m after T[+past], the defaults elsewhere.

Equations

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

Instances For

inductive Embick2015.Latin.Tense :

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

Instances For

@[instance_reducible]

instance Embick2015.Latin.instDecidableEqTense :

DecidableEq Tense

Equations

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

@[instance_reducible]

instance Embick2015.Latin.instReprTense :

Repr Tense

Equations

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

def Embick2015.Latin.instReprTense.repr :

Tense → ℕ → Std.Format

Equations

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

Instances For

def Embick2015.Latin.Tense.heads :

Tense → List (DistributedMorphology.Morpheme Feature String)

The Asp and T morphemes of each tense.

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] }]

Instances For

def Embick2015.Latin.word (t : Tense) (p₁ p₂ pl : Bool) :

DistributedMorphology.ComplexHead Feature String

√LAUD-v-(Asp)-T-Agr.

Equations

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

Instances For

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

List String

Surface morphs after inside-out insertion with the given discharge.

Equations

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

Instances For

def Embick2015.Latin.parseTense :

String → Option Tense

Equations

Embick2015.Latin.parseTense "present" = some Embick2015.Latin.Tense.present
Embick2015.Latin.parseTense "imperfect" = some Embick2015.Latin.Tense.imperfect
Embick2015.Latin.parseTense "perfect" = some Embick2015.Latin.Tense.perfect
Embick2015.Latin.parseTense "pluperfect" = some Embick2015.Latin.Tense.pluperfect
Embick2015.Latin.parseTense x✝ = none

Instances For

def Embick2015.Latin.parsePerson :

String → Option (Bool × Bool)

Equations

Embick2015.Latin.parsePerson "1" = some (true, false)
Embick2015.Latin.parsePerson "2" = some (false, true)
Embick2015.Latin.parsePerson "3" = some (false, false)
Embick2015.Latin.parsePerson x✝ = none

Instances For

def Embick2015.Latin.ofRow (ex : Data.Examples.LinguisticExample) :

Option (DistributedMorphology.ComplexHead Feature String × List String)

A row of the fragment as its word and its morphs.

Equations

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

Instances For

def Embick2015.Latin.rows :

List (DistributedMorphology.ComplexHead Feature String × List String)

Equations

Embick2015.Latin.rows = List.filterMap Embick2015.Latin.ofRow Embick2015.Examples.all

Instances For

theorem Embick2015.Latin.latin_rows (r : DistributedMorphology.ComplexHead Feature String × List String) :

r ∈ rows → morphs DistributedMorphology.ComplexHead.Discharge.nondeletion r.1 = r.2

The twenty-four forms of the fragment, with T[−past] pruned.

theorem Embick2015.Latin.card_rows :

rows.length = 24

theorem Embick2015.Latin.rewriting_loses_m :

morphs DistributedMorphology.ComplexHead.Discharge.rewriting (word Tense.imperfect true false false) = ["laud", "ā", "bā", "ō"] ∧ morphs DistributedMorphology.ComplexHead.Discharge.nondeletion (word Tense.imperfect true false false) = ["laud", "ā", "bā", "m"]

Rewriting T[+past]'s features away at its own insertion leaves Agr the default -ō: the -m of the imperfect needs non-deletion.

inductive Embick2015.Hungarian.Feature :

root (s : String) : Feature
pl : Feature
poss : Feature

Instances For

def Embick2015.Hungarian.instDecidableEqFeature.decEq (x✝ x✝¹ : Feature) :

Decidable (x✝ = x✝¹)

Equations

Embick2015.Hungarian.instDecidableEqFeature.decEq (Embick2015.Hungarian.Feature.root a) (Embick2015.Hungarian.Feature.root b) = if h : a = b then h ▸ isTrue ⋯ else isFalse ⋯
Embick2015.Hungarian.instDecidableEqFeature.decEq (Embick2015.Hungarian.Feature.root s) Embick2015.Hungarian.Feature.pl = isFalse ⋯
Embick2015.Hungarian.instDecidableEqFeature.decEq (Embick2015.Hungarian.Feature.root s) Embick2015.Hungarian.Feature.poss = isFalse ⋯
Embick2015.Hungarian.instDecidableEqFeature.decEq Embick2015.Hungarian.Feature.pl (Embick2015.Hungarian.Feature.root s) = isFalse ⋯
Embick2015.Hungarian.instDecidableEqFeature.decEq Embick2015.Hungarian.Feature.pl Embick2015.Hungarian.Feature.pl = isTrue ⋯
Embick2015.Hungarian.instDecidableEqFeature.decEq Embick2015.Hungarian.Feature.pl Embick2015.Hungarian.Feature.poss = isFalse Embick2015.Hungarian.instDecidableEqFeature.decEq._proof_6
Embick2015.Hungarian.instDecidableEqFeature.decEq Embick2015.Hungarian.Feature.poss (Embick2015.Hungarian.Feature.root s) = isFalse ⋯
Embick2015.Hungarian.instDecidableEqFeature.decEq Embick2015.Hungarian.Feature.poss Embick2015.Hungarian.Feature.pl = isFalse Embick2015.Hungarian.instDecidableEqFeature.decEq._proof_8
Embick2015.Hungarian.instDecidableEqFeature.decEq Embick2015.Hungarian.Feature.poss Embick2015.Hungarian.Feature.poss = isTrue ⋯

Instances For

@[instance_reducible]

instance Embick2015.Hungarian.instDecidableEqFeature :

DecidableEq Feature

Equations

Embick2015.Hungarian.instDecidableEqFeature = Embick2015.Hungarian.instDecidableEqFeature.decEq

def Embick2015.Hungarian.instReprFeature.repr :

Feature → ℕ → Std.Format

Equations

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

Instances For

@[instance_reducible]

instance Embick2015.Hungarian.instReprFeature :

Equations

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

def Embick2015.Hungarian.vocab :

List (DistributedMorphology.VocabularyItem Feature String)

The plural is -ai- before a possessive and -k otherwise.

Equations

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

Instances For

def Embick2015.Hungarian.word (r : String) (possessed : Bool) :

DistributedMorphology.ComplexHead Feature String

Equations

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

Instances For

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

Option String

Equations

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

Instances For

def Embick2015.Hungarian.ofRow (ex : Data.Examples.LinguisticExample) :

Option (DistributedMorphology.ComplexHead Feature String × String)

Equations

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

Instances For

def Embick2015.Hungarian.rows :

List (DistributedMorphology.ComplexHead Feature String × String)

Equations

Embick2015.Hungarian.rows = List.filterMap Embick2015.Hungarian.ofRow Embick2015.Examples.all

Instances For

theorem Embick2015.Hungarian.hungarian_rows (r : DistributedMorphology.ComplexHead Feature String × String) :

r ∈ rows → plural r.1 = some r.2

Outward conditioning by the possessive's features.

theorem Embick2015.Hungarian.outward_features_only :

((word "ruha" true).contextAt (fun (x : String) => x = "") DistributedMorphology.ComplexHead.Locality.concatenation (fun (x : String) => []) 0).rightCtx = [[Feature.poss]]

When the plural is reached the possessive ahead of it is still bare: what it sees outward is features, never an exponent.

inductive Embick2015.Korean.Feature :

root (s : String) : Feature
nom : Feature
cFinal : Feature
vFinal : Feature

Instances For

def Embick2015.Korean.instDecidableEqFeature.decEq (x✝ x✝¹ : Feature) :

Decidable (x✝ = x✝¹)

Equations

Instances For

@[instance_reducible]

instance Embick2015.Korean.instDecidableEqFeature :

DecidableEq Feature

Equations

Embick2015.Korean.instDecidableEqFeature = Embick2015.Korean.instDecidableEqFeature.decEq

def Embick2015.Korean.instReprFeature.repr :

Feature → ℕ → Std.Format

Equations

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

Instances For

@[instance_reducible]

instance Embick2015.Korean.instReprFeature :

Equations

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

def Embick2015.Korean.vocab :

List (DistributedMorphology.VocabularyItem Feature String)

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.

Instances For

def Embick2015.Korean.shape :

String → List Feature

The phonological shape of a stem, read off its exponent.

Equations

Embick2015.Korean.shape "pap" = [Embick2015.Korean.Feature.cFinal]
Embick2015.Korean.shape "ai" = [Embick2015.Korean.Feature.vFinal]
Embick2015.Korean.shape x✝ = []

Instances For

def Embick2015.Korean.word (r : String) :

DistributedMorphology.ComplexHead Feature String

Equations

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

Instances For

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

Option String

Equations

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

Instances For

def Embick2015.Korean.ofRow (ex : Data.Examples.LinguisticExample) :

Option (DistributedMorphology.ComplexHead Feature String × String)

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)

Instances For

def Embick2015.Korean.rows :

List (DistributedMorphology.ComplexHead Feature String × String)

Equations

Embick2015.Korean.rows = List.filterMap Embick2015.Korean.ofRow Embick2015.Examples.all

Instances For

theorem Embick2015.Korean.korean_rows (r : DistributedMorphology.ComplexHead Feature String × String) :

r ∈ rows → nominative r.1 = some r.2

Inward conditioning by the stem's phonology, visible through its exponent.