Jardine (2016): transformations as correspondence-graph relations

[Jar16] (Ch. 7) presents a phonological process as a relation between input and output, given by correspondence graphs carved out of GEN by banned-subgraph constraints. This file exercises the Autosegmental.Correspondence substrate on the intervocalic-voicing schema (Jardine's running example): a faithfulness constraint *[p↔p] — forbidding a p that corresponds to a p — admits the voicing correspondence apa ↔ aba and rejects the faithful apa ↔ apa.

Scope

This demonstrates the constraint mechanism at the correspondence-graph level. The full relation-level result R(CG(φ)) = R_voice additionally requires GEN (CG(Γ), the correspondence graphs built from primitives), which fixes the correspondence structure; and Jardine's output-only markedness *VTV needs the arc-labelled-subgraph refinement (Ch. 7 fn. 7). Both are deferred — see Autosegmental/Correspondence.lean.

inductive Jardine2016.Seg : Type

Toy alphabet for intervocalic voicing: a vowel a, voiceless p, voiced b.

• a : Seg
• p : Seg
• b : Seg

@[implicit_reducible]

instance Jardine2016.instDecidableEqSeg : DecidableEq Seg

Equations

• Jardine2016.instDecidableEqSeg x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

def Jardine2016.instReprSeg.repr : Seg → ℕ → Std.Format

Equations

• Jardine2016.instReprSeg.repr Jardine2016.Seg.a prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Jardine2016.Seg.a")).group prec✝
• Jardine2016.instReprSeg.repr Jardine2016.Seg.p prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Jardine2016.Seg.p")).group prec✝
• Jardine2016.instReprSeg.repr Jardine2016.Seg.b prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Jardine2016.Seg.b")).group prec✝

@[implicit_reducible]

instance Jardine2016.instReprSeg : Repr Seg

Equations

• Jardine2016.instReprSeg = { reprPrec := Jardine2016.instReprSeg.repr }

@[reducible, inline]

abbrev Jardine2016.CGraph : Type

A correspondence graph over the one alphabet (input and output both Seg).

Equations

• Jardine2016.CGraph = Autosegmental.Graph Jardine2016.Seg Jardine2016.Seg

def Jardine2016.noPP : CGraph

The faithfulness banned subgraph *[pⁱ↔p]: a p corresponding to a p. Forbidding it forces an intervocalic p to change.

Equations

• Jardine2016.noPP = { upper := LabeledTuple.ofList [Jardine2016.Seg.p], lower := LabeledTuple.ofList [Jardine2016.Seg.p], links := {(0, 0)} }

def Jardine2016.gVoice : CGraph

The voicing correspondence apa ↔ aba: identity positions, the medial p corresponding to a b.

Equations

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

def Jardine2016.gFaithful : CGraph

The faithful correspondence apa ↔ apa: the medial p stays p.

Equations

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

theorem Jardine2016.gVoice_io : Autosegmental.Correspondence.input gVoice = [Seg.a, Seg.p, Seg.a] ∧ Autosegmental.Correspondence.output gVoice = [Seg.a, Seg.b, Seg.a]

gVoice reads input apa, output aba.

theorem Jardine2016.gVoice_specified : Autosegmental.Correspondence.specifiedBy [noPP] gVoice

The voicing correspondence is admitted by the *[p↔p] grammar (no p↔p).

theorem Jardine2016.gFaithful_rejected : ¬Autosegmental.Correspondence.specifiedBy [noPP] gFaithful

The faithful correspondence is rejected — it contains a p↔p.

theorem Jardine2016.voicing_local : Autosegmental.Correspondence.rel (Autosegmental.Correspondence.specifiedBy [noPP]) [Seg.a, Seg.p, Seg.a] [Seg.a, Seg.b, Seg.a]

Hence apa ↔ aba lies in the relation presented by the local grammar *[p↔p], witnessed by gVoice ([Jar16] Def. 25).