Prince (1983): Relating to the Grid

Prince argues that the metrical grid alone, without the labelled tree, carries the theory of stress. For a uniformly labelled tree, Liberman and Prince's Relative Prominence Projection Rule says what the End Rule says, so the labelling does no work. Two grid entries clash when they are adjacent at a level with no entry one level down between them, and the Rhythm Rule is Move x, which slides a clashing entry within its level and can never move the peak of a phrase. Word stress is built from the End Rule at an edge, extrametricality, Perfect Grid Construction sweeping from an edge, and bipositional heavy syllables; together they derive the alternating systems of Garawa, Hawaiian and Winnebago and the quantity-sensitive systems of (98).

Main statements

• SWTree.uniform_rppr_iff: under uniform labelling at either edge the RPPR is the End Rule.
• moveXL_getD_peak, Marks.not_isContinuous_move: Move x never moves the peak, since the move would leave a hole in a column.
• postpeninitial_iff, antepenultimate_iff: stress three syllables from an edge comes only from extrametricality and a trough-first sweep from that edge.
• hawaiian_eq, hawaiian_ne_alternating: Hawaiian's initial dactyl needs the End Rule at both edges before the sweep, and no perfect grid gives it.

Implementation notes

• A grid is the substrate's Prosody.Grid, a list of column heights, so the Continuous Column Constraint holds by construction.
• The End Rule applies to the highest level present below the level it maps into, the reading of §3.7; without Forward Clash Override it withholds a promotion that would clash.
• Perfect Grid Construction is a greedy sweep that raises a column when neither neighbour is stressed, a trough start behaving as if a stress preceded the edge.
• The edges and directions of (119) are both Edge, a direction being named by the edge it starts from; the End Rule, Perfect Grid Construction and Move x run right to left as the List.revConj mirror images of their left-to-right versions. A syllable of two or more moras is bipositional.

TODO

The End Rule (Final) inside the stress level that makes Garawa's penultimate stress secondary rather than tertiary, Mora Sluicing, the Forward Clash Override option of Perfect Grid Construction, the bounding of Move x in §2.2, the extrametrical systems of (99), the feet of §4, and the pitch-accent systems of §5 are not formalized.

References

• [Pri83]
• [LP77]

Trees, the Relative Prominence Projection Rule, and the End Rule (§1.3, §2.1)

def Prince1983.place : Edge → List ℕ → List ℕ → List ℕ

place e a b sets a beside b, with a at edge e.

Equations

• Prince1983.place Edge.left x✝¹ x✝ = x✝¹ ++ x✝
• Prince1983.place Edge.right x✝¹ x✝ = x✝ ++ x✝¹

@[simp]

theorem Prince1983.mem_place {e : Edge} {a b : List ℕ} {x : ℕ} : x ∈ place e a b ↔ x ∈ a ∨ x ∈ b

theorem Prince1983.perm_place (e : Edge) (a b : List ℕ) : (place e a b).Perm (a ++ b)

inductive Prince1983.SWTree : Type

An s/w-labelled binary metrical tree whose terminals carry their grid column heights. A node holds its strong daughter s, its weak daughter w, and the edge e at which s stands, so the labelling is independent of linear order.

• leaf (h : ℕ) : SWTree
• node (s w : SWTree) (e : Edge) : SWTree

def Prince1983.instDecidableEqSWTree.decEq (x✝ x✝¹ : SWTree) : Decidable (x✝ = x✝¹)

Equations

• One or more equations did not get rendered due to their size.
• Prince1983.instDecidableEqSWTree.decEq (Prince1983.SWTree.leaf a) (Prince1983.SWTree.leaf b) = if h : a = b then h ▸ isTrue ⋯ else isFalse ⋯
• Prince1983.instDecidableEqSWTree.decEq (Prince1983.SWTree.leaf h) (s.node w e) = isFalse ⋯
• Prince1983.instDecidableEqSWTree.decEq (s.node w e) (Prince1983.SWTree.leaf h) = isFalse ⋯

@[instance_reducible]

instance Prince1983.instDecidableEqSWTree : DecidableEq SWTree

Equations

• Prince1983.instDecidableEqSWTree = Prince1983.instDecidableEqSWTree.decEq

@[instance_reducible]

instance Prince1983.instReprSWTree : Repr SWTree

Equations

• Prince1983.instReprSWTree = { reprPrec := Prince1983.instReprSWTree.repr }

def Prince1983.instReprSWTree.repr : SWTree → ℕ → Std.Format

Equations

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

def Prince1983.SWTree.heights : SWTree → Prosody.Grid

The grid over a tree lists the column heights of its terminals, left to right.

Equations

• (Prince1983.SWTree.leaf h).heights = [h]
• (s.node w e).heights = Prince1983.place e s.heights w.heights

def Prince1983.SWTree.headHeight : SWTree → ℕ

H(N) is the height of the head terminal, reached from the root through strong daughters.

Equations

• (Prince1983.SWTree.leaf h).headHeight = h
• (s.node w e).headHeight = s.headHeight

def Prince1983.SWTree.weakHeights : SWTree → List ℕ

weakHeights t lists the heights of the terminals other than the head.

Equations

• (Prince1983.SWTree.leaf h).weakHeights = []
• (s.node w e).weakHeights = Prince1983.place e s.weakHeights w.heights

theorem Prince1983.SWTree.mem_heights {t : SWTree} {h : ℕ} : h ∈ t.heights ↔ h = t.headHeight ∨ h ∈ t.weakHeights

theorem Prince1983.SWTree.headHeight_mem (t : SWTree) : t.headHeight ∈ t.heights

theorem Prince1983.SWTree.heights_perm (t : SWTree) : List.Perm t.heights (t.headHeight :: t.weakHeights)

The terminals are the head and the others.

def Prince1983.SWTree.Everywhere (P : SWTree → Prop) : SWTree → Prop

Everywhere P t says that P holds of every constituent of t.

Equations

• Prince1983.SWTree.Everywhere P (Prince1983.SWTree.leaf h) = P (Prince1983.SWTree.leaf h)
• Prince1983.SWTree.Everywhere P (s.node w e) = (Prince1983.SWTree.Everywhere P s ∧ Prince1983.SWTree.Everywhere P w ∧ P (s.node w e))

theorem Prince1983.SWTree.Everywhere.self {P : SWTree → Prop} {t : SWTree} (h : Everywhere P t) : P t

def Prince1983.SWTree.Rppr : SWTree → Prop

The Relative Prominence Projection Rule (7) requires H(s) > H(w) of every pair of sisters.

Equations

• (Prince1983.SWTree.leaf h).Rppr = True
• (s.node w e).Rppr = (s.Rppr ∧ w.Rppr ∧ w.headHeight < s.headHeight)

def Prince1983.SWTree.HeadStrong (t : SWTree) : Prop

The head of a constituent is stronger than each of its other terminals.

Equations

• t.HeadStrong = ∀ h ∈ t.weakHeights, h < t.headHeight

theorem Prince1983.SWTree.HeadStrong.le {t : SWTree} (ht : t.HeadStrong) {h : ℕ} (hh : h ∈ t.heights) : h ≤ t.headHeight

theorem Prince1983.SWTree.headStrong_node_iff {s w : SWTree} {e : Edge} (hs : s.HeadStrong) (hw : w.HeadStrong) : (s.node w e).HeadStrong ↔ w.headHeight < s.headHeight

Over head-strong daughters, a node is head-strong exactly when its sisters meet the RPPR.

theorem Prince1983.SWTree.rppr_iff (t : SWTree) : t.Rppr ↔ Everywhere HeadStrong t

The RPPR, a condition on sisters, says that the head is strongest in every constituent.

theorem Prince1983.SWTree.isCulminative_of_rppr {t : SWTree} (h : t.Rppr) : t.heights.IsCulminative

Under the RPPR the grid is culminative, the head terminal being its unique peak.

def Prince1983.SWTree.edgeHeight (e : Edge) : SWTree → ℕ

edgeHeight e t is the height of the terminal at edge e.

Equations

• Prince1983.SWTree.edgeHeight e (Prince1983.SWTree.leaf h) = h
• Prince1983.SWTree.edgeHeight e (s.node w e_1) = if e_1 = e then Prince1983.SWTree.edgeHeight e s else Prince1983.SWTree.edgeHeight e w

def Prince1983.SWTree.otherHeights (e : Edge) : SWTree → List ℕ

otherHeights e t lists the heights of the terminals other than the one at edge e.

Equations

• One or more equations did not get rendered due to their size.
• Prince1983.SWTree.otherHeights e (Prince1983.SWTree.leaf h) = []

def Prince1983.SWTree.EdgeStrong (e : Edge) (t : SWTree) : Prop

The End Rule (13) at edge e makes the terminal there stronger than every other terminal.

Equations

• Prince1983.SWTree.EdgeStrong e t = ∀ h ∈ Prince1983.SWTree.otherHeights e t, h < Prince1983.SWTree.edgeHeight e t

def Prince1983.SWTree.Uniform (e : Edge) : SWTree → Prop

A tree is uniformly labelled at edge e when every constituent is strong there.

Equations

• Prince1983.SWTree.Uniform e (Prince1983.SWTree.leaf h) = True
• Prince1983.SWTree.Uniform e (s.node w e_1) = (e_1 = e ∧ Prince1983.SWTree.Uniform e s ∧ Prince1983.SWTree.Uniform e w)

theorem Prince1983.SWTree.Uniform.headHeight_eq {e : Edge} {t : SWTree} (h : Uniform e t) : t.headHeight = edgeHeight e t

theorem Prince1983.SWTree.Uniform.weakHeights_eq {e : Edge} {t : SWTree} (h : Uniform e t) : t.weakHeights = otherHeights e t

theorem Prince1983.SWTree.uniform_rppr_iff {e : Edge} {t : SWTree} (h : Uniform e t) : t.Rppr ↔ Everywhere (EdgeStrong e) t

Under uniform labelling at either edge the RPPR says exactly what the End Rule says, so the labelling of nonterminals does no work.

Clash and Move x (§2.2)

def Prince1983.Clash (g : Prosody.Grid) (n i j : ℕ) : Prop

Columns i < j clash at level n (27) when both reach level n and no column between them reaches level n - 1.

Equations

• Prince1983.Clash g n i j = (i < j ∧ n ≤ List.getD g i 0 ∧ n ≤ List.getD g j 0 ∧ ∀ k < j, i < k → List.getD g k 0 + 1 < n)

@[instance_reducible]

instance Prince1983.instDecidableClash (g : Prosody.Grid) (n i j : ℕ) : Decidable (Clash g n i j)

Equations

• Prince1983.instDecidableClash g n i j = id inferInstance

def Prince1983.NoClash (g : Prosody.Grid) : Prop

A grid is eurhythmic when no two columns clash at any level from 2 up to the peak.

Equations

• Prince1983.NoClash g = ∀ n ≤ g.peak, 2 ≤ n → ∀ i < List.length g, ∀ j < List.length g, ¬Prince1983.Clash g n i j

@[instance_reducible]

instance Prince1983.instDecidableNoClash (g : Prosody.Grid) : Decidable (NoClash g)

Equations

• Prince1983.instDecidableNoClash g = id inferInstance

theorem Prince1983.noClash_of_alternating {g : Prosody.Grid} (h : ∀ x ∈ g, 1 ≤ x ∧ x ≤ 2) (hadj : List.IsChain (fun (a b : ℕ) => a < 2 ∨ b < 2) g) : NoClash g

A grid of stresses and unstressed columns with no two stresses adjacent is eurhythmic.

def Prince1983.landing? (g : Prosody.Grid) (n i : ℕ) : Option ℕ

The landing site of a leftward move at level n from column i is the nearest column to the left with an entry at level n - 1 and none at level n.

Equations

• Prince1983.landing? g n i = List.findRev? (fun (k : ℕ) => List.getD g k 0 == n - 1) (List.range i)

def Prince1983.clashing? (g : Prosody.Grid) (n : ℕ) : Option ℕ

The leftmost column that clashes at level n with a column to its right.

Equations

• Prince1983.clashing? g n = List.find? (fun (i : ℕ) => (List.range (List.length g)).any fun (j : ℕ) => decide (Prince1983.Clash g n i j)) (List.range (List.length g))

def Prince1983.moveXL (n : ℕ) (g : Prosody.Grid) : Prosody.Grid

Leftward Move x at level n slides the left member of the first clash within its level to the landing site, provided its column has no entry above level n.

Equations

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

def Prince1983.moveX : Edge → ℕ → Prosody.Grid → Prosody.Grid

Move x(D;L) of (119f) moves entries leftward when it runs right to left, and the rightward rule is its mirror image.

Equations

• Prince1983.moveX Edge.right x✝ = Prince1983.moveXL x✝
• Prince1983.moveX Edge.left x✝ = List.revConj (Prince1983.moveXL x✝)

def Prince1983.Marks.move (r i k : ℕ) (m : Prosody.Marks) : Prosody.Marks

Marks.move r i k slides one mark within row r from column i to column k.

Equations

• Prince1983.Marks.move r i k m = List.modify m r fun (row : List Bool) => (row.set i false).set k true

theorem Prince1983.Marks.not_isContinuous_move {g : Prosody.Grid} {n i k : ℕ} (hi : i < List.length g) (hn : n < g[i]) (hn1 : 1 ≤ n) (hk : k ≠ i) : ¬(move (n - 1) i k g.rows).IsContinuous

Sliding the level-n entry out of a column that reaches above level n leaves a hole (32), so no such move is available on well-formed grids.

theorem Prince1983.moveXL_eq_or (n : ℕ) (g : Prosody.Grid) : moveXL n g = g ∨ ∃ (i : ℕ) (j : ℕ) (k : ℕ), i < List.length g ∧ j < List.length g ∧ Clash g n i j ∧ List.getD g i 0 = n ∧ List.getD g k 0 = n - 1 ∧ moveXL n g = (List.set g i (n - 1)).set k n

theorem Prince1983.moveXL_eq_self_of_not_clash {n : ℕ} {g : Prosody.Grid} (h : ∀ i < List.length g, ∀ j < List.length g, ¬Clash g n i j) : moveXL n g = g

theorem Prince1983.moveXL_getD_of_lt {n c : ℕ} {g : Prosody.Grid} (hc : n < List.getD g c 0) : List.getD (moveXL n g) c 0 = List.getD g c 0

Move x at level n never touches a column taller than n, so no entry is slid out from under a taller column (32).

theorem Prince1983.not_clash_of_peak_le {g : Prosody.Grid} (hc : g.IsCulminative) {n i j : ℕ} (hn : g.peak ≤ n) (hi : i < List.length g) (hj : j < List.length g) : ¬Clash g n i j

A culminative grid has no clash at or above its peak, since both columns would be peaks.

theorem Prince1983.moveXL_getD_peak {g : Prosody.Grid} (hc : g.IsCulminative) {i n : ℕ} (hi : i < List.length g) (hp : g[i] = g.peak) : List.getD (moveXL n g) i 0 = g[i]

The absolute peak never moves (31), since below the peak Move x leaves taller columns alone and at or above it a culminative grid has no clash.

The End Rule, extrametricality, and Perfect Grid Construction (§3.2, §3.3)

The last index

def Prince1983.lastIdx? (p : ℕ → Bool) : List ℕ → Option ℕ

The last index whose element satisfies p.

Equations

• Prince1983.lastIdx? p [] = none
• Prince1983.lastIdx? p (x_1 :: l) = (Option.map (fun (x : ℕ) => x + 1) (Prince1983.lastIdx? p l)).or (if p x_1 = true then some 0 else none)

@[simp]

theorem Prince1983.lastIdx?_nil (p : ℕ → Bool) : lastIdx? p [] = none

theorem Prince1983.lastIdx?_cons (p : ℕ → Bool) (x : ℕ) (l : List ℕ) : lastIdx? p (x :: l) = (Option.map (fun (x : ℕ) => x + 1) (lastIdx? p l)).or (if p x = true then some 0 else none)

theorem Prince1983.lastIdx?_cons_of_some {p : ℕ → Bool} {l : List ℕ} {i : ℕ} (h : lastIdx? p l = some i) (x : ℕ) : lastIdx? p (x :: l) = some (i + 1)

theorem Prince1983.lastIdx?_append (p : ℕ → Bool) (l₁ l₂ : List ℕ) : lastIdx? p (l₁ ++ l₂) = (Option.map (fun (x : ℕ) => x + l₁.length) (lastIdx? p l₂)).or (lastIdx? p l₁)

theorem Prince1983.lastIdx?_eq_some {p : ℕ → Bool} {l : List ℕ} {i : ℕ} (h : lastIdx? p l = some i) : ∃ (hi : i < l.length), p l[i] = true

theorem Prince1983.lastIdx?_eq_none {p : ℕ → Bool} {l : List ℕ} : lastIdx? p l = none ↔ ∀ x ∈ l, p x = false

theorem Prince1983.lastIdx?_eq_findIdx?_reverse (p : ℕ → Bool) (l : List ℕ) : lastIdx? p l = Option.map (fun (x : ℕ) => l.length - 1 - x) (List.findIdx? p l.reverse)

The last index is the first index of the reversed list, counted back from the end.

The End Rule

def Prince1983.edgeIdx? : Edge → ℕ → Prosody.Grid → Option ℕ

The edge-most column reaching level n.

Equations

• Prince1983.edgeIdx? Edge.left x✝¹ x✝ = List.findIdx? (fun (x : ℕ) => decide (x✝¹ ≤ x)) x✝
• Prince1983.edgeIdx? Edge.right x✝¹ x✝ = Prince1983.lastIdx? (fun (x : ℕ) => decide (x✝¹ ≤ x)) x✝

def Prince1983.fromEdge : Edge → (Prosody.Grid → Prosody.Grid) → Prosody.Grid → Prosody.Grid

A rule applied at an edge runs as it is from the left and as its mirror image from the right.

Equations

• Prince1983.fromEdge Edge.left x✝ = x✝
• Prince1983.fromEdge Edge.right x✝ = List.revConj x✝

def Prince1983.endRule (e : Edge) (L : ℕ) (fco : Bool) : Prosody.Grid → Prosody.Grid

The End Rule ER(E;L;FCO) of (16), (97) and (119a) promotes the edge-most entry at the highest level present below L by one level, so that the edge-most stress of a constituent becomes its main stress and, absent stresses, its edge syllable is stressed. Without Forward Clash Override the promotion is withheld when it would clash.

Equations

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

theorem Prince1983.endRule_right (L : ℕ) (fco : Bool) (g : Prosody.Grid) : endRule Edge.right L fco g = List.reverse (endRule Edge.left L fco (List.reverse g))

def Prince1983.elm : Edge → (Prosody.Grid → Prosody.Grid) → Prosody.Grid → Prosody.Grid

Extrametricality elm(E) of (119c) hides the edge column from the rule applied inside.

Equations

• Prince1983.elm Edge.left x✝ [] = x✝ []
• Prince1983.elm Edge.left x✝ (x_3 :: t) = x_3 :: x✝ t
• Prince1983.elm Edge.right x✝¹ x✝ = x✝¹ (List.dropLast x✝) ++ List.drop (List.length x✝ - 1) x✝

def Prince1983.sweep : ℕ → Prosody.Grid → Prosody.Grid

One sweep of Perfect Grid Construction raises a column to the stress level when neither neighbour reaches it, prev being the height of the column just passed.

Equations

• Prince1983.sweep x✝ [] = []
• Prince1983.sweep x✝ (x_2 :: t) = (if x_2 < 2 ∧ x✝ < 2 ∧ t.headD 0 < 2 then 2 else x_2) :: Prince1983.sweep (if x_2 < 2 ∧ x✝ < 2 ∧ t.headD 0 < 2 then 2 else x_2) t

theorem Prince1983.sweep_cons_of_two_le {x : ℕ} (hx : 2 ≤ x) (p : ℕ) (t : Prosody.Grid) : sweep p (x :: t) = x :: sweep x t

inductive Prince1983.Altitude : Type

Whether a sweep starts at a peak or a trough, A of (119b).

• peak : Altitude
• trough : Altitude

@[instance_reducible]

instance Prince1983.instDecidableEqAltitude : DecidableEq Altitude

Equations

• Prince1983.instDecidableEqAltitude x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

@[instance_reducible]

instance Prince1983.instReprAltitude : Repr Altitude

Equations

• Prince1983.instReprAltitude = { reprPrec := Prince1983.instReprAltitude.repr }

def Prince1983.instReprAltitude.repr : Altitude → ℕ → Std.Format

Equations

• Prince1983.instReprAltitude.repr Prince1983.Altitude.peak prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Prince1983.Altitude.peak")).group prec✝
• Prince1983.instReprAltitude.repr Prince1983.Altitude.trough prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Prince1983.Altitude.trough")).group prec✝

def Prince1983.Altitude.flip : Altitude → Altitude

The other altitude.

Equations

• Prince1983.Altitude.peak.flip = Prince1983.Altitude.trough
• Prince1983.Altitude.trough.flip = Prince1983.Altitude.peak

def Prince1983.Altitude.height : Altitude → ℕ

The height of a column at a peak, stressed, or at a trough, unstressed.

Equations

• Prince1983.Altitude.peak.height = 2
• Prince1983.Altitude.trough.height = 1

def Prince1983.Altitude.start (a : Altitude) : ℕ

A sweep behaves as if it had passed a column of this height before its first column, an unstressed one before a peak and a stress before a trough.

Equations

• a.start = a.flip.height

def Prince1983.pg (d : Edge) (a : Altitude) : Prosody.Grid → Prosody.Grid

Perfect Grid Construction PG(D;A) of (61), (62) and (119b) lays down a clash-free, maximally alternating stress level by a sweep in direction D starting from a peak or a trough.

Equations

• Prince1983.pg Edge.left a = Prince1983.sweep a.start
• Prince1983.pg Edge.right a = List.revConj (Prince1983.sweep a.start)

def Prince1983.alt : Altitude → ℕ → Prosody.Grid

The alternating stress level is 2, 1, 2, … from a peak and 1, 2, 1, … from a trough.

Equations

• Prince1983.alt x✝ 0 = []
• Prince1983.alt x✝ n.succ = x✝.height :: Prince1983.alt x✝.flip n

@[simp]

theorem Prince1983.alt_length (a : Altitude) (n : ℕ) : List.length (alt a n) = n

theorem Prince1983.alt_getD (a : Altitude) (n i : ℕ) : List.getD (alt a n) i 0 = if i < n then if i % 2 = 0 ↔ a = Altitude.peak then 2 else 1 else 0

theorem Prince1983.mem_alt {a : Altitude} {n x : ℕ} (hx : x ∈ alt a n) : 1 ≤ x ∧ x ≤ 2

theorem Prince1983.sweep_replicate (a : Altitude) (n : ℕ) : sweep a.start (List.replicate n 1) = alt a n

theorem Prince1983.sweep_replicate_append (a : Altitude) (m : ℕ) : sweep a.start (List.replicate (m + 1) 1 ++ [2]) = alt a m ++ [1, 2]

def Prince1983.startDist : Edge → ℕ → ℕ → ℕ

The distance of column i of n from the edge a sweep in direction d starts at.

Equations

• Prince1983.startDist Edge.left x✝¹ x✝ = x✝
• Prince1983.startDist Edge.right x✝¹ x✝ = x✝¹ - 1 - x✝

theorem Prince1983.pg_replicate_getD (d : Edge) (a : Altitude) {n i : ℕ} (hi : i < n) : List.getD (pg d a (List.replicate n 1)) i 0 = if startDist d n i % 2 = 0 ↔ a = Altitude.peak then 2 else 1

A sweep over an unstressed word stresses the columns whose distance from the starting edge has the parity of the start, a peak stressing the even distances (62). Weri is (62d), sweeping right to left from a peak; Warao, (62c); Maranungku, (62b); Southern Paiute, (62a).

theorem Prince1983.noClash_pg_replicate (d : Edge) (a : Altitude) (n : ℕ) : NoClash (pg d a (List.replicate n 1))

Perfect Grid Construction is clash-free.

theorem Prince1983.endRule_of_peak {e : Edge} {L : ℕ} {fco : Bool} {g : Prosody.Grid} (hL : g.peak ≤ L - 1) {i : ℕ} (hi : edgeIdx? e g.peak g = some i) : endRule e L fco g = List.set g i (g.peak + 1)

theorem Prince1983.peak_replicate_one {n : ℕ} (hn : 0 < n) : Prosody.Grid.peak (List.replicate n 1) = 1

theorem Prince1983.endRule_left_replicate {n : ℕ} (hn : 0 < n) (fco : Bool) : endRule Edge.left 2 fco (List.replicate n 1) = 2 :: List.replicate (n - 1) 1

Stressing the first syllable of an unstressed word.

The End Rule at the stress level

theorem Prince1983.endRule_le_two {e : Edge} {fco : Bool} {g : Prosody.Grid} (h2 : ∀ x ∈ g, x ≤ 2) (x : ℕ) : x ∈ endRule e 2 fco g → x ≤ 2

The End Rule at the stress level never raises a column above it.

theorem Prince1983.endRule_left_of_two_le {x : ℕ} (hx : 2 ≤ x) (t : Prosody.Grid) (fco : Bool) : endRule Edge.left 2 fco (x :: t) = x :: t

An already stressed initial syllable is left alone.

theorem Prince1983.endRule_left_singleton {x : ℕ} (hx : 1 ≤ x) (fco : Bool) : endRule Edge.left 2 fco [x] = [max x 2]

theorem Prince1983.endRule_left_two {y : ℕ} (hy : 1 ≤ y) (t : Prosody.Grid) (fco : Bool) : endRule Edge.left 2 fco (1 :: y :: t) = if fco = true ∨ y < 2 then 2 :: y :: t else 1 :: y :: t

Stressing a light initial syllable, withheld before a stressed second position unless Forward Clash Override is on.

theorem Prince1983.endRule_right_singleton {x : ℕ} (hx : 1 ≤ x) (fco : Bool) : endRule Edge.right 2 fco [x] = [max x 2]

theorem Prince1983.endRule_right_two {y : ℕ} (hy : 1 ≤ y) (t : Prosody.Grid) (fco : Bool) : endRule Edge.right 2 fco (t ++ [y, 1]) = if fco = true ∨ y < 2 then t ++ [y, 2] else t ++ [y, 1]

Stressing a light final syllable, withheld after a stressed penultimate position unless Forward Clash Override is on.

theorem Prince1983.endRule_right_replicate {n : ℕ} (hn : 0 < n) (fco : Bool) : endRule Edge.right 2 fco (List.replicate n 1) = List.replicate (n - 1) 1 ++ [2]

Main stress

def Prince1983.MainStressAt (g : Prosody.Grid) (i : ℕ) : Prop

Column i carries the main stress when it is strictly taller than every other column.

Equations

• Prince1983.MainStressAt g i = (i < List.length g ∧ ∀ j < List.length g, j ≠ i → List.getD g j 0 < List.getD g i 0)

@[instance_reducible]

instance Prince1983.instDecidableMainStressAt (g : Prosody.Grid) (i : ℕ) : Decidable (MainStressAt g i)

Equations

• Prince1983.instDecidableMainStressAt g i = id inferInstance

theorem Prince1983.MainStressAt.isCulminative {g : Prosody.Grid} {i : ℕ} (h : MainStressAt g i) : g.IsCulminative

theorem Prince1983.mainStressAt_set {g : Prosody.Grid} {m i : ℕ} (h2 : ∀ x ∈ g, x ≤ m) (hi : i < List.length g) : MainStressAt (List.set g i (m + 1)) i

theorem Prince1983.mainStressAt_append_cons {t u : Prosody.Grid} {y : ℕ} (ht : ∀ x ∈ t, x < y) (hu : ∀ x ∈ u, x < y) : MainStressAt (t ++ y :: u) (List.length t)

theorem Prince1983.mainStressAt_endRule {e : Edge} {L : ℕ} {fco : Bool} {g : Prosody.Grid} (hL : g.peak ≤ L - 1) {i : ℕ} (hi : edgeIdx? e g.peak g = some i) : MainStressAt (endRule e L fco g) i

The End Rule at the level above the peak puts the main stress on the edge-most peak.

theorem Prince1983.endRule_three_of_edgeIdx? {e : Edge} {fco : Bool} {g : Prosody.Grid} (h2 : ∀ x ∈ g, x ≤ 2) {i : ℕ} (hi : edgeIdx? e 2 g = some i) : endRule e 3 fco g = List.set g i 3

On a grid of stresses and unstressed columns the End Rule at word level promotes the edge-most stress.

theorem Prince1983.mainStressAt_of_edgeIdx? {e : Edge} {fco : Bool} {g : Prosody.Grid} (h2 : ∀ x ∈ g, x ≤ 2) {i : ℕ} (hi : edgeIdx? e 2 g = some i) : MainStressAt (endRule e 3 fco g) i

Garawa and Winnebago (63), (65)

def Prince1983.garawa (n : ℕ) : Prosody.Grid

In Garawa (63) the End Rule stresses the initial syllable, Perfect Grid Construction sweeps right to left from a trough, and the End Rule at word level makes the initial stress the main stress.

Equations

• Prince1983.garawa n = Prince1983.endRule Edge.left 3 false (Prince1983.pg Edge.right Prince1983.Altitude.trough (Prince1983.endRule Edge.left 2 false (List.replicate n 1)))

theorem Prince1983.garawa_eq {n : ℕ} (hn : 2 ≤ n) : garawa n = 3 :: 1 :: List.reverse (alt Altitude.trough (n - 2))

theorem Prince1983.garawa_initial {n : ℕ} (hn : 2 ≤ n) : List.getD (garawa n) 0 0 = 3

theorem Prince1983.garawa_second {n : ℕ} (hn : 2 ≤ n) : List.getD (garawa n) 1 0 = 1

Clash blocks the sweep next to the initial stress, so "nonprimary stress may never occur on syllables directly following the main stress".

theorem Prince1983.garawa_getD {n i : ℕ} (hi : 2 ≤ i) (hin : i < n) : List.getD (garawa n) i 0 = if (n - 1 - i) % 2 = 1 then 2 else 1

Nonprimary stress on the penult, and alternating back from it.

def Prince1983.winnebago (n : ℕ) : Prosody.Grid

In Winnebago (65), with the initial syllable extrametrical, a trough-first sweep from the left and the End Rule at word level put main stress on the third syllable.

Equations

• Prince1983.winnebago n = Prince1983.endRule Edge.left 3 false (Prince1983.elm Edge.left (Prince1983.pg Edge.left Prince1983.Altitude.trough) (List.replicate n 1))

theorem Prince1983.winnebago_eq {n : ℕ} (hn : 3 ≤ n) : winnebago n = 1 :: 1 :: 3 :: alt Altitude.trough (n - 3)

Stress three syllables from an edge (§3.2, §3.3)

def Prince1983.alternating (d : Edge) (a : Altitude) (x : Option Edge) (n : ℕ) : Prosody.Grid

Perfect Grid Construction stresses an unstressed word, with or without an extrametrical syllable at an edge, in the parameter space of §3.2.

Equations

• Prince1983.alternating d a x n = x.elim (Prince1983.pg d a) (fun (x : Edge) => Prince1983.elm x (Prince1983.pg d a)) (List.replicate n 1)

theorem Prince1983.postpeninitial_iff (d : Edge) (a : Altitude) (x : Option Edge) : (∀ (n : ℕ), 4 ≤ n → List.findIdx? (fun (x : ℕ) => decide (2 ≤ x)) (alternating d a x n) = some 2) ↔ d = Edge.left ∧ a = Altitude.trough ∧ x = some Edge.left

Stress three syllables in, in every word long enough, is the extrametricality variant of a trough-first sweep from the left and arises from no other setting of the parameters, so grid theory derives postpeninitial stress only as Winnebago has it.

theorem Prince1983.antepenultimate_iff (d : Edge) (a : Altitude) (x : Option Edge) : (∀ (n : ℕ), 4 ≤ n → lastIdx? (fun (x : ℕ) => decide (2 ≤ x)) (alternating d a x n) = some (n - 3)) ↔ d = Edge.right ∧ a = Altitude.trough ∧ x = some Edge.right

Antepenultimate stress, the mirror image, is the extrametricality variant of a trough-first sweep from the right and arises from no other setting of the parameters.

Hawaiian (64)

def Prince1983.hawaiian (n : ℕ) : Prosody.Grid

In simplified Hawaiian (64), long vowels aside, the final syllable is extrametrical, the End Rule applies finally and then initially at the stress level, Perfect Grid Construction sweeps right to left from the final stress, and the End Rule applies finally at word level.

Equations

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

theorem Prince1983.hawaiian_three : hawaiian 3 = [1, 3, 1]

In a three-syllable word (64a) the End Rule (Initial) is blocked by the clash it would create with the penultimate stress.

theorem Prince1983.hawaiian_eq {n : ℕ} (hn : 4 ≤ n) : hawaiian n = 2 :: 1 :: List.reverse (alt Altitude.trough (n - 4)) ++ [3, 1]

After the End Rule stresses both edges, the sweep back from the penult leaves an initial dactyl when the alternation would stress the second syllable ((64b), (64c)).

theorem Prince1983.hawaiian_initial {n : ℕ} (hn : 4 ≤ n) : List.getD (hawaiian n) 0 0 = 2

"All long words (greater than three syllables) begin with a stress."

theorem Prince1983.hawaiian_mainStressAt {n : ℕ} (hn : 2 ≤ n) : MainStressAt (hawaiian n) (n - 2)

Main stress falls on the penult.

theorem Prince1983.hawaiian_ne_alternating (d : Edge) (a : Altitude) (x : Option Edge) : endRule Edge.right 3 false (alternating d a x 5) ≠ hawaiian 5

No perfect grid gives Hawaiian's initial dactyl, whatever its direction, starting altitude and extrametricality, so the End Rule must stress both edges before the sweep.

The End Rule at the phrase and Move x (28) to (31)

def Prince1983.achromatic : Prosody.Grid

The citation grids of achromatic, lens, Dundee, marmalade (28), antique, dealer, and chair (31).

Equations

• Prince1983.achromatic = [2, 1, 3, 1]

def Prince1983.lens : Prosody.Grid

Equations

• Prince1983.lens = [3]

def Prince1983.dundee : Prosody.Grid

Equations

• Prince1983.dundee = [2, 3]

def Prince1983.marmalade : Prosody.Grid

Equations

• Prince1983.marmalade = [3, 1, 2]

def Prince1983.antique : Prosody.Grid

Equations

• Prince1983.antique = [2, 3]

def Prince1983.dealer : Prosody.Grid

Equations

• Prince1983.dealer = [3, 1]

def Prince1983.chair : Prosody.Grid

Equations

• Prince1983.chair = [3]

theorem Prince1983.achromatic_lens : moveX Edge.right 3 (endRule Edge.right 4 false (achromatic ++ lens)) = [3, 1, 2, 1, 4]

Phrasal stress on lens creates a word-level clash with -ma- (29a), which Move x resolves by sliding the entry to the initial syllable (30a).

theorem Prince1983.dundee_marmalade : moveX Edge.right 3 (endRule Edge.right 4 false (dundee ++ marmalade)) = [3, 2, 4, 1, 2]

Move x resolves the clash in Dundee marmalade the same way ((29b), (30b)).

theorem Prince1983.antique_dealer : moveX Edge.right 3 (endRule Edge.left 4 false (antique ++ dealer)) = [2, 4, 3, 1]

In the compound antique dealer (31a) the clashing entry sits under the phrasal peak, so Move x cannot touch it.

theorem Prince1983.antique_chair : moveX Edge.right 3 (endRule Edge.right 4 false (antique ++ chair)) = [3, 2, 4]

In the phrase antique chair (31b) the same clash is resolved.

Quantity: bipositional heavy syllables (§3.5, §3.7)

def Prince1983.mora (m : Prosody.Syllable.Weight) : Prosody.Grid

A heavy syllable, one of two or more moras, occupies two grid positions with its nucleus above the second, so it is intrinsically stressed (74); a light syllable occupies one.

Equations

• Prince1983.mora m = if 2 ≤ m then [2, 1] else [1]

def Prince1983.qs (w : List Prosody.Syllable.Weight) : Prosody.Grid

Quantity Sensitivity QS of (119d) maps a syllable string to its grid.

Equations

• Prince1983.qs w = List.flatMap Prince1983.mora w

def Prince1983.nucleus (w : List Prosody.Syllable.Weight) (k : ℕ) : ℕ

The grid position of the nucleus of syllable k.

Equations

• Prince1983.nucleus w k = List.length (Prince1983.qs (List.take k w))

theorem Prince1983.mora_of_two_le {m : Prosody.Syllable.Weight} (h : 2 ≤ m) : mora m = [2, 1]

theorem Prince1983.mora_of_lt {m : Prosody.Syllable.Weight} (h : m < 2) : mora m = [1]

theorem Prince1983.qs_cons (m : Prosody.Syllable.Weight) (w : List Prosody.Syllable.Weight) : qs (m :: w) = mora m ++ qs w

theorem Prince1983.qs_append (w v : List Prosody.Syllable.Weight) : qs (w ++ v) = qs w ++ qs v

theorem Prince1983.mem_mora {m x : ℕ} (hx : x ∈ mora m) : 1 ≤ x ∧ x ≤ 2

theorem Prince1983.mem_qs {w : List Prosody.Syllable.Weight} {x : ℕ} (hx : x ∈ qs w) : 1 ≤ x ∧ x ≤ 2

theorem Prince1983.qs_le_two (w : List Prosody.Syllable.Weight) (x : ℕ) : x ∈ qs w → x ≤ 2

theorem Prince1983.qs_singleton (m : Prosody.Syllable.Weight) : qs [m] = mora m

theorem Prince1983.qs_isChain (w : List Prosody.Syllable.Weight) : List.IsChain (fun (a b : ℕ) => a < 2 ∨ b < 2) (qs w)

Heavy syllables never clash, since their nuclei are separated by their second positions (74).

theorem Prince1983.noClash_qs (w : List Prosody.Syllable.Weight) : NoClash (qs w)

theorem Prince1983.qs_eq_nil_iff {w : List Prosody.Syllable.Weight} : qs w = [] ↔ w = []

theorem Prince1983.exists_qs_eq_append_one {v : List Prosody.Syllable.Weight} (hv : v ≠ []) : ∃ (t : List ℕ), qs v = t ++ [1]

Every syllable ends in a weak position.

@[simp]

theorem Prince1983.nucleus_zero (w : List Prosody.Syllable.Weight) : nucleus w 0 = 0

theorem Prince1983.nucleus_cons_succ (m : Prosody.Syllable.Weight) (w : List Prosody.Syllable.Weight) (k : ℕ) : nucleus (m :: w) (k + 1) = List.length (mora m) + nucleus w k

theorem Prince1983.nucleus_append_length (v : List Prosody.Syllable.Weight) (m : Prosody.Syllable.Weight) : nucleus (v ++ [m]) v.length = List.length (qs v)

theorem Prince1983.findIdx?_qs (w : List Prosody.Syllable.Weight) : List.findIdx? (fun (x : ℕ) => decide (2 ≤ x)) (qs w) = Option.map (nucleus w) (List.findIdx? (fun (x : Prosody.Syllable.Weight) => decide (2 ≤ x)) w)

The first stress of the quantity-sensitive grid is the nucleus of the first heavy syllable.

theorem Prince1983.lastIdx?_qs (w : List Prosody.Syllable.Weight) : lastIdx? (fun (x : ℕ) => decide (2 ≤ x)) (qs w) = Option.map (nucleus w) (lastIdx? (fun (x : ℕ) => decide (2 ≤ x)) w)

The last stress of the quantity-sensitive grid is the nucleus of the last heavy syllable.

theorem Prince1983.qs_eq_replicate {w : List Prosody.Syllable.Weight} (h : ∀ m ∈ w, m < 2) : qs w = List.replicate w.length 1

A word of light syllables is an unstressed grid.

theorem Prince1983.nucleus_of_light {w : List Prosody.Syllable.Weight} (h : ∀ m ∈ w, m < 2) (k : ℕ) : nucleus w k = min k w.length

theorem Prince1983.lastIdx?_replicate_one (n : ℕ) : lastIdx? (fun (x : ℕ) => decide (2 ≤ x)) (List.replicate n 1) = none

theorem Prince1983.lastIdx?_replicate_one_pos (n : ℕ) : lastIdx? (fun (x : ℕ) => decide (1 ≤ x)) (List.replicate (n + 1) 1) = some n

The three kinds of quantity-sensitive system without alternation (97), (98)

def Prince1983.opposite : Edge → Edge

The opposite edge, Ē of (97).

Equations

• Prince1983.opposite Edge.left = Edge.right
• Prince1983.opposite Edge.right = Edge.left

def Prince1983.fixedStress (e : Edge) (fco : Bool) (w : List Prosody.Syllable.Weight) : Prosody.Grid

Fixed stress, (97) I, applies QS, ER(E;Σ) and ER(E;Wd), so the edge syllable and every heavy syllable are stressed and the edge-most stress is the main stress.

Equations

• Prince1983.fixedStress e fco w = Prince1983.endRule e 3 fco (Prince1983.endRule e 2 fco (Prince1983.qs w))

def Prince1983.defaultOpposite (e : Edge) (w : List Prosody.Syllable.Weight) : Prosody.Grid

The system of (97) II, E defaulting to Ē, applies QS, ER(Ē;Σ) and ER(E;Wd), putting main stress on the E-most heavy syllable or, lacking heavies, on the Ē syllable.

Equations

• Prince1983.defaultOpposite e w = Prince1983.endRule e 3 false (Prince1983.endRule (Prince1983.opposite e) 2 false (Prince1983.qs w))

def Prince1983.defaultSame (e : Edge) (w : List Prosody.Syllable.Weight) : Prosody.Grid

The system of (97) III, E defaulting to E, applies QS and then ER(E;Wd) to the highest level present, putting main stress on the E-most heavy syllable or, lacking heavies, on the E syllable.

Equations

• Prince1983.defaultSame e w = Prince1983.endRule e 3 false (Prince1983.qs w)

theorem Prince1983.khalkha_heavy {w : List Prosody.Syllable.Weight} {k : ℕ} (hk : List.findIdx? (fun (x : Prosody.Syllable.Weight) => decide (2 ≤ x)) w = some k) : MainStressAt (defaultSame Edge.left w) (nucleus w k)

In Khalkha Mongolian, Fore and Yana, (98) III.i, main stress falls on the first heavy syllable.

theorem Prince1983.khalkha_light {w : List Prosody.Syllable.Weight} (hw : w ≠ []) (hl : ∀ m ∈ w, m < 2) : MainStressAt (defaultSame Edge.left w) 0

Lacking heavy syllables, main stress falls on the first syllable ((98) III.i).

theorem Prince1983.aguacatec_heavy {w : List Prosody.Syllable.Weight} {k : ℕ} (hk : lastIdx? (fun (x : ℕ) => decide (2 ≤ x)) w = some k) : MainStressAt (defaultSame Edge.right w) (nucleus w k)

In Aguacatec and Golin, (98) III.ii, main stress falls on the last heavy syllable.

theorem Prince1983.aguacatec_light {w : List Prosody.Syllable.Weight} (hw : w ≠ []) (hl : ∀ m ∈ w, m < 2) : MainStressAt (defaultSame Edge.right w) (nucleus w (w.length - 1))

Lacking heavy syllables, main stress falls on the last syllable ((98) III.ii).

theorem Prince1983.lastIdx?_endRule_left {g : Prosody.Grid} (hg : ∀ x ∈ g, 1 ≤ x ∧ x ≤ 2) (hne : g ≠ []) : lastIdx? (fun (x : ℕ) => decide (2 ≤ x)) (endRule Edge.left 2 false g) = (Option.map (fun (x : ℕ) => x + 1) (lastIdx? (fun (x : ℕ) => decide (2 ≤ x)) (List.tail g))).or (some 0)

After the End Rule stresses the initial syllable, the last stress is the last stress of the rest of the word, or the initial syllable itself.

theorem Prince1983.lastIdx?_endRule_left_of_some {g : Prosody.Grid} (hg : ∀ x ∈ g, 1 ≤ x ∧ x ≤ 2) {p : ℕ} (hp : lastIdx? (fun (x : ℕ) => decide (2 ≤ x)) g = some p) : lastIdx? (fun (x : ℕ) => decide (2 ≤ x)) (endRule Edge.left 2 false g) = some p

The End Rule at the initial edge leaves the last stress where it is.

theorem Prince1983.cheremis_heavy {w : List Prosody.Syllable.Weight} {k : ℕ} (hk : lastIdx? (fun (x : ℕ) => decide (2 ≤ x)) w = some k) : MainStressAt (defaultOpposite Edge.right w) (nucleus w k)

In Classical Arabic, Eastern Cheremis, Chuvash, Hindi, Huasteco and Dongolese Nubian, (98) II.i, main stress falls on the last heavy syllable.

theorem Prince1983.cheremis_light {w : List Prosody.Syllable.Weight} (hw : w ≠ []) (hl : ∀ m ∈ w, m < 2) : MainStressAt (defaultOpposite Edge.right w) 0

Lacking heavy syllables, main stress falls on the first syllable ((98) II.i).

theorem Prince1983.endRule_right_qs (v : List Prosody.Syllable.Weight) (m : Prosody.Syllable.Weight) : endRule Edge.right 2 false (qs (v ++ [m])) = if 2 ≤ m then qs (v ++ [m]) else qs v ++ [2]

The End Rule leaves a heavy final syllable alone and stresses a light one.

theorem Prince1983.komi_heavy {w : List Prosody.Syllable.Weight} {k : ℕ} (hk : List.findIdx? (fun (x : Prosody.Syllable.Weight) => decide (2 ≤ x)) w = some k) : MainStressAt (defaultOpposite Edge.left w) (nucleus w k)

In Komi, (98) II.ii, main stress falls on the first heavy syllable.

theorem Prince1983.komi_light {v : List Prosody.Syllable.Weight} {m : Prosody.Syllable.Weight} (hl : ∀ x ∈ v ++ [m], x < 2) : MainStressAt (defaultOpposite Edge.left (v ++ [m])) (nucleus (v ++ [m]) v.length)

Lacking heavy syllables, main stress falls on the last syllable ((98) II.ii).

theorem Prince1983.westGreenlandic (v : List Prosody.Syllable.Weight) (m : Prosody.Syllable.Weight) : MainStressAt (fixedStress Edge.right false (v ++ [m])) (nucleus (v ++ [m]) v.length)

In West Greenlandic Eskimo, (98) I.ii, the last syllable is stressed and carries the main stress, whether heavy or light.

theorem Prince1983.findIdx?_endRule_left_fco {g : Prosody.Grid} (hg : ∀ x ∈ g, 1 ≤ x ∧ x ≤ 2) (hne : g ≠ []) : List.findIdx? (fun (x : ℕ) => decide (2 ≤ x)) (endRule Edge.left 2 true g) = some 0

The initial syllable is stressed under Forward Clash Override.

theorem Prince1983.koya {w : List Prosody.Syllable.Weight} (hw : w ≠ []) : MainStressAt (fixedStress Edge.left true w) 0

In Koya, (98) I.i, the first syllable is stressed, with Forward Clash Override, and carries the main stress.

theorem Prince1983.malayalam_first {m : Prosody.Syllable.Weight} {w : List Prosody.Syllable.Weight} (h : ¬(m < 2 ∧ ∃ m₁ ∈ w.head?, 2 ≤ m₁)) : MainStressAt (fixedStress Edge.left false (m :: w)) 0

In Malayalam (§3.7) the first syllable carries the main stress unless it is light and the second heavy, the End Rule being blocked by clash there.

theorem Prince1983.malayalam_second {m₀ m₁ : Prosody.Syllable.Weight} {w : List Prosody.Syllable.Weight} (h₀ : m₀ < 2) (h₁ : 2 ≤ m₁) : MainStressAt (fixedStress Edge.left false (m₀ :: m₁ :: w)) 1

In Malayalam a heavy second syllable after a light first one carries the main stress.