Jackendoff and Audring (2020): The Texture of the Lexicon

This file formalizes the Relational Morphology of [jackendoff-audring-2020], in which morphological motivation is shared structure recorded by nondirectional relational links between fully specified lexical entries, not inheritance from an abstract base. The mixed-direction pairs of Objection 10 to inheritance, Section 3.4.4, are the test: assassin and assassinate build the second on the first in phonology and the first on the second in semantics, so no acyclic inheritance hierarchy holds both demands (assassin_cycle), though default inheritance itself computes as the taxonomy of Figure 3.5 intends (ostrich_overrides), while a sister link with a coindex per shared part carries both, (41) (assassin_pairs), and reads the same transposed (assassin_pairs_symm). Bumped up a level, Section 4.8.2, the link between the -ism and -ist schemas, (47), pairs every ideology's noun with its adherent's, whatever the base and the ideology (ismist_pairs), the open-ended relation the book illustrates with Trumpism. Ablaut, Section 5.3, is a sister link off the syllabic nucleus: the general schema (25) pairs exactly the stems and pasts that are the same except at the nucleus (ablaut_pairs_iff), the sing/sang subschema (26) is a special case of it (ablaut_pairs_of_nucleusPair) whose pairs are nucleus contrasts (contrast_of_nucleusPair), and the German present-tense schema (45) has the same phonological shape. The cells (45) serves, the second and third singular present, are a morphome, Section 5.4.4: the syncretism class of the special stem of sprechen is a value conjunction of no feature of the paradigm (spricht_morphome). The Same Verb Problem, Section 5.6, is a shared morphosyntax-phonology pivot without a shared semantics: two lexemes selecting the same pivot inflect alike at every cell (realize_eq_of_sameVerb), which pairs the two draws of (60) and take with take part, (57) to (59), and separates the homophones ring and wring. Structural Intersection, Section 7.8.1, is the meet: the schema (6) is the intersection of its three sisters (5) (ishSchema_body_eq_inf), is the most they have in common (instantiates_ishSchema_iff), and absorbs a newly encountered sister (ishSchema_inf_foolish).

Implementation notes

• Lexical entries and schemas are slot-indexed descriptions over a flat carrier, a constant above ⊥ and a variable at ⊥; a relational coindex is a variable subscripting a slot of each entry, which a paired instantiation fills alike (ConstructionMorphology.Schema.InstantiatesAt). The containment of the semantics of assassinate in that of assassin, (41), is rendered as a shared slot.
• The zero exponence of the present and the infinitive of walk, (19), the double coindexation of Section 4.3, appears as a syncretism of the paradigm (walk_syncretism).
• The cycle theorem renders the paradox of Objection 10 through the well-foundedness of an inheritance hierarchy; the book argues from the above-and-below paradox and makes no well-foundedness claim.
• The syllables and the -ish adjectives are the CLDF forms of Data/Forms/JackendoffAudring2020.json, read as slot-indexed segments by Data.Forms.Form.slots; a syllable's positions are onset, nucleus and coda.
• The correspondence between a schema's variable coindices and the constant coindices of its instances, left unformalized in Section 4.13.2, is the subscripting of ConstructionMorphology.Schema.InstantiatesAt; a productive variable is one marked open over and above its attested fillers.

References

• [jackendoff-audring-2020]
• [booij-2010]
• [aronoff-1994]
• [spencer-2013]
• [albright-hayes-2003]

Open and closed variables, (17) and (18)

The toponym patterns (17): a name and the type of a geographical feature, the name an open variable and the feature type a closed one, whose fillers are learned pattern by pattern; in (18d) the and of are constants.

def JackendoffAudring2020.toponymA : ConstructionMorphology.Schema (Fin 2) (Flat String)

The pattern (18a), name then feature: the name open, the feature closed.

Equations

• JackendoffAudring2020.toponymA = { body := fun (x : Fin 2) => ⊥, opens := {0} }

def JackendoffAudring2020.toponymB : ConstructionMorphology.Schema (Fin 2) (Flat String)

The pattern (18b), feature then name.

Equations

• JackendoffAudring2020.toponymB = { body := fun (x : Fin 2) => ⊥, opens := {1} }

def JackendoffAudring2020.toponymD : ConstructionMorphology.Schema (Fin 4) (Flat String)

The pattern (18d), the feature of name: two constants, a closed feature, an open name.

Equations

• JackendoffAudring2020.toponymD = { body := ![↑"the", ⊥, ↑"of", ⊥], opens := {3} }

def JackendoffAudring2020.toponymsA : Set (Fin 2 → Flat String)

The stored toponyms of (17a).

Equations

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

def JackendoffAudring2020.toponymsB : Set (Fin 2 → Flat String)

The stored toponyms of (17b).

Equations

• JackendoffAudring2020.toponymsB = {JackendoffAudring2020.Forms.mountEverest.slots, JackendoffAudring2020.Forms.lakeMichigan.slots, JackendoffAudring2020.Forms.capeCod.slots}

def JackendoffAudring2020.toponymsD : Set (Fin 4 → Flat String)

The stored toponyms of (17d).

Equations

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

theorem JackendoffAudring2020.morrisMountain_generates : toponymA.Generates toponymsA Forms.morrisMountain.slots

Morris Mountain is licensed by (18a): the name is open and Mountain is attested.

theorem JackendoffAudring2020.mountMorris_generates : toponymB.Generates toponymsB Forms.mountMorris.slots

Mount Morris is licensed by (18b) likewise.

theorem JackendoffAudring2020.not_mountainMorris_generates : ¬toponymB.Generates toponymsB ![↑"Mountain", ↑"Morris"]

Mountain Morris is not: Mountain is not an attested feature of the pattern (18b).

theorem JackendoffAudring2020.not_mountOfHalle_generates : ¬toponymD.Generates toponymsD ![↑"the", ↑"Mount", ↑"of", ↑"Halle"]

The Mount of Halle is not licensed by (18d): Mount is not among its attested features.

Default inheritance and override, Figure 3.5

The taxonomy of Figure 3.5: birds fly by default, the ostrich overrides, and the canary inherits flight.

inductive JackendoffAudring2020.Animal : Type

The nodes of Figure 3.5.

• animal : Animal
• bird : Animal
• fish : Animal
• canary : Animal
• ostrich : Animal

@[instance_reducible]

instance JackendoffAudring2020.instDecidableEqAnimal : DecidableEq Animal

Equations

• JackendoffAudring2020.instDecidableEqAnimal x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

@[instance_reducible]

instance JackendoffAudring2020.instFintypeAnimal : Fintype Animal

Equations

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

def JackendoffAudring2020.animalHierarchy : ConstructionMorphology.Hierarchy Animal

The taxonomy: birds and fish are animals, canaries and ostriches are birds.

Equations

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

def JackendoffAudring2020.flies : Animal → Option Bool

Flight as a local specification: birds fly, the ostrich overrides.

Equations

• JackendoffAudring2020.flies JackendoffAudring2020.Animal.bird = some true
• JackendoffAudring2020.flies JackendoffAudring2020.Animal.ostrich = some false
• JackendoffAudring2020.flies x✝ = none

theorem JackendoffAudring2020.ostrich_overrides : animalHierarchy.value flies Animal.ostrich = some false ∧ animalHierarchy.value flies Animal.canary = some true

The ostrich's override and the canary's inheritance compute as intended.

Sister words

inductive JackendoffAudring2020.Part : Type

The parts of the entries (41): the shared phonology and the shared predicate MURDER, the person that assassin adds and the affix that assassinate adds.

• asasin : Part
• murder : Part
• person : Part
• ate : Part

@[instance_reducible]

instance JackendoffAudring2020.instDecidableEqPart : DecidableEq Part

Equations

• JackendoffAudring2020.instDecidableEqPart x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

inductive JackendoffAudring2020.AssassinVar : Type

The variables of (41): the phonology of assassin, which is the base of assassinate (coindex 2), the predicate MURDER of both (coindex 1), the person that assassin adds and the affix that assassinate adds.

• phon : AssassinVar
• murder : AssassinVar
• person : AssassinVar
• ate : AssassinVar

@[instance_reducible]

instance JackendoffAudring2020.instDecidableEqAssassinVar : DecidableEq AssassinVar

Equations

• JackendoffAudring2020.instDecidableEqAssassinVar x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

inductive JackendoffAudring2020.AssassinSlot : Type

The slots of assassin: its phonology, the predicate it contains, and the person.

• phon : AssassinSlot
• murder : AssassinSlot
• person : AssassinSlot

@[instance_reducible]

instance JackendoffAudring2020.instDecidableEqAssassinSlot : DecidableEq AssassinSlot

Equations

• JackendoffAudring2020.instDecidableEqAssassinSlot x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

inductive JackendoffAudring2020.AssassinateSlot : Type

The slots of assassinate: its base, its affix, and its predicate.

• base : AssassinateSlot
• affix : AssassinateSlot
• murder : AssassinateSlot

@[instance_reducible]

instance JackendoffAudring2020.instDecidableEqAssassinateSlot : DecidableEq AssassinateSlot

Equations

• JackendoffAudring2020.instDecidableEqAssassinateSlot x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

def JackendoffAudring2020.assassinPair : ConstructionMorphology.Schema AssassinVar (Flat Part)

The entries (41a) and (41b) with their coindices, as one fully specified description over the shared variables.

Equations

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

def JackendoffAudring2020.assassinSub : AssassinSlot → AssassinVar

The subscripting of the slots of assassin by the variables of (41).

Equations

• JackendoffAudring2020.assassinSub JackendoffAudring2020.AssassinSlot.phon = JackendoffAudring2020.AssassinVar.phon
• JackendoffAudring2020.assassinSub JackendoffAudring2020.AssassinSlot.murder = JackendoffAudring2020.AssassinVar.murder
• JackendoffAudring2020.assassinSub JackendoffAudring2020.AssassinSlot.person = JackendoffAudring2020.AssassinVar.person

def JackendoffAudring2020.assassinateSub : AssassinateSlot → AssassinVar

The subscripting of the slots of assassinate by the variables of (41).

Equations

• JackendoffAudring2020.assassinateSub JackendoffAudring2020.AssassinateSlot.base = JackendoffAudring2020.AssassinVar.phon
• JackendoffAudring2020.assassinateSub JackendoffAudring2020.AssassinateSlot.affix = JackendoffAudring2020.AssassinVar.ate
• JackendoffAudring2020.assassinateSub JackendoffAudring2020.AssassinateSlot.murder = JackendoffAudring2020.AssassinVar.murder

def JackendoffAudring2020.assassin : ConstructionMorphology.Schema AssassinSlot (Flat Part)

The entry (41a): the pair read at the slots of assassin.

Equations

• JackendoffAudring2020.assassin = JackendoffAudring2020.assassinPair.comap JackendoffAudring2020.assassinSub

def JackendoffAudring2020.assassinate : ConstructionMorphology.Schema AssassinateSlot (Flat Part)

The entry (41b): the pair read at the slots of assassinate.

Equations

• JackendoffAudring2020.assassinate = JackendoffAudring2020.assassinPair.comap JackendoffAudring2020.assassinateSub

theorem JackendoffAudring2020.assassin_pairs : assassinPair.InstantiatesAt (Sum.elim assassinSub assassinateSub) (Sum.elim assassin.body assassinate.body)

The two entries are a paired instantiation of (41): they share the base phonology and the predicate, and neither contains all of the other.

theorem JackendoffAudring2020.assassin_pairs_symm : assassinPair.InstantiatesAt (Sum.elim assassinateSub assassinSub) (Sum.elim assassinate.body assassin.body)

The link is nondirectional: neither word is derived from the other.

inductive JackendoffAudring2020.Pair : Type

The pair as nodes of an inheritance hierarchy.

• assassin : Pair
• assassinate : Pair

@[instance_reducible]

instance JackendoffAudring2020.instDecidableEqPair : DecidableEq Pair

Equations

• JackendoffAudring2020.instDecidableEqPair x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

theorem JackendoffAudring2020.assassin_cycle (h : ConstructionMorphology.Hierarchy Pair) (hphon : h.parent Pair.assassinate = some Pair.assassin) (hsem : h.parent Pair.assassin = some Pair.assassinate) : False

Objection 10: the phonology demands that assassinate inherit from assassin and the semantics that assassin inherit from assassinate; no acyclic hierarchy holds both.

Sister schemas

inductive JackendoffAudring2020.Atom (B : Type u_1) (I : Type u_2) : Type (max u_1 u_2)

The material of the schemas (47) over bases B and ideologies I: a base, an ideology, the two affixes, and the relation ADHERENT.

• base {B : Type u_1} {I : Type u_2} (b : B) : Atom B I
• ideology {B : Type u_1} {I : Type u_2} (i : I) : Atom B I
• ism {B : Type u_1} {I : Type u_2} : Atom B I
• ist {B : Type u_1} {I : Type u_2} : Atom B I
• adherent {B : Type u_1} {I : Type u_2} : Atom B I

inductive JackendoffAudring2020.IsmIstVar : Type

The variables of the schemas (47): the base X and the ideology, shared by the two schemas (coindices α and β), the two affixes and the relation ADHERENT.

• base : IsmIstVar
• ideology : IsmIstVar
• ism : IsmIstVar
• ist : IsmIstVar
• adherent : IsmIstVar

@[instance_reducible]

instance JackendoffAudring2020.instDecidableEqIsmIstVar : DecidableEq IsmIstVar

Equations

• JackendoffAudring2020.instDecidableEqIsmIstVar x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

inductive JackendoffAudring2020.IsmSlot : Type

The slots of the -ism schema: base, affix, semantics.

• base : IsmSlot
• affix : IsmSlot
• sem : IsmSlot

@[instance_reducible]

instance JackendoffAudring2020.instDecidableEqIsmSlot : DecidableEq IsmSlot

Equations

• JackendoffAudring2020.instDecidableEqIsmSlot x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

inductive JackendoffAudring2020.IstSlot : Type

The slots of the -ist schema: base, affix, the relation ADHERENT, and its ideology.

• base : IstSlot
• affix : IstSlot
• relation : IstSlot
• ideology : IstSlot

@[instance_reducible]

instance JackendoffAudring2020.instDecidableEqIstSlot : DecidableEq IstSlot

Equations

• JackendoffAudring2020.instDecidableEqIstSlot x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

def JackendoffAudring2020.ismist {B : Type u_1} {I : Type u_2} : ConstructionMorphology.Schema IsmIstVar (Flat (Atom B I))

(47): the -ism and -ist schemas with their coindices as one description, the affixes and ADHERENT pinned, the base and the ideology open.

Equations

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

def JackendoffAudring2020.ismSub : IsmSlot → IsmIstVar

The subscripting of the slots of the -ism schema by the variables of (47).

Equations

• JackendoffAudring2020.ismSub JackendoffAudring2020.IsmSlot.base = JackendoffAudring2020.IsmIstVar.base
• JackendoffAudring2020.ismSub JackendoffAudring2020.IsmSlot.affix = JackendoffAudring2020.IsmIstVar.ism
• JackendoffAudring2020.ismSub JackendoffAudring2020.IsmSlot.sem = JackendoffAudring2020.IsmIstVar.ideology

def JackendoffAudring2020.istSub : IstSlot → IsmIstVar

The subscripting of the slots of the -ist schema by the variables of (47).

Equations

• JackendoffAudring2020.istSub JackendoffAudring2020.IstSlot.base = JackendoffAudring2020.IsmIstVar.base
• JackendoffAudring2020.istSub JackendoffAudring2020.IstSlot.affix = JackendoffAudring2020.IsmIstVar.ist
• JackendoffAudring2020.istSub JackendoffAudring2020.IstSlot.relation = JackendoffAudring2020.IsmIstVar.adherent
• JackendoffAudring2020.istSub JackendoffAudring2020.IstSlot.ideology = JackendoffAudring2020.IsmIstVar.ideology

def JackendoffAudring2020.ismSchema {B : Type u_1} {I : Type u_2} : ConstructionMorphology.Schema IsmSlot (Flat (Atom B I))

(47a): the affix pinned to -ism, the base and the ideology open.

Equations

• JackendoffAudring2020.ismSchema = JackendoffAudring2020.ismist.comap JackendoffAudring2020.ismSub

def JackendoffAudring2020.istSchema {B : Type u_1} {I : Type u_2} : ConstructionMorphology.Schema IstSlot (Flat (Atom B I))

(47b): the affix pinned to -ist and the semantics to ADHERENT of an open ideology.

Equations

• JackendoffAudring2020.istSchema = JackendoffAudring2020.ismist.comap JackendoffAudring2020.istSub

def JackendoffAudring2020.ismWord {B : Type u_1} {I : Type u_2} (b : B) (i : I) : IsmSlot → Flat (Atom B I)

The -ism noun on base b denoting the ideology i.

Equations

• JackendoffAudring2020.ismWord b i JackendoffAudring2020.IsmSlot.base = ↑(JackendoffAudring2020.Atom.base b)
• JackendoffAudring2020.ismWord b i JackendoffAudring2020.IsmSlot.affix = ↑JackendoffAudring2020.Atom.ism
• JackendoffAudring2020.ismWord b i JackendoffAudring2020.IsmSlot.sem = ↑(JackendoffAudring2020.Atom.ideology i)

def JackendoffAudring2020.istWord {B : Type u_1} {I : Type u_2} (b : B) (i : I) : IstSlot → Flat (Atom B I)

The -ist noun on base b denoting an adherent of i.

Equations

• JackendoffAudring2020.istWord b i JackendoffAudring2020.IstSlot.base = ↑(JackendoffAudring2020.Atom.base b)
• JackendoffAudring2020.istWord b i JackendoffAudring2020.IstSlot.affix = ↑JackendoffAudring2020.Atom.ist
• JackendoffAudring2020.istWord b i JackendoffAudring2020.IstSlot.relation = ↑JackendoffAudring2020.Atom.adherent
• JackendoffAudring2020.istWord b i JackendoffAudring2020.IstSlot.ideology = ↑(JackendoffAudring2020.Atom.ideology i)

def JackendoffAudring2020.ismistWord {B : Type u_1} {I : Type u_2} (b : B) (i : I) : IsmIstVar → Flat (Atom B I)

The variables of (47) filled by the base b and the ideology i.

Equations

• JackendoffAudring2020.ismistWord b i JackendoffAudring2020.IsmIstVar.base = ↑(JackendoffAudring2020.Atom.base b)
• JackendoffAudring2020.ismistWord b i JackendoffAudring2020.IsmIstVar.ideology = ↑(JackendoffAudring2020.Atom.ideology i)
• JackendoffAudring2020.ismistWord b i JackendoffAudring2020.IsmIstVar.ism = ↑JackendoffAudring2020.Atom.ism
• JackendoffAudring2020.ismistWord b i JackendoffAudring2020.IsmIstVar.ist = ↑JackendoffAudring2020.Atom.ist
• JackendoffAudring2020.ismistWord b i JackendoffAudring2020.IsmIstVar.adherent = ↑JackendoffAudring2020.Atom.adherent

theorem JackendoffAudring2020.ismist_pairs {B : Type u_1} {I : Type u_2} (b : B) (i : I) : ismist.InstantiatesAt (Sum.elim ismSub istSub) (Sum.elim (ismWord b i) (istWord b i))

The relation is open-ended: for any base and any ideology, X-ism and X-ist are a paired instantiation of the sister schemas, Trumpism and Trumpist included.

Ablaut as a link off the nucleus

inductive JackendoffAudring2020.NucleusVar : Type

The variables of the ablaut schemas: the onset and the coda, shared by stem and past, and the two nuclei.

• onset : NucleusVar
• coda : NucleusVar
• stem : NucleusVar
• past : NucleusVar

@[instance_reducible]

instance JackendoffAudring2020.instDecidableEqNucleusVar : DecidableEq NucleusVar

Equations

• JackendoffAudring2020.instDecidableEqNucleusVar x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

def JackendoffAudring2020.stemSub : Fin 3 → NucleusVar

The subscripting of the stem's three positions, onset, nucleus and coda, by the variables of the ablaut schemas.

Equations

• JackendoffAudring2020.stemSub = ![JackendoffAudring2020.NucleusVar.onset, JackendoffAudring2020.NucleusVar.stem, JackendoffAudring2020.NucleusVar.coda]

def JackendoffAudring2020.pastSub : Fin 3 → NucleusVar

The subscripting of the past's positions by the variables of the ablaut schemas.

Equations

• JackendoffAudring2020.pastSub = ![JackendoffAudring2020.NucleusVar.onset, JackendoffAudring2020.NucleusVar.past, JackendoffAudring2020.NucleusVar.coda]

def JackendoffAudring2020.nucleusPair (v w : Flat String) : ConstructionMorphology.Schema NucleusVar (Flat String)

Two syllables linked at every position but the nucleus, whose description pins the nuclei v and w, ⊥ for an open nucleus: the shape of the ablaut schemas (25) and (26) and of the German present-tense schema (45).

Equations

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

def JackendoffAudring2020.ablaut : ConstructionMorphology.Schema NucleusVar (Flat String)

The general ablaut schema (25): both nuclei open.

Equations

• JackendoffAudring2020.ablaut = JackendoffAudring2020.nucleusPair ⊥ ⊥

def JackendoffAudring2020.singSang : ConstructionMorphology.Schema NucleusVar (Flat String)

The sing/sang subschema (26): /ɪ/ in the stem, /æ/ in the past.

Equations

• JackendoffAudring2020.singSang = JackendoffAudring2020.nucleusPair ↑"ɪ" ↑"æ"

def JackendoffAudring2020.stringStrung : ConstructionMorphology.Schema NucleusVar (Flat String)

The string/strung subschema, (26) with /ʌ/ for /æ/.

Equations

• JackendoffAudring2020.stringStrung = JackendoffAudring2020.nucleusPair ↑"ɪ" ↑"ʌ"

theorem JackendoffAudring2020.comap_stemSub_instantiates_iff {v w : Flat String} {s : Fin 3 → Flat String} : ((nucleusPair v w).comap stemSub).Instantiates s ↔ v ≤ s 1

A syllable instantiates a nucleus pair's stem side exactly when its nucleus is the pinned one.

theorem JackendoffAudring2020.comap_pastSub_instantiates_iff {v w : Flat String} {p : Fin 3 → Flat String} : ((nucleusPair v w).comap pastSub).Instantiates p ↔ w ≤ p 1

theorem JackendoffAudring2020.nucleusPair_iff {v w : Flat String} {s p : Fin 3 → Flat String} : (nucleusPair v w).InstantiatesAt (Sum.elim stemSub pastSub) (Sum.elim s p) ↔ v ≤ s 1 ∧ w ≤ p 1 ∧ Set.EqOn s p {1}ᶜ

A paired instantiation of a nucleus pair is a stem and a past that are the same except at the nucleus, with the pinned nuclei.

theorem JackendoffAudring2020.ablaut_pairs_iff {s p : Fin 3 → Flat String} : ablaut.InstantiatesAt (Sum.elim stemSub pastSub) (Sum.elim s p) ↔ Set.EqOn s p {1}ᶜ

(25) pairs exactly the stems and pasts that are the same except at the nucleus.

theorem JackendoffAudring2020.ablaut_pairs_of_nucleusPair {v w : Flat String} {s p : Fin 3 → Flat String} (h : (nucleusPair v w).InstantiatesAt (Sum.elim stemSub pastSub) (Sum.elim s p)) : ablaut.InstantiatesAt (Sum.elim stemSub pastSub) (Sum.elim s p)

A subschema with pinned nuclei is a special case of the general ablaut schema: every pair of (26) is a pair of (25).

theorem JackendoffAudring2020.contrast_of_nucleusPair {v w : String} (hvw : v ≠ w) {s p : Fin 3 → Flat String} (h : (nucleusPair ↑v ↑w).InstantiatesAt (Sum.elim stemSub pastSub) (Sum.elim s p)) : ConstructionMorphology.Contrast s p {1}

A pair under a subschema with distinct pinned nuclei is a nucleus contrast: the same except at the nucleus, where both are present and differ.

theorem JackendoffAudring2020.syllable_pairs (o v w c : String) : (nucleusPair ↑v ↑w).InstantiatesAt (Sum.elim stemSub pastSub) (Sum.elim ![↑o, ↑v, ↑c] ![↑o, ↑w, ↑c])

Two syllables differing only in their nucleus are a paired instantiation of the subschema pinning those nuclei.

theorem JackendoffAudring2020.ablaut_words : singSang.InstantiatesAt (Sum.elim stemSub pastSub) (Sum.elim Forms.sing.slots Forms.sang.slots) ∧ stringStrung.InstantiatesAt (Sum.elim stemSub pastSub) (Sum.elim Forms.string.slots Forms.strung.slots) ∧ ablaut.InstantiatesAt (Sum.elim stemSub pastSub) (Sum.elim Forms.sprech.slots Forms.sprich.slots)

sing/sang, (24), under (26); string/strung under its subschema; and the German sprech-/sprich- of (43) under the shape of (45).

The present-tense cells of (45) as a morphome

inductive JackendoffAudring2020.Person : Type

Person.

• first : Person
• second : Person
• third : Person

@[instance_reducible]

instance JackendoffAudring2020.instDecidableEqPerson : DecidableEq Person

Equations

• JackendoffAudring2020.instDecidableEqPerson x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

@[instance_reducible]

instance JackendoffAudring2020.instFintypePerson : Fintype Person

Equations

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

inductive JackendoffAudring2020.Number : Type

Number.

• sg : Number
• pl : Number

@[instance_reducible]

instance JackendoffAudring2020.instDecidableEqNumber : DecidableEq Number

Equations

• JackendoffAudring2020.instDecidableEqNumber x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

@[instance_reducible]

instance JackendoffAudring2020.instFintypeNumber : Fintype Number

Equations

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

@[reducible, inline]

abbrev JackendoffAudring2020.GCell : Type

The present-tense cells of the paradigm (41).

Equations

• JackendoffAudring2020.GCell = (JackendoffAudring2020.Person × JackendoffAudring2020.Number)

inductive JackendoffAudring2020.GStem : Type

The two present-tense stems of sprechen, (41) to (43).

• sprech : GStem
• sprich : GStem

@[instance_reducible]

instance JackendoffAudring2020.instDecidableEqGStem : DecidableEq GStem

Equations

• JackendoffAudring2020.instDecidableEqGStem x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

def JackendoffAudring2020.sprechen : GCell → GStem

The stem of each present-tense cell of sprechen, (41).

Equations

• JackendoffAudring2020.sprechen (JackendoffAudring2020.Person.second, JackendoffAudring2020.Number.sg) = JackendoffAudring2020.GStem.sprich
• JackendoffAudring2020.sprechen (JackendoffAudring2020.Person.third, JackendoffAudring2020.Number.sg) = JackendoffAudring2020.GStem.sprich
• JackendoffAudring2020.sprechen x✝ = JackendoffAudring2020.GStem.sprech

inductive JackendoffAudring2020.GFeature : Type

The features of the paradigm.

• person : GFeature
• number : GFeature

@[instance_reducible]

instance JackendoffAudring2020.instDecidableEqGFeature : DecidableEq GFeature

Equations

• JackendoffAudring2020.instDecidableEqGFeature x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

@[instance_reducible]

instance JackendoffAudring2020.instFintypeGFeature : Fintype GFeature

Equations

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

def JackendoffAudring2020.gFeatures : GFeature → Setoid GCell

The partitions the features induce.

Equations

• JackendoffAudring2020.gFeatures JackendoffAudring2020.GFeature.person = Setoid.ker Prod.fst
• JackendoffAudring2020.gFeatures JackendoffAudring2020.GFeature.number = Setoid.ker Prod.snd

@[instance_reducible]

instance JackendoffAudring2020.instDecidableRelGCellR (i : GFeature) : DecidableRel ⇑(gFeatures i)

Equations

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

def JackendoffAudring2020.specialCells : Finset GCell

The cells of the special stem: second and third singular.

Equations

• JackendoffAudring2020.specialCells = {(JackendoffAudring2020.Person.second, JackendoffAudring2020.Number.sg), (JackendoffAudring2020.Person.third, JackendoffAudring2020.Number.sg)}

theorem JackendoffAudring2020.sprechen_formCells : Morphology.formCells sprechen GStem.sprich = specialCells

theorem JackendoffAudring2020.specialCells_not_natural : ¬Morphology.IsValueConjunction gFeatures ↑specialCells

The special cells are a value conjunction of neither feature.

theorem JackendoffAudring2020.spricht_morphome : Morphology.IsMorphome sprechen (Morphology.IsValueConjunction gFeatures) ↑specialCells

The pattern (45) is morphomic, as the book says citing [aronoff-1994]: the cells the special stem serves are a syncretism class and no natural class of the paradigm.

The Same Verb Problem

inductive JackendoffAudring2020.Lexeme : Type

The lexemes of Section 5.6: main verb take and take part, (57) to (59); the two draws of (60) and withdraw, (62); and the homophones ring, wring and ring 'encircle'.

• take : Lexeme
• takePart : Lexeme
• drawPicture : Lexeme
• drawElicit : Lexeme
• withdraw : Lexeme
• ring : Lexeme
• wring : Lexeme
• ringCity : Lexeme

@[instance_reducible]

instance JackendoffAudring2020.instDecidableEqLexeme : DecidableEq Lexeme

Equations

• JackendoffAudring2020.instDecidableEqLexeme x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

@[instance_reducible]

instance JackendoffAudring2020.instFintypeLexeme : Fintype Lexeme

Equations

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

inductive JackendoffAudring2020.Pivot : Type

The morphosyntax-phonology pivots, one per relational coindex shared across lexemes.

• take : Pivot
• draw : Pivot
• ring : Pivot
• wring : Pivot
• ringCity : Pivot

@[instance_reducible]

instance JackendoffAudring2020.instDecidableEqPivot : DecidableEq Pivot

Equations

• JackendoffAudring2020.instDecidableEqPivot x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

@[instance_reducible]

instance JackendoffAudring2020.instFintypePivot : Fintype Pivot

Equations

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

inductive JackendoffAudring2020.Tense : Type

Tense.

• pres : Tense
• past : Tense

@[instance_reducible]

instance JackendoffAudring2020.instDecidableEqTense : DecidableEq Tense

Equations

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

@[instance_reducible]

instance JackendoffAudring2020.instFintypeTense : Fintype Tense

Equations

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

def JackendoffAudring2020.linkage : Morphology.Linkage Lexeme Pivot Tense

The paradigm linkage: each lexeme selects its pivot in every cell, with the cell's own property set.

Equations

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

def JackendoffAudring2020.SameVerb (l₁ l₂ : Lexeme) : Prop

Two lexemes are the same verb when they share their form correspondents at every cell: the relational coindex 23 of (60), a shared morphosyntax and phonology with no shared semantics.

Equations

• JackendoffAudring2020.SameVerb l₁ l₂ = ∀ (σ : JackendoffAudring2020.Tense), JackendoffAudring2020.linkage.corr l₁ σ = JackendoffAudring2020.linkage.corr l₂ σ

@[instance_reducible]

instance JackendoffAudring2020.instDecidableRelLexemeSameVerb : DecidableRel SameVerb

Equations

• JackendoffAudring2020.instDecidableRelLexemeSameVerb l₁ l₂ = JackendoffAudring2020.instDecidableRelLexemeSameVerb._aux_1 l₁ l₂

theorem JackendoffAudring2020.realize_eq_of_sameVerb {W : Type u_3} [DecidableEq W] (rf : Pivot → Tense → W) {l₁ l₂ : Lexeme} (h : SameVerb l₁ l₂) (σ : Tense) : linkage.realize rf l₁ σ = linkage.realize rf l₂ σ

Same verbs inflect alike at every cell, whatever their semantics: (57) to (61).

theorem JackendoffAudring2020.SameVerb.symm {l₁ l₂ : Lexeme} (h : SameVerb l₁ l₂) : SameVerb l₂ l₁

Sameness of verb is nondirectional: no use is the basic one, Section 3.6.

The regular paradigm

inductive JackendoffAudring2020.VCell : Type

The six cells of (16).

• pres : VCell
• pres3sg : VCell
• past : VCell
• inf : VCell
• prespt : VCell
• ptcp : VCell

@[instance_reducible]

instance JackendoffAudring2020.instDecidableEqVCell : DecidableEq VCell

Equations

• JackendoffAudring2020.instDecidableEqVCell x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

@[instance_reducible]

instance JackendoffAudring2020.instFintypeVCell : Fintype VCell

Equations

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

inductive JackendoffAudring2020.Exponent : Type

The exponents of the regular paradigm (19): none for the present and the infinitive, whose phonology is coindexed with the stem's.

• bare : Exponent
• s : Exponent
• t : Exponent
• ing : Exponent

@[instance_reducible]

instance JackendoffAudring2020.instDecidableEqExponent : DecidableEq Exponent

Equations

• JackendoffAudring2020.instDecidableEqExponent x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

def JackendoffAudring2020.walk : VCell → Exponent

The paradigm of walk, (19).

Equations

• JackendoffAudring2020.walk JackendoffAudring2020.VCell.pres = JackendoffAudring2020.Exponent.bare
• JackendoffAudring2020.walk JackendoffAudring2020.VCell.inf = JackendoffAudring2020.Exponent.bare
• JackendoffAudring2020.walk JackendoffAudring2020.VCell.pres3sg = JackendoffAudring2020.Exponent.s
• JackendoffAudring2020.walk JackendoffAudring2020.VCell.past = JackendoffAudring2020.Exponent.t
• JackendoffAudring2020.walk JackendoffAudring2020.VCell.ptcp = JackendoffAudring2020.Exponent.t
• JackendoffAudring2020.walk JackendoffAudring2020.VCell.prespt = JackendoffAudring2020.Exponent.ing

theorem JackendoffAudring2020.walk_syncretism : Morphology.formCells walk Exponent.bare = {VCell.pres, VCell.inf} ∧ Morphology.formCells walk Exponent.t = {VCell.past, VCell.ptcp}

The double coindexation of Section 4.3 as a syncretism: the present and the infinitive share the stem's phonology, and the past the past participle's.

Structural Intersection

def JackendoffAudring2020.ishSchema : ConstructionMorphology.Schema (Fin 2) (Flat String)

The schema (6) over the two slots of an -ish adjective, base and affix: the affix pinned, the base a variable.

Equations

• JackendoffAudring2020.ishSchema = ConstructionMorphology.Schema.productive ![⊥, ↑"ish"]

theorem JackendoffAudring2020.ishSchema_body_eq_inf : ishSchema.body = Forms.piggish.slots ⊓ Forms.childish.slots ⊓ Forms.sluggish.slots

Structural Intersection constructs the schema: the description of (6) is the meet of the three sisters of (5), keeping what they share and leaving a variable where they differ.

theorem JackendoffAudring2020.instantiates_ishSchema_iff {s : ConstructionMorphology.Schema (Fin 2) (Flat String)} : s.Instantiates ishSchema.body ↔ s.Instantiates Forms.piggish.slots ∧ s.Instantiates Forms.childish.slots ∧ s.Instantiates Forms.sluggish.slots

The schema is the most the sisters have in common: a description is instantiated by all three exactly when it is instantiated by the schema's description.

theorem JackendoffAudring2020.ishSchema_le_foolish : ishSchema.body ≤ Forms.foolish.slots

theorem JackendoffAudring2020.ishSchema_inf_foolish : ishSchema.body ⊓ Forms.foolish.slots = ishSchema.body

A newly encountered sister intersected with the schema yields the schema again, the Minimal Generalization Learner's fixed point.