Phonological transformations as correspondence-graph relations

[Jar16] (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 ([Jar16] 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 ([Jar16] Def. 25).
• Correspondence.specifiedBy — CG(φ), a process presented by a banned-subgraph grammar.
• Correspondence.IsLocal — a relation presented by a finite banned-subgraph grammar.

def Autosegmental.Correspondence.input {S : Type u_1} {T : Type u_2} (G : Graph S T) : List S

The input string of a correspondence graph: its upper tier.

Equations

• Autosegmental.Correspondence.input G = G.upper.toList

def Autosegmental.Correspondence.output {S : Type u_1} {T : Type u_2} (G : Graph S T) : List T

The output string of a correspondence graph: its lower tier.

Equations

• Autosegmental.Correspondence.output G = G.lower.toList

def Autosegmental.Correspondence.rel {S : Type u_1} {T : Type u_2} (CG : Graph S T → Prop) (w : List S) (v : List T) : Prop

R(CG) ([Jar16] Def. 25): the string relation realized by a set CG of correspondence graphs — the input/output pairs of its members.

Equations

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

theorem Autosegmental.Correspondence.rel_mono {S : Type u_1} {T : Type u_2} {CG CG' : Graph S T → Prop} (h : ∀ (G : Graph S T), CG G → CG' G) {w : List S} {v : List T} : rel CG w v → rel CG' w v

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

def Autosegmental.Correspondence.specifiedBy {S : Type u_1} {T : Type u_2} (φ : List (Graph S T)) (G : Graph S T) : Prop

A process specified by banned subgraphs φ: the correspondence graphs free of every forbidden pattern (Jardine's CG(φ); reuses Graph.Free, the L^NL_G banned-subgraph grammar — markedness and faithfulness as forbidden correspondence substructures).

Equations

• Autosegmental.Correspondence.specifiedBy φ G = G.Free φ

@[implicit_reducible]

instance Autosegmental.Correspondence.instDecidableSpecifiedByOfDecidableEq {S : Type u_1} {T : Type u_2} [DecidableEq S] [DecidableEq T] (φ : List (Graph S T)) (G : Graph S T) : Decidable (specifiedBy φ G)

Equations

• Autosegmental.Correspondence.instDecidableSpecifiedByOfDecidableEq φ G = Autosegmental.Correspondence.instDecidableSpecifiedByOfDecidableEq._aux_1 φ G

def Autosegmental.Correspondence.IsLocal {S : Type u_1} {T : Type u_2} (R : List S → List T → Prop) : Prop

A string relation is local when presented by a finite banned-subgraph grammar over correspondence graphs — the locality of phonological processes [Jar16].

Equations

• Autosegmental.Correspondence.IsLocal R = ∃ (φ : List (Autosegmental.Graph S T)), R = Autosegmental.Correspondence.rel (Autosegmental.Correspondence.specifiedBy φ)

theorem Autosegmental.Correspondence.specifiedBy_append {S : Type u_1} {T : Type u_2} (φ ψ : List (Graph S T)) (G : Graph S T) : specifiedBy (φ ++ ψ) G ↔ specifiedBy φ G ∧ specifiedBy ψ G

Banned-subgraph grammars compose by union: CG(φ ++ ψ) = CG(φ) ∩ CG(ψ) — the L^NL_G conjunction of two local constraint sets.

@[simp]

theorem Autosegmental.Correspondence.specifiedBy_nil {S : Type u_1} {T : Type u_2} (G : Graph S T) : specifiedBy [] G ↔ True

The empty grammar specifies all of GEN.