Documentation

Linglib.Phonology.Autosegmental.Melody

Lexical melodies #

This file defines the melody of a morpheme, its underlying autosegmental contribution as a form built from lists.

A melody consists of the autosegments and slots that one morpheme sponsors, with its lexical pre-linking in melody-local coordinates. Pre-linking is a matter of analysis. A melody with no lines is the universally unlinked underlying form of harmonic serialism, and a partially linked one is a stratal form such as /M^H/. The valued, unvalued, and floating autosegments of Rolle's typology of grammatical tone are the linked slots, the unlinked slots, and the floating autosegments of a candidate. A word is the product of the melodies of its morphemes in the concatenation monoid, as in the Generalized Nonlinear Affixation program.

Main definitions #

Implementation notes #

Consistency of Exponence, that GEN never alters morphemic affiliation, holds by the typing of Candidate, whose tiers are those of its form.

References #

def Autosegmental.Form.melody {S : Type u_1} {T : Type u_2} {M : Type u_3} (m : M) (tones : List T) (tbus : List S) (links : Finset (ℕ × ℕ)) :
Form S T M

melody m tones tbus links is the form of the morpheme m, with the autosegments tones over the slots tbus and the pre-links links in melody-local coordinates, given as pairs of positions.

Equations
  • One or more equations did not get rendered due to their size.
Instances For
    @[simp]
    theorem Autosegmental.Form.melody_upper {S : Type u_1} {T : Type u_2} {M : Type u_3} (m : M) (tones : List T) (tbus : List S) (links : Finset (ℕ × ℕ)) :
    (melody m tones tbus links).upper = List.map (fun (x : T) => { value := x, morpheme := m }) tones
    @[simp]
    theorem Autosegmental.Form.melody_lower {S : Type u_1} {T : Type u_2} {M : Type u_3} (m : M) (tones : List T) (tbus : List S) (links : Finset (ℕ × ℕ)) :
    (melody m tones tbus links).lower = List.map (fun (x : S) => { value := x, morpheme := m }) tbus
    @[simp]
    theorem Autosegmental.Form.melody_upper_morpheme {S : Type u_1} {T : Type u_2} {M : Type u_3} (m : M) (tones : List T) (tbus : List S) (links : Finset (ℕ × ℕ)) (k : Fin (melody m tones tbus links).upper.length) :
    (melody m tones tbus links).upper[k].morpheme = m

    Every autosegment of a melody is sponsored by its morpheme.

    @[simp]
    theorem Autosegmental.Form.melody_lower_morpheme {S : Type u_1} {T : Type u_2} {M : Type u_3} (m : M) (tones : List T) (tbus : List S) (links : Finset (ℕ × ℕ)) (i : Fin (melody m tones tbus links).lower.length) :
    (melody m tones tbus links).lower[i].morpheme = m

    Every slot of a melody is sponsored by its morpheme.