Phonological transformations as correspondence-graph relations

[Jar16b] (Ch. 7) models a phonological process not as a function but as a relation between input and output, presented by a set of correspondence graphs and carved out of GEN by banned-subgraph constraints (markedness + faithfulness) — which is what makes the relation local.

A string correspondence graph is exactly a bipartite Graph S T reinterpreted: the upper tier is the input string, the lower tier the output string, and the association links are the input↔output correspondence arcs. (Precedence is carried by the tier order; Jardine's separate precedence/correspondence arc-labeling ℓ_A is here the structural split between tier-order and links.) The banned-subgraph grammar is Graph.Free ([Jar16b] Ch. 5's L^NL_G).

This is the process layer of the substrate's three-layer spec (objects AR, precedence-morphisms PrecAR, processes here). The autosegmental case — correspondence between multi-tier APGs — extends it over MultiGraph.

Scope note

SubgraphEmbeds matches contiguous blocks of both tiers plus links, so it expresses correspondence (input↔output) banned subgraphs directly. Jardine's output-only markedness constraints (e.g. forbid an output apa regardless of input) need the arc-labelled-subgraph refinement he flags in Ch. 7 fn. 7; that is deferred.

Main definitions

• Correspondence.input/output — the two strings a correspondence graph relates.
• Correspondence.rel — R(CG), the string relation of a set of correspondence graphs ([Jar16b] Def. 25).
• Correspondence.specifiedBy — CG(φ), a process presented by a banned-subgraph grammar.
• Correspondence.IsLocal — a relation presented by a finite banned-subgraph grammar.

Correspondence on the graph foundation

The same layer over two-tier representations: input over true, output over false, correspondence arcs the links, banned subgraphs AR.Free.

@[reducible, inline]

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

A finite two-tier correspondence representation.

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: 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: 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

R is monotone: more correspondence graphs realize a larger relation.

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

A process specified by banned subgraphs φ (Jardine's CG(φ)): 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.