Neighborhoods

The local environment a postsyntactic rule inspects: a focus terminal with the terminals to either side, nearest first. Vocabulary Items and Impoverishment rules are stated over the same neighborhoods. An item's site is itself a neighborhood of feature lists, and the item applies wherever each feature the site mentions sits at the same offset from the focus: the Subset Principle's inclusion of sites, ⊆.

Main definitions

• Neighborhood: focus, left context, right context.
• Neighborhood.nth: the terminal at an integer offset from the focus.
• (i, f) ∈ n: the terminal at offset i bears the feature f; s ⊆ n when every positioned feature of s is one of n.
• Neighborhood.positioned, Neighborhood.toFinset: the positioned features, listed and as a finite set.
• Neighborhood.project, Neighborhood.window: the neighborhood on a tier, and the focus with the terminals within a radius of it.
• Neighborhood.around, Neighborhood.along: the neighborhood of a position of a string, and each terminal of a string in its neighborhood.

Main results

• Neighborhood.mem_positioned: positioned lists exactly the positioned features, so it decides ⊆.
• Neighborhood.subset_iff_nth: inclusion compares terminal by terminal.
• Neighborhood.ofBundle_subset_iff: a context-free site is included where its features are on the focus.
• Neighborhood.weight_strictMono: a strictly larger site has more features on the focus, or as many there and more elsewhere, the ground of the Subset Principle's specificity.
• Neighborhood.toList_of_mem_along, Neighborhood.nth_around: each neighborhood of a string reassembles to it, and terminal k stands at offset k - i from position i.

Implementation notes

Offsets are integers, indexed as for Turing.Tape.nth: 0 is the focus, -(k + 1) the k-th terminal to the left (toward the root), k + 1 the k-th to the right (toward the clause), and past either end nth returns default, for a feature list []. Inclusion ignores the order and repetition of features on a terminal and empty terminals past the ends, so it is a preorder and not a partial order; as for PSet, the preorder is written ⊆.

A bare bundle coerces to the context-free neighborhood and ∅ is the empty site, so a context-free Vocabulary Item is written ⟨[f₁, f₂], e⟩ and the Elsewhere item ⟨∅, e⟩.

References

• M. Halle and A. Marantz, Distributed Morphology and the pieces of inflection
• M. Halle, Distributed Morphology: Impoverishment and Fission
• D. Embick, Localism versus Globalism in Morphology and Phonology
• K. Arregi and A. Nevins, Morphotactics

structure DistributedMorphology.Neighborhood (Bundle : Type u_3) : Type u_3

A neighborhood is the local context a postsyntactic rule may inspect, the focus terminal and the terminals to either side, nearest first. A condition that only inspects focus is paradigmatic; one that reads leftCtx or rightCtx is syntagmatic.

• focus : Bundle

  The terminal the rule inspects.

• leftCtx : List Bundle

  The terminals to its left, nearest first.

• rightCtx : List Bundle

  The terminals to its right, nearest first.

@[instance_reducible]

instance DistributedMorphology.instReprNeighborhood {Bundle✝ : Type u_3} [Repr Bundle✝] : Repr (Neighborhood Bundle✝)

Equations

• DistributedMorphology.instReprNeighborhood = { reprPrec := DistributedMorphology.instReprNeighborhood.repr }

def DistributedMorphology.instReprNeighborhood.repr {Bundle✝ : Type u_3} [Repr Bundle✝] : Neighborhood Bundle✝ → ℕ → Std.Format

Equations

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

def DistributedMorphology.instDecidableEqNeighborhood.decEq {Bundle✝ : Type u_3} [DecidableEq Bundle✝] (x✝ x✝¹ : Neighborhood Bundle✝) : Decidable (x✝ = x✝¹)

Equations

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

@[instance_reducible]

instance DistributedMorphology.instDecidableEqNeighborhood {Bundle✝ : Type u_3} [DecidableEq Bundle✝] : DecidableEq (Neighborhood Bundle✝)

Equations

• DistributedMorphology.instDecidableEqNeighborhood = DistributedMorphology.instDecidableEqNeighborhood.decEq

def DistributedMorphology.Neighborhood.ofBundle {Bundle : Type u_1} (fb : Bundle) : Neighborhood Bundle

A bundle, viewed as a context-free neighborhood.

Equations

• ↑fb = { focus := fb }

@[instance_reducible]

instance DistributedMorphology.Neighborhood.instCoe {Bundle : Type u_1} : Coe Bundle (Neighborhood Bundle)

Equations

• DistributedMorphology.Neighborhood.instCoe = { coe := DistributedMorphology.Neighborhood.ofBundle }

@[instance_reducible]

instance DistributedMorphology.Neighborhood.instEmptyCollection {Bundle : Type u_1} [EmptyCollection Bundle] : EmptyCollection (Neighborhood Bundle)

Equations

• DistributedMorphology.Neighborhood.instEmptyCollection = { emptyCollection := ↑∅ }

@[simp]

theorem DistributedMorphology.Neighborhood.focus_ofBundle {Bundle : Type u_1} (fb : Bundle) : (↑fb).focus = fb

@[simp]

theorem DistributedMorphology.Neighborhood.leftCtx_ofBundle {Bundle : Type u_1} (fb : Bundle) : (↑fb).leftCtx = []

@[simp]

theorem DistributedMorphology.Neighborhood.rightCtx_ofBundle {Bundle : Type u_1} (fb : Bundle) : (↑fb).rightCtx = []

@[simp]

theorem DistributedMorphology.Neighborhood.ofBundle_nil {F : Type u_2} : ↑[] = ∅

Offsets

def DistributedMorphology.Neighborhood.nth {Bundle : Type u_1} [Inhabited Bundle] (n : Neighborhood Bundle) : ℤ → Bundle

n.nth i is the terminal at offset i from the focus, where 0 is the focus, -(k + 1) the k-th terminal to the left, k + 1 the k-th to the right, and default lies past either end.

Equations

• n.nth 0 = n.focus
• n.nth (Int.ofNat k.succ) = n.rightCtx.getD k default
• n.nth (Int.negSucc k) = n.leftCtx.getD k default

@[simp]

theorem DistributedMorphology.Neighborhood.nth_zero {Bundle : Type u_1} [Inhabited Bundle] (n : Neighborhood Bundle) : n.nth 0 = n.focus

@[simp]

theorem DistributedMorphology.Neighborhood.nth_natCast_add_one {Bundle : Type u_1} [Inhabited Bundle] (n : Neighborhood Bundle) (k : ℕ) : n.nth (↑k + 1) = n.rightCtx.getD k default

@[simp]

theorem DistributedMorphology.Neighborhood.nth_neg_natCast_add_one {Bundle : Type u_1} [Inhabited Bundle] (n : Neighborhood Bundle) (k : ℕ) : n.nth (-(↑k + 1)) = n.leftCtx.getD k default

Tiers and windows

def DistributedMorphology.Neighborhood.project {Bundle : Type u_1} (T : Bundle → Prop) [DecidablePred T] (n : Neighborhood Bundle) : Neighborhood Bundle

The projection onto the tier T keeps the focus and the terminals on either side that T keeps, nearest first. Pruning null terminals is the projection onto the overt ones.

Equations

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

@[simp]

theorem DistributedMorphology.Neighborhood.focus_project {Bundle : Type u_1} (T : Bundle → Prop) [DecidablePred T] (n : Neighborhood Bundle) : (project T n).focus = n.focus

@[simp]

theorem DistributedMorphology.Neighborhood.leftCtx_project {Bundle : Type u_1} (T : Bundle → Prop) [DecidablePred T] (n : Neighborhood Bundle) : (project T n).leftCtx = List.filter (fun (b : Bundle) => decide (T b)) n.leftCtx

@[simp]

theorem DistributedMorphology.Neighborhood.rightCtx_project {Bundle : Type u_1} (T : Bundle → Prop) [DecidablePred T] (n : Neighborhood Bundle) : (project T n).rightCtx = List.filter (fun (b : Bundle) => decide (T b)) n.rightCtx

def DistributedMorphology.Neighborhood.window {Bundle : Type u_1} (k : ℕ) (n : Neighborhood Bundle) : Neighborhood Bundle

The window of radius k keeps the focus and the k terminals nearest it on either side. A condition is adjacent on the tier T when it factors through window 1 ∘ project T; the linear adjacency of [Emb10] and [AN12] is adjacency on the tier of overt terminals.

Equations

• DistributedMorphology.Neighborhood.window k n = { focus := n.focus, leftCtx := List.take k n.leftCtx, rightCtx := List.take k n.rightCtx }

@[simp]

theorem DistributedMorphology.Neighborhood.window_window {Bundle : Type u_1} (k m : ℕ) (n : Neighborhood Bundle) : window k (window m n) = window (min k m) n

theorem DistributedMorphology.Neighborhood.nth_window {Bundle : Type u_1} [Inhabited Bundle] (n : Neighborhood Bundle) {k : ℕ} {i : ℤ} (hi : i.natAbs ≤ k) : (window k n).nth i = n.nth i

The window of radius k agrees with the neighborhood up to offset k.

Neighborhoods of a string

def DistributedMorphology.Neighborhood.toList {Bundle : Type u_1} (n : Neighborhood Bundle) : List Bundle

The terminals of a neighborhood, in linear order.

Equations

• n.toList = n.leftCtx.reverse ++ n.focus :: n.rightCtx

def DistributedMorphology.Neighborhood.around {Bundle : Type u_1} (d : List Bundle) (i : ℕ) (b : Bundle) : Neighborhood Bundle

around d i b is the neighborhood of position i of the string d with b in focus, the earlier terminals to its left and the later ones to its right, nearest first.

Equations

• DistributedMorphology.Neighborhood.around d i b = { focus := b, leftCtx := (List.take i d).reverse, rightCtx := List.drop (i + 1) d }

def DistributedMorphology.Neighborhood.along {Bundle : Type u_1} (d : List Bundle) : List (Neighborhood Bundle)

Each terminal of the string d in its neighborhood, in order.

Equations

• DistributedMorphology.Neighborhood.along d = List.mapIdx (DistributedMorphology.Neighborhood.around d) d

@[simp]

theorem DistributedMorphology.Neighborhood.toList_ofBundle {Bundle : Type u_1} (b : Bundle) : (↑b).toList = [b]

@[simp]

theorem DistributedMorphology.Neighborhood.focus_around {Bundle : Type u_1} (d : List Bundle) (i : ℕ) (b : Bundle) : (around d i b).focus = b

theorem DistributedMorphology.Neighborhood.toList_around {Bundle : Type u_1} (d : List Bundle) (i : ℕ) (b : Bundle) (h : i < d.length) : (around d i b).toList = d.set i b

Reassembling the neighborhood of position i gives the string with b at i.

theorem DistributedMorphology.Neighborhood.nth_around {Bundle : Type u_1} (d : List Bundle) (i : ℕ) (b : Bundle) [Inhabited Bundle] {k : ℕ} (hi : i ≤ d.length) (hk : k ≠ i) : (around d i b).nth (↑k - ↑i) = d.getD k default

Terminal k of the string sits at offset k - i from position i.

@[simp]

theorem DistributedMorphology.Neighborhood.length_along {Bundle : Type u_1} (d : List Bundle) : (along d).length = d.length

@[simp]

theorem DistributedMorphology.Neighborhood.getElem_along {Bundle : Type u_1} (d : List Bundle) (i : ℕ) (h : i < (along d).length) : (along d)[i] = around d i d[i]

@[simp]

theorem DistributedMorphology.Neighborhood.map_focus_along {Bundle : Type u_1} (d : List Bundle) : List.map focus (along d) = d

theorem DistributedMorphology.Neighborhood.toList_of_mem_along {Bundle : Type u_1} (d : List Bundle) {n : Neighborhood Bundle} (h : n ∈ along d) : n.toList = d

Each neighborhood of a string reassembles to the string.

Positioned features

@[instance_reducible]

instance DistributedMorphology.Neighborhood.instMembershipProdIntList {F : Type u_2} : Membership (ℤ × F) (Neighborhood (List F))

(i, f) ∈ n holds when the terminal at offset i from the focus bears the feature f.

Equations

• DistributedMorphology.Neighborhood.instMembershipProdIntList = { mem := fun (n : DistributedMorphology.Neighborhood (List F)) (x : ℤ × F) => x.2 ∈ n.nth x.1 }

theorem DistributedMorphology.Neighborhood.mem_def {F : Type u_2} {n : Neighborhood (List F)} {x : ℤ × F} : x ∈ n ↔ x.2 ∈ n.nth x.1

@[instance_reducible]

instance DistributedMorphology.Neighborhood.instDecidableMemProdIntListOfDecidableEq {F : Type u_2} [DecidableEq F] (x : ℤ × F) (n : Neighborhood (List F)) : Decidable (x ∈ n)

Equations

• DistributedMorphology.Neighborhood.instDecidableMemProdIntListOfDecidableEq x n = { decide := decide (List.elem x.2 (n.nth x.1) = true), reflects_decide := ⋯ }

def DistributedMorphology.Neighborhood.positioned {F : Type u_2} (n : Neighborhood (List F)) : List (ℤ × F)

n.positioned lists the positioned features of a neighborhood of feature lists, the focus's at offset 0, then the left context's, then the right context's.

Equations

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

@[simp]

theorem DistributedMorphology.Neighborhood.mem_positioned {F : Type u_2} {n : Neighborhood (List F)} {x : ℤ × F} : x ∈ n.positioned ↔ x ∈ n

@[simp]

theorem DistributedMorphology.Neighborhood.positioned_ofBundle {F : Type u_2} (fs : List F) : (↑fs).positioned = List.map (fun (x : F) => (0, x)) fs

@[simp]

theorem DistributedMorphology.Neighborhood.positioned_empty {F : Type u_2} : ∅.positioned = []

@[simp]

theorem DistributedMorphology.Neighborhood.mem_ofBundle {F : Type u_2} {x : ℤ × F} {fs : List F} : x ∈ ↑fs ↔ x.1 = 0 ∧ x.2 ∈ fs

@[simp]

theorem DistributedMorphology.Neighborhood.notMem_empty {F : Type u_2} {x : ℤ × F} : x ∉ ∅

Inclusion

@[instance_reducible]

instance DistributedMorphology.Neighborhood.instPreorderList {F : Type u_2} : Preorder (Neighborhood (List F))

A site is included in a neighborhood when every positioned feature it mentions is present; a terminal it does not mention is unconstrained. This is the Subset Principle's inclusion.

Equations

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

theorem DistributedMorphology.Neighborhood.subset_iff {F : Type u_2} {s n : Neighborhood (List F)} : s ⊆ n ↔ ∀ ⦃x : ℤ × F⦄, x ∈ s → x ∈ n

theorem DistributedMorphology.Neighborhood.mem_of_subset {F : Type u_2} {s n : Neighborhood (List F)} {x : ℤ × F} (h : s ⊆ n) (hx : x ∈ s) : x ∈ n

theorem DistributedMorphology.Neighborhood.subset_iff_nth {F : Type u_2} {s n : Neighborhood (List F)} : s ⊆ n ↔ ∀ (i : ℤ), s.nth i ⊆ n.nth i

Inclusion compares terminal by terminal.

theorem DistributedMorphology.Neighborhood.focus_subset_focus {F : Type u_2} {s n : Neighborhood (List F)} (h : s ⊆ n) : s.focus ⊆ n.focus

theorem DistributedMorphology.Neighborhood.subset_iff_positioned {F : Type u_2} {s n : Neighborhood (List F)} : s ⊆ n ↔ s.positioned ⊆ n.positioned

@[instance_reducible]

instance DistributedMorphology.Neighborhood.instDecidableLEListOfDecidableEq {F : Type u_2} [DecidableEq F] : DecidableLE (Neighborhood (List F))

Equations

• x✝¹.instDecidableLEListOfDecidableEq x✝ = decidable_of_iff (x✝¹.positioned ⊆ x✝.positioned) ⋯

@[simp]

theorem DistributedMorphology.Neighborhood.empty_subset {F : Type u_2} (n : Neighborhood (List F)) : ∅ ⊆ n

@[simp]

theorem DistributedMorphology.Neighborhood.ofBundle_subset_iff {F : Type u_2} {n : Neighborhood (List F)} {fs : List F} : ↑fs ⊆ n ↔ fs ⊆ n.focus

A context-free site is included in a neighborhood exactly when its features are on the focus.

Counting positioned features

def DistributedMorphology.Neighborhood.toFinset {F : Type u_2} [DecidableEq F] (n : Neighborhood (List F)) : Finset (ℤ × F)

The positioned features of a neighborhood of feature lists, as a finite set.

Equations

• n.toFinset = n.positioned.toFinset

@[simp]

theorem DistributedMorphology.Neighborhood.mem_toFinset {F : Type u_2} {n : Neighborhood (List F)} {x : ℤ × F} [DecidableEq F] : x ∈ n.toFinset ↔ x ∈ n

@[simp]

theorem DistributedMorphology.Neighborhood.toFinset_empty {F : Type u_2} [DecidableEq F] : ∅.toFinset = ∅

@[simp]

theorem DistributedMorphology.Neighborhood.toFinset_subset_toFinset {F : Type u_2} {s n : Neighborhood (List F)} [DecidableEq F] : s.toFinset ⊆ n.toFinset ↔ s ⊆ n

@[simp]

theorem DistributedMorphology.Neighborhood.toFinset_ssubset_toFinset {F : Type u_2} {s n : Neighborhood (List F)} [DecidableEq F] : s.toFinset ⊂ n.toFinset ↔ s ⊂ n

theorem DistributedMorphology.Neighborhood.card_toFinset_strictMono {F : Type u_2} [DecidableEq F] : StrictMono fun (n : Neighborhood (List F)) => n.toFinset.card

A strictly larger site has strictly more positioned features.

def DistributedMorphology.Neighborhood.weight {F : Type u_2} [DecidableEq F] (n : Neighborhood (List F)) : Lex (ℕ × ℕ)

The weight of a neighborhood counts its distinct features on the focus, then those elsewhere.

Equations

• n.weight = toLex ({x ∈ n.toFinset | x.1 = 0}.card, {x ∈ n.toFinset | x.1 ≠ 0}.card)

theorem DistributedMorphology.Neighborhood.not_weight_lt_empty {F : Type u_2} [DecidableEq F] (n : Neighborhood (List F)) : ¬n.weight < ∅.weight

No neighborhood weighs less than the empty one.

theorem DistributedMorphology.Neighborhood.weight_strictMono {F : Type u_2} [DecidableEq F] : StrictMono weight

A strictly larger site has more features on the focus, or as many there and more elsewhere.