Hayes (1989): Compensatory Lengthening in Moraic Phonology

This file formalizes the moraic theory of compensatory lengthening (CL) of [Hay89]: a syllabification that gives vowels their moras underlyingly and coda consonants theirs by the language-particular rule of Weight by Position, deletion on the segmental tier only, Parasitic Delinking, and CL as the filling of a stranded mora by a language-particular convention, all under the ban on crossing association lines. The typological argument of the paper's §5 is derived from the representations: cl_delete_of_isOnset is the onset-deletion asymmetry (an onset projects no mora, so its loss strands nothing, and Moraic Conservation holds by construction), NoCrossing.cl says that filling from the nearest linked segment never crosses a line, and not_noCrossing_link_of_onset is the vowel-loss asymmetry (the vowel to the right of a stranded mora lies outside the mora's Autosegmental.window, past that syllable's onset line). The seven CL types of the typology, the weight prerequisite of §6, and the two-mora limit and trimoraic syllables of §7 are run as derivations on the paper's forms.

Implementation notes

A Form places every prosodic node at the timeline slot of the segment that projected it, so the syllable, mora, and segmental tiers share one order and the lines a syllable node draws directly to its onset consonants can cross the lines of a mora; Autosegmental.IsNonCrossing on the node-to-segment lines is then the ban on crossing association lines as (66) and (68) use it. The melody alphabet Seg is schematic, as the paper's forms are: segment features play no role in the argument. Intervocalic clusters divide after their first consonant; every form below has a one-consonant onset, so the language-particular division principles of §2.1 are not needed. A CL convention takes the nearest linked segment on its side; the vowel-only restriction of (17b) and the sonority-graded Degemination (41) of Ilokano are not modelled.

TODO

• The cluster cases of (27d), where Stray Erasure removes the unsyllabifiable half of the geminate, and Degemination (41).
• The X-theory derivations of §3.1, §4, and §5.3 that the moraic account is compared against.

References

• [Hay89]
• [Hym85]
• [Ito86]
• [Ste82]

Prosodic nodes

inductive Hayes1989.Tier : Type

The prosodic tiers above the melody.

• syl : Tier
• mora : Tier

@[instance_reducible]

instance Hayes1989.instDecidableEqTier : DecidableEq Tier

Equations

• Hayes1989.instDecidableEqTier x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

@[instance_reducible]

instance Hayes1989.instReprTier : Repr Tier

Equations

• Hayes1989.instReprTier = { reprPrec := Hayes1989.instReprTier.repr }

def Hayes1989.instReprTier.repr : Tier → ℕ → Std.Format

Equations

• Hayes1989.instReprTier.repr Hayes1989.Tier.syl prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Hayes1989.Tier.syl")).group prec✝
• Hayes1989.instReprTier.repr Hayes1989.Tier.mora prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Hayes1989.Tier.mora")).group prec✝

structure Hayes1989.Node : Type

A prosodic node records its tier and the timeline slot of the segment that projected it, the nucleus for a syllable node and the mora-bearing segment for a mora; idx tells apart the two morae of one long vowel ((3a)).

• tier : Tier
• slot : ℕ
• idx : ℕ

def Hayes1989.instDecidableEqNode.decEq (x✝ x✝¹ : Node) : Decidable (x✝ = x✝¹)

Equations

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

@[instance_reducible]

instance Hayes1989.instDecidableEqNode : DecidableEq Node

Equations

• Hayes1989.instDecidableEqNode = Hayes1989.instDecidableEqNode.decEq

def Hayes1989.instReprNode.repr : Node → ℕ → Std.Format

Equations

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

@[instance_reducible]

instance Hayes1989.instReprNode : Repr Node

Equations

• Hayes1989.instReprNode = { reprPrec := Hayes1989.instReprNode.repr }

@[reducible, inline]

abbrev Hayes1989.Node.σ (v : ℕ) : Node

The syllable node over the nucleus at slot v.

Equations

• Hayes1989.Node.σ v = { tier := Hayes1989.Tier.syl, slot := v }

@[reducible, inline]

abbrev Hayes1989.Node.μ (i : ℕ) (k : ℕ := 0) : Node

The k-th mora projected from slot i.

Equations

• Hayes1989.Node.μ i k = { tier := Hayes1989.Tier.mora, slot := i, idx := k }

@[instance_reducible]

instance Hayes1989.Node.instPreorder : Preorder Node

Nodes are ordered by slot: the order in which association lines are drawn.

Equations

• Hayes1989.Node.instPreorder = Preorder.lift Hayes1989.Node.slot

@[instance_reducible]

instance Hayes1989.Node.instDecidableLT : DecidableLT Node

Equations

• a.instDecidableLT b = { decide := a.slot.succ.ble b.slot, reflects_decide := ⋯ }

@[instance_reducible]

instance Hayes1989.Node.instDecidableLE : DecidableLE Node

Equations

• a.instDecidableLE b = { decide := a.slot.ble b.slot, reflects_decide := ⋯ }

Forms

structure Hayes1989.Form (α : Type u_1) : Type u_1

A moraic representation over a melody, in which segment i occupies timeline slot i.

• melody : List α

  The segmental tier.

• nodes : Finset Node

  The prosodic nodes present: a syllable deleted by Parasitic Delinking is gone, a stranded mora survives.

• dom : Finset (Node × Node)

  Domination of morae by syllable nodes.

• links : Finset (Node × ℕ)

  Association lines run to the melody, from a syllable node to its onset consonants and from a mora to the segments it dominates.

def Hayes1989.Form.NoCrossing {α : Type u_1} (f : Form α) : Prop

The ban on crossing association lines, on both layers.

Equations

• f.NoCrossing = (Autosegmental.IsNonCrossing f.links ∧ Autosegmental.IsNonCrossing f.dom)

@[instance_reducible]

instance Hayes1989.Form.instDecidableNoCrossing {α : Type u_1} (f : Form α) : Decidable f.NoCrossing

Equations

• f.instDecidableNoCrossing = id inferInstance

def Hayes1989.Form.span {α : Type u_1} (f : Form α) (n : Node) : Finset ℕ

The slots node n is associated to.

Equations

• f.span n = Finset.image (fun (x : Hayes1989.Node × ℕ) => x.2) ({x ∈ f.links | x.1 = n})

def Hayes1989.Form.morae {α : Type u_1} (f : Form α) (s : Node) : Finset Node

The morae of syllable node s.

Equations

• f.morae s = Finset.image (fun (x : Hayes1989.Node × Hayes1989.Node) => x.2) ({x ∈ f.dom | x.1 = s})

def Hayes1989.Form.weight {α : Type u_1} (f : Form α) (s : Node) : ℕ

Syllable weight is the number of morae.

Equations

• f.weight s = (f.morae s).card

def Hayes1989.Form.nuclear {α : Type u_1} (f : Form α) (s : Node) : Finset ℕ

The nuclear segments of syllable node s: the slots its morae dominate.

Equations

• f.nuclear s = (f.morae s).biUnion f.span

def Hayes1989.Form.length {α : Type u_1} (f : Form α) (i : ℕ) : ℕ

The number of association lines at slot i: one for a short segment, two for a long vowel ((3a)) or a geminate ((9a)).

Equations

• f.length i = {x ∈ f.links | x.2 = i}.card

def Hayes1989.Form.stranded {α : Type u_1} (f : Form α) : Finset Node

The morae stranded by a deletion on the segmental tier are those dominating nothing.

Equations

• f.stranded = {n ∈ f.nodes | n.tier = Hayes1989.Tier.mora ∧ f.span n = ∅}

def Hayes1989.Form.free {α : Type u_1} (f : Form α) : Finset Node

Morae no syllable node dominates.

Equations

• f.free = {n ∈ f.nodes | n.tier = Hayes1989.Tier.mora ∧ n ∉ Finset.image (fun (x : Hayes1989.Node × Hayes1989.Node) => x.2) f.dom}

def Hayes1989.Form.moraCount {α : Type u_1} (f : Form α) : ℕ

The mora count of the form.

Equations

• f.moraCount = {x ∈ f.nodes | x.tier = Hayes1989.Tier.mora}.card

def Hayes1989.Form.surface {α : Type u_1} (f : Form α) : List (α × ℕ)

The surface string after Stray Erasure pairs each linked segment with its number of lines.

Equations

• f.surface = List.filterMap (fun (p : α × ℕ) => if 0 < f.length p.2 then some (p.1, f.length p.2) else none) f.melody.zipIdx

Operations

def Hayes1989.Form.delete {α : Type u_1} (f : Form α) (i : ℕ) : Form α

Deletion on the segmental tier only ((17a)): slot i loses every association line, and a mora that dominated it alone is stranded.

Equations

• f.delete i = { melody := f.melody, nodes := f.nodes, dom := f.dom, links := {x ∈ f.links | x.2 ≠ i} }

def Hayes1989.Form.delink {α : Type u_1} (f : Form α) (n : Node) (i : ℕ) : Form α

delink erases one association line, as Glide Formation (37) disassociates a vowel from its mora.

Equations

• f.delink n i = { melody := f.melody, nodes := f.nodes, dom := f.dom, links := f.links.erase (n, i) }

def Hayes1989.Form.link {α : Type u_1} (f : Form α) (n : Node) (i : ℕ) : Form α

link draws one association line, for spreading onto a stranded mora or adjunction of a stray segment.

Equations

• f.link n i = { melody := f.melody, nodes := f.nodes, dom := f.dom, links := insert (n, i) f.links }

def Hayes1989.Form.parasitic {α : Type u_1} (f : Form α) : Form α

Parasitic Delinking (23): a syllable node with no nuclear segment is deleted with its lines; its morae survive, now free.

Equations

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

def Hayes1989.Form.adjoin {α : Type u_1} (f : Form α) : Form α

Prosodic Licensing ([Ito86]): a free mora adjoins the nearest syllable node to its left.

Equations

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

inductive Hayes1989.Form.Convention : Type

A language's CL convention ((17b), (25a), (40a)): fill a stranded mora from the nearest segment linked to a node on its left, or on its right.

• fromLeft : Convention
• fromRight : Convention

@[instance_reducible]

instance Hayes1989.Form.instDecidableEqConvention : DecidableEq Convention

Equations

• Hayes1989.Form.instDecidableEqConvention x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

def Hayes1989.Form.instReprConvention.repr : Convention → ℕ → Std.Format

Equations

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

@[instance_reducible]

instance Hayes1989.Form.instReprConvention : Repr Convention

Equations

• Hayes1989.Form.instReprConvention = { reprPrec := Hayes1989.Form.instReprConvention.repr }

def Hayes1989.Form.fills {α : Type u_1} (f : Form α) : Convention → Finset (Node × ℕ)

fills is the set of lines CL draws, from each stranded mora to the nearest segment linked on the convention's side, the endpoint of the mora's window.

Equations

• f.fills Hayes1989.Form.Convention.fromLeft = f.stranded.biUnion fun (m : Hayes1989.Node) => WithBot.recBotCoe ∅ (fun (j : ℕ) => {(m, j)}) (Autosegmental.leftBound f.links m)
• f.fills Hayes1989.Form.Convention.fromRight = f.stranded.biUnion fun (m : Hayes1989.Node) => WithTop.recTopCoe ∅ (fun (j : ℕ) => {(m, j)}) (Autosegmental.rightBound f.links m)

def Hayes1989.Form.cl {α : Type u_1} (f : Form α) (c : Convention) : Form α

Compensatory lengthening fills every stranded mora with the convention's segment; a mora with none stays stranded, for Stray Erasure.

Equations

• f.cl c = { melody := f.melody, nodes := f.nodes, dom := f.dom, links := f.links ∪ f.fills c }

Moraic Conservation (64)

No operation but Stray Erasure touches the mora tier, so CL conserves mora count by construction.

@[simp]

theorem Hayes1989.Form.moraCount_delete {α : Type u_1} (f : Form α) (i : ℕ) : (f.delete i).moraCount = f.moraCount

@[simp]

theorem Hayes1989.Form.moraCount_delink {α : Type u_1} (f : Form α) (n : Node) (i : ℕ) : (f.delink n i).moraCount = f.moraCount

@[simp]

theorem Hayes1989.Form.moraCount_link {α : Type u_1} (f : Form α) (n : Node) (i : ℕ) : (f.link n i).moraCount = f.moraCount

@[simp]

theorem Hayes1989.Form.moraCount_adjoin {α : Type u_1} (f : Form α) : f.adjoin.moraCount = f.moraCount

@[simp]

theorem Hayes1989.Form.moraCount_cl {α : Type u_1} (f : Form α) (c : Convention) : (f.cl c).moraCount = f.moraCount

@[simp]

theorem Hayes1989.Form.moraCount_parasitic {α : Type u_1} (f : Form α) : f.parasitic.moraCount = f.moraCount

@[simp]

theorem Hayes1989.Form.nodes_delete {α : Type u_1} (f : Form α) (i : ℕ) : (f.delete i).nodes = f.nodes

Stranding

def Hayes1989.Form.IsOnset {α : Type u_1} (f : Form α) (i : ℕ) : Prop

Slot i is an onset: linked from syllable nodes only, so it projects no mora.

Equations

• f.IsOnset i = ∀ p ∈ f.links, p.2 = i → p.1.tier = Hayes1989.Tier.syl

@[instance_reducible]

instance Hayes1989.Form.instDecidableIsOnset {α : Type u_1} (f : Form α) (i : ℕ) : Decidable (f.IsOnset i)

Equations

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

theorem Hayes1989.Form.span_delete {α : Type u_1} (f : Form α) (n : Node) (i : ℕ) : (f.delete i).span n = (f.span n).erase i

theorem Hayes1989.Form.stranded_delete {α : Type u_1} (f : Form α) (i : ℕ) : (f.delete i).stranded = f.stranded ∪ {n ∈ f.nodes | n.tier = Tier.mora ∧ f.span n = {i}}

Deleting slot i strands exactly the morae whose only segment was at i.

theorem Hayes1989.Form.stranded_delete_of_isOnset {α : Type u_1} (f : Form α) {i : ℕ} (h : f.IsOnset i) : (f.delete i).stranded = f.stranded

The onset-deletion asymmetry (§5.3.1): an onset bears no mora, so deleting it strands nothing.

theorem Hayes1989.Form.cl_eq_self {α : Type u_1} (f : Form α) (h : f.stranded = ∅) (c : Convention) : f.cl c = f

A form with no stranded mora is untouched by CL.

theorem Hayes1989.Form.cl_delete_of_isOnset {α : Type u_1} (f : Form α) {i : ℕ} (h : f.IsOnset i) (h₀ : f.stranded = ∅) (c : Convention) : (f.delete i).cl c = f.delete i

CL from onset deletion is impossible ((57), (63)): with nothing stranded, the convention finds nothing to fill, and the mora count could only grow by a mora the representation does not provide.

Crossing

Removing lines keeps a form free of crossing lines, and so does CL, which links each stranded mora to the endpoint of its window, the nearest segment linked on the convention's side. Only link can cross, and noCrossing_link_iff says exactly when.

theorem Hayes1989.Form.NoCrossing.delete {α : Type u_1} {f : Form α} (h : f.NoCrossing) (i : ℕ) : (f.delete i).NoCrossing

theorem Hayes1989.Form.NoCrossing.delink {α : Type u_1} {f : Form α} (h : f.NoCrossing) (n : Node) (i : ℕ) : (f.delink n i).NoCrossing

theorem Hayes1989.Form.NoCrossing.parasitic {α : Type u_1} {f : Form α} (h : f.NoCrossing) : f.parasitic.NoCrossing

theorem Hayes1989.Form.mem_fills_fromLeft {α : Type u_1} {f : Form α} {p : Node × ℕ} : p ∈ f.fills Convention.fromLeft ↔ p.1 ∈ f.stranded ∧ Autosegmental.leftBound f.links p.1 = ↑p.2

theorem Hayes1989.Form.mem_fills_fromRight {α : Type u_1} {f : Form α} {p : Node × ℕ} : p ∈ f.fills Convention.fromRight ↔ p.1 ∈ f.stranded ∧ Autosegmental.rightBound f.links p.1 = ↑p.2

theorem Hayes1989.Form.NoCrossing.cl {α : Type u_1} {f : Form α} (h : f.NoCrossing) (c : Convention) : (f.cl c).NoCrossing

The lines CL draws from stranded morae to the nearest segment on one side cross neither one another nor the lines of a form without crossings.

theorem Hayes1989.Form.noCrossing_link_iff {α : Type u_1} {f : Form α} {m : Node} {i : ℕ} : (f.link m i).NoCrossing ↔ f.NoCrossing ∧ i ∈ Autosegmental.window f.links m

Drawing a line keeps a form free of crossings iff its slot lies in the node's window.

theorem Hayes1989.Form.not_noCrossing_link_of_onset {α : Type u_1} {f : Form α} {m : Node} {v c : ℕ} (hc : (Node.σ v, c) ∈ f.links) (hm : m.slot < v) (hcv : c < v) : ¬(f.link m v).NoCrossing

A stranded mora to the left of a syllable cannot lengthen its nucleus v, which lies past its window because the onset consonant c is linked from the syllable node to its right (§5.3.2, (61) and (66)). Rightward CL through vowel loss is unattested.

theorem Hayes1989.Form.not_noCrossing_link_of_coda {α : Type u_1} {f : Form α} {m : Node} {v c : ℕ} (hc : (Node.μ c, c) ∈ f.links) (hv : v < c) (hm : c < m.slot) : ¬(f.link m v).NoCrossing

(68): a moraic coda c between the nucleus v and a stranded mora to its right puts v before the mora's window, so vowel-loss CL favours open syllables.

Syllabification (§2.1)

An underlying form lists each segment with its mora count ((3)–(7)): none for a consonant or glide, one for a short vowel, two for a long vowel. Moraic segments are nuclei; a consonant adjoins as onset to the following nucleus when prevocalic and otherwise as coda to the preceding one; Weight by Position (10) gives a coda its own mora while the syllable is below the language's mora limit, and a later coda rides the syllable's last mora (§7, (73)).

@[reducible, inline]

abbrev Hayes1989.Underlying (α : Type u_1) : Type u_1

An underlying form lists segments with their mora counts.

Equations

• Hayes1989.Underlying α = List (α × ℕ)

def Hayes1989.Underlying.morae {α : Type u_1} (u : Underlying α) (i : ℕ) : ℕ

The underlying mora count at slot i.

Equations

• u.morae i = (Option.map Prod.snd u[i]?).getD 0

def Hayes1989.Underlying.nuclei {α : Type u_1} (u : Underlying α) : List ℕ

The nucleus slots.

Equations

• u.nuclei = List.filter (fun (i : ℕ) => decide (0 < u.morae i)) (List.range (List.length u))

def Hayes1989.Underlying.host {α : Type u_1} (u : Underlying α) (i : ℕ) : Option ℕ

host i is the nucleus of the syllable slot i belongs to: its own if moraic, the following one if the slot is the consonant right before it, and the preceding one otherwise.

Equations

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

def Hayes1989.Underlying.onsetHost {α : Type u_1} (u : Underlying α) (c : ℕ) : Option ℕ

The nucleus slot c is an onset consonant of, if any.

Equations

• u.onsetHost c = (u.host c).bind fun (v : ℕ) => if c < v then some v else none

def Hayes1989.Underlying.codaHost {α : Type u_1} (u : Underlying α) (c : ℕ) : Option ℕ

The nucleus slot c is a coda consonant of, if any.

Equations

• u.codaHost c = (u.host c).bind fun (v : ℕ) => if v < c then some v else none

def Hayes1989.Underlying.codaRank {α : Type u_1} (u : Underlying α) (c : ℕ) : ℕ

The number of coda consonants of the same syllable before c.

Equations

• u.codaRank c = (List.filter (fun (c' : ℕ) => decide (u.codaHost c' = u.codaHost c)) (List.range c)).length

def Hayes1989.Underlying.Projects {α : Type u_1} (u : Underlying α) (wbp : Bool) (limit v c : ℕ) : Prop

Weight by Position (10) gives coda c of the syllable at v its own mora: the language has the rule and the syllable is still below its mora limit.

Equations

• u.Projects wbp limit v c = (wbp = true ∧ u.morae v + u.codaRank c < limit)

@[instance_reducible]

instance Hayes1989.Underlying.instDecidableProjects {α : Type u_1} (u : Underlying α) (wbp : Bool) (limit v c : ℕ) : Decidable (u.Projects wbp limit v c)

Equations

• u.instDecidableProjects wbp limit v c = id inferInstance

def Hayes1989.Underlying.codaMora {α : Type u_1} (u : Underlying α) (wbp : Bool) (limit v c : ℕ) : Node

The mora dominating coda c of the syllable at v: its own under Weight by Position, else the syllable's last mora so far.

Equations

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

def Hayes1989.Underlying.onsets {α : Type u_1} (u : Underlying α) : List (Node × ℕ)

The onset lines.

Equations

• u.onsets = List.filterMap (fun (c : ℕ) => Option.map (fun (v : ℕ) => (Hayes1989.Node.σ v, c)) (u.onsetHost c)) (List.range (List.length u))

def Hayes1989.Underlying.codas {α : Type u_1} (u : Underlying α) : List (ℕ × ℕ)

The coda consonants with their syllables.

Equations

• u.codas = List.filterMap (fun (c : ℕ) => Option.map (fun (v : ℕ) => (v, c)) (u.codaHost c)) (List.range (List.length u))

def Hayes1989.Underlying.syllabify {α : Type u_1} (u : Underlying α) (wbp : Bool) (limit : ℕ := 2) : Form α

Syllabification projects syllable nodes from nuclei over their morae, adjoins onsets to the syllable node and codas to a mora, with Weight by Position for a language that has it (wbp) up to its mora limit (two by default, §7).

Equations

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

The forms of the paper

inductive Hayes1989.Seg : Type

The schematic melody alphabet of the paper's forms.

• a : Seg
• e : Seg
• i : Seg
• o : Seg
• u : Seg
• schwa : Seg
• b : Seg
• d : Seg
• g : Seg
• k : Seg
• l : Seg
• m : Seg
• n : Seg
• p : Seg
• r : Seg
• s : Seg
• t : Seg
• v : Seg
• w : Seg
• x : Seg
• θ : Seg
• ng : Seg

@[instance_reducible]

instance Hayes1989.instDecidableEqSeg : DecidableEq Seg

Equations

• Hayes1989.instDecidableEqSeg x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

def Hayes1989.instReprSeg.repr : Seg → ℕ → Std.Format

Equations

• Hayes1989.instReprSeg.repr Hayes1989.Seg.a prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Hayes1989.Seg.a")).group prec✝
• Hayes1989.instReprSeg.repr Hayes1989.Seg.e prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Hayes1989.Seg.e")).group prec✝
• Hayes1989.instReprSeg.repr Hayes1989.Seg.i prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Hayes1989.Seg.i")).group prec✝
• Hayes1989.instReprSeg.repr Hayes1989.Seg.o prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Hayes1989.Seg.o")).group prec✝
• Hayes1989.instReprSeg.repr Hayes1989.Seg.u prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Hayes1989.Seg.u")).group prec✝
• Hayes1989.instReprSeg.repr Hayes1989.Seg.schwa prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Hayes1989.Seg.schwa")).group prec✝
• Hayes1989.instReprSeg.repr Hayes1989.Seg.b prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Hayes1989.Seg.b")).group prec✝
• Hayes1989.instReprSeg.repr Hayes1989.Seg.d prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Hayes1989.Seg.d")).group prec✝
• Hayes1989.instReprSeg.repr Hayes1989.Seg.g prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Hayes1989.Seg.g")).group prec✝
• Hayes1989.instReprSeg.repr Hayes1989.Seg.k prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Hayes1989.Seg.k")).group prec✝
• Hayes1989.instReprSeg.repr Hayes1989.Seg.l prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Hayes1989.Seg.l")).group prec✝
• Hayes1989.instReprSeg.repr Hayes1989.Seg.m prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Hayes1989.Seg.m")).group prec✝
• Hayes1989.instReprSeg.repr Hayes1989.Seg.n prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Hayes1989.Seg.n")).group prec✝
• Hayes1989.instReprSeg.repr Hayes1989.Seg.p prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Hayes1989.Seg.p")).group prec✝
• Hayes1989.instReprSeg.repr Hayes1989.Seg.r prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Hayes1989.Seg.r")).group prec✝
• Hayes1989.instReprSeg.repr Hayes1989.Seg.s prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Hayes1989.Seg.s")).group prec✝
• Hayes1989.instReprSeg.repr Hayes1989.Seg.t prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Hayes1989.Seg.t")).group prec✝
• Hayes1989.instReprSeg.repr Hayes1989.Seg.v prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Hayes1989.Seg.v")).group prec✝
• Hayes1989.instReprSeg.repr Hayes1989.Seg.w prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Hayes1989.Seg.w")).group prec✝
• Hayes1989.instReprSeg.repr Hayes1989.Seg.x prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Hayes1989.Seg.x")).group prec✝
• Hayes1989.instReprSeg.repr Hayes1989.Seg.θ prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Hayes1989.Seg.θ")).group prec✝
• Hayes1989.instReprSeg.repr Hayes1989.Seg.ng prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Hayes1989.Seg.ng")).group prec✝

@[instance_reducible]

instance Hayes1989.instReprSeg : Repr Seg

Equations

• Hayes1989.instReprSeg = { reprPrec := Hayes1989.instReprSeg.repr }

@[reducible, inline]

abbrev Hayes1989.V (seg : Seg) : Seg × ℕ

A short vowel.

Equations

• Hayes1989.V seg = (seg, 1)

@[reducible, inline]

abbrev Hayes1989.VV (seg : Seg) : Seg × ℕ

A long vowel ((3a)).

Equations

• Hayes1989.VV seg = (seg, 2)

@[reducible, inline]

abbrev Hayes1989.C (seg : Seg) : Seg × ℕ

A consonant or glide ((4), (5)).

Equations

• Hayes1989.C seg = (seg, 0)

Classical CL: Latin (12), (17)

def Hayes1989.kasnus : Form Seg

Latin kasnus 'gray' ((12b)), CVC heavy.

Equations

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

theorem Hayes1989.kasnus_stranded : (kasnus.delete 2).stranded = {Node.μ 2}

s deletes before an anterior sonorant on the segmental tier only ((17a)), stranding the coda mora.

def Hayes1989.kaanus : Form Seg

(17c): the stranded mora is filled by spreading from the left.

Equations

• Hayes1989.kaanus = (Hayes1989.kasnus.delete 2).cl Hayes1989.Form.Convention.fromLeft

theorem Hayes1989.kaanus_noCrossing : kaanus.NoCrossing

theorem Hayes1989.kaanus_surface : kaanus.surface = [(Seg.k, 1), (Seg.a, 2), (Seg.n, 1), (Seg.u, 1), (Seg.s, 1)]

theorem Hayes1989.kaanus_moraCount : kaanus.moraCount = kasnus.moraCount

Moraic Conservation (64) on the derivation.

Onset deletion: Latin (14), (18) and Turkish

def Hayes1989.smereo : Form Seg

Latin smereō 'deserve' ((14)): word-initial s is an onset.

Equations

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

theorem Hayes1989.mereo_no_cl : (smereo.delete 0).cl Form.Convention.fromLeft = smereo.delete 0

As in (18) for snurus, deleting the onset s strands nothing, so the convention has nothing to fill.

def Hayes1989.savmak : Form Seg

Turkish savmak 'to get rid of' (§5.2.1, after Sezer 1986): coda v deletes with CL.

Equations

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

theorem Hayes1989.saamak_surface : ((savmak.delete 2).cl Form.Convention.fromLeft).surface = [(Seg.s, 1), (Seg.a, 2), (Seg.m, 1), (Seg.a, 1), (Seg.k, 1)]

def Hayes1989.davul : Form Seg

Turkish davul 'drum': onset v deletes without CL, [daul] and not *[daːul].

Equations

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

theorem Hayes1989.daul_no_cl : (davul.delete 2).cl Form.Convention.fromLeft = davul.delete 2

Double flop: Ancient Greek (19), (21)

def Hayes1989.odwos : Form Seg

East Ionic odwos 'threshold' ((19)): d is a moraic coda, w the next onset.

Equations

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

def Hayes1989.odwos_flop : Form Seg

Deleting the onset w strands nothing; the d then resyllabifies as the onset of the following syllable, and only that strands its mora ((21)).

Equations

• Hayes1989.odwos_flop = ((Hayes1989.odwos.delete 2).delink (Hayes1989.Node.μ 1) 1).link (Hayes1989.Node.σ 3) 1

theorem Hayes1989.odwos_delete_stranded : (odwos.delete 2).stranded = ∅

theorem Hayes1989.odwos_flop_stranded : odwos_flop.stranded = {Node.μ 1}

theorem Hayes1989.oodos_surface : (odwos_flop.cl Form.Convention.fromLeft).surface = [(Seg.o, 2), (Seg.d, 1), (Seg.o, 1), (Seg.s, 1)]

In nonlocal CL the vowel that lengthens is not adjacent to the consonant that deleted.

theorem Hayes1989.oodos_noCrossing : (odwos_flop.cl Form.Convention.fromLeft).NoCrossing

Vowel loss: Middle English (24)–(26) and the asymmetry (61), (66), (68)

def Hayes1989.tale : Form Seg

Middle English tale 'tale' (Minkova 1982).

Equations

• Hayes1989.tale = Hayes1989.Underlying.syllabify [Hayes1989.C Hayes1989.Seg.t, Hayes1989.V Hayes1989.Seg.a, Hayes1989.C Hayes1989.Seg.l, Hayes1989.V Hayes1989.Seg.schwa] true

def Hayes1989.tal_free : Form Seg

Schwa Drop and Parasitic Delinking (24): the second syllable goes, its mora is free.

Equations

• Hayes1989.tal_free = (Hayes1989.tale.delete 3).parasitic

theorem Hayes1989.tal_free_nodes : tal_free.nodes = {Node.σ 1, Node.μ 1, Node.μ 3}

def Hayes1989.taal : Form Seg

(25)–(26): CL from the left, then the stray l adjoins to the migrated mora, which the first syllable adopts.

Equations

• Hayes1989.taal = ((Hayes1989.tal_free.cl Hayes1989.Form.Convention.fromLeft).link (Hayes1989.Node.μ 3) 2).adjoin

theorem Hayes1989.taal_noCrossing : taal.NoCrossing

theorem Hayes1989.taal_surface : taal.surface = [(Seg.t, 1), (Seg.a, 2), (Seg.l, 1)]

theorem Hayes1989.taal_weight : taal.weight (Node.σ 1) = 2

theorem Hayes1989.taal_moraCount : taal.moraCount = tale.moraCount

def Hayes1989.ala : Form Seg

The mirror image (61), (66): #ala with the first vowel deleted.

Equations

• Hayes1989.ala = Hayes1989.Underlying.syllabify [Hayes1989.V Hayes1989.Seg.a, Hayes1989.C Hayes1989.Seg.l, Hayes1989.V Hayes1989.Seg.a] true

def Hayes1989.la_free : Form Seg

After Parasitic Delinking the first mora is free, but the l remains the second syllable's onset.

Equations

• Hayes1989.la_free = (Hayes1989.ala.delete 0).parasitic

theorem Hayes1989.la_free_stranded : la_free.stranded = {Node.μ 0}

theorem Hayes1989.no_rightward_vowel_loss : ¬(la_free.link (Node.μ 0) 2).NoCrossing

Rightward vowel lengthening crosses the onset line: #laː cannot arise.

theorem Hayes1989.lla_surface : (la_free.cl Form.Convention.fromRight).surface = [(Seg.l, 2), (Seg.a, 1)]

The remaining option without crossings is (56): the l geminates, the first half in its own syllable.

theorem Hayes1989.lla_noCrossing : (la_free.cl Form.Convention.fromRight).NoCrossing

def Hayes1989.talpa : Form Seg

(68): talpa with the final vowel deleted; the first syllable is closed by a moraic l.

Equations

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

def Hayes1989.talp_free : Form Seg

Equations

• Hayes1989.talp_free = (Hayes1989.talpa.delete 4).parasitic

theorem Hayes1989.talp_no_vowel_lengthening : ¬(talp_free.link (Node.μ 4) 1).NoCrossing

The vowel cannot lengthen across its coda's line.

theorem Hayes1989.talp_consonant_lengthening : (talp_free.link (Node.μ 4) 2).NoCrossing

The l could, at the price of a consonant linked to two morae of one syllable ((7)), the configuration Estonian permits.

theorem Hayes1989.talp_consonant_length : (talp_free.link (Node.μ 4) 2).length 2 = 2

Glide Formation: Ilokano (38)–(40) and Managerial Lengthening (44), (46)

def Hayes1989.bagien : Form Seg

Ilokano bagi + en 'to have as one's own' ((27a)), CVC heavy.

Equations

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

def Hayes1989.bagien_gf : Form Seg

Glide Formation (37) delinks the stem vowel from its mora, Parasitic Delinking removes its syllable, and the stray g and glide adjoin to the following syllable (39).

Equations

• Hayes1989.bagien_gf = ((Hayes1989.bagien.delink (Hayes1989.Node.μ 3) 3).parasitic.link (Hayes1989.Node.σ 4) 2).link (Hayes1989.Node.σ 4) 3

theorem Hayes1989.bagien_gf_stranded : bagien_gf.stranded = {Node.μ 3}

theorem Hayes1989.bagien_gf_noCrossing : bagien_gf.NoCrossing

def Hayes1989.baggyen : Form Seg

Ilokano fills from the right ((40a)): the g, now an onset of the following syllable, spreads onto the mora, which the first syllable adopts, giving bag.gyen.

Equations

• Hayes1989.baggyen = (Hayes1989.bagien_gf.cl Hayes1989.Form.Convention.fromRight).adjoin

theorem Hayes1989.baggyen_rightBound : Autosegmental.rightBound bagien_gf.links (Node.μ 3) = ↑2

theorem Hayes1989.baggyen_surface : baggyen.surface = [(Seg.b, 1), (Seg.a, 1), (Seg.g, 2), (Seg.i, 1), (Seg.e, 1), (Seg.n, 1)]

theorem Hayes1989.baggyen_noCrossing : baggyen.NoCrossing

theorem Hayes1989.baggyen_weight : baggyen.weight (Node.σ 1) = 2

def Hayes1989.baagyen : Form Seg

Nothing but the convention keeps the preceding vowel from filling the mora instead ((44)): baagyen, the Managerial Lengthening of English patience ((46)).

Equations

• Hayes1989.baagyen = (Hayes1989.bagien_gf.cl Hayes1989.Form.Convention.fromLeft).adjoin

theorem Hayes1989.baagyen_leftBound : Autosegmental.leftBound bagien_gf.links (Node.μ 3) = ↑1

theorem Hayes1989.baagyen_surface : baagyen.surface = [(Seg.b, 1), (Seg.a, 2), (Seg.g, 1), (Seg.i, 1), (Seg.e, 1), (Seg.n, 1)]

theorem Hayes1989.baagyen_noCrossing : baagyen.NoCrossing

Total assimilation (49b) and prenasalization (52)

def Hayes1989.asta : Form Seg

Regressive total assimilation, asta → atta: the coda deletes and the following consonant fills its mora, the convention of Lesbian and Thessalian Greek (§3.3).

Equations

• Hayes1989.asta = Hayes1989.Underlying.syllabify [Hayes1989.V Hayes1989.Seg.a, Hayes1989.C Hayes1989.Seg.s, Hayes1989.C Hayes1989.Seg.t, Hayes1989.V Hayes1989.Seg.a] true

theorem Hayes1989.atta_surface : ((asta.delete 1).cl Form.Convention.fromRight).surface = [(Seg.a, 1), (Seg.t, 2), (Seg.a, 1)]

theorem Hayes1989.atta_noCrossing : ((asta.delete 1).cl Form.Convention.fromRight).NoCrossing

def Hayes1989.amba : Form Seg

Bantu prenasalization, amba → aːmba, which the paper lists without a derivation: here the nasal leaves its mora for the onset of the following syllable, and the vowel fills it.

Equations

• Hayes1989.amba = Hayes1989.Underlying.syllabify [Hayes1989.V Hayes1989.Seg.a, Hayes1989.C Hayes1989.Seg.m, Hayes1989.C Hayes1989.Seg.b, Hayes1989.V Hayes1989.Seg.a] true

def Hayes1989.aamba : Form Seg

Equations

• Hayes1989.aamba = ((Hayes1989.amba.delink (Hayes1989.Node.μ 1) 1).link (Hayes1989.Node.σ 3) 1).cl Hayes1989.Form.Convention.fromLeft

theorem Hayes1989.aamba_surface : aamba.surface = [(Seg.a, 2), (Seg.m, 1), (Seg.b, 1), (Seg.a, 1)]

theorem Hayes1989.aamba_noCrossing : aamba.NoCrossing

Inverse CL: Luganda (55a)

def Hayes1989.aika : Form Seg

In Luganda aika → akka, the vowel deletes and the following consonant geminates.

Equations

• Hayes1989.aika = Hayes1989.Underlying.syllabify [Hayes1989.V Hayes1989.Seg.a, Hayes1989.V Hayes1989.Seg.i, Hayes1989.C Hayes1989.Seg.k, Hayes1989.V Hayes1989.Seg.a] true

def Hayes1989.akka : Form Seg

Equations

• Hayes1989.akka = ((Hayes1989.aika.delete 1).parasitic.cl Hayes1989.Form.Convention.fromRight).adjoin

theorem Hayes1989.akka_surface : akka.surface = [(Seg.a, 1), (Seg.k, 2), (Seg.a, 1)]

theorem Hayes1989.akka_noCrossing : akka.NoCrossing

The weight prerequisite (§6, (71))

def Hayes1989.pas_light : Form Seg

In pas, in a language without Weight by Position, the coda rides the nucleus mora.

Equations

• Hayes1989.pas_light = Hayes1989.Underlying.syllabify [Hayes1989.C Hayes1989.Seg.p, Hayes1989.V Hayes1989.Seg.a, Hayes1989.C Hayes1989.Seg.s] false

def Hayes1989.pas_heavy : Form Seg

pas in a language with Weight by Position.

Equations

• Hayes1989.pas_heavy = Hayes1989.Underlying.syllabify [Hayes1989.C Hayes1989.Seg.p, Hayes1989.V Hayes1989.Seg.a, Hayes1989.C Hayes1989.Seg.s] true

theorem Hayes1989.pas_light_no_cl : (pas_light.delete 2).stranded = ∅

Without a weight distinction, coda deletion strands no mora and CL cannot occur.

theorem Hayes1989.pas_heavy_cl : (pas_heavy.delete 2).stranded = {Node.μ 2}

theorem Hayes1989.pas_light_weight : pas_light.weight (Node.σ 1) = 1

theorem Hayes1989.pas_heavy_weight : pas_heavy.weight (Node.σ 1) = 2

The two-mora limit and trimoraic syllables (§7)

def Hayes1989.sultni : Form Seg

Komi sult.ni 'to stand up' ((73)): in a doubly closed syllable under the two-mora limit the t shares the l's mora.

Equations

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

theorem Hayes1989.sutni_no_cl : (sultni.delete 2).stranded = ∅

Deleting the l strands nothing, giving [sutni] with no CL.

def Hayes1989.sultali : Form Seg

Komi sul.ta.li 'I stood up': the l alone closes its syllable and bears a mora.

Equations

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

theorem Hayes1989.suutali_surface : ((sultali.delete 2).cl Form.Convention.fromLeft).surface = [(Seg.s, 1), (Seg.u, 2), (Seg.t, 1), (Seg.a, 1), (Seg.l, 1), (Seg.i, 1)]

def Hayes1989.θangxta : Form Seg

Proto-Germanic θangxta 'thought' ((74)): CL in a nonfinal doubly closed syllable needs a trimoraic syllable, a mora limit of three.

Equations

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

theorem Hayes1989.θangxta_weight : θangxta.weight (Node.σ 1) = 3

theorem Hayes1989.θaaxta_surface : ((θangxta.delete 2).cl Form.Convention.fromLeft).surface = [(Seg.θ, 1), (Seg.a, 2), (Seg.x, 1), (Seg.t, 1), (Seg.a, 1)]

theorem Hayes1989.θangxta_limit_two_no_cl : ((Underlying.syllabify [C Seg.θ, V Seg.a, C Seg.ng, C Seg.x, C Seg.t, V Seg.a] true).delete 2).stranded = ∅

Under the two-mora limit the same change is underivable.

def Hayes1989.spreeke : Form Seg

Dithmarschen German spreeke 'speak, 1sg' ((76c)): vowel loss with CL lengthens a long vowel to overlong, a trimoraic syllable ((77)).

Equations

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

def Hayes1989.spreeek : Form Seg

Equations

• Hayes1989.spreeek = (((Hayes1989.spreeke.delete 5).parasitic.cl Hayes1989.Form.Convention.fromLeft).link (Hayes1989.Node.μ 5) 4).adjoin

theorem Hayes1989.spreeek_surface : spreeek.surface = [(Seg.s, 1), (Seg.p, 1), (Seg.r, 1), (Seg.e, 3), (Seg.k, 1)]

theorem Hayes1989.spreeek_weight : spreeek.weight (Node.σ 3) = 3

theorem Hayes1989.spreeek_noCrossing : spreeek.NoCrossing