Phenomena.Morphology.Studies.BickelNichols2013

@cite{bickel-nichols-2013a} @cite{bickel-nichols-2013b} @cite{bickel-nichols-2013c} @cite{bickel-nichols-2001}

Cross-linguistic analyses anchored on Bickel & Nichols's WALS chapters (Ch 20 fusion, Ch 21 exponence, Ch 22 inflectional synthesis) and their 2001 paper on the orthogonality of fusion and flexivity. The 18-language MorphProfile sample is the testbed.

Bickel & Nichols's central insight

The traditional 1D typological scale `isolating > agglutinating > fusional

polysynthetic conflates two orthogonal parameters: **fusion** (whether formatives are concatenative, nonlinear, or isolating) and **flexivity** (whether classes are predictable from form vs. arbitrary). Both "agglutinating" (concatenative + nonflexive) and "fusional" (concatenative + flexive`) are attested in the sample, demonstrating the two parameters are independent.

Contents

• §1. The 18-language MorphProfile sample (drawn from per-language Fragment profiles).
• §2. Substantive structural / orthogonality theorems on the B&N decomposition: both flexivity values attested under concatenative; every concatenative language is agglutinating ∨ fusional; nonlinear cell witnessed by Arabic; isolating cell has no flexivity.

Out of scope

The substrate types (MorphProfile, Fusion, Flexivity, ...) and WALS converters live in Core/Morphology/MorphProfile.lean. Per-language B&N classification commitments (e.g., "German is fusional") live in each Fragments/{Lang}/Morph.lean as local bridge theorems. @cite{ackerman-malouf-2013}'s E-complexity / I-complexity analysis lives in Studies/AckermanMalouf2013.lean.

This file deliberately omits aggregate-count theorems (sample_X_count = N) — exact counts go stale every time a Fragment is added to the sample. The mutual-exclusion theorem MorphProfile.agglutinating_fusional_exclusive is structural and lives in Core/Morphology/MorphProfile.lean §6.

Per-language Fragment profiles, with values derived from WALS data via Core.Morphology.wals* lookup helpers. Aliases here for concise reference in theorems below.

def Phenomena.Morphology.Studies.BickelNichols2013.allMorphProfiles : List Core.Morphology.MorphProfile

18-language morphological sample.

Equations

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

theorem Phenomena.Morphology.Studies.BickelNichols2013.morph_iso_unique : (List.map (fun (x : Core.Morphology.MorphProfile) => x.iso) allMorphProfiles).eraseDups.length = allMorphProfiles.length

Sentry: ISO codes are pairwise distinct across the sample. Catches accidental cross-language duplicates (two Fragments stipulating the same ISO) that per-Fragment sentries cannot see.

@cite{bickel-nichols-2001} argue fusion and flexivity are orthogonal, and that the four cells of the (concatenative ∪ nonlinear ∪ isolating) × (flexive ∪ nonflexive ∪ none) space are independently attested. The theorems below witness the cells the sample populates.

theorem Phenomena.Morphology.Studies.BickelNichols2013.concatenative_admits_both_flexivities : have concats := List.filter (fun (p : Core.Morphology.MorphProfile) => decide p.IsConcatenative) allMorphProfiles; (List.filter (fun (p : Core.Morphology.MorphProfile) => decide p.IsFlexive) concats).length > 0 ∧ (List.filter (fun (p : Core.Morphology.MorphProfile) => decide p.IsNonflexive) concats).length > 0

Key orthogonality test: among concatenative languages, both flexive and nonflexive are attested. This refutes the traditional 1D scale's claim that fusion-axis values determine flexivity-axis values.

theorem Phenomena.Morphology.Studies.BickelNichols2013.arabic_nonlinear_flexive : Phenomena.Morphology.Studies.BickelNichols2013.arabicMorph✝.IsNonlinear ∧ Phenomena.Morphology.Studies.BickelNichols2013.arabicMorph✝.IsFlexive ∧ Phenomena.Morphology.Studies.BickelNichols2013.arabicMorph✝.IsCumulative

Nonlinear cell witnessed by Arabic root-and-pattern morphology. The sample's only nonlinear member is also flexive and cumulative — the classic templatic profile.

theorem Phenomena.Morphology.Studies.BickelNichols2013.isolating_no_flexivity : Phenomena.Morphology.Studies.BickelNichols2013.mandarinMorph✝.flexivity = none ∧ Phenomena.Morphology.Studies.BickelNichols2013.thaiMorph✝.flexivity = none

Isolating cell (Mandarin, Thai) has no flexivity / no exponence marking — the B&N parameters do not apply to isolating typology.

theorem Phenomena.Morphology.Studies.BickelNichols2013.exponence_scope_independent : (List.filter (fun (p : Core.Morphology.MorphProfile) => decide (p.exponence = Core.Morphology.Exponence.polyexponential ∧ p.bnExponence = some Core.Morphology.ExponenceScope.separative)) allMorphProfiles).length > 0 ∧ (List.filter (fun (p : Core.Morphology.MorphProfile) => decide (p.exponence = Core.Morphology.Exponence.monoexponential ∧ p.bnExponence = some Core.Morphology.ExponenceScope.cumulative)) allMorphProfiles).length > 0

WALS Exponence (Ch 21A, case-specific) and B&N ExponenceScope (general) are independent: both poly+sep (Finnish, Tagalog) and mono+cum (Hindi, Georgian, Spanish) are attested in the sample.

theorem Phenomena.Morphology.Studies.BickelNichols2013.concatenative_partition (p : Core.Morphology.MorphProfile) : p ∈ allMorphProfiles → p.IsConcatenative → p.IsAgglutinating ∨ p.IsFusional

B&N decomposition is exhaustive on the concatenative dimension: every concatenative language in the sample is either agglutinating (concatenative + nonflexive + separative) or fusional (concatenative + flexive + cumulative).

theorem Phenomena.Morphology.Studies.BickelNichols2013.sample_type_exhaustive : allMorphProfiles.length = (List.filter (fun (p : Core.Morphology.MorphProfile) => decide p.IsAgglutinating) allMorphProfiles).length + (List.filter (fun (p : Core.Morphology.MorphProfile) => decide p.IsFusional) allMorphProfiles).length + (List.filter (fun (p : Core.Morphology.MorphProfile) => decide p.IsNonlinear) allMorphProfiles).length + (List.filter (fun (p : Core.Morphology.MorphProfile) => decide p.IsIsolating) allMorphProfiles).length

Sample partition: every language falls into exactly one of agglutinating / fusional / nonlinear / isolating. The disjointness half lives in Core/Morphology/MorphProfile.lean §6 as a structural theorem (MorphProfile.agglutinating_fusional_exclusive); this is the empirical claim that the four cells exhaust the sample.