Laoide-Kemp (2026): Strict modularity at the morphosyntax-phonology interface

This file formalizes the analysis of [LK26] of the Irish historic-tense particle d', which appears before vowel-initial and lenited f-initial verbs but not before other consonants ((11)), an apparent paradox for the autosegmental account of initial consonant mutation, since the particle taken to trigger lenition seems to be inserted only once lenition has applied. On the paper's account the exponent of historic tense is a floating segment (d) followed by the lenition-inducing bundle {L} ((18)): both are inserted in every environment, {L} docks onto the following consonant, deleting the segmental content of an f (§2.2), and (d) is pronounced only if it can link to an adjacent skeletal C-slot that is empty and directly followed by a filled V-slot (§4.1). Over the library's floating autosegmental forms on a strict-CV skeleton ([Low96]), the historic exponent is prefixed by concatenation, lenition is the surface delinking of a word-initial f, and the docking condition is read off the surface form: (d) surfaces before ól and fág but not before bog (Figure 1), and never before a past-tense impersonal, whose empty initial CV unit blocks both lenition and docking (Figure 5, §6.2), the two effects of one piece of structure (laoideKemp_fig1_fig5, impersonal_blocks_lenition). The analysis is strictly modular in the sense of [BO12]: the morpheme is inserted uniformly and the phonology decides.

Implementation notes

The segment inventory covers the paper's examples only. Lenition is modelled as the deletion of f alone, the one effect that bears on the distribution of (d), and targets the melody linked to the leftmost skeletal slot, so the empty CV unit of an impersonal keeps the stem's f out of reach. The infrasegmental-government domains that license (d) before the lenited clusters of (12) (Figure 2, [Sch98]), the Munster reanalysis of (d) as part of the lenition bundle (§6.1, Table 3), and the rejected morphosyntactic alternative of §5 are not modelled.

TODO

Model Figure 2, the r- against fr-initial contrast, once a government substrate exists.

References

• [LK26]
• [BO12], [Low96], [Gus86], [NC91], [Sch98]

Segments and skeleton

inductive LaoideKemp2026.Segment : Type

The segments of the paper's worked examples.

• b : Segment

  Consonant b.

• g : Segment

  Consonant g.

• l : Segment

  Consonant l.

• f : Segment

  Consonant f.

• r : Segment

  Consonant r.

• m : Segment

  Consonant m.

• o : Segment

  Vowel o.

• ó : Segment

  Vowel ó.

• á : Segment

  Vowel á.

• i : Segment

  Vowel i.

• a : Segment

  Schwa-like vowel a (Irish a).

• dPrime : Segment

  The historic-tense floating segment (d).

@[instance_reducible]

instance LaoideKemp2026.instDecidableEqSegment : DecidableEq Segment

Equations

• LaoideKemp2026.instDecidableEqSegment x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

@[instance_reducible]

instance LaoideKemp2026.instReprSegment : Repr Segment

Equations

• LaoideKemp2026.instReprSegment = { reprPrec := LaoideKemp2026.instReprSegment.repr }

def LaoideKemp2026.instReprSegment.repr : Segment → ℕ → Std.Format

Equations

• One or more equations did not get rendered due to their size.
• LaoideKemp2026.instReprSegment.repr LaoideKemp2026.Segment.b prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "LaoideKemp2026.Segment.b")).group prec✝
• LaoideKemp2026.instReprSegment.repr LaoideKemp2026.Segment.g prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "LaoideKemp2026.Segment.g")).group prec✝
• LaoideKemp2026.instReprSegment.repr LaoideKemp2026.Segment.l prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "LaoideKemp2026.Segment.l")).group prec✝
• LaoideKemp2026.instReprSegment.repr LaoideKemp2026.Segment.f prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "LaoideKemp2026.Segment.f")).group prec✝
• LaoideKemp2026.instReprSegment.repr LaoideKemp2026.Segment.r prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "LaoideKemp2026.Segment.r")).group prec✝
• LaoideKemp2026.instReprSegment.repr LaoideKemp2026.Segment.m prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "LaoideKemp2026.Segment.m")).group prec✝
• LaoideKemp2026.instReprSegment.repr LaoideKemp2026.Segment.o prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "LaoideKemp2026.Segment.o")).group prec✝
• LaoideKemp2026.instReprSegment.repr LaoideKemp2026.Segment.ó prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "LaoideKemp2026.Segment.ó")).group prec✝
• LaoideKemp2026.instReprSegment.repr LaoideKemp2026.Segment.á prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "LaoideKemp2026.Segment.á")).group prec✝
• LaoideKemp2026.instReprSegment.repr LaoideKemp2026.Segment.i prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "LaoideKemp2026.Segment.i")).group prec✝
• LaoideKemp2026.instReprSegment.repr LaoideKemp2026.Segment.a prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "LaoideKemp2026.Segment.a")).group prec✝

def LaoideKemp2026.Segment.isF : Segment → Bool

The segment f, whose content lenition deletes (§2.2).

Equations

• LaoideKemp2026.Segment.f.isF = true
• x✝.isF = false

inductive LaoideKemp2026.CVKind : Type

A slot of the strict-CV skeleton ([Low96]).

• C : CVKind
• V : CVKind

@[instance_reducible]

instance LaoideKemp2026.instDecidableEqCVKind : DecidableEq CVKind

Equations

• LaoideKemp2026.instDecidableEqCVKind x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

def LaoideKemp2026.instReprCVKind.repr : CVKind → ℕ → Std.Format

Equations

• LaoideKemp2026.instReprCVKind.repr LaoideKemp2026.CVKind.C prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "LaoideKemp2026.CVKind.C")).group prec✝
• LaoideKemp2026.instReprCVKind.repr LaoideKemp2026.CVKind.V prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "LaoideKemp2026.CVKind.V")).group prec✝

@[instance_reducible]

instance LaoideKemp2026.instReprCVKind : Repr CVKind

Equations

• LaoideKemp2026.instReprCVKind = { reprPrec := LaoideKemp2026.instReprCVKind.repr }

Morphemes

Every tier and skeletal element carries its morpheme: the verb stem, the historic-tense exponent bearing the floating (d), and the past-tense impersonal exponent bearing the empty CV unit (§6.2).

def LaoideKemp2026.mStem (s : String) : Morphology.Morph

The verb-stem morpheme (a free word), keyed by orthographic form.

Equations

• LaoideKemp2026.mStem s = Morphology.Morph.root s

def LaoideKemp2026.mHist : Morphology.Morph

The historic-tense exponent, bearing (d) and {L}.

Equations

• LaoideKemp2026.mHist = Morphology.Morph.pref "d'"

def LaoideKemp2026.mImpers : Morphology.Morph

The past-tense impersonal exponent (§6.2).

Equations

• LaoideKemp2026.mImpers = Morphology.Morph.pref ""

Verb stems

A stem is a floating form whose upper tier is the melody, whose lower tier is the CV skeleton, and whose association lines (k, j) link melody element k to skeletal slot j; on input the surface state is the underlying one.

def LaoideKemp2026.stemForm (name : String) (skeleton : List CVKind) (mel : List Segment) (links : Finset (ℕ × ℕ)) : Autosegmental.Form CVKind Segment Morphology.Morph

Build a single-morpheme verb stem from its CV skeleton, melody, and association lines.

Equations

• LaoideKemp2026.stemForm name skeleton mel links = Autosegmental.Form.melody (LaoideKemp2026.mStem name) mel skeleton links

def LaoideKemp2026.bog : Autosegmental.Form CVKind Segment Morphology.Morph

bog 'move', consonant-initial (Figure 1a).

Equations

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

def LaoideKemp2026.ól : Autosegmental.Form CVKind Segment Morphology.Morph

ól 'drink', vowel-initial (Figure 1b): the initial C-slot is empty underlyingly.

Equations

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

def LaoideKemp2026.fág : Autosegmental.Form CVKind Segment Morphology.Morph

fág 'leave', f-initial (Figure 1c).

Equations

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

The exponents

The historic-tense morpheme contributes a floating (d) with no skeleton of its own ((18)), and the past-tense impersonal morpheme an empty CV unit with no melody (Figure 5); each is prefixed to a stem by concatenation, which shifts the stem's association lines by the prefix's tier lengths.

def LaoideKemp2026.historicExponent : Autosegmental.Form CVKind Segment Morphology.Morph

The historic-tense exponent ((18)): a floating (d), no skeleton, no associations.

Equations

• LaoideKemp2026.historicExponent = Autosegmental.Form.melody LaoideKemp2026.mHist [LaoideKemp2026.Segment.dPrime] [] ∅

def LaoideKemp2026.impersonalExponent : Autosegmental.Form CVKind Segment Morphology.Morph

The past-tense impersonal exponent (§6.2, Figure 5): an empty CV unit, no melody.

Equations

• LaoideKemp2026.impersonalExponent = Autosegmental.Form.melody LaoideKemp2026.mImpers [] [LaoideKemp2026.CVKind.C, LaoideKemp2026.CVKind.V] ∅

def LaoideKemp2026.withHist (stem : Autosegmental.Form CVKind Segment Morphology.Morph) : Autosegmental.Form CVKind Segment Morphology.Morph

In the historic-tense form of a stem, (d) becomes melody element 0.

Equations

• LaoideKemp2026.withHist stem = LaoideKemp2026.historicExponent.concat stem

def LaoideKemp2026.withImpers (stem : Autosegmental.Form CVKind Segment Morphology.Morph) : Autosegmental.Form CVKind Segment Morphology.Morph

The past-tense impersonal of a stem adds an empty CV unit at the left edge.

Equations

• LaoideKemp2026.withImpers stem = LaoideKemp2026.impersonalExponent.concat stem

Lenition

Of the effects of lenition only the deletion of a word-initial f bears on the distribution of (d) (§2.2, [Gus86], [NC91]): {L} docks onto the initial consonant and removes its segmental content, leaving the skeletal slot behind. This is a surface delinking of the f from its slot, and it targets the melody linked to the leftmost skeletal slot, so that behind an empty CV unit (Figure 5) the stem's f is out of reach.

def LaoideKemp2026.initialConsonantIdx {u : Autosegmental.Form CVKind Segment Morphology.Morph} (c : Autosegmental.Candidate u) : Option (Fin u.upper.length)

The melody index of the consonant linked to the leftmost skeletal slot, the target of {L}.

Equations

• LaoideKemp2026.initialConsonantIdx c = List.find? (fun (k : Fin u.upper.length) => decide (∃ l ∈ c.links, l.1 = k ∧ ↑l.2 = 0)) (List.finRange u.upper.length)

def LaoideKemp2026.lenite {u : Autosegmental.Form CVKind Segment Morphology.Morph} (c : Autosegmental.Candidate u) : Autosegmental.Candidate u

Lenition deletes the melodic content of an f on the leftmost skeletal slot on the surface, leaving the slot empty.

Equations

• LaoideKemp2026.lenite c = match LaoideKemp2026.initialConsonantIdx c with | some k => if u.upper[k].value = LaoideKemp2026.Segment.f then c.deleteTierElem k else c | none => c

Docking

(d) is pronounced iff, after lenition, the first skeletal slot is an empty C-slot directly followed by a filled V-slot (§4.1).

def LaoideKemp2026.dDockable {u : Autosegmental.Form CVKind Segment Morphology.Morph} (c : Autosegmental.Candidate u) : Prop

The configuration that licenses the docking of (d) on the surface has slot 0 an empty C-slot and slot 1 a filled V-slot (§4.1).

Equations

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

@[instance_reducible]

instance LaoideKemp2026.instDecidableDDockable {u : Autosegmental.Form CVKind Segment Morphology.Morph} (c : Autosegmental.Candidate u) : Decidable (dDockable c)

Equations

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

def LaoideKemp2026.dPrimeSurfaces {u : Autosegmental.Form CVKind Segment Morphology.Morph} (c : Autosegmental.Candidate u) : Prop

(d) surfaces in a historic-tense form iff the lenited form licenses its docking.

Equations

• LaoideKemp2026.dPrimeSurfaces c = LaoideKemp2026.dDockable (LaoideKemp2026.lenite c)

@[instance_reducible]

instance LaoideKemp2026.instDecidableDPrimeSurfaces {u : Autosegmental.Form CVKind Segment Morphology.Morph} (c : Autosegmental.Candidate u) : Decidable (dPrimeSurfaces c)

Equations

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

Figure 1

In every historic-tense form (d) is melody element 0 and floating before docking.

theorem LaoideKemp2026.dPrime_floating_bog : (Autosegmental.Candidate.input (withHist bog)).IsFloating ⟨0, dPrime_floating_bog._proof_1⟩

(d) is floating in a historic-tense form before docking.

theorem LaoideKemp2026.bog_no_dPrime : ¬dPrimeSurfaces (Autosegmental.Candidate.input (withHist bog))

In Figure 1a, bog → bhog, the first C-slot is occupied and lenition leaves a segment in it, so (d) cannot dock ((11c)).

theorem LaoideKemp2026.ól_yes_dPrime : dPrimeSurfaces (Autosegmental.Candidate.input (withHist ól))

In Figure 1b, ól → d' ól, the first C-slot is empty underlyingly, {L} has nothing to dock onto, and (d) links ((11a)).

theorem LaoideKemp2026.fág_yes_dPrime : dPrimeSurfaces (Autosegmental.Candidate.input (withHist fág))

In Figure 1c, fág → d' fhág, lenition deletes the f, leaving the first C-slot empty on the surface, and (d) links ((11b)).

Figure 5

A past-tense impersonal carries an empty CV unit at its left edge (§6.2), which does double duty: {L} finds no consonant to dock onto, and the empty C-slot is followed by an empty V-slot, so (d) cannot link either ((27)).

theorem LaoideKemp2026.bogadh_no_dPrime : ¬dPrimeSurfaces (Autosegmental.Candidate.input (withHist (withImpers bog)))

Figure 5a, bogadh, has no (d).

theorem LaoideKemp2026.óladh_no_dPrime : ¬dPrimeSurfaces (Autosegmental.Candidate.input (withHist (withImpers ól)))

In Figure 5b, óladh, the empty V-slot of the prefix blocks docking although the verb is vowel-initial.

theorem LaoideKemp2026.fágadh_no_dPrime : ¬dPrimeSurfaces (Autosegmental.Candidate.input (withHist (withImpers fág)))

In Figure 5c, fágadh, the empty C-slot keeps {L} from the stem's f, and the empty V-slot blocks (d).

theorem LaoideKemp2026.laoideKemp_fig1_fig5 : (¬dPrimeSurfaces (Autosegmental.Candidate.input (withHist bog)) ∧ dPrimeSurfaces (Autosegmental.Candidate.input (withHist ól)) ∧ dPrimeSurfaces (Autosegmental.Candidate.input (withHist fág))) ∧ ¬dPrimeSurfaces (Autosegmental.Candidate.input (withHist (withImpers bog))) ∧ ¬dPrimeSurfaces (Autosegmental.Candidate.input (withHist (withImpers ól))) ∧ ¬dPrimeSurfaces (Autosegmental.Candidate.input (withHist (withImpers fág)))

In the historic tense (d) surfaces before a vowel-initial or f-initial verb and not before a consonant-initial one, and never before a past-tense impersonal (Figures 1 and 5).

theorem LaoideKemp2026.impersonal_blocks_lenition : initialConsonantIdx (Autosegmental.Candidate.input (withImpers fág)) = none

Seen from the other side of Figure 5, the empty CV unit leaves {L} no consonant to dock onto, so an impersonal resists lenition even after a lenition-triggering particle ((26b)).