Doubling Theory: Identity vs. Reduplication

The theoretical framework for the double identity of doubling: the same surface form XX is structurally ambiguous between phonological identity (two independent identical segments, banned by OCP) and morphological reduplication (RED + base, preferred when the morphological context licenses it).

Key types

• DoublingFunction: what morphological category doubling expresses (plurality, diminutive, etc.)
• DoublingGrammar: parameterizes the model by a speaker's L1 — which functions the L1 marks morphologically, and which it marks by reduplication specifically
• DoublingParse: the structural parse of a doubled form
• realizeMorphAvailable: derives whether REALIZE-MORPH is active for a given function from the L1's DoublingGrammar

Positive and negative transfer

Following @cite{berent-bat-el-brentari-dupuis-vaknin-nusbaum-2016}:

• Positive transfer: if the L1 expresses function f morphologically, speakers can interpret XX as morphological reduplication for f
• Negative transfer: if the L1 uses reduplication for other functions but specifically NOT for f, that blocks the reduplication interpretation for f

The realizeMorphAvailable predicate encodes both transfer directions: REALIZE-MORPH is active for function f when (i) the L1 marks f morphologically AND (ii) the L1 has no negative evidence (does not use reduplication for other functions while excluding f).

@cite{berent-bat-el-brentari-dupuis-vaknin-nusbaum-2016} @cite{berent-2026}

inductive Phonology.Doubling.DoublingFunction : Type

Morphological function that doubling can express.

Different languages use reduplication for different morphological categories. The availability of the reduplication parse for a given semantic context depends on the speaker's L1 morphology.

• plurality : DoublingFunction
• diminutive : DoublingFunction

@[implicit_reducible]

instance Phonology.Doubling.instDecidableEqDoublingFunction : DecidableEq DoublingFunction

Equations

• Phonology.Doubling.instDecidableEqDoublingFunction x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

def Phonology.Doubling.instReprDoublingFunction.repr : DoublingFunction → ℕ → Std.Format

Equations

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

@[implicit_reducible]

instance Phonology.Doubling.instReprDoublingFunction : Repr DoublingFunction

Equations

• Phonology.Doubling.instReprDoublingFunction = { reprPrec := Phonology.Doubling.instReprDoublingFunction.repr }

def Phonology.Doubling.DoublingFunction.all : List DoublingFunction

Complete enumeration of DoublingFunction constructors. Used by hasAnyRedup so that adding a constructor automatically updates the check (compile will fail on all_complete if the list is not updated).

Equations

• Phonology.Doubling.DoublingFunction.all = [Phonology.Doubling.DoublingFunction.plurality, Phonology.Doubling.DoublingFunction.diminutive]

theorem Phonology.Doubling.DoublingFunction.all_complete (f : DoublingFunction) : f ∈ all

structure Phonology.Doubling.DoublingGrammar : Type

A speaker's L1 morphological knowledge relevant to interpreting doubled forms.

Two dimensions determine whether a speaker interprets XX as morphological reduplication for function f:

1. morphFor f: does the L1 express f by any morphological means? (Necessary for morphological interpretation of XX-as-f.)
2. redupFor f: does the L1 express f specifically by reduplication? (Determines positive vs. negative transfer.)

• morphFor : DoublingFunction → Bool

  Does the L1 express function f by any morphological means? E.g., English marks plurality (dog-s) but not diminutives productively.

• redupFor : DoublingFunction → Bool

  Does the L1 express function f specifically by reduplication? E.g., Hebrew uses reduplication for diminutives but not plurality.

def Phonology.Doubling.DoublingGrammar.hasAnyRedup (g : DoublingGrammar) : Bool

Does the L1 use reduplication for any morphological function?

Defined via DoublingFunction.all rather than manual disjunction. Adding a new constructor to DoublingFunction will cause all_complete to fail unless all is updated, which automatically extends this check.

Equations

• g.hasAnyRedup = Phonology.Doubling.DoublingFunction.all.any g.redupFor

def Phonology.Doubling.realizeMorphAvailable (g : DoublingGrammar) (f : DoublingFunction) : Bool

Is REALIZE-MORPH available for function f given the speaker's L1?

REALIZE-MORPH is active when: (i) the L1 expresses f morphologically (morphFor f), AND (ii) there is no negative transfer — if the L1 uses reduplication at all, it must include f among the functions expressed by reduplication.

Negative transfer (@cite{berent-bat-el-brentari-dupuis-vaknin-nusbaum-2016}): when a speaker's L1 uses reduplication for function A but not B, the speaker has positive evidence that reduplication != B. This blocks the reduplication parse for B even if B is morphologically marked by other means.

Equations

• Phonology.Doubling.realizeMorphAvailable g f = (g.morphFor f && (!g.hasAnyRedup || g.redupFor f))

theorem Phonology.Doubling.no_morph_no_realizeMorph (g : DoublingGrammar) (f : DoublingFunction) (h : g.morphFor f = false) : realizeMorphAvailable g f = false

No morphology → no REALIZE-MORPH, regardless of reduplication status.

This is the prerequisite: the L1 must express f morphologically at all before the reduplication parse is even considered.

theorem Phonology.Doubling.no_redup_no_negative_transfer (g : DoublingGrammar) (f : DoublingFunction) (h : g.hasAnyRedup = false) : realizeMorphAvailable g f = g.morphFor f

Without productive reduplication, there is no negative transfer: REALIZE-MORPH availability reduces to whether the L1 marks f morphologically.

This is why English-type grammars (no productive reduplication) have no negative transfer — without reduplication in the L1, there is no evidence against any particular function.

theorem Phonology.Doubling.redup_positive_transfer (g : DoublingGrammar) (f : DoublingFunction) (hm : g.morphFor f = true) (hr : g.redupFor f = true) : realizeMorphAvailable g f = true

When the L1 uses reduplication for f AND marks f morphologically, REALIZE-MORPH is available (positive transfer).

This is why Hebrew diminutives get positive transfer: Hebrew uses reduplication specifically for diminutives.

theorem Phonology.Doubling.redup_negative_transfer (g : DoublingGrammar) (f : DoublingFunction) (hany : g.hasAnyRedup = true) (hnot : g.redupFor f = false) : realizeMorphAvailable g f = false

When the L1 uses reduplication for some function but NOT for f, negative transfer blocks REALIZE-MORPH for f even if f is morphologically marked.

This is why Hebrew speakers disprefer XX for plurality: Hebrew uses reduplication for diminutives but not plurality, providing evidence that reduplication != plurality.

theorem Phonology.Doubling.realizeMorphAvailable_complete (g : DoublingGrammar) (f : DoublingFunction) : (g.morphFor f = false → realizeMorphAvailable g f = false) ∧ (g.morphFor f = true → g.hasAnyRedup = false → realizeMorphAvailable g f = true) ∧ (g.morphFor f = true → g.redupFor f = true → realizeMorphAvailable g f = true) ∧ (g.hasAnyRedup = true → g.redupFor f = false → realizeMorphAvailable g f = false)

Complete characterization of realizeMorphAvailable: the four transfer theorems above exhaust all cases. Every combination of morphFor f, hasAnyRedup, and redupFor f is covered.

This is the mathlib-style exhaustive case analysis: any function satisfying these four properties agrees with realizeMorphAvailable on all inputs.

theorem Phonology.Doubling.redupFor_not_monotone : ∃ (g₁ : DoublingGrammar) (g₂ : DoublingGrammar) (f : DoublingFunction), g₁.morphFor = g₂.morphFor ∧ (∀ (x : DoublingFunction), g₁.redupFor x = true → g₂.redupFor x = true) ∧ realizeMorphAvailable g₁ f = true ∧ realizeMorphAvailable g₂ f = false

redupFor is NOT monotone: adding reduplication for another function can block REALIZE-MORPH for f (negative transfer).

Witness: g₁ has no reduplication and marks plurality morphologically, so REALIZE-MORPH is available. g₂ adds reduplication for diminutives only. Now REALIZE-MORPH for plurality is blocked — the speaker has evidence that reduplication ≠ plurality.

def Phonology.Doubling.noRedupGrammar (morphFor : DoublingFunction → Bool) : DoublingGrammar

Languages without productive reduplication (WALS Ch 27) have no reduplication for any DoublingFunction.

This connects the DoublingGrammar framework to the coarse-grained MorphProfile.Reduplication typology: if Reduplication = .noProductive, then redupFor f = false for all f, which means hasAnyRedup = false and negative transfer is impossible (by no_redup_no_negative_transfer).

Equations

• Phonology.Doubling.noRedupGrammar morphFor = { morphFor := morphFor, redupFor := fun (x : Phonology.Doubling.DoublingFunction) => false }

theorem Phonology.Doubling.noRedupGrammar_no_redup (morphFor : DoublingFunction → Bool) : (noRedupGrammar morphFor).hasAnyRedup = false

theorem Phonology.Doubling.noRedup_realizeMorph (morphFor : DoublingFunction → Bool) (f : DoublingFunction) : realizeMorphAvailable (noRedupGrammar morphFor) f = morphFor f

For languages without productive reduplication, REALIZE-MORPH availability equals morphFor f — no negative transfer is possible. Connects MorphProfile.reduplication = .noProductive to the doubling predictions.

inductive Phonology.Doubling.DoublingParse : Type

Parse of a doubled form XX.

The same surface form XX is structurally ambiguous between two parses:

• Identity (phonological): two independent identical segments. Banned by OCP — the phonological grammar disprefers it.

• Reduplication (morphological): a RED morpheme copies the base. Preferred when the morphological context licenses it.

• Nonidentical: XY control (no doubling).

• identity : DoublingParse
• reduplication : DoublingParse
• nonidentical : DoublingParse

@[implicit_reducible]

instance Phonology.Doubling.instDecidableEqDoublingParse : DecidableEq DoublingParse

Equations

• Phonology.Doubling.instDecidableEqDoublingParse x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

def Phonology.Doubling.instReprDoublingParse.repr : DoublingParse → ℕ → Std.Format

Equations

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

@[implicit_reducible]

instance Phonology.Doubling.instReprDoublingParse : Repr DoublingParse

Equations

• Phonology.Doubling.instReprDoublingParse = { reprPrec := Phonology.Doubling.instReprDoublingParse.repr }

def Phonology.Doubling.ocpXX : Core.Constraint.OT.NamedConstraint DoublingParse

OCP-XX: penalizes phonological identity. Violated by the identity parse, not by reduplication or XY.

Conceptually related to the general mkOCP constraint in Constraints.lean (both penalize adjacent identity), but operates at a different level of abstraction: mkOCP counts adjacent identical pairs on a feature tier, while ocpXX classifies the parse of a doubled form as phonological identity vs. morphological reduplication.

Equations

• Phonology.Doubling.ocpXX = Core.Constraint.OT.mkMark "OCP-XX" fun (x : Phonology.Doubling.DoublingParse) => x = Phonology.Doubling.DoublingParse.identity

def Phonology.Doubling.starRED : Core.Constraint.OT.NamedConstraint DoublingParse

*RED: general markedness against reduplication. Violated by the reduplicative parse (morphological cost of RED).

Equations

• Phonology.Doubling.starRED = Core.Constraint.OT.mkMark "*RED" fun (x : Phonology.Doubling.DoublingParse) => x = Phonology.Doubling.DoublingParse.reduplication

def Phonology.Doubling.realizeMorph : Core.Constraint.OT.NamedConstraint DoublingParse

REALIZE-MORPH: faithfulness to the morphological specification. When the input specifies a morphological operation (e.g., plurality expressed via reduplication), the output must realize it.

Violated by the nonidentical parse (XY doesn't express the morphological specification). Active only when the speaker's L1 makes the reduplication interpretation available for the relevant morphological function (see realizeMorphAvailable).

Equations

• Phonology.Doubling.realizeMorph = Phonology.Constraints.mkMax "REALIZE-MORPH" fun (x : Phonology.Doubling.DoublingParse) => x = Phonology.Doubling.DoublingParse.nonidentical

def Phonology.Doubling.phonRanking : List (Core.Constraint.OT.NamedConstraint DoublingParse)

Phonological ranking: only OCP-XX and *RED are active. REALIZE-MORPH is absent (no morphological specification).

Equations

• Phonology.Doubling.phonRanking = [Phonology.Doubling.ocpXX, Phonology.Doubling.starRED]

def Phonology.Doubling.morphRanking : List (Core.Constraint.OT.NamedConstraint DoublingParse)

Morphological ranking: OCP-XX >> REALIZE-MORPH >> *RED. Active when the morphological context licenses reduplication AND the speaker's L1 makes it available.

Equations

• Phonology.Doubling.morphRanking = [Phonology.Doubling.ocpXX, Phonology.Doubling.realizeMorph, Phonology.Doubling.starRED]

def Phonology.Doubling.phonCandidates : List DoublingParse

Candidates in a phonological context or when reduplication is unavailable: identity or nonidentical. Reduplication is not a candidate (no morphological trigger or no L1 support).

Equations

• Phonology.Doubling.phonCandidates = [Phonology.Doubling.DoublingParse.identity, Phonology.Doubling.DoublingParse.nonidentical]

def Phonology.Doubling.morphCandidates : List DoublingParse

Candidates in a morphological context where reduplication is available: all three parses compete.

Equations

• Phonology.Doubling.morphCandidates = [Phonology.Doubling.DoublingParse.identity, Phonology.Doubling.DoublingParse.reduplication, Phonology.Doubling.DoublingParse.nonidentical]

def Phonology.Doubling.l1CandidatesFor (g : DoublingGrammar) (f : DoublingFunction) : List DoublingParse

Candidate set for a given L1 and morphological function. Reduplication is a candidate only when the L1 makes it available for the relevant function.

Equations

• Phonology.Doubling.l1CandidatesFor g f = if Phonology.Doubling.realizeMorphAvailable g f = true then Phonology.Doubling.morphCandidates else Phonology.Doubling.phonCandidates

def Phonology.Doubling.l1RankingFor (g : DoublingGrammar) (f : DoublingFunction) : List (Core.Constraint.OT.NamedConstraint DoublingParse)

Constraint ranking for a given L1 and morphological function. REALIZE-MORPH is in the ranking only when the L1 makes it available for the relevant function.

Equations

• Phonology.Doubling.l1RankingFor g f = if Phonology.Doubling.realizeMorphAvailable g f = true then Phonology.Doubling.morphRanking else Phonology.Doubling.phonRanking

theorem Phonology.Doubling.l1CandidatesFor_ne (g : DoublingGrammar) (f : DoublingFunction) : l1CandidatesFor g f ≠ []

theorem Phonology.Doubling.phon_prefers_XY : (Core.Constraint.OT.mkTableau phonCandidates phonRanking ⋯).optimal = {DoublingParse.nonidentical}

In phonological contexts (no morphological trigger), XY wins. OCP-XX bans identity; *RED is irrelevant since reduplication is not a candidate.

theorem Phonology.Doubling.morph_prefers_reduplication : (Core.Constraint.OT.mkTableau morphCandidates morphRanking ⋯).optimal = {DoublingParse.reduplication}

In morphological contexts where reduplication is available, reduplication wins. OCP-XX bans identity; REALIZE-MORPH bans nonidentical; reduplication violates only low-ranked *RED.

theorem Phonology.Doubling.doubling_reversal : (Core.Constraint.OT.mkTableau phonCandidates phonRanking ⋯).optimal = {DoublingParse.nonidentical} ∧ (Core.Constraint.OT.mkTableau morphCandidates morphRanking ⋯).optimal = {DoublingParse.reduplication}

The phonology--morphology reversal: context determines which constraints are active, producing opposite surface preferences from the same underlying OCP-XX.