Documentation

Linglib.Phonology.Harmony.System

Harmony systems #

A harmony system is Rose and Walker's descriptive object: a Phonology.Harmony.Pattern, whose participation classes are the triggers, blockers and transparent segments, together with the targets and a write of the harmonic value into them. It commits to no mechanism. Its search-and-copy reading (System.searchCopy) is Nevins's procedure with the pattern's tier as the visible segments, its participating segments as the sources and its direction as the direction of search; the rival accounts, Goldsmith's autosegmental spreading, Rose and Walker's Agreement by Correspondence and OT alignment, are not derived here. Under that reading a harmonic word is a fixed point of the run (System.scan_eq_self_of_harmonic), and on a saturated system the fixed points are exactly the harmonic words (System.harmonic_iff_scan_eq_self), the TSL₂ language of Pattern.harmonic_iff_mem_tsl.

Main definitions #

System: a pattern, its targets and its write; System.mk' compiles the Rose and Walker roles over Phonology.Segment.
System.searchCopy: the search-and-copy reading of a system.
System.Saturated: every visible segment is a participating target with a value.

Main results #

System.scan_eq_self_of_harmonic, System.harmonic_iff_scan_eq_self, System.harmonic_scan: the run's fixed points and image against the pattern's surface harmonicity.
System.scan_eq_map: on a saturated system the run writes the first visible segment's value into every visible segment.

Implementation notes #

Under the search-and-copy reading a blocker is a visible non-source: the search stops at it and the target takes the default, as in Nevins's defective intervention and Belth's Khalkha rule. Ritter and van der Hulst's reading, on which a blocker imposes its own value, is the case where the blocker's pattern value is the default; Pattern.Harmonic follows that reading, so the fixed-point results assume no default and blockers that are not targets. Every participating segment donates whether or not it is a target, as Nevins requires. An icy target is a target that is not a source, which the reading expresses because participation is stored on the segment; on bare segments Burness, McMullin and Nevins show that search and copy cannot. A bidirectional pattern is run left to right; the outward-from-root pass is not modelled. A single tier is not always enough: Uyghur backness harmony is not TSL, as Mayer and Major show.

References #

def Phonology.Harmony.Direction.scanEdge :

Direction → Edge

The edge a pattern's scan starts from, bidirectional patterns being run from the left.

Equations

Instances For

Systems #

structure Phonology.Harmony.System (α : Type u_1) :

Type u_1

A harmony system consists of a pattern, the targets, a write of the harmonic value into a target, which with the pattern's valuation forms a lens on the targets, and a last-resort default.

pattern : Pattern α Bool
The descriptive pattern.
IsTarget : α → Prop
The segments that undergo.
decTarget : DecidablePred self.IsTarget
write : Bool → α → α
The segment with the harmonic value written into it.
value_write (v : Bool) (s : α) : self.IsTarget s → self.pattern.value (self.write v s) = some v
Reading back a value written into a target gives that value.
write_value (v : Bool) (s : α) : self.IsTarget s → self.pattern.value s = some v → self.write v s = s
Writing the value a target already carries leaves it unchanged.
default : Option Bool
The value a target takes when no source reaches it.

Instances For

def Phonology.Harmony.System.searchCopy {α : Type u_1} (sys : System α) :

The search-and-copy reading of a system takes the pattern's tier as the visible segments, its participating segments as the sources, and its direction as the direction of search.

Equations

One or more equations did not get rendered due to their size.

Instances For

@[simp]

theorem Phonology.Harmony.System.searchCopy_tier {α : Type u_1} (sys : System α) :

sys.searchCopy.tier = sys.pattern.OnTier

@[simp]

theorem Phonology.Harmony.System.searchCopy_isTarget {α : Type u_1} (sys : System α) :

sys.searchCopy.IsTarget = sys.IsTarget

@[simp]

theorem Phonology.Harmony.System.searchCopy_isSource {α : Type u_1} (sys : System α) (s t : α) :

sys.searchCopy.IsSource s t ↔ sys.pattern.participation s = Participation.participating

@[simp]

theorem Phonology.Harmony.System.searchCopy_value {α : Type u_1} (sys : System α) :

sys.searchCopy.value = sys.pattern.value

@[simp]

theorem Phonology.Harmony.System.searchCopy_write {α : Type u_1} (sys : System α) :

sys.searchCopy.write = sys.write

@[simp]

theorem Phonology.Harmony.System.searchCopy_default {α : Type u_1} (sys : System α) :

sys.searchCopy.default = sys.default

@[simp]

theorem Phonology.Harmony.System.searchCopy_direction {α : Type u_1} (sys : System α) :

sys.searchCopy.direction = sys.pattern.direction.scanEdge

theorem Phonology.Harmony.System.found_some_of_participating {α : Type u_1} (sys : System α) {a : α} (h : sys.pattern.participation a = Participation.participating) (t : α) :

sys.searchCopy.found t (some a) = sys.pattern.value a

theorem Phonology.Harmony.System.found_some_of_not_participating {α : Type u_1} (sys : System α) {a : α} (h : sys.pattern.participation a ≠ Participation.participating) (t : α) :

sys.searchCopy.found t (some a) = none

@[simp]

theorem Phonology.Harmony.System.searchCopy_relation {α : Type u_1} (sys : System α) :

sys.searchCopy.relation = SearchCopy.Relation.agree

theorem Phonology.Harmony.System.emit_eq_write_of_found_eq_some {α : Type u_1} (sys : System α) {s : α} (h : sys.IsTarget s) {w : Option α} {v : Bool} (hf : sys.searchCopy.found s w = some v) :

sys.searchCopy.emit w s = sys.write v s

def Phonology.Harmony.System.mk' (feature : Feature) (IsTarget IsTransparent : Segment → Prop) [DecidablePred IsTarget] [DecidablePred IsTransparent] (direction : Direction := Direction.rightward) (IsBlocker : Segment → Prop := fun (x : Segment) => False) [DecidablePred IsBlocker] (default : Option Bool := none) :

Compiles the [RW11] roles over Phonology.Segment from the harmonic feature, the targets, the transparent segments, the direction, the blockers, and the default; every other segment is a trigger.

Equations

One or more equations did not get rendered due to their size.

Instances For

Fixed points and image #

theorem Phonology.Harmony.System.scan_eq_self_of_harmonic {α : Type u_1} (sys : System α) (hd : sys.default = none) (hb : ∀ (s : α), sys.pattern.participation s = Participation.opaque → ¬sys.IsTarget s) {w : List α} (h : sys.pattern.Harmonic w) :

sys.searchCopy.scan w = w

A harmonic word is a fixed point of the run, provided there is no default and blockers do not undergo.

def Phonology.Harmony.System.Saturated {α : Type u_1} (sys : System α) :

A system is saturated when every visible segment is a participating target with a value; on such a system the run decides the surface language.

Equations

One or more equations did not get rendered due to their size.

Instances For

theorem Phonology.Harmony.System.harmonic_iff_scan_eq_self {α : Type u_1} (sys : System α) (hs : sys.Saturated) (hd : sys.default = none) (hb : ∀ (s : α), sys.pattern.participation s = Participation.opaque → ¬sys.IsTarget s) (w : List α) :

sys.pattern.Harmonic w ↔ sys.searchCopy.scan w = w

On a saturated system without a default the harmonic words are exactly the fixed points of the run.

theorem Phonology.Harmony.System.scan_eq_map {α : Type u_1} (sys : System α) (hs : sys.Saturated) (hw : sys.searchCopy.TierClosed) (hd : sys.default = none) (w : List α) :

sys.searchCopy.scan w = List.map (fun (s : α) => if sys.pattern.OnTier s then ((sys.pattern.tier w).head?.bind sys.pattern.value).elim s fun (x : Bool) => sys.write x s else s) w

On a saturated system without a default whose writes stay visible, the run writes the first visible segment's value into every visible segment.

theorem Phonology.Harmony.System.harmonic_scan {α : Type u_1} (sys : System α) (hs : sys.Saturated) (hw : sys.searchCopy.TierClosed) (w : List α) :

sys.pattern.Harmonic (sys.searchCopy.scan w)

On a saturated system whose writes stay visible, the run's output is harmonic.