Nordlinger (2023) [Nor23]

Reciprocal constructions: a typological-formal review.

Formalizes the apparatus of [Nor23]'s review of reciprocal constructions, which summarizes earlier classificatory work ([KK06], [Mas08], [Eva08], [Ned07a], [Sil08], [Sil12], [DKK+98], [ELGM11]) and organizes the empirical picture around strategy/valency correlations (§3.2) and Siloni's discontinuity asymmetry (§3.3).

The underlying primitives (Marker, Strategy, Valency, Formation, ReflexiveRelation) live in Syntax/Reciprocal.lean, anchored on the earlier sources the review synthesizes — which preserves chronological dependency for Studies/Siloni2012.lean. Each profile below records a marker inventory; the primary strategy and the WALS Ch 106 reflexive-relation value are derived from it, and the WALS theorems check the derived values against the external WALS rows.

Contents

• RecipProfile per-language profiles (12 languages): marker inventory + observed valency, formation, and discontinuity judgments
• Strategy-valency correlation theorems (§3.2), including the derived default-valency check against Strategy.defaultValency
• Siloni's discontinuity prediction checked against attested judgments (§3.3)
• WALS Ch 106 grounding for the derived reflexive relation (via lookupISO)
• ReciprocityType semantic 6-way classification (§4), realized as the relation shapes of Semantics.Plurality.Reciprocal
• Polysemous markers beyond the profile sample (§4.2)
• Fragment grounding for English reciprocals

def Nordlinger2023.ofWALS106A : Data.WALS.F106A.ReciprocalType → Reciprocal.ReflexiveRelation

Convert a WALS 106A value to ReflexiveRelation (study-local: WALS grounding is this study's business, not the substrate's).

Equations

• Nordlinger2023.ofWALS106A Data.WALS.F106A.ReciprocalType.noReciprocalConstruction = Reciprocal.ReflexiveRelation.noDedicated
• Nordlinger2023.ofWALS106A Data.WALS.F106A.ReciprocalType.distinctFromReflexive = Reciprocal.ReflexiveRelation.distinctFromReflexive
• Nordlinger2023.ofWALS106A Data.WALS.F106A.ReciprocalType.mixed = Reciprocal.ReflexiveRelation.mixed
• Nordlinger2023.ofWALS106A Data.WALS.F106A.ReciprocalType.identicalToReflexive = Reciprocal.ReflexiveRelation.identicalToReflexive

Reciprocal profiles

structure Nordlinger2023.RecipProfile : Type

Per-language reciprocal profile: the marker inventory (primary strategy first) plus the observed valency, formation locus, and discontinuity judgments from [Nor23]'s review. The primary strategy and the WALS Ch 106 reflexive relation are derived from the inventory.

• language : String
• iso : String
• markers : List Reciprocal.Marker

  Marker inventory (primary strategy first), sourced from the language's Fragments/{Lang}/Reciprocals.lean.

• valency : Reciprocal.Valency

  Observed valency of the primary construction

• formation : Option Reciprocal.Formation

  Formation locus of verb-marked reciprocals ([Sil12])

• discontinuousAttested : Option Bool

  Attested availability of the discontinuous reciprocal construction ([Nor23] §3.3 judgments), independent of formation so Siloni's prediction can be checked rather than stipulated

@[instance_reducible]

instance Nordlinger2023.instReprRecipProfile : Repr RecipProfile

Equations

• Nordlinger2023.instReprRecipProfile = { reprPrec := Nordlinger2023.instReprRecipProfile.repr }

def Nordlinger2023.instReprRecipProfile.repr : RecipProfile → ℕ → Std.Format

Equations

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

@[instance_reducible]

instance Nordlinger2023.instDecidableEqRecipProfile : DecidableEq RecipProfile

Equations

• Nordlinger2023.instDecidableEqRecipProfile = Nordlinger2023.instDecidableEqRecipProfile.decEq

def Nordlinger2023.instDecidableEqRecipProfile.decEq (x✝ x✝¹ : RecipProfile) : Decidable (x✝ = x✝¹)

Equations

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

def Nordlinger2023.RecipProfile.primaryStrategy (p : RecipProfile) : Option Reciprocal.Strategy

Primary strategy: the strategy of the inventory's first marker.

Equations

• p.primaryStrategy = Option.map (fun (x : Reciprocal.Marker) => x.strategy) p.markers.head?

def Nordlinger2023.RecipProfile.reflexiveRelation (p : RecipProfile) : Reciprocal.ReflexiveRelation

WALS Ch 106 reflexive relation, derived from the marker inventory.

Equations

• p.reflexiveRelation = Reciprocal.ofInventory p.markers

def Nordlinger2023.rpEnglish : RecipProfile

English: bipartite NP each other (bivalent, distinct from reflexive; [Nor23] ex. 1b) plus lexical reciprocals (quarrel, meet, ex. 7). Per [Sil12] the lexical class is lexicon-formed, but kiss/hug resist the discontinuous construction (fn. 32), so no formation-level discontinuity value is recorded. Expresses all six reciprocity types (ex. 44).

Equations

• Nordlinger2023.rpEnglish = { language := "English", iso := "eng", markers := English.Reciprocals.markers, valency := Reciprocal.Valency.bivalent }

def Nordlinger2023.rpRussian : RecipProfile

Russian: bipartite NP drug druga 'other other-ACC' ([Nor23] ex. 9, grouped with English each other as the bipartite strategy) plus reflexive-identical verbal postfix -sja (monovalent; ex. 31). Unlike French se (a separable clitic), -sja is a bound suffix. Derived WALS value: mixed.

Equations

• Nordlinger2023.rpRussian = { language := "Russian", iso := "rus", markers := Russian.Reciprocals.markers, valency := Reciprocal.Valency.bivalent }

def Nordlinger2023.rpSwahili : RecipProfile

Swahili: verbal affix -an- (monovalent, distinct from reflexive -ji-; [Nor23] ex. 12). Forms discontinuous reciprocals with comitative na (ex. 37 from [Hur12], ex. 40 from [Dim04]), hence lexicon-formed under Siloni's typology as presented in §3.3 ([Sil12] itself does not discuss Swahili). The morphological rule is Swahili.Reciprocals.reciprocalAffix.

Equations

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

def Nordlinger2023.rpHungarian : RecipProfile

Hungarian: verbal affix -óz- (monovalent; [Nor23] ex. 19, 30, citing [Sil08]). Lexicon-formed per [Sil12]'s own classification; forms discontinuous reciprocals with comitative -val (ex. 38, from [Dim08]).

Equations

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

def Nordlinger2023.rpFrench : RecipProfile

French: reciprocal clitic se (monovalent, reflexive-identical; [Nor23] ex. 28, 47) plus distinct bipartite l'un l'autre. The review argues (after [Sil08], [Sil12]) that se is not a reciprocal object: embedded se-reciprocals lack the "I" reading (ex. 35). Syntax-formed, and discontinuous reciprocals are ungrammatical (ex. 39).

Equations

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

def Nordlinger2023.rpGreek : RecipProfile

Greek (Modern): nonactive voice morphology (monovalent, reflexive- identical in form) plus a distinct periphrastic reciprocal (o enas ton allon — its existence is implied by the WALS mixed classification, [MN13]). Forms discontinuous reciprocals with me 'with': "O Giannis filithike me ti Maria" ([Nor23] ex. 27b, 36, from [Dim08]) — hence lexicon-formed under Siloni's typology as presented in §3.3 ([Sil12] itself does not discuss Greek).

Equations

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

def Nordlinger2023.rpGerman : RecipProfile

German: dedicated reciprocal pronoun einander alongside reflexive sich in reciprocal use — the two markers' readings now encode the WALS "mixed" configuration. Both fill the object slot, preserving bivalent syntax. [Sil12] fn. 13 suggests German sich-reciprocals are syntactic reciprocal verbs; the review does not take this up, so no formation value is recorded.

Equations

• Nordlinger2023.rpGerman = { language := "German", iso := "deu", markers := German.Reciprocals.markers, valency := Reciprocal.Valency.bivalent }

def Nordlinger2023.rpMandarin : RecipProfile

Mandarin: compound verb strategy dǎ-lái-dǎ-qù (beat-come-beat-go = 'beat each other'), single subject NP. Distinct from reflexive. [Nor23] ex. 13 (citing [KK06]); [Eva08] treats verb compounding as a multiclausal strategy.

Equations

• Nordlinger2023.rpMandarin = { language := "Mandarin", iso := "cmn", markers := Mandarin.Reciprocals.markers, valency := Reciprocal.Valency.monovalent }

def Nordlinger2023.rpWambaya : RecipProfile

Wambaya: reciprocal clitic -ngg- (RR morpheme in the auxiliary), identical to reflexive. [Nor23] ex. 11 (citing [Nor98], p. 142). Bivalent: nominal subjects retain ergative marking under reciprocalization ([EGN07]: transitivity is compromised but argument structure undisturbed); the NOM subject in ex. 11 is a free pronoun, which declines nominative/accusative regardless of transitivity ([Nor98]).

Equations

• Nordlinger2023.rpWambaya = { language := "Wambaya", iso := "wmb", markers := Wambaya.Reciprocals.markers, valency := Reciprocal.Valency.bivalent }

def Nordlinger2023.rpIcelandic : RecipProfile

Icelandic: bipartite NP hvort annað, each part independently inflected for case (annað takes the argument-position case, hvort agrees with the antecedent). Bivalent — the accusative on annað shows the clause remains transitive. [Nor23] ex. 17 (citing [HN21]).

Equations

• Nordlinger2023.rpIcelandic = { language := "Icelandic", iso := "isl", markers := Icelandic.Reciprocals.markers, valency := Reciprocal.Valency.bivalent }

def Nordlinger2023.rpChichewa : RecipProfile

Chicheŵa: verbal affix -an- (monovalent). [Nor23] ex. 20 (citing [DMP94]).

Equations

• Nordlinger2023.rpChichewa = { language := "Chicheŵa", iso := "nya", markers := Chichewa.Reciprocals.markers, valency := Reciprocal.Valency.monovalent }

def Nordlinger2023.rpCzech : RecipProfile

Czech: reciprocal clitic se (monovalent, reflexive-identical; [Nor23] ex. 29, citing [Sil08]), alongside the periphrastic jeden druhého 'each other' attested in [Sil12]'s Czech examples — the derived WALS value is therefore mixed (WALS itself has no Czech row). Syntax-formed; discontinuous reciprocals are unavailable ([Nor23] p. 86, with French).

Equations

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

def Nordlinger2023.allRecipProfiles : List RecipProfile

Equations

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

Strategy-valency correlation (§3.2)

theorem Nordlinger2023.nominal_strategy_bivalent : ((List.filter (fun (p : RecipProfile) => Option.any (fun (x : Reciprocal.Strategy) => x.isNominal) p.primaryStrategy) allRecipProfiles).all fun (p : RecipProfile) => p.valency == Reciprocal.Valency.bivalent) = true

[Nor23] §3.2: NP/argument strategies tend to preserve valency (bivalent), while verb-marking strategies tend to reduce it. [Ned07a] (p. 21) links this to the morphosyntactic type: morphological markers "reduce the valency of the underlying verb by deleting the direct or indirect object."

In this sample: all nominal-primary profiles are bivalent. The correlation is a tendency — outside the sample, Tonga combines verbal marking with two argument NPs ([Mas08]) and Malagasy verb-marked reciprocals stay bivalent at f-structure ([Hur12]).

theorem Nordlinger2023.verbal_affix_monovalent : ((List.filter (fun (p : RecipProfile) => p.primaryStrategy == some Reciprocal.Strategy.verbalAffix) allRecipProfiles).all fun (p : RecipProfile) => p.valency == Reciprocal.Valency.monovalent) = true

Verbal affixes (Swahili -an-, Hungarian -óz-, Greek nonactive, Chicheŵa -an-) are uniformly monovalent in this sample.

theorem Nordlinger2023.monovalent_implies_verbal : ((List.filter (fun (p : RecipProfile) => p.valency == Reciprocal.Valency.monovalent) allRecipProfiles).all fun (p : RecipProfile) => !Option.any (fun (x : Reciprocal.Strategy) => x.isNominal) p.primaryStrategy) = true

Converse of nominal_strategy_bivalent: monovalent reciprocal strategies are never nominal (NP/argument) in this sample ([Ned07a], p. 21; [Nor23] §3.2).

theorem Nordlinger2023.valency_follows_default_except_wambaya : (allRecipProfiles.all fun (p : RecipProfile) => Option.any (fun (s : Reciprocal.Strategy) => p.valency == s.defaultValency) p.primaryStrategy || p.iso == "wmb") = true

Observed valency follows the strategy's default — derived in the substrate from Alternation.reciprocalization's detransitivizing coding-frame effect — throughout the sample, except Wambaya, whose ergative-retaining RR clause stays bivalent ([EGN07]).

Siloni's discontinuity prediction (§3.3)

theorem Nordlinger2023.siloni_discontinuity_prediction : (allRecipProfiles.all fun (p : RecipProfile) => match p.formation, p.discontinuousAttested with | some f, some d => (Siloni2012.predictedProperties f).discontinuous == d | x, x_1 => true) = true

[Sil08]/[Sil12] predict: discontinuous reciprocals (subject + comitative with-phrase) are possible only when the reciprocal verb is lexically formed.

Checked against independently recorded judgments: every profile carrying both a formation locus and an attested discontinuity judgment ([Nor23] ex. 36–40) satisfies the cluster value Siloni2012.predictedProperties derives from the formation locus — Greek, Swahili, Hungarian (lexical, attested) vs French, Czech (syntactic, ungrammatical).

WALS grounding

The reflexive-relation value is derived from each profile's marker inventory (ofInventory), so these theorems check a computed value against the external WALS row — inventory facts vs WALS coding, joined structurally on ISO 639-3 via Datapoint.lookupISO.

theorem Nordlinger2023.rpEnglish_wals : Option.map (fun (x : Data.WALS.Datapoint Data.WALS.F106A.ReciprocalType) => ofWALS106A x.value) (Data.WALS.F106A.lookupISO rpEnglish.iso) = some rpEnglish.reflexiveRelation

theorem Nordlinger2023.rpRussian_wals : Option.map (fun (x : Data.WALS.Datapoint Data.WALS.F106A.ReciprocalType) => ofWALS106A x.value) (Data.WALS.F106A.lookupISO rpRussian.iso) = some rpRussian.reflexiveRelation

theorem Nordlinger2023.rpSwahili_wals : Option.map (fun (x : Data.WALS.Datapoint Data.WALS.F106A.ReciprocalType) => ofWALS106A x.value) (Data.WALS.F106A.lookupISO rpSwahili.iso) = some rpSwahili.reflexiveRelation

theorem Nordlinger2023.rpFrench_wals : Option.map (fun (x : Data.WALS.Datapoint Data.WALS.F106A.ReciprocalType) => ofWALS106A x.value) (Data.WALS.F106A.lookupISO rpFrench.iso) = some rpFrench.reflexiveRelation

theorem Nordlinger2023.rpGreek_wals : Option.map (fun (x : Data.WALS.Datapoint Data.WALS.F106A.ReciprocalType) => ofWALS106A x.value) (Data.WALS.F106A.lookupISO rpGreek.iso) = some rpGreek.reflexiveRelation

theorem Nordlinger2023.rpGerman_wals : Option.map (fun (x : Data.WALS.Datapoint Data.WALS.F106A.ReciprocalType) => ofWALS106A x.value) (Data.WALS.F106A.lookupISO rpGerman.iso) = some rpGerman.reflexiveRelation

theorem Nordlinger2023.rpMandarin_wals : Option.map (fun (x : Data.WALS.Datapoint Data.WALS.F106A.ReciprocalType) => ofWALS106A x.value) (Data.WALS.F106A.lookupISO rpMandarin.iso) = some rpMandarin.reflexiveRelation

theorem Nordlinger2023.rpWambaya_wals : Option.map (fun (x : Data.WALS.Datapoint Data.WALS.F106A.ReciprocalType) => ofWALS106A x.value) (Data.WALS.F106A.lookupISO rpWambaya.iso) = some rpWambaya.reflexiveRelation

Semantic reciprocity types (§4)

inductive Nordlinger2023.ReciprocityType : Type

Semantic type of reciprocal relation.

[Nor23] §4 presents the semantic typology of [ELGM11], who take as their starting point the symmetric relations identified by [DKK+98] and distinguish six types of mutual relation ([Nor23] ex. 44, [ELGM11] p. 8):

• strong: every participant reciprocates with every other ("The members of this family love one another.")
• pairwise: participants are paired off ("The people at the dinner party were married to one another.")
• chain: sequential, each with the next ("The graduating students followed one another up onto the stage.")
• radial: one central participant acts on all others ("The teacher and her pupils intimidated one another.")
• melee: widespread but not exhaustive reciprocation ("The drunks in the pub were punching one another.")
• ring: circular chain, last links back to first ("The children chased each other round in a ring.")

• strong : ReciprocityType
• pairwise : ReciprocityType
• chain : ReciprocityType
• radial : ReciprocityType
• melee : ReciprocityType
• ring : ReciprocityType

@[instance_reducible]

instance Nordlinger2023.instDecidableEqReciprocityType : DecidableEq ReciprocityType

Equations

• Nordlinger2023.instDecidableEqReciprocityType x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

@[instance_reducible]

instance Nordlinger2023.instReprReciprocityType : Repr ReciprocityType

Equations

• Nordlinger2023.instReprReciprocityType = { reprPrec := Nordlinger2023.instReprReciprocityType.repr }

def Nordlinger2023.instReprReciprocityType.repr : ReciprocityType → ℕ → Std.Format

Equations

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

def Nordlinger2023.ReciprocityType.Realizes {A : Type u_1} : ReciprocityType → (A → A → Prop) → Finset A → Prop

The relation shape each configurational label denotes over a participant plurality — [MEGL11]'s extensional schemas as the exact-extension conditions of Semantics.Plurality.Reciprocal. Symmetry and participant-exhaustiveness are theorems there (ChainConfig.not_pairSymmetricOn, RadialConfig.inclusiveAlternativeOrdering, melee failing InclusiveAlternativeOrdering by definition, …), not stipulated features of the labels.

Equations

• Nordlinger2023.ReciprocityType.strong.Realizes x✝¹ x✝ = Semantics.Plurality.Reciprocal.StrongReciprocity x✝¹ x✝
• Nordlinger2023.ReciprocityType.pairwise.Realizes x✝¹ x✝ = Semantics.Plurality.Reciprocal.PairwiseConfig x✝¹ x✝
• Nordlinger2023.ReciprocityType.chain.Realizes x✝¹ x✝ = Semantics.Plurality.Reciprocal.ChainConfig x✝¹ x✝
• Nordlinger2023.ReciprocityType.radial.Realizes x✝¹ x✝ = Semantics.Plurality.Reciprocal.RadialConfig x✝¹ x✝
• Nordlinger2023.ReciprocityType.melee.Realizes x✝¹ x✝ = Semantics.Plurality.Reciprocal.MeleeConfig x✝¹ x✝
• Nordlinger2023.ReciprocityType.ring.Realizes x✝¹ x✝ = Semantics.Plurality.Reciprocal.RingConfig x✝¹ x✝

def Nordlinger2023.englishReciprocityTypes : List ReciprocityType

The six reciprocity types English each other can express ([ELGM11], p. 8; [Nor23] ex. 44).

Equations

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

theorem Nordlinger2023.english_expresses_all_types (t : ReciprocityType) : t ∈ englishReciprocityTypes

English each other expresses every reciprocity type — an empirical observation about English, not a structural property; some languages restrict which types their reciprocal construction can express.

Swahili fragment cross-reference (§3)

theorem Nordlinger2023.rpSwahili_grounded_in_fragment : rpSwahili.primaryStrategy = some Reciprocal.Strategy.verbalAffix ∧ rpSwahili.valency = Reciprocal.Valency.monovalent

The Swahili reciprocal suffix -an- ([Nor23] ex. 40, citing [Dim04]): rpSwahili's verbalAffix strategy with monovalent valency records the valence reduction (transitive → intransitive); the marker itself is Swahili.Reciprocals.anSuffix.

Polysemous markers beyond the sample (§4.2)

Reflexive polysemy is carried by the profile inventories above (French se, German sich, Wambaya -ngg-, Russian -sja) and drives their derived WALS values. The review's further polysemy types are attested by markers outside the 12-language sample.

def Nordlinger2023.yakutUs : Reciprocal.Marker

Yakut -üs: reciprocal + collective/sociative — ölör-üs 'kill each other' or 'kill somebody together' ([Nor23] ex. 49, citing [Ned07b]).

Equations

• Nordlinger2023.yakutUs = { form := "-üs", strategy := Reciprocal.Strategy.verbalAffix, readings := [Reciprocal.Reading.reciprocal, Reciprocal.Reading.collective, Reciprocal.Reading.sociative] }

def Nordlinger2023.eastFutunanFeAki : Reciprocal.Marker

East Futunan fe-...-ʼaki: reciprocal + iterative — fe-tapa-ʼaki 'sparkle again and again' ([Nor23] ex. 50, citing [Ned07b]).

Equations

• Nordlinger2023.eastFutunanFeAki = { form := "fe-...-ʼaki", strategy := Reciprocal.Strategy.verbalAffix, readings := [Reciprocal.Reading.reciprocal, Reciprocal.Reading.iterative] }

Fragment connection: English reciprocal-reflexive distinction

theorem Nordlinger2023.english_profile_grounded : rpEnglish.primaryStrategy = some Reciprocal.Strategy.bipartiteNP ∧ rpEnglish.valency = Reciprocal.Valency.bivalent ∧ Binding.bindingClassOf English.Pronouns.eachOther.toWord = some Features.BindingClass.reciprocal ∧ Binding.bindingClassOf English.Pronouns.eachOther.toWord ≠ some Features.BindingClass.reflexive

The English RecipProfile is grounded in the Fragment: English has reciprocal pronouns that are categorically different from reflexive pronouns, and the profile records each other as a bipartite NP strategy. The WALS substrate anchor for the reflexive-reciprocal distinction is rpEnglish_wals.

Cross-paper verification: Nordlinger 2023 vs Siloni 2012

theorem Nordlinger2023.hungarian_agrees_with_siloni : rpHungarian.formation = some Siloni2012.hungarian.formation

[Nor23]'s RecipProfile formation classifications agree with [Sil12]'s LangRecipVerb.formation for languages discussed in both. The newer paper checks consistency with the older (chronological dependency).

theorem Nordlinger2023.french_agrees_with_siloni : rpFrench.formation = some Siloni2012.french.formation

theorem Nordlinger2023.czech_agrees_with_siloni : rpCzech.formation = some Siloni2012.czech.formation