Search and copy

A search-and-copy rule is the Harmonic Search-and-Copy procedure of Nevins: a needy segment, one unspecified for a feature, searches in one direction for the closest segment visible to it and copies that segment's value, or the opposite value for dissimilation, and takes a last-resort default when the search fails. The procedure is stated by its visibility predicate, direction and feature; a target may further require its source to meet a condition of its own, and a visible source failing it halts the search with the default, which is defective intervention, since the search gets no second chance. A copied value is donated onward, so harmony iterates morpheme by morpheme, and every visible valued segment donates whether or not it searches itself. Mailhot and Reiss's SEARCH and COPY rule components, as Bale and Reiss present them, are a sibling formulation with simultaneous application over the input. Belth's learner constructs one, written Rel(A, F) / C __ ∘ proj(·, T) with A the targets, C the sources and T the visible segments, and Nevins reads Rose and Walker's blockers and transparent segments as defective interveners and invisible segments.

Run over a word, the rule is a Mealy machine on the visible segments whose state is the closest visible segment read so far (SearchCopy.toMealy), the memory window of Burness, McMullin and Nevins's tier-based strictly local reading of the procedure, and when the write keeps a segment visible the output tier-based strictly 2-local rule of Burness and McMullin computes the same function (SearchCopy.toOSLRule_applyOnTier). So such a rule for one feature in one direction is a tier-based strictly local function, the result of Andersson, Dolatian and Hao that Burness, McMullin and Nevins report. Every rule is subsequential in its direction over a finite alphabet (SearchCopy.apply_isSubsequential), as Gainor, Lai and Heinz found of Nevins's analyses.

Main definitions

• SearchCopy: a rule, with its visible segments, targets, sources, relation, lens on the feature, default and direction.
• SearchCopy.scan, SearchCopy.apply: the left-to-right run over the visible segments, and the run in the rule's direction.
• SearchCopy.sourceAfter, SearchCopy.sourceValue: the closest visible segment of a string and the value it offers to what follows.
• SearchCopy.toMealy, SearchCopy.toOSLRule: the machine and the OSL rule computing the run.

Main results

• SearchCopy.toOSLRule_applyOnTier: the OSL rule run with its window over the visible output is the Mealy run, when the write keeps a segment visible.
• SearchCopy.filter_scan: restricted to the visible segments, the run is the 2-OSL rule.
• SearchCopy.apply_isSubsequential, SearchCopy.scan_isMealyComputable: the run is finite-state in the rule's direction over a finite alphabet.

Implementation notes

The window holds the last visible output segment, so a copied value is donated onward, as Nevins's derivations of stacked Turkish suffixes show; Burness, McMullin and Nevins instead model the procedure by an input-oriented function with the needy segments off the tier, which agrees whenever a needy segment's nearest visible source precedes it in the input, and the run is Nevins's cyclic derivation only where morphological order runs away from the root in the search direction. IsSource is more general than Nevins's conditions on a source, which are identity for an orthogonal feature or morphological affiliation. A source unspecified for the feature yields the default, where Belth counts a failed application, and a default of none, outside both sources, leaves a failed target unspecified for the fixed-point results of Harmony.System. The lens laws hold on targets only, since only targets are written. Not modelled are search in both directions at once, sonority hurdles, the distance parameters of Nevins's fifth chapter, more than one feature per search, and the patterns Burness, McMullin and Nevins place beyond the procedure: icy targets, persistent search and circumambient harmony.

References

• [Nev10]
• [BR18]
• [BMcMN24]
• [BMcM19]
• [CEH15]
• [Bel26]
• [RW11]

inductive Phonology.SearchCopy.Relation : Type

Whether a target copies its source's value or, for dissimilation, the opposite value.

• agree : Relation
• disagree : Relation

@[instance_reducible]

instance Phonology.SearchCopy.instDecidableEqRelation : DecidableEq Relation

Equations

• Phonology.SearchCopy.instDecidableEqRelation x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

@[instance_reducible]

instance Phonology.SearchCopy.instReprRelation : Repr Relation

Equations

• Phonology.SearchCopy.instReprRelation = { reprPrec := Phonology.SearchCopy.instReprRelation.repr }

def Phonology.SearchCopy.instReprRelation.repr : Relation → ℕ → Std.Format

Equations

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

def Phonology.SearchCopy.Relation.act : Relation → Bool → Bool

The value the relation writes into a target from its source's value.

Equations

• Phonology.SearchCopy.Relation.agree.act x✝ = x✝
• Phonology.SearchCopy.Relation.disagree.act x✝ = !x✝

@[simp]

theorem Phonology.SearchCopy.Relation.act_agree (v : Bool) : agree.act v = v

@[simp]

theorem Phonology.SearchCopy.Relation.act_disagree (v : Bool) : disagree.act v = !v

structure Phonology.SearchCopy (α : Type u_1) : Type u_1

A search-and-copy rule consists of the visible segments, the targets, the sources each target may copy from, the relation, a lens reading and writing the feature on targets, a last-resort default, and a direction.

• tier : α → Prop

  The visible segments, the rule's tier.

• decTier : DecidablePred self.tier
• IsTarget : α → Prop

  The needy segments, which search.

• decTarget : DecidablePred self.IsTarget
• IsSource : α → α → Prop

  IsSource s t holds when the visible segment s may donate to the target t.

• decSource : DecidableRel self.IsSource
• relation : Relation

  Whether a target copies or negates its source's value.

• value : α → Option Bool

  The feature's value on a segment, none when the segment is unspecified for it.

• write : Bool → α → α

  The segment with the feature's value written into it.

• value_write (v : Bool) (s : α) : self.IsTarget s → self.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.value s = some v → self.write v s = s

  Writing the value a target already carries leaves it unchanged.

• default : Option Bool

  The last-resort value a target takes when its search fails.

• direction : Edge

  The direction of search, a rightward search scanning right to left.

def Phonology.SearchCopy.found {α : Type u_1} (r : SearchCopy α) (t : α) (w : Option α) : Option Bool

The value the target t finds in the window w, the window segment's value when it may donate to t.

Equations

• r.found t w = w.bind fun (c : α) => if r.IsSource c t then r.value c else none

def Phonology.SearchCopy.copied {α : Type u_1} (r : SearchCopy α) (t : α) (w : Option α) : Option Bool

The value the search of t yields from the window w, the default when it finds nothing.

Equations

• r.copied t w = (Option.map r.relation.act (r.found t w)).or r.default

def Phonology.SearchCopy.emit {α : Type u_1} (r : SearchCopy α) (w : Option α) (s : α) : α

The segment output at s with the window w.

Equations

• r.emit w s = if r.IsTarget s then (r.copied s w).elim s fun (x : Bool) => r.write x s else s

def Phonology.SearchCopy.TierClosed {α : Type u_1} (r : SearchCopy α) : Prop

The write keeps a visible segment visible.

Equations

• r.TierClosed = ∀ (v : Bool) (s : α), r.tier s → r.tier (r.write v s)

@[simp]

theorem Phonology.SearchCopy.found_none {α : Type u_1} (r : SearchCopy α) (t : α) : r.found t none = none

@[simp]

theorem Phonology.SearchCopy.found_some {α : Type u_1} (r : SearchCopy α) (t c : α) : r.found t (some c) = if r.IsSource c t then r.value c else none

theorem Phonology.SearchCopy.found_some_of_isSource {α : Type u_1} (r : SearchCopy α) {t c : α} (h : r.IsSource c t) : r.found t (some c) = r.value c

theorem Phonology.SearchCopy.found_some_of_not_isSource {α : Type u_1} (r : SearchCopy α) {t c : α} (h : ¬r.IsSource c t) : r.found t (some c) = none

theorem Phonology.SearchCopy.emit_of_not_isTarget {α : Type u_1} (r : SearchCopy α) {s : α} (h : ¬r.IsTarget s) (w : Option α) : r.emit w s = s

theorem Phonology.SearchCopy.emit_of_isTarget {α : Type u_1} (r : SearchCopy α) {s : α} (h : r.IsTarget s) (w : Option α) : r.emit w s = (r.copied s w).elim s fun (x : Bool) => r.write x s

theorem Phonology.SearchCopy.emit_of_found_eq_none {α : Type u_1} (r : SearchCopy α) (hd : r.default = none) {s : α} {w : Option α} (hf : r.found s w = none) : r.emit w s = s

A target whose search finds nothing is left unchanged when there is no default.

theorem Phonology.SearchCopy.emit_eq_self {α : Type u_1} (r : SearchCopy α) {s : α} {w : Option α} {v : Bool} (hf : r.found s w = some v) (h : r.value s = some (r.relation.act v)) : r.emit w s = s

A target already carrying the value its search finds is emitted unchanged.

The run

def Phonology.SearchCopy.toMealy {α : Type u_1} (r : SearchCopy α) : Mealy (Option α) α α

The machine computing the rule, whose state is the closest visible segment read so far and which passes invisible segments through untouched.

Equations

• r.toMealy = { start := none, step := fun (w : Option α) (s : α) => if r.tier s then some (r.emit w s) else w, output := fun (w : Option α) (s : α) => if r.tier s then r.emit w s else s }

@[simp]

theorem Phonology.SearchCopy.toMealy_start {α : Type u_1} (r : SearchCopy α) : r.toMealy.start = none

@[simp]

theorem Phonology.SearchCopy.toMealy_step {α : Type u_1} (r : SearchCopy α) (w : Option α) (s : α) : r.toMealy.step w s = if r.tier s then some (r.emit w s) else w

@[simp]

theorem Phonology.SearchCopy.toMealy_output {α : Type u_1} (r : SearchCopy α) (w : Option α) (s : α) : r.toMealy.output w s = if r.tier s then r.emit w s else s

theorem Phonology.SearchCopy.toMealy_runFrom_cons_of_tier {α : Type u_1} (r : SearchCopy α) {x : α} (hx : r.tier x) (w : Option α) (xs : List α) : r.toMealy.runFrom w (x :: xs) = r.emit w x :: r.toMealy.runFrom (some (r.emit w x)) xs

theorem Phonology.SearchCopy.toMealy_runFrom_cons_of_not_tier {α : Type u_1} (r : SearchCopy α) {x : α} (hx : ¬r.tier x) (w : Option α) (xs : List α) : r.toMealy.runFrom w (x :: xs) = x :: r.toMealy.runFrom w xs

def Phonology.SearchCopy.scan {α : Type u_1} (r : SearchCopy α) : List α → List α

The left-to-right run over the visible segments, in which each target copies from the closest visible segment before it.

Equations

• r.scan = r.toMealy.run

theorem Phonology.SearchCopy.scan_eq_runFrom {α : Type u_1} (r : SearchCopy α) (w : List α) : r.scan w = r.toMealy.runFrom none w

def Phonology.SearchCopy.apply {α : Type u_1} (r : SearchCopy α) : List α → List α

The run in the rule's direction.

Equations

• r.apply = match (motive := Edge → List α → List α) r.direction with | Edge.left => r.toMealy.run | Edge.right => r.toMealy.runRight

def Phonology.SearchCopy.sourceAfter {α : Type u_1} (r : SearchCopy α) (w : List α) : Option α

The closest visible segment of a string for a target that follows it in the rule's direction.

Equations

• r.sourceAfter w = match r.direction with | Edge.left => r.toMealy.stateAfter none w | Edge.right => r.toMealy.stateAfter none w.reverse

def Phonology.SearchCopy.sourceValue {α : Type u_1} (r : SearchCopy α) (w : List α) : Option Bool

The value a string offers to a target that follows it in the rule's direction.

Equations

• r.sourceValue w = (r.sourceAfter w).bind r.value

@[simp]

theorem Phonology.SearchCopy.scan_nil {α : Type u_1} (r : SearchCopy α) : r.scan [] = []

@[simp]

theorem Phonology.SearchCopy.length_scan {α : Type u_1} (r : SearchCopy α) (w : List α) : (r.scan w).length = w.length

@[simp]

theorem Phonology.SearchCopy.length_apply {α : Type u_1} (r : SearchCopy α) (w : List α) : (r.apply w).length = w.length

theorem Phonology.SearchCopy.scan_isMealyComputable {α : Type u_1} (r : SearchCopy α) [Fintype α] : IsMealyComputable r.scan

theorem Phonology.SearchCopy.scan_isLeftSubsequential {α : Type u_1} (r : SearchCopy α) [Fintype α] : IsLeftSubsequential r.scan

theorem Phonology.SearchCopy.apply_isSubsequential {α : Type u_1} (r : SearchCopy α) [Fintype α] : IsSubsequential r.direction r.apply

The rule's string function is subsequential in the rule's direction over a finite alphabet.

The run as a tier-based OSL rule

theorem Phonology.SearchCopy.tier_emit {α : Type u_1} (r : SearchCopy α) (hw : r.TierClosed) {s : α} (hs : r.tier s) (w : Option α) : r.tier (r.emit w s)

def Phonology.SearchCopy.toOSLRule {α : Type u_1} (r : SearchCopy α) : Subregular.OSLRule 2 α α

The rule as a 2-OSL rule ([CEH15]) in which each visible target copies from the previous output segment and invisible segments pass through.

Equations

• r.toOSLRule = { windowOutput := fun (window : List α) (s : α) => if r.tier s then [r.emit window.getLast? s] else [s] }

@[simp]

theorem Phonology.SearchCopy.toOSLRule_windowOutput {α : Type u_1} (r : SearchCopy α) (window : List α) (s : α) : r.toOSLRule.windowOutput window s = if r.tier s then [r.emit window.getLast? s] else [s]

theorem Phonology.SearchCopy.toOSLRule_applyOnTier {α : Type u_1} (r : SearchCopy α) (hw : r.TierClosed) : r.toOSLRule.applyOnTier r.tier = r.scan

Run with its window over the visible output ([BMcM19]), the OSL rule is the Mealy run, the last visible output segment being the machine's state, provided the write keeps a segment visible.

theorem Phonology.SearchCopy.filter_scan {α : Type u_1} (r : SearchCopy α) (hw : r.TierClosed) (w : List α) : List.filter (fun (x : α) => decide (r.tier x)) (r.scan w) = r.toOSLRule.apply (List.filter (fun (x : α) => decide (r.tier x)) w)

Restricted to the visible segments, the run is the 2-OSL rule, provided the write keeps a segment visible.