Documentation

Studies.Sen2015

Sen (2015): Syllable and Segment in Latin #

This file formalizes the second chapter's analysis of clear and dark /l/. The colouring of a preceding vowel, read off the grammarians' statements and the internal history of Latin words (§2.3), orders the contexts of /l/ by darkness (18): the syllable coda, then onset /l/ before /a o u/, before /e/, before /ē/, and last onset /l/ before /i/ and geminate /ll/ (Context, darkness; Figure 2.1, colouring). The distribution is categorical across three positions and gradient within one: coda /l/ is dark, geminate /ll/ is clear, and onset /l/ darkens with the backness of the following vowel. The equipollent analysis (23) states this as surface specifications on the Fragment's single /l/, [+high, +back] in the coda, [+high, −back] in the geminate and [+high, Ø back] in the onset (spec, spec_ternary). The specified variants sit at the ends of the scale (coda_darkest, geminate_clearest), colouring follows the scale (colouring_monotone), and the unspecified onset ranges over three degrees (onset_gradient): the specification does not determine darkness, which is why the chapter rejects synchronic feature spreading as the source of the colouring (§2.5) in favour of phonetic interpolation through the underspecified segment, in the sense of [Kea88].

Implementation notes #

Sen takes /l/ to be underlyingly unspecified for [back], the coda and geminate values being filled once a string is syllabified (§2.4); spec is the surface specification by position, built from the Fragment's /l/ with Segment.setFeature.
colouring is the regular outcome of Figure 2.1; its exceptions (after /w j/, after dorsals, forms with particular histories) are not encoded. The gradient phonetic implementation (Figure 2.3), the diachronic account of the split, and the parallel analysis of /r/ in the fourth chapter are out of scope.

References #

inductive Sen2015.Position :

The three categorical positions of /l/ (19) are the syllable coda, the onset, and the geminate.

coda : Position
onset : Position
geminate : Position

Instances For

@[instance_reducible]

instance Sen2015.instDecidableEqPosition :

DecidableEq Position

Equations

Sen2015.instDecidableEqPosition x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

@[instance_reducible]

instance Sen2015.instReprPosition :

Equations

Sen2015.instReprPosition = { reprPrec := Sen2015.instReprPosition.repr }

def Sen2015.instReprPosition.repr :

Position → ℕ → Std.Format

Equations

Sen2015.instReprPosition.repr Sen2015.Position.coda prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Sen2015.Position.coda")).group prec✝
Sen2015.instReprPosition.repr Sen2015.Position.onset prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Sen2015.Position.onset")).group prec✝
Sen2015.instReprPosition.repr Sen2015.Position.geminate prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Sen2015.Position.geminate")).group prec✝

Instances For

inductive Sen2015.Context :

The contexts of /l/ that the colouring evidence distinguishes (18), Figure 2.1, are the coda, onset /l/ before /a o u/, before /e/, before /ē/, before /i/, and the geminate.

coda : Context
preBack : Context
preE : Context
preLongE : Context
preI : Context
geminate : Context

Instances For

@[instance_reducible]

instance Sen2015.instDecidableEqContext :

DecidableEq Context

Equations

Sen2015.instDecidableEqContext x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

def Sen2015.instReprContext.repr :

Context → ℕ → Std.Format

Equations

Sen2015.instReprContext.repr Sen2015.Context.coda prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Sen2015.Context.coda")).group prec✝
Sen2015.instReprContext.repr Sen2015.Context.preBack prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Sen2015.Context.preBack")).group prec✝
Sen2015.instReprContext.repr Sen2015.Context.preE prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Sen2015.Context.preE")).group prec✝
Sen2015.instReprContext.repr Sen2015.Context.preLongE prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Sen2015.Context.preLongE")).group prec✝
Sen2015.instReprContext.repr Sen2015.Context.preI prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Sen2015.Context.preI")).group prec✝
Sen2015.instReprContext.repr Sen2015.Context.geminate prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Sen2015.Context.geminate")).group prec✝

Instances For

@[instance_reducible]

instance Sen2015.instReprContext :

Equations

Sen2015.instReprContext = { reprPrec := Sen2015.instReprContext.repr }

@[instance_reducible]

instance Sen2015.instFintypeContext :

Fintype Context

Equations

Sen2015.instFintypeContext = { elems := { val := ↑Sen2015.Context.enumList, nodup := Sen2015.Context.enumList_nodup }, complete := Sen2015.instFintypeContext._proof_1 }

def Sen2015.Context.position :

Context → Position

The categorical position of a context.

Equations

Instances For

def Sen2015.Context.darkness :

Context → ℕ

The scale of darkness (18), as a rank with the coda highest; onset /l/ before /i/ and the geminate share the clearest degree.

Equations

Instances For

@[instance_reducible]

instance Sen2015.instPreorderContext :

Preorder Context

Contexts are ordered by darkness.

Equations

Sen2015.instPreorderContext = Preorder.lift Sen2015.Context.darkness

@[instance_reducible]

instance Sen2015.instDecidableRelContextLe :

DecidableRel fun (x1 x2 : Context) => x1 ≤ x2

Equations

Sen2015.instDecidableRelContextLe a b = { decide := a.darkness.ble b.darkness, reflects_decide := ⋯ }

@[instance_reducible]

instance Sen2015.instDecidableRelContextLt :

DecidableRel fun (x1 x2 : Context) => x1 < x2

Equations

Sen2015.instDecidableRelContextLt a b = { decide := a.darkness.succ.ble b.darkness, reflects_decide := ⋯ }

inductive Sen2015.Colouring :

A short vowel before /l/ is coloured to /u/, coloured to /o/, or left unchanged.

toU : Colouring
toO : Colouring
unchanged : Colouring

Instances For

@[instance_reducible]

instance Sen2015.instDecidableEqColouring :

DecidableEq Colouring

Equations

Sen2015.instDecidableEqColouring x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

@[instance_reducible]

instance Sen2015.instReprColouring :

Equations

Sen2015.instReprColouring = { reprPrec := Sen2015.instReprColouring.repr }

def Sen2015.instReprColouring.repr :

Colouring → ℕ → Std.Format

Equations

Sen2015.instReprColouring.repr Sen2015.Colouring.toU prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Sen2015.Colouring.toU")).group prec✝
Sen2015.instReprColouring.repr Sen2015.Colouring.toO prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Sen2015.Colouring.toO")).group prec✝
Sen2015.instReprColouring.repr Sen2015.Colouring.unchanged prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Sen2015.Colouring.unchanged")).group prec✝

Instances For

def Sen2015.Colouring.vowel :

Colouring → Option Phonology.Segment

The vowel a colouring produces, from the Fragment.

Equations

Sen2015.Colouring.toU.vowel = some Latin.u
Sen2015.Colouring.toO.vowel = some Latin.o
Sen2015.Colouring.unchanged.vowel = none

Instances For

def Sen2015.Colouring.strength :

Colouring → ℕ

Colouring to /u/ is stronger than colouring to /o/, which is stronger than none.

Equations

Sen2015.Colouring.toU.strength = 2
Sen2015.Colouring.toO.strength = 1
Sen2015.Colouring.unchanged.strength = 0

Instances For

inductive Sen2015.Syllable :

Whether the coloured vowel sits in an internal or an initial syllable (Figure 2.1).

internal : Syllable
initial : Syllable

Instances For

@[instance_reducible]

instance Sen2015.instDecidableEqSyllable :

DecidableEq Syllable

Equations

Sen2015.instDecidableEqSyllable x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

@[instance_reducible]

instance Sen2015.instReprSyllable :

Equations

Sen2015.instReprSyllable = { reprPrec := Sen2015.instReprSyllable.repr }

def Sen2015.instReprSyllable.repr :

Syllable → ℕ → Std.Format

Equations

Sen2015.instReprSyllable.repr Sen2015.Syllable.internal prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Sen2015.Syllable.internal")).group prec✝
Sen2015.instReprSyllable.repr Sen2015.Syllable.initial prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Sen2015.Syllable.initial")).group prec✝

Instances For

def Sen2015.colouring :

Syllable → Context → Colouring

The regular colouring of a preceding short vowel by context (Figure 2.1) is in an internal syllable to /u/ before the coda and before onset /l/ followed by /a o u/ or /e/, to /o/ before /lē/, and none before /li/ and /ll/; in an initial syllable to /u/ before the coda and to /o/ before /la lo lu/ only.

Equations

Instances For

theorem Sen2015.colouring_monotone (s : Syllable) :

Monotone fun (c : Context) => (colouring s c).strength

Colouring follows the scale of darkness (18), in that a darker context colours at least as strongly in either syllable.

theorem Sen2015.coda_darkest (c : Context) :

c ≤ Context.coda

The coda is the darkest context and the geminate the clearest ((18), Figure 2.2).

theorem Sen2015.geminate_clearest (c : Context) :

Context.geminate ≤ c

def Sen2015.spec :

Position → Phonology.Segment

The surface specification of /l/ by position (23) is the Fragment's /l/ with the dorsal articulation [+high] common to the three variants, [+back] in the coda, [−back] in the geminate, and no value for [back] in the onset.

Equations

Sen2015.spec Sen2015.Position.coda = (Latin.l.setFeature Phonology.Feature.high true).setFeature Phonology.Feature.back true
Sen2015.spec Sen2015.Position.geminate = (Latin.l.setFeature Phonology.Feature.high true).setFeature Phonology.Feature.back false
Sen2015.spec Sen2015.Position.onset = Latin.l.setFeature Phonology.Feature.high true

Instances For

theorem Sen2015.spec_ternary :

(spec Position.coda).HasValue Phonology.Feature.back true ∧ (spec Position.geminate).HasValue Phonology.Feature.back false ∧ (spec Position.onset).Unspecified Phonology.Feature.back ∧ ∀ (p : Position), (spec p).HasValue Phonology.Feature.high true

The surface contrast (19), (23) is ternary, with plus, minus and unspecified [back], all [+high].

theorem Sen2015.extremes_specified (c : Context) :

(Context.coda ≤ c → c = Context.coda) ∧ (c ≤ Context.geminate → c = Context.geminate ∨ c = Context.preI)

The specified variants are the extremes of the scale. A context at least as dark as the coda is the coda, and one at least as clear as the geminate is the geminate or onset /l/ before /i/, its equal in darkness.

theorem Sen2015.onset_gradient :

Context.preBack.position = Position.onset ∧ Context.preE.position = Position.onset ∧ Context.preI.position = Position.onset ∧ Context.preI < Context.preE ∧ Context.preE < Context.preBack

Within the onset the specification is one and the darkness is not. Before /a o u/, /e/ and /i/ the same [Ø back] /l/ ranges over three degrees, so the categorical specification does not determine the colouring, the chapter's reason for rejecting synchronic feature spreading as its mechanism (§2.5).