Berent et al. (2016): The double identity of linguistic doubling

This file formalizes the account of doubling by Berent, Bat-El, Brentari, Dupuis and Vaknin-Nusbaum. A doubled form XX has two parses. As a single morpheme it contains two identical constituents, which the Obligatory Contour Principle (OCP) bans. As a base followed by its copy it is morphological reduplication, which languages favour. In twelve experiments speakers disliked doubled novel words and novel ASL signs presented in isolation, and preferred them once doubling was linked to the meaning of a taught base. English speakers preferred doubled signs as plurals and not as diminutives, while Hebrew speakers, whose reduplication marks diminution and never plurality, showed the opposite pattern.

The authors' formal analysis has two constraints and no ranking. At the phonological level XX violates the OCP and the control XY does not. At the morphological level the copy escapes the OCP, which operates within a morpheme, and satisfies DEP, the ban on output material without an input correspondent, which XY violates by adding material to the base. Here both violation patterns are computed from the parses, over any type of prosodic constituent. The winner at each level harmonically bounds its competitors, so the predictions hold under both rankings.

Main definitions

• Parse: a name as a single morpheme or as a base followed by its copy.
• ocp, dep: the OCP within each morpheme, and DEP against the taught base.
• Level, tableau: the level of analysis, and the competition it induces between a doubled name and its control.
• SpokenLanguage, SpokenLanguage.Licenses: the meanings a language marks morphologically and by reduplication, and the two transfer conditions on a morphological parse of doubling.

Main results

• Parse.surface_reduplicated: the two parses of doubling share a surface form.
• optimal_phonology, optimal_morphology: the control wins at the phonological level and the reduplicative parse at the morphological level, under every ranking.
• SpokenLanguage.licenses_iff: a language licenses a meaning when it reduplicates for it, or reduplicates for nothing and marks it otherwise.
• exists_optimal_surface_iff: doubling is preferred exactly for the licensed meanings.
• english_licenses_iff, hebrew_licenses_iff, licenses_not_monotone: English licenses the plural alone and Hebrew the diminutive alone, although Hebrew morphology extends English morphology on both dimensions.

Implementation notes

The control XY is a single morpheme at both levels, and DEP counts the constituents of a name's stem beyond the taught base. With no base taught a name is its own input, so DEP is vacuous. The reduplicative parse competes only at the morphological level, where the input contains the reduplicative morpheme. Negative evidence against reduplication for a meaning is read as the language reduplicating for other meanings only. The illicit conditions, where the base and the doubled form name objects of different kinds, are not modelled.

References

• [BBEB+16]
• [McC86]
• [McCP95]

The two parses of doubling

inductive BerentEtAl2016.Parse (α : Type u_3) : Type u_3

A morphological parse of a name over prosodic constituents of type α.

• simplex {α : Type u_3} (form : List α) : Parse α

  A single morpheme.

• reduplicated {α : Type u_3} (base : List α) : Parse α

  A base followed by its copy.

@[instance_reducible]

instance BerentEtAl2016.instDecidableEqParse {α✝ : Type u_3} [DecidableEq α✝] : DecidableEq (Parse α✝)

Equations

• BerentEtAl2016.instDecidableEqParse = BerentEtAl2016.instDecidableEqParse.decEq

def BerentEtAl2016.instDecidableEqParse.decEq {α✝ : Type u_3} [DecidableEq α✝] (x✝ x✝¹ : Parse α✝) : Decidable (x✝ = x✝¹)

Equations

• BerentEtAl2016.instDecidableEqParse.decEq (BerentEtAl2016.Parse.simplex a) (BerentEtAl2016.Parse.simplex b) = if h : a = b then h ▸ isTrue ⋯ else isFalse ⋯
• BerentEtAl2016.instDecidableEqParse.decEq (BerentEtAl2016.Parse.simplex form) (BerentEtAl2016.Parse.reduplicated base) = isFalse ⋯
• BerentEtAl2016.instDecidableEqParse.decEq (BerentEtAl2016.Parse.reduplicated base) (BerentEtAl2016.Parse.simplex form) = isFalse ⋯
• BerentEtAl2016.instDecidableEqParse.decEq (BerentEtAl2016.Parse.reduplicated a) (BerentEtAl2016.Parse.reduplicated b) = if h : a = b then h ▸ isTrue ⋯ else isFalse ⋯

def BerentEtAl2016.Parse.morphemes {α : Type u_1} : Parse α → List (List α)

The morphemes of a parse, in order.

Equations

• (BerentEtAl2016.Parse.simplex form).morphemes = [form]
• (BerentEtAl2016.Parse.reduplicated base).morphemes = [base, base]

def BerentEtAl2016.Parse.surface {α : Type u_1} (p : Parse α) : List α

The surface form of a parse, which does not record its morphemes.

Equations

• p.surface = p.morphemes.flatten

theorem BerentEtAl2016.Parse.surface_reduplicated {α : Type u_1} (base : List α) : (reduplicated base).surface = (simplex (base ++ base)).surface

A base followed by its copy has the surface form of the simplex double, so doubling is structurally ambiguous.

def BerentEtAl2016.Parse.correspondence {α : Type u_1} (input : List α) : Parse α → OptimalityTheory.Correspondence OptimalityTheory.ReduplicationRole α

The correspondence diagram of a parse against an input treats a simplex name as all stem, and the copy of a reduplicated name as its reduplicant.

Equations

• BerentEtAl2016.Parse.correspondence input (BerentEtAl2016.Parse.simplex form) = OptimalityTheory.Correspondence.reduplication input form []
• BerentEtAl2016.Parse.correspondence input (BerentEtAl2016.Parse.reduplicated base) = OptimalityTheory.Correspondence.reduplication input base base

The two levels of analysis

inductive BerentEtAl2016.Level : Type

The level at which a speaker analyses a name.

• phonology : Level

  A pattern of meaningless elements: the name in isolation.

• morphology : Level

  A form linked to the meaning of a taught base.

@[instance_reducible]

instance BerentEtAl2016.instDecidableEqLevel : DecidableEq Level

Equations

• BerentEtAl2016.instDecidableEqLevel x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

def BerentEtAl2016.Level.input {α : Type u_1} (x : α) : Level → Option (List α)

The taught base x is the input at the morphological level only.

Equations

• BerentEtAl2016.Level.input x BerentEtAl2016.Level.phonology = none
• BerentEtAl2016.Level.input x BerentEtAl2016.Level.morphology = some [x]

def BerentEtAl2016.candidates {α : Type u_1} (x y : α) : Level → List (Parse α)

The competitors for a doubled name XX and its control XY are the simplex parses at both levels, joined by the reduplicative parse at the morphological level.

Equations

• BerentEtAl2016.candidates x y BerentEtAl2016.Level.phonology = [BerentEtAl2016.Parse.simplex [x, y], BerentEtAl2016.Parse.simplex [x, x]]
• BerentEtAl2016.candidates x y BerentEtAl2016.Level.morphology = [BerentEtAl2016.Parse.reduplicated [x], BerentEtAl2016.Parse.simplex [x, y], BerentEtAl2016.Parse.simplex [x, x]]

theorem BerentEtAl2016.candidates_ne_nil {α : Type u_1} (x y : α) (l : Level) : candidates x y l ≠ []

The constraints

def BerentEtAl2016.dep {α : Type u_1} (base : Option (List α)) : OptimalityTheory.Constraint (Parse α)

DEP counts the constituents of the stem without a correspondent in the taught base. With no base taught, a name is its own input and DEP is vacuous.

Equations

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

@[simp]

theorem BerentEtAl2016.dep_none {α : Type u_1} (p : Parse α) : dep none p = 0

@[simp]

theorem BerentEtAl2016.dep_some_simplex {α : Type u_1} (b form : List α) : dep (some b) (Parse.simplex form) = form.length - b.length

A simplex name adds to the base whatever it has beyond the base's length.

@[simp]

theorem BerentEtAl2016.dep_some_reduplicated {α : Type u_1} (b base : List α) : dep (some b) (Parse.reduplicated base) = base.length - b.length

A reduplicated name adds to the taught base whatever its own base has beyond it, and its copy adds nothing.

def BerentEtAl2016.ocp {α : Type u_1} [DecidableEq α] : OptimalityTheory.Constraint (Parse α)

The OCP counts the adjacent identical constituents within each morpheme.

Equations

• BerentEtAl2016.ocp p = (List.map OptimalityTheory.Constraint.ocp p.morphemes).sum

@[simp]

theorem BerentEtAl2016.ocp_simplex_double {α : Type u_1} [DecidableEq α] (x : α) : ocp (Parse.simplex [x, x]) = 1

@[simp]

theorem BerentEtAl2016.ocp_simplex_pair {α : Type u_1} {x y : α} [DecidableEq α] (h : x ≠ y) : ocp (Parse.simplex [x, y]) = 0

@[simp]

theorem BerentEtAl2016.ocp_reduplicated_singleton {α : Type u_1} [DecidableEq α] (x : α) : ocp (Parse.reduplicated [x]) = 0

The OCP is inapplicable to a base and its copy, which are separate morphemes.

The competition between a doubled name and its control

def BerentEtAl2016.con {α : Type u_1} [DecidableEq α] (x : α) (l : Level) : OptimalityTheory.ConstraintSet (Parse α) (Fin 2)

The OCP and DEP against the input of the level.

Equations

• BerentEtAl2016.con x l = ![BerentEtAl2016.ocp, BerentEtAl2016.dep (BerentEtAl2016.Level.input x l)]

def BerentEtAl2016.tableau {α : Type u_1} [DecidableEq α] (x y : α) (l : Level) (r : OptimalityTheory.Ranking (Fin 2) 2) : OptimalityTheory.Tableau (Parse α) 2

The competition between XX and XY at a level, under a ranking of the OCP and DEP.

Equations

• BerentEtAl2016.tableau x y l r = OptimalityTheory.Tableau.ofPerm (BerentEtAl2016.con x l) r (BerentEtAl2016.candidates x y l) ⋯

theorem BerentEtAl2016.optimal_phonology {α : Type u_1} {x y : α} [DecidableEq α] (h : x ≠ y) (r : OptimalityTheory.Ranking (Fin 2) 2) : (tableau x y Level.phonology r).optimal = {Parse.simplex [x, y]}

At the phonological level the control wins under either ranking, because doubling is identity within a morpheme, which the OCP bans.

theorem BerentEtAl2016.optimal_morphology {α : Type u_1} {x y : α} [DecidableEq α] (h : x ≠ y) (r : OptimalityTheory.Ranking (Fin 2) 2) : (tableau x y Level.morphology r).optimal = {Parse.reduplicated [x]}

At the morphological level the reduplicative parse wins under either ranking, because it escapes the OCP and adds nothing to the base, while the control violates DEP.

Transfer from the spoken language

structure BerentEtAl2016.SpokenLanguage (M : Type u_3) : Type u_3

The morphology of a spoken language as it bears on doubling, over meanings M.

• marked : Finset M

  The meanings the language expresses by some morphological means.

• reduplicated : Finset M

  The meanings the language expresses by reduplication.

• reduplicated_subset : self.reduplicated ⊆ self.marked

  Reduplication is a morphological means.

def BerentEtAl2016.SpokenLanguage.Licenses {M : Type u_2} (l : SpokenLanguage M) (f : M) : Prop

A speaker parses doubling with meaning f morphologically when the spoken language gives positive evidence that morphology expresses f and no negative evidence that reduplication cannot: if it reduplicates at all, it does so for f.

Equations

• l.Licenses f = (f ∈ l.marked ∧ (l.reduplicated.Nonempty → f ∈ l.reduplicated))

@[instance_reducible]

instance BerentEtAl2016.SpokenLanguage.instDecidablePredLicensesOfDecidableEq {M : Type u_2} {l : SpokenLanguage M} [DecidableEq M] : DecidablePred l.Licenses

Equations

• BerentEtAl2016.SpokenLanguage.instDecidablePredLicensesOfDecidableEq x✝ = { decide := decide (x✝ ∈ l.marked) && decide (l.reduplicated.Nonempty → x✝ ∈ l.reduplicated), reflects_decide := ⋯ }

theorem BerentEtAl2016.SpokenLanguage.licenses_iff {M : Type u_2} {l : SpokenLanguage M} {f : M} : l.Licenses f ↔ f ∈ l.reduplicated ∨ l.reduplicated = ∅ ∧ f ∈ l.marked

theorem BerentEtAl2016.SpokenLanguage.licenses_of_mem {M : Type u_2} {l : SpokenLanguage M} {f : M} (h : f ∈ l.reduplicated) : l.Licenses f

Reduplication for a meaning licenses it, which is positive transfer.

theorem BerentEtAl2016.SpokenLanguage.not_licenses_of_mem_of_notMem {M : Type u_2} {l : SpokenLanguage M} {f g : M} (hg : g ∈ l.reduplicated) (hf : f ∉ l.reduplicated) : ¬l.Licenses f

Reduplication for another meaning only withdraws the licence, which is negative transfer.

theorem BerentEtAl2016.SpokenLanguage.licenses_iff_of_eq_empty {M : Type u_2} {l : SpokenLanguage M} {f : M} (h : l.reduplicated = ∅) : l.Licenses f ↔ f ∈ l.marked

A language without reduplication licenses exactly the meanings it marks.

def BerentEtAl2016.SpokenLanguage.level {M : Type u_2} [DecidableEq M] (l : SpokenLanguage M) (f : M) : Level

The level at which a speaker analyses a doubled name taught with meaning f.

Equations

• l.level f = if l.Licenses f then BerentEtAl2016.Level.morphology else BerentEtAl2016.Level.phonology

theorem BerentEtAl2016.exists_optimal_surface_iff {α : Type u_1} {M : Type u_2} {x y : α} [DecidableEq α] [DecidableEq M] (l : SpokenLanguage M) (f : M) (h : x ≠ y) (r : OptimalityTheory.Ranking (Fin 2) 2) : (∃ p ∈ (tableau x y (l.level f) r).optimal, p.surface = [x, x]) ↔ l.Licenses f

Doubling is preferred exactly for the meanings the spoken language licenses, in that the winner surfaces as XX when the meaning is licensed and as XY otherwise.

English and Hebrew

inductive BerentEtAl2016.Meaning : Type

The meanings paired with doubled signs in experiments 6 and 10–12.

• plural : Meaning
• diminutive : Meaning

@[instance_reducible]

instance BerentEtAl2016.instDecidableEqMeaning : DecidableEq Meaning

Equations

• BerentEtAl2016.instDecidableEqMeaning x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

def BerentEtAl2016.english : SpokenLanguage Meaning

English marks plurality, by suffixation (dog-s), has no productive diminutive, and reduplicates for nothing.

Equations

• BerentEtAl2016.english = { marked := {BerentEtAl2016.Meaning.plural}, reduplicated := ∅, reduplicated_subset := BerentEtAl2016.english._proof_1 }

def BerentEtAl2016.hebrew : SpokenLanguage Meaning

Hebrew marks plurality by suffixation (shir 'song', shirim 'songs') and diminution by reduplication (kelev 'dog', klavlav 'puppy'), which never marks plurality.

Equations

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

theorem BerentEtAl2016.english_licenses_iff {f : Meaning} : english.Licenses f ↔ f = Meaning.plural

theorem BerentEtAl2016.hebrew_licenses_iff {f : Meaning} : hebrew.Licenses f ↔ f = Meaning.diminutive

theorem BerentEtAl2016.licenses_not_monotone : english.marked ⊆ hebrew.marked ∧ english.reduplicated ⊆ hebrew.reduplicated ∧ english.Licenses Meaning.plural ∧ ¬hebrew.Licenses Meaning.plural

Licensing is not monotone in the morphology. Hebrew marks and reduplicates for everything English does, yet English speakers alone parse a doubled plural morphologically.

theorem BerentEtAl2016.doubling_dissociation {α : Type u_1} {x y : α} [DecidableEq α] (f : Meaning) (h : x ≠ y) (r : OptimalityTheory.Ranking (Fin 2) 2) : ((∃ p ∈ (tableau x y (english.level f) r).optimal, p.surface = [x, x]) ↔ f = Meaning.plural) ∧ ((∃ p ∈ (tableau x y (hebrew.level f) r).optimal, p.surface = [x, x]) ↔ f = Meaning.diminutive)

In the Language × Meaning interaction of experiments 6a and 10a–12a, English speakers prefer doubled plurals and Hebrew speakers doubled diminutives, under either ranking and for any constituents.