A skeleton is strict when it is a sequence of CV units.
The definition is too large to print here; read it in the source.
Used by instDecidableIsStrict
Used in LaoideKemp2026
Docs / Phonology / StrictCV / Skeleton
Strict CV skeletons
import Linglib.Phonology.StrictCV.Skeleton · namespace StrictCV
A strict-CV skeleton is a sequence of CV units, consonantal and vocalic slots in strict
alternation. The units of a form are numbered from the left, unit j having its onset at slot
2j and its nucleus at slot 2j + 1. A candidate presents the profile that the lateral
computation reads: the nuclei that host melody, and the units whose onset may be governed by the
next onset, as two consonants that contract infrasegmental government. A nucleus of a candidate
has associated melody or none, since a floating object is linked to no slot.
Main definitions
StrictCV.IsStrict: the skeleton is a sequence of CV units.StrictCV.units,StrictCV.onset,StrictCV.nucleus: the CV units and their slots.StrictCV.hosting,StrictCV.clusters: the nuclei of a candidate that host melody, and the units whose onsets may contract infrasegmental government.StrictCV.nucleusOf,StrictCV.surface: the nuclei of a candidate as the lateral computation reads them, those hosting melody pronounced.
References
- Lowenstamm 1996, CV as the Only Syllable Type
- Scheer 2004, A Lateral Theory of Phonology: What is CVCV and Why Should It Be? formalized
Declarations
{T : Type u_1} {M : Type u_2} (u : Autosegmental.Form Autosegmental.Slot T M) :
Decidable (IsStrict u)
Built from
The number of CV units.
Used by onset, nucleus, hosting, clusters, nucleusOf, surface, mem_hosting
Used in LaoideKemp2026
The onset of CV unit j.
{T : Type u_1} {M : Type u_2} (u : Autosegmental.Form Autosegmental.Slot T M) (j : Fin (units u)) :
Fin u.lower.length
- onset u j = ⟨2 * ↑j, ⋯⟩
Built from
Used in LaoideKemp2026
The nucleus of CV unit j.
{T : Type u_1} {M : Type u_2} (u : Autosegmental.Form Autosegmental.Slot T M) (j : Fin (units u)) :
Fin u.lower.length
- nucleus u j = ⟨2 * ↑j + 1, ⋯⟩
Built from
Used by hosting, mem_hosting
Used in LaoideKemp2026
The nuclei that host an object satisfying P on the surface.
{T : Type u_1} {M : Type u_2} {u : Autosegmental.Form Autosegmental.Slot T M} (c : Autosegmental.Candidate u) (P : T → Prop) [DecidablePred P] :
Finset (Fin (units u))
- hosting c P = {j : Fin (units u) | ∃ t ∈ c.tierValues (nucleus u j), P t}
Built from ,
Used by nucleusOf, surface, mem_hosting
The units whose onset may be governed by the next onset, given which melodies MayGovern
allows to contract infrasegmental government (Scheer 2004 (49a)).
{T : Type u_1} {M : Type u_2} {u : Autosegmental.Form Autosegmental.Slot T M} (c : Autosegmental.Candidate u) (MayGovern : List T → List T → Prop) [(a b : List T) → Decidable (MayGovern a b)] :
Finset (Fin (units u))
The definition is too large to print here; read it in the source.
Built from
Used in LaoideKemp2026
The nucleus of CV unit j, with associated melody when it hosts an object satisfying P, and
between consonants that may contract infrasegmental government when j ∈ cl.
{T : Type u_1} {M : Type u_2} {u : Autosegmental.Form Autosegmental.Slot T M} (c : Autosegmental.Candidate u) (P : T → Prop) [DecidablePred P] (cl : Finset (Fin (units u))) (j : Fin (units u)) :
- nucleusOf c P cl j = { melody := if j ∈ hosting c P then Melody.associated else Melody.empty, cluster := decide (j ∈ cl) }
Built from ,
Used by surface
The nuclei of a candidate as its surface presents them, those hosting an object satisfying P
pronounced.
{T : Type u_1} {M : Type u_2} {u : Autosegmental.Form Autosegmental.Slot T M} (c : Autosegmental.Candidate u) (P : T → Prop) [DecidablePred P] (cl : Finset (Fin (units u))) :
List (Nucleus × Bool)
- surface c P cl = List.ofFn fun (j : Fin (units u)) => (nucleusOf c P cl j, decide (j ∈ hosting c P))
Built from , ,
{T : Type u_1} {M : Type u_2} {u : Autosegmental.Form Autosegmental.Slot T M} {c : Autosegmental.Candidate u} {P : T → Prop} [DecidablePred P] {j : Fin (units u)} :
Built from , ,