Docs / Phonology / Autosegmental / IntervalOrder

Representations in time

import Linglib.Phonology.Autosegmental.IntervalOrder · namespace Autosegmental

Source

Read in time, the order of each tier is precedence and an association line is overlap. A representation has an interval order when some interval order on its positions extends the order of each tier and leaves associated positions incomparable. The 2 + 2 condition of an interval order is the No-Crossing Constraint between two tiers, and when lines join only tiers adjacent in a forest, every non-crossing representation has an interval order. Around a cycle of three tiers, lines that cross none pairwise can chain into a precedence that no interval order admits.

Main definitions

Main results

Implementation notes

A representation fixes precedence only within tiers, so a floating tone and a toneless timing slot can be ordered either way: a representation has interval orders, generally many, and is not one. The least precedence it forces is not an interval order in general, since two tiers without lines form a 2 + 2. The intervals for a forest of tiers are built one leaf tier at a time, each step passing to the lexicographic product of the previous line of time with ℕ.

References

Relations between two tiers

A relation whose pairs are overlaps of intervals placed in tier order is non-crossing (Sagey 1988's derivation of the No-Crossing Constraint).

theorem IsNonCrossing.of_intervalsL62–70
{ι : Type u_1} {κ : Type u_2} {T : Type u_3} [Preorder ι] [LinearOrder κ] [LinearOrder T] {R : SetRel ι κ} {I : ι → NonemptyInterval T} {J : κ → NonemptyInterval T} (hI : ∀ ⦃a b : ι⦄, a < b → (I a).Precedes (I b)) (hJ : ∀ ⦃a b : κ⦄, a < b → (J a).Precedes (J b)) (hR : ∀ x ∈ R, (I x.1).Overlaps (J x.2)) :
IsNonCrossing R

Representations

X has an interval order: an interval order on its positions that extends the order of each tier and leaves associated positions incomparable.

def AR.HasIntervalOrderL81–86
{ι : Type u_1} {τ : ι → Type u_2} (X : AR τ) :
Prop

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

Used by AR.hasIntervalOrder_of_intervals, AR.HasIntervalOrder.noCrossing, AR.noCrossing_iff_hasIntervalOrder_of_isAcyclic, AR.noCrossing_iff_hasIntervalOrder, AR.exists_noCrossing_not_hasIntervalOrder

Used in BirdKlein1990

L90–94

On a cycle of three tiers the converse fails: with each tier's first position linked to the next tier's second, no two lines cross, yet the precedences chain from the last tier's first position to the first tier's second, to which it is linked.

theorem AR.exists_noCrossing_not_hasIntervalOrderL193–207
:
∃ (X : AR fun (x : Fin 3) => Unit), X.NoCrossing ∧ ¬X.HasIntervalOrder

Built from