Docs / Phonology / StrictCV / Basic

Strict CV: proper government and the Empty Category Principle

import Linglib.Phonology.StrictCV.Basic · namespace StrictCV

In Strict CV the skeleton is a strict sequence of CV units, so the nuclei of a domain form a sequence. A nucleus has associated melody, floating melody, or none, and only associated melody must be pronounced. Any other nucleus may stay silent only when its silence is licensed: by proper government from the nuclei after it, by enclosure in a domain of infrasegmental government, or at the end of the domain where the language allows an empty final nucleus. This is the Empty Category Principle. Government is discharged from right to left by lateral actors: pronounced nuclei and, where the language allows it, an empty final nucleus. A realized stretch pairs each nucleus with whether it is pronounced, and the lateral relations of a nucleus are read off the stretch after it. The standard realization, computed from the right, pronounces a nucleus exactly when it has associated melody, is required, or nothing licenses its silence.

Main definitions

Main results

Implementation notes

The lateral actors are the pronounced nuclei, an epenthetic one included, as in Scheer's "only phonetically expressed Nuclei can govern and license"; Cavirani's alternative grants actorship to unpronounced nuclei with melody and is not built. An empty final nucleus either acts, governing and licensing, or does not, a single parameter, as Scheer and Ziková conclude. Government passes over a nucleus enclosed in a domain of infrasegmental government and binds the first nucleus whose silence is not licensed otherwise. Only a nucleus without melody is enclosed: a vowel that alternates with zero, a "hidden" zero, breaks up the cluster around it. Whether two consonants may contract infrasegmental government is a fact about their melody, supplied with the nucleus between them; that the governing consonant must be licensed by its own nucleus is built in. The distribution of government and licensing over onsets, which the two versions of the Coda Mirror state differently, is not modelled: proper government of nuclei is the same in both. A nucleus can be required on independent grounds, as a guttural needs a pronounced licensor or an initial empty CV unit needs a pronounced first nucleus to govern it.

References

Declarations

The melody of a nucleus (Scheer 2004 (73)). A full vowel has associated melody, a vowel that alternates with zero has floating melody, and the nucleus inside a branching onset or a coda-onset cluster has none.

inductive MelodyL74–84
  • empty : Melody

    No melody.

  • floating : Melody

    Floating melody, which associates unless the nucleus is governed.

  • associated : Melody

    Associated melody.

Derives DecidableEq, Repr.

Used by Nucleus

Used in FaustLampitelli2026

A nucleus as the lateral computation reads it.

structure NucleusL86–95
  • melody : Melody

    The melody of the nucleus.

  • forced : Bool

    The nucleus must be pronounced on independent grounds.

  • cluster : Bool

    The consonants flanking the nucleus may contract infrasegmental government, the following one governing the preceding one (Scheer 2004 (49a)).

Derives DecidableEq, Repr.

Built from

Used by Acts, Enclosed, instDecidablePredListProdNucleusBoolEnclosed, Governs, ProperlyGoverned, instDecidablePredListProdNucleusBoolProperlyGoverned, SilenceLicensed, instDecidablePredListProdNucleusBoolSilenceLicensed, SatisfiesECP, standard, standard_cons, map_fst_standard, length_standard, standard_drop, satisfiesECP_standard, Enclosed.melody_eq_empty, Enclosed.cluster_eq_true, governs_cons_iff, silenceLicensed_of_floating, standard_append_of_floating

Used in Phonology/StrictCV/Skeleton, FaustLampitelli2026, Scheer2004

How a language treats the final nucleus of a domain (Scheer & Ziková 2010 §5).

structure FinalNucleusL97–103
  • empty : Bool

    A final nucleus may stay empty.

  • acts : Bool

    An empty final nucleus is a lateral actor, governing and licensing.

Derives DecidableEq, Repr, Fintype.

Used by Acts, instDecidablePredListProdNucleusBoolActs, Governs, instDecidablePredGoverns, ProperlyGoverned, instDecidablePredListProdNucleusBoolProperlyGoverned, SilenceLicensed, instDecidablePredListProdNucleusBoolSilenceLicensed, SatisfiesECP, instDecidablePredSatisfiesECP, standard, standard_nil, standard_cons, map_fst_standard, length_standard, standard_drop, satisfiesECP_standard, governs_cons_iff, silenceLicensed_of_floating, standard_append_of_floating

Used in CaviraniVandenWyngaerd2026, FaustLampitelli2026, Scheer2004

A nucleus before a realized stretch is enclosed in a domain of infrasegmental government when it has no melody, its flanking consonants may contract government, and the governing consonant is licensed by its own nucleus, which only a pronounced nucleus can do (Scheer 2004 (49), (50)).

def EnclosedL117–123
(x : Nucleus) :
List (Nucleus × Bool) → Prop

Built from

Used by instDecidablePredListProdNucleusBoolEnclosed, Governs, instDecidablePredGoverns, ProperlyGoverned, SilenceLicensed, Enclosed.melody_eq_empty, Enclosed.cluster_eq_true, governs_cons_iff

A realized stretch governs the nucleus before it when government reaches a lateral actor, passing over enclosed nuclei only (Scheer 2004 §75).

def GovernsL129–133
(p : FinalNucleus) :
List (Nucleus × Bool) → Prop

Built from , , ,

Used by instDecidablePredGoverns, ProperlyGoverned, governs_cons_iff, silenceLicensed_of_floating, standard_append_of_floating

Used in FaustLampitelli2026

The silence of a nucleus before a realized stretch is licensed when it is properly governed, enclosed, or final where final nuclei may be empty (Scheer 2004 (53)).

def SilenceLicensedL149–152
(p : FinalNucleus) (x : Nucleus) (r : List (Nucleus × Bool)) :

Built from , , ,

Used by instDecidablePredListProdNucleusBoolSilenceLicensed, SatisfiesECP, standard_cons, silenceLicensed_of_floating

A realized stretch satisfies the Empty Category Principle when associated melody is pronounced and the silence of every silent nucleus is licensed by the nuclei after it.

def SatisfiesECPL157–162
(p : FinalNucleus) :
List (Nucleus × Bool) → Prop

Built from , ,

Used by instDecidablePredSatisfiesECP, satisfiesECP_standard

The standard realization, computed from the right: a nucleus is pronounced when it has associated melody, is required, or the nuclei after it do not license its silence.

def standardL170–174
(p : FinalNucleus) (l : List Nucleus) :
List (Nucleus × Bool)

The definition is too large to print here; read it in the source.

Built from ,

Used by standard_nil, standard_cons, map_fst_standard, length_standard, standard_drop, satisfiesECP_standard, standard_append_of_floating

Used in CaviraniVandenWyngaerd2026, FaustLampitelli2026, Scheer2004

The standard realization

The realization of the last nuclei of a domain is computed from them alone, since lateral relations are discharged from right to left.

theorem standard_dropL196–205
{p : FinalNucleus} (k : ℕ) (l : List Nucleus) :
standard p (List.drop k l) = List.drop k (standard p l)

Built from , ,

Government from the following nucleus

L235–239

Havlík's Law

In a run of floating melodies, pronunciation alternates from the right: every other one is pronounced, counting from the right edge of the run.

In a run of floating melodies before a governing stretch or a final empty non-acting nucleus, every other yer survives, counting from the right (Scheer 2004 (304)).

theorem standard_append_of_floatingL258–288
{p : FinalNucleus} {xs ys : List Nucleus} (hxs : ∀ x ∈ xs, x.melody = Melody.floating ∧ x.forced = false) (hys : Governs p (standard p ys) ∨ ys = [] ∧ p.empty = true ∧ p.acts = false) :
standard p (xs ++ ys) = List.mapIdx (fun (i : ℕ) (x : Nucleus) => (x, decide (Even (xs.length - i)))) xs ++ standard p ys

Built from , , ,