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 it applies where every feature it mentions, at the focus or on a neighbor, is present (Neighborhood.positioned, ⊆).

Main definitions

• Neighborhood — focus, left context, right context.
• Neighborhood.positioned — the features of a neighborhood of feature lists, each tagged with its Position.
• ⊆ on Neighborhood (List F) — inclusion of positioned features.

Implementation notes

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⟩. Positions count outward from the focus: left toward the root, right toward the clause.

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

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
• leftCtx : List Bundle
• rightCtx : List Bundle

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.

@[instance_reducible]

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

Equations

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

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

• DistributedMorphology.Neighborhood.ofBundle 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 := { focus := ∅ } }

@[simp]

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

@[simp]

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

@[simp]

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

Positioned features

inductive DistributedMorphology.Neighborhood.Position : Type

A position in a neighborhood: the focus, or the i-th terminal to a side, nearest first.

• focus : Position
• left (i : ℕ) : Position
• right (i : ℕ) : Position

@[instance_reducible]

instance DistributedMorphology.Neighborhood.instDecidableEqPosition : DecidableEq Position

Equations

• DistributedMorphology.Neighborhood.instDecidableEqPosition = DistributedMorphology.Neighborhood.instDecidableEqPosition.decEq

def DistributedMorphology.Neighborhood.instDecidableEqPosition.decEq (x✝ x✝¹ : Position) : Decidable (x✝ = x✝¹)

Equations

• One or more equations did not get rendered due to their size.
• DistributedMorphology.Neighborhood.instDecidableEqPosition.decEq DistributedMorphology.Neighborhood.Position.focus DistributedMorphology.Neighborhood.Position.focus = isTrue ⋯
• DistributedMorphology.Neighborhood.instDecidableEqPosition.decEq DistributedMorphology.Neighborhood.Position.focus (DistributedMorphology.Neighborhood.Position.left i) = isFalse ⋯
• DistributedMorphology.Neighborhood.instDecidableEqPosition.decEq DistributedMorphology.Neighborhood.Position.focus (DistributedMorphology.Neighborhood.Position.right i) = isFalse ⋯
• DistributedMorphology.Neighborhood.instDecidableEqPosition.decEq (DistributedMorphology.Neighborhood.Position.left i) DistributedMorphology.Neighborhood.Position.focus = isFalse ⋯
• DistributedMorphology.Neighborhood.instDecidableEqPosition.decEq (DistributedMorphology.Neighborhood.Position.left i) (DistributedMorphology.Neighborhood.Position.right i_1) = isFalse ⋯
• DistributedMorphology.Neighborhood.instDecidableEqPosition.decEq (DistributedMorphology.Neighborhood.Position.right i) DistributedMorphology.Neighborhood.Position.focus = isFalse ⋯
• DistributedMorphology.Neighborhood.instDecidableEqPosition.decEq (DistributedMorphology.Neighborhood.Position.right i) (DistributedMorphology.Neighborhood.Position.left i_1) = isFalse ⋯

@[instance_reducible]

instance DistributedMorphology.Neighborhood.instReprPosition : Repr Position

Equations

• DistributedMorphology.Neighborhood.instReprPosition = { reprPrec := DistributedMorphology.Neighborhood.instReprPosition.repr }

def DistributedMorphology.Neighborhood.instReprPosition.repr : Position → ℕ → Std.Format

Equations

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

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

The features of a neighborhood of feature lists, each tagged with the position it sits at.

Equations

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

@[instance_reducible]

instance DistributedMorphology.Neighborhood.instHasSubsetList {F : Type u_2} : HasSubset (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 — the Subset Principle over neighborhoods.

Equations

• DistributedMorphology.Neighborhood.instHasSubsetList = { Subset := fun (s n : DistributedMorphology.Neighborhood (List F)) => s.positioned ⊆ n.positioned }

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

@[instance_reducible]

instance DistributedMorphology.Neighborhood.instDecidableRelListSubsetOfDecidableEq {F : Type u_2} [DecidableEq F] : DecidableRel fun (x1 x2 : Neighborhood (List F)) => x1 ⊆ x2

Equations

• s.instDecidableRelListSubsetOfDecidableEq n = s.positioned.instDecidableRelSubsetOfDecidableEq n.positioned

theorem DistributedMorphology.Neighborhood.Subset.refl {F : Type u_2} (n : Neighborhood (List F)) : n ⊆ n

theorem DistributedMorphology.Neighborhood.Subset.trans {F : Type u_2} {a b c : Neighborhood (List F)} (h₁ : a ⊆ b) (h₂ : b ⊆ c) : a ⊆ c

instance DistributedMorphology.Neighborhood.instReflListSubset {F : Type u_2} : Std.Refl fun (x1 x2 : Neighborhood (List F)) => x1 ⊆ x2

@[instance_reducible]

instance DistributedMorphology.Neighborhood.instTransListSubset {F : Type u_2} : Trans (fun (x1 x2 : Neighborhood (List F)) => x1 ⊆ x2) (fun (x1 x2 : Neighborhood (List F)) => x1 ⊆ x2) fun (x1 x2 : Neighborhood (List F)) => x1 ⊆ x2

Equations

• DistributedMorphology.Neighborhood.instTransListSubset = { trans := ⋯ }

@[simp]

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

@[simp]

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

theorem DistributedMorphology.Neighborhood.ofBundle_subset_ofBundle {F : Type u_2} {s t : List F} : ofBundle s ⊆ ofBundle t ↔ s ⊆ t

Context-free sites compare by feature inclusion.