The association conventions

This file defines the universal conventions that associate the melodic elements of a tier with the slots of a template, as [McC81] states them after [CF79]. First, the unassociated melodic elements associate one to one, from left to right, with the free slots. Second, a single unassociated melodic element that remains associates with every free slot. Third, a slot still free takes the melodic element on the nearest slot to its left. A slot with a line from any tier is unavailable to every other tier, the prohibition against many-to-one association. A language-particular rule that erases a line is followed by the conventions again, which restore or respread it.

Main definitions

• Morphology.TemplateMatch.associateOneToOne, associateRemaining, spread: the three conventions on one tier.
• Morphology.TemplateMatch.associate: the three in order.

Main results

• Morphology.TemplateMatch.associate_map: the conventions never look at the melodic elements, so they commute with relabeling them.

References

• [McC81]
• [CF79]

def Morphology.TemplateMatch.bearers {α : Type u_1} (m : TemplateMatch α) (s : AssocSource) : List ℕ

The slots that bear a tier's melody: the V-slots for the vocalism, the C-slots for the root and the affixes.

Equations

• m.bearers s = if s = Morphology.AssocSource.vocalism then m.template.vSlots else m.template.cSlots

def Morphology.TemplateMatch.IsFilled {α : Type u_1} (m : TemplateMatch α) (i : ℕ) : Bool

Whether some line reaches a slot, from any tier.

Equations

• m.IsFilled i = m.associations.any fun (x : Morphology.Association) => x.slotIndex == i

def Morphology.TemplateMatch.IsAssociated {α : Type u_1} (m : TemplateMatch α) (s : AssocSource) (k : ℕ) : Bool

Whether some line leaves a melodic element of a tier.

Equations

• m.IsAssociated s k = m.associations.any fun (a : Morphology.Association) => a.source == s && a.melodyIndex == k

def Morphology.TemplateMatch.unassociated {α : Type u_1} (m : TemplateMatch α) (s : AssocSource) : List ℕ

The unassociated elements of a tier, left to right.

Equations

• m.unassociated s = List.filter (fun (x : ℕ) => !m.IsAssociated s x) (List.range (m.melody s).length)

def Morphology.TemplateMatch.freeBearers {α : Type u_1} (m : TemplateMatch α) (s : AssocSource) : List ℕ

The free slots that bear a tier's melody, left to right: a slot with a line from any tier is unavailable.

Equations

• m.freeBearers s = List.filter (fun (x : ℕ) => !m.IsFilled x) (m.bearers s)

def Morphology.TemplateMatch.link {α : Type u_1} (m : TemplateMatch α) (l : List Association) : TemplateMatch α

The match with some lines added.

Equations

• m.link l = { root := m.root, vocalism := m.vocalism, affix := m.affix, template := m.template, associations := m.associations ++ l }

def Morphology.TemplateMatch.leftLine {α : Type u_1} (m : TemplateMatch α) (s : AssocSource) (i : ℕ) : Option Association

The line of a tier on the nearest slot left of i that has one.

Equations

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

def Morphology.TemplateMatch.associateOneToOne {α : Type u_1} (m : TemplateMatch α) (s : AssocSource) : TemplateMatch α

The first convention: the unassociated melodic elements associate one to one, from left to right, with the free slots.

Equations

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

def Morphology.TemplateMatch.associateRemaining {α : Type u_1} (m : TemplateMatch α) (s : AssocSource) : TemplateMatch α

The second convention: a single unassociated melodic element associates with every free slot. After the first convention no element is left with a free slot, so this changes only a match the first has not been applied to.

Equations

• m.associateRemaining s = match m.unassociated s with | [k] => m.link (List.map (fun (i : ℕ) => { source := s, melodyIndex := k, slotIndex := i }) (m.freeBearers s)) | x => m

def Morphology.TemplateMatch.spread {α : Type u_1} (m : TemplateMatch α) (s : AssocSource) : TemplateMatch α

The third convention: a free slot takes the melodic element of the tier on the nearest slot to its left.

Equations

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

def Morphology.TemplateMatch.associate {α : Type u_1} (m : TemplateMatch α) (s : AssocSource) : TemplateMatch α

The three conventions, in order.

Equations

• m.associate s = ((m.associateOneToOne s).associateRemaining s).spread s

Relabeling

@[simp]

theorem Morphology.TemplateMatch.unassociated_map {α : Type u_1} {β : Type u_2} (m : TemplateMatch α) (s : AssocSource) (f : α → β) : (m.map f).unassociated s = m.unassociated s

@[simp]

theorem Morphology.TemplateMatch.freeBearers_map {α : Type u_1} {β : Type u_2} (m : TemplateMatch α) (s : AssocSource) (f : α → β) : (m.map f).freeBearers s = m.freeBearers s

theorem Morphology.TemplateMatch.link_map {α : Type u_1} {β : Type u_2} (m : TemplateMatch α) (f : α → β) (l : List Association) : (m.map f).link l = (m.link l).map f

theorem Morphology.TemplateMatch.associateOneToOne_map {α : Type u_1} {β : Type u_2} (m : TemplateMatch α) (s : AssocSource) (f : α → β) : (m.map f).associateOneToOne s = (m.associateOneToOne s).map f

theorem Morphology.TemplateMatch.associateRemaining_map {α : Type u_1} {β : Type u_2} (m : TemplateMatch α) (s : AssocSource) (f : α → β) : (m.map f).associateRemaining s = (m.associateRemaining s).map f

theorem Morphology.TemplateMatch.spread_map {α : Type u_1} {β : Type u_2} (m : TemplateMatch α) (s : AssocSource) (f : α → β) : (m.map f).spread s = (m.spread s).map f

theorem Morphology.TemplateMatch.associate_map {α : Type u_1} {β : Type u_2} (m : TemplateMatch α) (s : AssocSource) (f : α → β) : (m.map f).associate s = (m.associate s).map f

The conventions never look at the melodic elements.