Phonological transformations as correspondence relations

[Jar16b] (Ch. 7) models a phonological process as a relation between input and output strings, presented by a set of correspondence graphs and carved out by banned-subgraph constraints, which is what makes the relation local. A correspondence graph is a two-tier representation with the input over true, the output over false, and the correspondence arcs as its links; precedence is the order on each tier. A banned subgraph is a factor (AR.FactorEmbeds), so an output-only markedness constraint is a factor with an empty input tier and no links.

Main definitions

• Rep, Rep.input, Rep.output: a finite correspondence representation and the two strings it relates.
• relRep: the string relation of a set of correspondence graphs ([Jar16b] Def. 25).
• specifiedByRep, IsLocalRep: a process presented by a banned-subgraph grammar, and a relation presented by a finite one.
• Rep.ofWords: the correspondence graph of an input word, an output word and a correspondence relation on their positions.

References

• [Jar16b]

@[reducible, inline]

abbrev Autosegmental.Correspondence.Rep (S T : Type u) : Type (max 0 1 u)

A correspondence representation is a finite two-tier representation, the input over true and the output over false, on a vertex type in Type, where AR.ofData builds.

Equations

• Autosegmental.Correspondence.Rep S T = { G : Autosegmental.AR Sigma.fst // Finite G.obj.V }

noncomputable def Autosegmental.Correspondence.Rep.input {S T : Type u} (G : Rep S T) : List S

The input string is the true-tier word.

Equations

• G.input = Autosegmental.AR.tierWord true

noncomputable def Autosegmental.Correspondence.Rep.output {S T : Type u} (G : Rep S T) : List T

The output string is the false-tier word.

Equations

• G.output = Autosegmental.AR.tierWord false

def Autosegmental.Correspondence.relRep {S T : Type u} (CG : Rep S T → Prop) (w : List S) (v : List T) : Prop

R(CG) ([Jar16b] Def. 25) on the foundation: the string relation realized by a set of correspondence representations.

Equations

• Autosegmental.Correspondence.relRep CG w v = ∃ (G : Autosegmental.Correspondence.Rep S T), CG G ∧ G.input = w ∧ G.output = v

theorem Autosegmental.Correspondence.relRep_mono {S T : Type u} {CG CG' : Rep S T → Prop} (h : ∀ (G : Rep S T), CG G → CG' G) {w : List S} {v : List T} : relRep CG w v → relRep CG' w v

More correspondence graphs realize a larger relation.

def Autosegmental.Correspondence.specifiedByRep {S T : Type u} (φ : List (Rep S T)) (G : Rep S T) : Prop

The process specified by banned subgraphs φ (Jardine's CG(φ)) holds of the representations free of every forbidden pattern.

Equations

• Autosegmental.Correspondence.specifiedByRep φ G = (↑G).Free φ

def Autosegmental.Correspondence.IsLocalRep {S T : Type u} (R : List S → List T → Prop) : Prop

A string relation is local when presented by a finite banned-subgraph grammar over correspondence representations.

Equations

• Autosegmental.Correspondence.IsLocalRep R = ∃ (φ : List (Autosegmental.Correspondence.Rep S T)), R = Autosegmental.Correspondence.relRep (Autosegmental.Correspondence.specifiedByRep φ)

theorem Autosegmental.Correspondence.specifiedByRep_append {S T : Type u} (φ ψ : List (Rep S T)) (G : Rep S T) : specifiedByRep (φ ++ ψ) G ↔ specifiedByRep φ G ∧ specifiedByRep ψ G

Banned-subgraph grammars compose by union, the L^NL_G conjunction of two local constraint sets.

@[simp]

theorem Autosegmental.Correspondence.specifiedByRep_nil {S T : Type u} (G : Rep S T) : specifiedByRep [] G ↔ True

The empty grammar specifies all of GEN.

instance Autosegmental.Correspondence.instFiniteVSigmaBoolTwoTierObjGraphAndIsTierOrderedArcsTierFstNoInternalAssocEdgesValAR {S T : Type u} (G : Rep S T) : Finite (↑G).obj.V

theorem Autosegmental.Correspondence.specifiedByRep_cons {S T : Type u} (F : Rep S T) (φ : List (Rep S T)) (G : Rep S T) : specifiedByRep (F :: φ) G ↔ ¬(↑F).FactorEmbeds ↑G ∧ specifiedByRep φ G

A grammar tests its banned subgraphs one by one.

Correspondence graphs from words

def Autosegmental.Correspondence.Rep.ofWords {S T : Type u} (w : List S) (v : List T) (C : ℕ → ℕ → Prop) : Rep S T

The correspondence graph of the input word w and the output word v under the correspondence relation C on their positions.

Equations

• Autosegmental.Correspondence.Rep.ofWords w v C = ⟨Autosegmental.AR.ofWords w v C, ⋯⟩

@[simp]

theorem Autosegmental.Correspondence.Rep.input_ofWords {S T : Type u} (w : List S) (v : List T) (C : ℕ → ℕ → Prop) : (ofWords w v C).input = w

@[simp]

theorem Autosegmental.Correspondence.Rep.output_ofWords {S T : Type u} (w : List S) (v : List T) (C : ℕ → ℕ → Prop) : (ofWords w v C).output = v

@[instance_reducible]

instance Autosegmental.Correspondence.instDecidableFactorEmbedsBoolTwoTierValARSigmaFstFiniteVObjGraphAndIsTierOrderedArcsTierNoInternalAssocEdgesOfWordsOfDecidableEqOfDecidableRelNat {S T : Type u} [DecidableEq S] [DecidableEq T] (w w' : List S) (v v' : List T) (C C' : ℕ → ℕ → Prop) [DecidableRel C] [DecidableRel C'] : Decidable ((↑(Rep.ofWords w v C)).FactorEmbeds ↑(Rep.ofWords w' v' C'))

Equations

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