Jardine (2016): intervocalic voicing as a local string relation

This file formalizes chapter 7 of [jardine-2016b], which presents a phonological process as a relation between input and output strings: a set of correspondence graphs, carved out of GEN by banned-subgraph constraints. Section 7.2 runs the idea on intervocalic voicing, (7.1), whose relation over a, b and p is Rvoice, (7.5). The primitives Γ of (7.14), an input symbol over its output, generate GEN by concatenation, (7.15) (g), and five banned subgraphs cut the voicing relation out of it: φ_apa, (7.19), forbids a surface apa, and the four of (7.21) forbid a p surfacing as b word-initially, word-finally, after a p and before a p. The grammar is φ_apba, (7.22), and the relation it presents is R(CG(φ_apba)), Definition 25 (voicing): a pair is in it iff the Γ-string spelling it, which is unique, is free of the grammar (voicing_iff_spell), so membership decides, and on the pairs of (7.5) and (7.17) the relation agrees with Rvoice (rows_agree). The identity R(CG(φ_apba)) = Rvoice that the text leaves to the reader fails: no subgraph of (7.22) mentions a b beside the target, so the grammar admits bpa ↦ bba, which the rule (7.1) does not (voicing_ne_voiceRule).

Implementation notes

• Correspondence graphs are Autosegmental.Correspondence.Rep; the word boundaries ⋊ and ⋉ that (7.21) reads are symbols of the alphabet, and a Γ-string's graph is wrapped in them.
• Rvoice is written as the rule (7.1) applied pointwise, voiceRule, a p between two as surfacing as b.

References

• [jardine-2016b]

inductive Jardine2016b.Seg : Type

Σ = ∆ = {a, b, p} of (7.1), with the word boundaries ⋊ (lb) and ⋉ (rb) that the subgraphs of (7.21) read.

• a : Seg
• b : Seg
• p : Seg
• lb : Seg
• rb : Seg

@[instance_reducible]

instance Jardine2016b.instDecidableEqSeg : DecidableEq Seg

Equations

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

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

Equations

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

@[instance_reducible]

instance Jardine2016b.instReprSeg : Repr Seg

Equations

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

inductive Jardine2016b.Pair : Type

The correspondence primitives Γ = {aa, pb, pp, bb} of (7.14) — an input symbol over its output — with the boundary primitives ⋊ over ⋊ and ⋉ over ⋉.

• aa : Pair
• pb : Pair
• pp : Pair
• bb : Pair
• lb : Pair
• rb : Pair

@[instance_reducible]

instance Jardine2016b.instDecidableEqPair : DecidableEq Pair

Equations

• Jardine2016b.instDecidableEqPair x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

def Jardine2016b.instReprPair.repr : Pair → ℕ → Std.Format

Equations

• Jardine2016b.instReprPair.repr Jardine2016b.Pair.aa prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Jardine2016b.Pair.aa")).group prec✝
• Jardine2016b.instReprPair.repr Jardine2016b.Pair.pb prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Jardine2016b.Pair.pb")).group prec✝
• Jardine2016b.instReprPair.repr Jardine2016b.Pair.pp prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Jardine2016b.Pair.pp")).group prec✝
• Jardine2016b.instReprPair.repr Jardine2016b.Pair.bb prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Jardine2016b.Pair.bb")).group prec✝
• Jardine2016b.instReprPair.repr Jardine2016b.Pair.lb prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Jardine2016b.Pair.lb")).group prec✝
• Jardine2016b.instReprPair.repr Jardine2016b.Pair.rb prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Jardine2016b.Pair.rb")).group prec✝

@[instance_reducible]

instance Jardine2016b.instReprPair : Repr Pair

Equations

• Jardine2016b.instReprPair = { reprPrec := Jardine2016b.instReprPair.repr }

def Jardine2016b.Pair.input : Pair → Seg

The input symbol of a primitive.

Equations

• Jardine2016b.Pair.aa.input = Jardine2016b.Seg.a
• Jardine2016b.Pair.pb.input = Jardine2016b.Seg.p
• Jardine2016b.Pair.pp.input = Jardine2016b.Seg.p
• Jardine2016b.Pair.bb.input = Jardine2016b.Seg.b
• Jardine2016b.Pair.lb.input = Jardine2016b.Seg.lb
• Jardine2016b.Pair.rb.input = Jardine2016b.Seg.rb

def Jardine2016b.Pair.output : Pair → Seg

The output symbol of a primitive.

Equations

• Jardine2016b.Pair.aa.output = Jardine2016b.Seg.a
• Jardine2016b.Pair.pb.output = Jardine2016b.Seg.b
• Jardine2016b.Pair.pp.output = Jardine2016b.Seg.p
• Jardine2016b.Pair.bb.output = Jardine2016b.Seg.b
• Jardine2016b.Pair.lb.output = Jardine2016b.Seg.lb
• Jardine2016b.Pair.rb.output = Jardine2016b.Seg.rb

theorem Jardine2016b.Pair.ext {x y : Pair} (hi : x.input = y.input) (ho : x.output = y.output) : x = y

A primitive is its input–output pair.

theorem Jardine2016b.Pair.map_injective {γs γs' : List Pair} (hi : List.map input γs = List.map input γs') (ho : List.map output γs = List.map output γs') : γs = γs'

A Γ-string is determined by the strings it spells.

def Jardine2016b.Pair.ofSegs : Seg → Seg → Option Pair

The primitive spelling an input symbol over an output symbol, if any.

Equations

• Jardine2016b.Pair.ofSegs Jardine2016b.Seg.a Jardine2016b.Seg.a = some Jardine2016b.Pair.aa
• Jardine2016b.Pair.ofSegs Jardine2016b.Seg.p Jardine2016b.Seg.b = some Jardine2016b.Pair.pb
• Jardine2016b.Pair.ofSegs Jardine2016b.Seg.p Jardine2016b.Seg.p = some Jardine2016b.Pair.pp
• Jardine2016b.Pair.ofSegs Jardine2016b.Seg.b Jardine2016b.Seg.b = some Jardine2016b.Pair.bb
• Jardine2016b.Pair.ofSegs Jardine2016b.Seg.lb Jardine2016b.Seg.lb = some Jardine2016b.Pair.lb
• Jardine2016b.Pair.ofSegs Jardine2016b.Seg.rb Jardine2016b.Seg.rb = some Jardine2016b.Pair.rb
• Jardine2016b.Pair.ofSegs x✝¹ x✝ = none

theorem Jardine2016b.Pair.ofSegs_eq_some_iff {i o : Seg} {γ : Pair} : ofSegs i o = some γ ↔ γ.input = i ∧ γ.output = o

theorem Jardine2016b.Pair.ofSegs_input_output (γ : Pair) : ofSegs γ.input γ.output = some γ

def Jardine2016b.spell : List Seg → List Seg → Option (List Pair)

The Γ-string spelling an input and an output string, if any.

Equations

• Jardine2016b.spell [] [] = some []
• Jardine2016b.spell (i :: w) (o :: v) = match Jardine2016b.Pair.ofSegs i o, Jardine2016b.spell w v with | some γ, some γs => some (γ :: γs) | x, x_1 => none
• Jardine2016b.spell x✝¹ x✝ = none

theorem Jardine2016b.spell_map (γs : List Pair) : spell (List.map Pair.input γs) (List.map Pair.output γs) = some γs

theorem Jardine2016b.spell_eq_some {w v : List Seg} {γs : List Pair} (h : spell w v = some γs) : List.map Pair.input γs = w ∧ List.map Pair.output γs = v

theorem Jardine2016b.spell_eq_some_iff {w v : List Seg} {γs : List Pair} : spell w v = some γs ↔ List.map Pair.input γs = w ∧ List.map Pair.output γs = v

A pair is spelled by a Γ-string exactly when it is the string's input and output.

@[reducible, inline]

abbrev Jardine2016b.g (γs : List Pair) : Autosegmental.Correspondence.Rep Seg Seg

Jardine's g on Γ-strings ((7.15)): the correspondence graph spelling the input and output symbols position by position.

Equations

• Jardine2016b.g γs = Autosegmental.Correspondence.Rep.ofWords (List.map Jardine2016b.Pair.input γs) (List.map Jardine2016b.Pair.output γs) fun (x1 x2 : ℕ) => x1 = x2

@[reducible, inline]

abbrev Jardine2016b.gen (γs : List Pair) : Autosegmental.Correspondence.Rep Seg Seg

A Γ-string's graph between the boundaries ⋊ and ⋉.

Equations

• Jardine2016b.gen γs = Jardine2016b.g (Jardine2016b.Pair.lb :: γs ++ [Jardine2016b.Pair.rb])

The grammar φ_apba

@[reducible, inline]

abbrev Jardine2016b.banApa : Autosegmental.Correspondence.Rep Seg Seg

φ_apa (7.19): a surface apa — output-only, the markedness constraint *VTV.

Equations

• Jardine2016b.banApa = Autosegmental.Correspondence.Rep.ofWords [] [Jardine2016b.Seg.a, Jardine2016b.Seg.p, Jardine2016b.Seg.a] fun (x x_1 : ℕ) => False

@[reducible, inline]

abbrev Jardine2016b.banInitialPb : Autosegmental.Correspondence.Rep Seg Seg

φ_⋊pb (7.21): a p surfacing as b word-initially.

Equations

• Jardine2016b.banInitialPb = Autosegmental.Correspondence.Rep.ofWords [Jardine2016b.Seg.p] [Jardine2016b.Seg.lb, Jardine2016b.Seg.b] fun (i o : ℕ) => i = 0 ∧ o = 1

@[reducible, inline]

abbrev Jardine2016b.banFinalPb : Autosegmental.Correspondence.Rep Seg Seg

φ_pb⋉ (7.21): a p surfacing as b word-finally.

Equations

• Jardine2016b.banFinalPb = Autosegmental.Correspondence.Rep.ofWords [Jardine2016b.Seg.p] [Jardine2016b.Seg.b, Jardine2016b.Seg.rb] fun (i o : ℕ) => i = 0 ∧ o = 0

@[reducible, inline]

abbrev Jardine2016b.banPbAfterP : Autosegmental.Correspondence.Rep Seg Seg

φ_ppb (7.21): a p surfacing as b after a surface p.

Equations

• Jardine2016b.banPbAfterP = Autosegmental.Correspondence.Rep.ofWords [Jardine2016b.Seg.p] [Jardine2016b.Seg.p, Jardine2016b.Seg.b] fun (i o : ℕ) => i = 0 ∧ o = 1

@[reducible, inline]

abbrev Jardine2016b.banPbBeforeP : Autosegmental.Correspondence.Rep Seg Seg

φ_pbp (7.21): a p surfacing as b before a surface p.

Equations

• Jardine2016b.banPbBeforeP = Autosegmental.Correspondence.Rep.ofWords [Jardine2016b.Seg.p] [Jardine2016b.Seg.b, Jardine2016b.Seg.p] fun (i o : ℕ) => i = 0 ∧ o = 0

def Jardine2016b.voicingGrammar : List (Autosegmental.Correspondence.Rep Seg Seg)

φ_apba (7.22).

Equations

• Jardine2016b.voicingGrammar = [Jardine2016b.banApa, Jardine2016b.banInitialPb, Jardine2016b.banFinalPb, Jardine2016b.banPbAfterP, Jardine2016b.banPbBeforeP]

theorem Jardine2016b.specifiedByRep_voicingGrammar (G : Autosegmental.Correspondence.Rep Seg Seg) : Autosegmental.Correspondence.specifiedByRep voicingGrammar G ↔ ¬(↑banApa).FactorEmbeds ↑G ∧ ¬(↑banInitialPb).FactorEmbeds ↑G ∧ ¬(↑banFinalPb).FactorEmbeds ↑G ∧ ¬(↑banPbAfterP).FactorEmbeds ↑G ∧ ¬(↑banPbBeforeP).FactorEmbeds ↑G

@[instance_reducible]

instance Jardine2016b.instDecidableSpecifiedByRepSegVoicingGrammarGen (γs : List Pair) : Decidable (Autosegmental.Correspondence.specifiedByRep voicingGrammar (gen γs))

On GEN the grammar decides.

Equations

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

The relation R(CG(φ_apba))

def Jardine2016b.CG (G : Autosegmental.Correspondence.Rep Seg Seg) : Prop

CG(φ_apba): the graphs of GEN = CG(Γ) free of the grammar.

Equations

• Jardine2016b.CG G = ((∃ (γs : List Jardine2016b.Pair), G = Jardine2016b.gen γs) ∧ Autosegmental.Correspondence.specifiedByRep Jardine2016b.voicingGrammar G)

def Jardine2016b.voicing (w v : List Seg) : Prop

R(CG(φ_apba)) (Def. 25), on boundary-augmented strings.

Equations

• Jardine2016b.voicing w v = Autosegmental.Correspondence.relRep Jardine2016b.CG (Jardine2016b.Seg.lb :: w ++ [Jardine2016b.Seg.rb]) (Jardine2016b.Seg.lb :: v ++ [Jardine2016b.Seg.rb])

theorem Jardine2016b.voicing_iff {w v : List Seg} : voicing w v ↔ ∃ (γs : List Pair), List.map Pair.input γs = w ∧ List.map Pair.output γs = v ∧ Autosegmental.Correspondence.specifiedByRep voicingGrammar (gen γs)

Def. 25 unwound: (w, v) is in the relation iff some Γ-string spells both and its graph is free of the grammar.

theorem Jardine2016b.voicing_iff_spell {w v : List Seg} : voicing w v ↔ ∃ (γs : List Pair), spell w v = some γs ∧ Autosegmental.Correspondence.specifiedByRep voicingGrammar (gen γs)

Definition 25 by spelling: the Γ-string spelling the pair is unique, so (w, v) is in the relation iff that string exists and its graph is free of the grammar.

@[instance_reducible]

instance Jardine2016b.instDecidableVoicing (w v : List Seg) : Decidable (voicing w v)

Equations

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

The data of (7.5) and (7.17)

def Jardine2016b.segOf : Char → Seg

A segment from its spelling.

Equations

• Jardine2016b.segOf 'a' = Jardine2016b.Seg.a
• Jardine2016b.segOf 'b' = Jardine2016b.Seg.b
• Jardine2016b.segOf x✝ = Jardine2016b.Seg.p

structure Jardine2016b.Row : Type

A row: an input and an output string, and whether the pair is in Rvoice.

• input : List Seg
• output : List Seg
• inRvoice : Bool

def Jardine2016b.instDecidableEqRow.decEq (x✝ x✝¹ : Row) : Decidable (x✝ = x✝¹)

Equations

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

@[instance_reducible]

instance Jardine2016b.instDecidableEqRow : DecidableEq Row

Equations

• Jardine2016b.instDecidableEqRow = Jardine2016b.instDecidableEqRow.decEq

def Jardine2016b.Row.ofExample (e : Data.Examples.LinguisticExample) : Option Row

A row from the paper's features.

Equations

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

def Jardine2016b.rows : List Row

The pairs of Rvoice, (7.5), and the pairs of GEN outside it, (7.17).

Equations

• Jardine2016b.rows = List.filterMap Jardine2016b.Row.ofExample Jardine2016b.Examples.all

theorem Jardine2016b.rows_agree (r : Row) : r ∈ rows → (voicing r.input r.output ↔ r.inRvoice = true)

On the paper's pairs the grammar's relation agrees with Rvoice: the pairs of (7.5) are in it and those of (7.17) outside Rvoice, (7.18b) and (7.20), are excluded.

def Jardine2016b.voiceRule (w : List Seg) : List Seg

The rule (7.1) pointwise: a p between two as surfaces as b.

Equations

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

theorem Jardine2016b.voiceRule_rows (r : Row) : r ∈ rows → (voiceRule r.input = r.output ↔ r.inRvoice = true)

Rvoice is the rule's graph on the paper's pairs.

theorem Jardine2016b.voicing_bpa_bba : voicing [Seg.b, Seg.p, Seg.a] [Seg.b, Seg.b, Seg.a]

The grammar admits bpa ↦ bba: no subgraph of (7.22) mentions a b beside the target.

theorem Jardine2016b.voicing_ne_voiceRule : ¬∀ (w v : List Seg), voicing w v ↔ voiceRule w = v

So the identity R(CG(φ_apba)) = Rvoice that the text leaves to the reader fails: the rule (7.1) leaves bpa unchanged.