Phrase-level prosodic structure

The φ and ι layers above the prosodic word: Strict-Layer well-formedness one level up ([Sel96]; overview [IK22]). A phrase is a φ-node over well-formed ω-trees; an utterance is an ι-node over phrases. HeadUnique is the culminativity of prominence — at most one head child per node — the structural hook the metrical weak–strong calculus of [buring-2015] reads ([buring-2016]). phrases reads the φ-constituents off an utterance; φ-edges are what demarcative focus reflexes (Semantics.Focus.Reflex.boundary) realize.

def Prosody.isPhraseTree (t : Tree) : Bool

A φ-node over well-formed prosodic words: the Strict Layer at the phrase level.

Equations

• Prosody.isPhraseTree t = ((RoseTree.value t).isPh && (RoseTree.children t).all Prosody.isWordTree)

def Prosody.IsPhrase (t : Tree) : Prop

Well-formed phonological phrase.

Equations

• Prosody.IsPhrase t = (Prosody.isPhraseTree t = true)

@[implicit_reducible]

instance Prosody.instDecidableIsPhrase (t : Tree) : Decidable (IsPhrase t)

Equations

• Prosody.instDecidableIsPhrase t = Prosody.instDecidableIsPhrase._aux_1 t

def Prosody.isUtteranceTree (t : Tree) : Bool

An ι-node over well-formed phrases: the utterance level.

Equations

• Prosody.isUtteranceTree t = ((RoseTree.value t).isIota && (RoseTree.children t).all Prosody.isPhraseTree)

def Prosody.IsUtterance (t : Tree) : Prop

Well-formed intonational phrase (utterance).

Equations

• Prosody.IsUtterance t = (Prosody.isUtteranceTree t = true)

@[implicit_reducible]

instance Prosody.instDecidableIsUtterance (t : Tree) : Decidable (IsUtterance t)

Equations

• Prosody.instDecidableIsUtterance t = Prosody.instDecidableIsUtterance._aux_1 t

def Prosody.HeadUnique (t : Tree) : Prop

Culminativity of prominence: at most one child heads its parent.

Equations

• Prosody.HeadUnique t = ((List.filter (fun (c : RoseTree Prosody.Constituent) => c.value.isHead) (RoseTree.children t)).length ≤ 1)

@[implicit_reducible]

instance Prosody.instDecidableHeadUnique (t : Tree) : Decidable (HeadUnique t)

Equations

• Prosody.instDecidableHeadUnique t = Prosody.instDecidableHeadUnique._aux_1 t

def Prosody.phrases (t : Tree) : List Tree

The φ-constituents of a tree, outermost-first.

Equations

• Prosody.phrases t = Prosody.maximalProjections Prosody.Constituent.isPh t

theorem Prosody.IsPhrase.children_isWord {t : Tree} (h : IsPhrase t) (c : RoseTree Constituent) : c ∈ RoseTree.children t → IsWord c

Every child of a well-formed phrase is a well-formed word.

theorem Prosody.IsUtterance.children_isPhrase {t : Tree} (h : IsUtterance t) (c : RoseTree Constituent) : c ∈ RoseTree.children t → IsPhrase c

Every child of a well-formed utterance is a well-formed phrase.