Jardine (2016): transformations as correspondence-graph relations

[Jar16a] (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

@[instance_reducible]

instance Jardine2016.instDecidableEqSeg : DecidableEq Seg

Equations

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

@[instance_reducible]

instance Jardine2016.instReprSeg : Repr Seg

Equations

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

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✝

@[reducible, inline]

abbrev Jardine2016.CRep : Type 1

A correspondence representation over the one alphabet.

Equations

• Jardine2016.CRep = Autosegmental.Correspondence.Rep Jardine2016.Seg Jardine2016.Seg

def Jardine2016.noPP : CRep

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

Equations

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

def Jardine2016.gVoice : CRep

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

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

Equations

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

instance Jardine2016.instFiniteVSigmaBoolTwoTierSegObjGraphAndIsTierOrderedArcsTierFstNoInternalAssocEdgesValARNoPP : Finite (↑noPP).obj.V

instance Jardine2016.instFiniteVSigmaBoolTwoTierSegObjGraphAndIsTierOrderedArcsTierFstNoInternalAssocEdgesValARGVoice : Finite (↑gVoice).obj.V

instance Jardine2016.instFiniteVSigmaBoolTwoTierSegObjGraphAndIsTierOrderedArcsTierFstNoInternalAssocEdgesValARGFaithful : Finite (↑gFaithful).obj.V

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

gVoice reads input apa, output aba.

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

The faithful correspondence is rejected — it contains a p↔p, embedded at position 1 of both tiers.

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

The voicing correspondence is admitted by the *[p↔p] grammar: the p↔p link would have to land on the output b.

theorem Jardine2016.voicing_local : Autosegmental.Correspondence.relRep (Autosegmental.Correspondence.specifiedByRep [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 ([Jar16a] Def. 25).