refactor(Fragments/Turkish): place mI before the first clitic of a predicate

Linglib/Fragments/Turkish/Morphotactics.lean

@@ -45,6 +45,8 @@ exactly when it differs from the last segment of the stem in being a vowel.
 * `Turkish.underlying`, `Turkish.realize`: the underlying and the surface form of a stem with
   a string of suffixes.
 * `Exponent.form`: the citation form of an exponent.
+* `Verb.Exponent.IsClitic`: the copular markers, -DIr and the group-2 person markers, which
+  are clitics (§11.1).
 * `Nominal.forms`: the forms of a string of nominal exponents, with the final `n` of a
   third-person possessive before a case suffix.
 
@@ -60,14 +62,15 @@ exactly when it differs from the last segment of the stem in being a vowel.
 
 ## Implementation notes
 
-The clitics mI and dA, which can interrupt the inflectional string (§6.3 (5)), are Chapter 11
-material outside both templates. The markers' meanings are the matter of Chapter 21 and Appendix
-2. There -DI marks past tense, perfective aspect and direct knowledge, -mIş marks relative past
-tense, perfective aspect and indirect knowledge (evidential modality, §21.4.3), and the copular
--(y)mIş marks evidential modality alone; -mIş followed by a copular marker or -DIr is perfective
-only (§8.2.3.3). The final `n` that the third-person possessives take before a case suffix
-(§6.2, §8.1.2) belongs to neither citation form and is supplied by `Nominal.forms`. Negation of
-the aorist is irregular, -mAz for -(A/I)r (§8.2.2; see `Turkish.Negation`). The grammar's
+The question clitic mI stands among the predicate markers, before the first clitic (§6.3 (5),
+§11.1.1.5), and is placed by `Turkish.QuestionParticles.mi.insert`; the clitic dA, which can
+interrupt -(y)Abil (§6.3 (4)), is not represented. The markers' meanings are the matter of Chapter
+21 and Appendix 2. There -DI marks past tense, perfective aspect and direct knowledge, -mIş marks
+relative past tense, perfective aspect and indirect knowledge (evidential modality, §21.4.3), and
+the copular -(y)mIş marks evidential modality alone; -mIş followed by a copular marker or -DIr is
+perfective only (§8.2.3.3). The final `n` that the third-person possessives take before a case
+suffix (§6.2, §8.1.2) belongs to neither citation form and is supplied by `Nominal.forms`. Negation
+of the aorist is irregular, -mAz for -(A/I)r (§8.2.2; see `Turkish.Negation`). The grammar's
 examples are checked against both templates in `Studies/GokselKerslake2005.lean`.
 
 ## References
@@ -214,11 +217,13 @@ inductive Slot where
 instance : LinearOrder Slot := .lift' Slot.ctorIdx (by decide)
 
 /-- A person-marker group of §8.4. Group 1 follows -DI, -sA and the copular markers -(y)DI and
--(y)sA, and group 2 follows the other position-3 markers, the copular -(y)mIş and nominal
-predicates. The optative and imperative groups 3 and 4 are not represented. -/
+-(y)sA, group 2 follows the other position-3 markers, the copular -(y)mIş and nominal
+predicates, and group 3 the optative, its third-person forms following the verb directly. The
+imperative group 4 is not represented. -/
 inductive PersonGroup where
   | one
   | two
+  | three
   deriving DecidableEq, Repr
 
 /-- The person markers of group 1 (§8.4). The second-person plural is also the formal
@@ -238,10 +243,21 @@ def PersonGroup.two.paradigm : Agreement.Paradigm Suffix :=
    (.personNumber .second .plural, ⟨none, [s, I, n, I, z]⟩),
    (.personNumber .third .plural, ⟨none, [l, A, r]⟩)]
 
+/-- The person markers of group 3 (§8.4). The second-person plural is also the formal singular,
+and the third-person plural is -sIn with -lAr. -/
+def PersonGroup.three.paradigm : Agreement.Paradigm Suffix :=
+  [(.personNumber .first .singular, ⟨none, [y, I, m]⟩),
+   (.personNumber .second .singular, ⟨none, [s, I, n]⟩),
+   (.personNumber .third .singular, ⟨none, [s, I, n]⟩),
+   (.personNumber .first .plural, ⟨none, [l, I, m]⟩),
+   (.personNumber .second .plural, ⟨none, [s, I, n, I, z]⟩),
+   (.personNumber .third .plural, ⟨none, [s, I, n, l, A, r]⟩)]
+
 /-- The paradigm of a person-marker group. -/
 def PersonGroup.paradigm : PersonGroup → Agreement.Paradigm Suffix
   | .one => PersonGroup.one.paradigm
   | .two => PersonGroup.two.paradigm
+  | .three => PersonGroup.three.paradigm
 
 /-- The exponents of each slot (§8.2.1 to §8.4). -/
 inductive Exponent : Slot → Type where
@@ -328,6 +344,16 @@ def Exponent.form : Exponent σ → Suffix
   | .person g c => (g.paradigm.realize c).getD ⟨none, []⟩
   | .dir => ⟨none, [D, I, r]⟩
 
+/-- The exponents that are clitics, the copular markers, -DIr and the person markers of group 2
+(§11.1). -/
+def Exponent.IsClitic : Exponent σ → Prop
+  | .pastCopula | .evidentialCopula | .conditionalCopula | .dir => True
+  | .person g _ => g = .two
+  | _ => False
+
+instance : DecidablePred (Exponent.IsClitic (σ := σ)) := fun e ↦ by
+  cases e <;> unfold Exponent.IsClitic <;> infer_instance
+
 /-- The template of the finite verb lists its slots in the order of §8.2, each of which a verb
 may skip, the voice slot taking any number of suffixes. -/
 def template : Morphology.AffixTemplate Slot where

Linglib/Fragments/Turkish/Phonology.lean

@@ -313,9 +313,9 @@ def ofChar : Char → Option Segment
 writes one. -/
 def ofString? (s : String) : Option (List Segment) := s.toList.mapM ofChar
 
-/-- `ofSegmented? s` reads a word written with its morpheme boundaries marked `-`, as glossed
-examples print it, dropping the boundaries. -/
+/-- `ofSegmented? s` reads a word written with its morpheme boundaries marked `-` and its clitic
+boundaries `=`, as glossed examples print it, dropping the boundaries. -/
 def ofSegmented? (s : String) : Option (List Segment) :=
-  (s.toList.filter (· ≠ '-')).mapM ofChar
+  (s.toList.filter fun c ↦ c ≠ '-' ∧ c ≠ '=').mapM ofChar
 
 end Turkish.Phonology

Linglib/Fragments/Turkish/QuestionParticles.lean

@@ -1,23 +1,47 @@
 module
 
+public import Linglib.Fragments.Turkish.Morphotactics
 public import Linglib.Syntax.Category.Particle.Basic
 
 /-!
 # Turkish question particles
 
-Turkish forms yes/no questions and alternative questions with the clitic *mI*, written as a
-separate word and harmonizing with the preceding vowel as *mı*, *mi*, *mu* or *mü*
-([goksel-kerslake-2005] §11.1, §11.1.1.5). It attaches to the predicate when the whole
-proposition is questioned and can instead attach to a subject, object or adverbial (§19.1.1,
-§19.1.3); in an alternative question it follows each alternative (§19.1.2). It is obligatory
-in polar questions ([turk-hirsch-2026]). Indirect alternative questions keep *mI* after each
-alternative, while indirect yes/no questions are formed with the -(y)Ip…-mA construction
-instead (§24.4.3.2).
+Turkish forms yes/no and alternative questions with the clitic *mI*, written as a separate word
+and harmonizing as an I-type suffix does, as *mı*, *mi*, *mu* or *mü* (§3.2, §11.1.1.5). It
+follows the questioned phrase, which is the predicate when the whole proposition is questioned,
+and each alternative of an alternative question (§19.1). On the predicate it stands among the
+markers, immediately before the first clitic, a copular marker, -DIr or a group-2 person marker
+other than the third-person plural, and after every other marker, so that *Gidiyor musun?*
+'Are you going?' contrasts with *Gördün mü?* 'Did you see?'. The markers after it attach to it,
+as in *bil-iyor mu-ydu-nuz* (§6.3 (5)).
+
+## Main definitions
+
+* `Turkish.QuestionParticles.mi`: the particle.
+* `mi.suffix`, `mi.Precedes`, `mi.insert`: the segments of *mI*, the markers it precedes, and
+  the markers of a predicate with *mI* among them.
+
+## Main results
+
+* `mi.insert_append_cons`, `mi.insert_of_forall_not_precedes`: *mI* immediately precedes the
+  first marker it precedes, and follows the last marker if it precedes none.
+
+## Implementation notes
+
+The distribution follows Türk and Hirsch, for whom *mI* is obligatory in polar questions, and
+the grammar. A quoted question keeps it (§24.3.1 (16)), and so does a question under *diye*, as
+in Türk and Hirsch's (14) and Qing et al.'s examples, while a noun clause expresses 'whether (or
+not)' with -(y)Ip…-mA and keeps *mI* only after alternatives other than the negation of the
+predicate (§24.4.3.2). Echo questions (§19.3), adverbial clauses after -DI and doubled forms
+(§11.1.1.5) also take *mI*, so the constituent and declarative cells are not recorded. The
+colloquial contractions of -(y)AcAK with a person marker (§11.1.1.5 (e)) are not represented,
+and the conditional copula -(y)sA has no example with *mI*.
 
 ## References
 
 * [goksel-kerslake-2005]
 * [turk-hirsch-2026]
+* [qing-uegaki-2025]
 -/
 
 @[expose] public section
@@ -29,9 +53,59 @@ def mi : Particle where
   form := "mI"
   position := some .postHost
   distribution
-    | .polar, .matrix => some .obligatory
-    | .alternative, .matrix => some .obligatory
-    | .alternative, .subordinated => some .obligatory
+    | .polar, .matrix | .polar, .quotation | .alternative, .matrix => some .obligatory
+    | .polar, .subordinated | .alternative, .subordinated => some .optional
     | _, _ => none
 
+open Turkish.Phonology in
+/-- The segments of *mI*, which attach as a suffix does (§3.2). -/
+def mi.suffix : Suffix := ⟨none, [m, I]⟩
+
+/-- *mI* precedes the clitics among the predicate markers but the third-person plural -lAr
+(§11.1.1.5). -/
+def mi.Precedes (x : Σ σ, Verb.Exponent σ) : Prop :=
+  x.2.IsClitic ∧ x ≠ ⟨_, .person .two (.personNumber .third .plural)⟩
+
+instance : DecidablePred mi.Precedes := fun _ ↦ inferInstanceAs (Decidable (_ ∧ _))
+
+/-- The forms of the markers of a predicate with *mI* before the first marker it precedes, or
+after the last. -/
+def mi.insert : List (Σ σ, Verb.Exponent σ) → List Suffix
+  | [] => [mi.suffix]
+  | x :: xs =>
+    if mi.Precedes x then mi.suffix :: (x :: xs).map (·.2.form) else x.2.form :: mi.insert xs
+
+variable {x : Σ σ, Verb.Exponent σ} {xs pre post : List (Σ σ, Verb.Exponent σ)}
+
+@[simp] theorem mi.insert_nil : mi.insert [] = [mi.suffix] := rfl
+
+@[simp] theorem mi.insert_cons_of_precedes (h : mi.Precedes x) :
+    mi.insert (x :: xs) = mi.suffix :: (x :: xs).map (·.2.form) :=
+  ite_eq_left h
+
+@[simp] theorem mi.insert_cons_of_not_precedes (h : ¬ mi.Precedes x) :
+    mi.insert (x :: xs) = x.2.form :: mi.insert xs :=
+  ite_eq_right h
+
+/-- *mI* immediately precedes the first marker it precedes (§11.1.1.5). -/
+theorem mi.insert_append_cons (hpre : ∀ y ∈ pre, ¬ mi.Precedes y) (hx : mi.Precedes x) :
+    mi.insert (pre ++ x :: post) =
+      pre.map (·.2.form) ++ mi.suffix :: (x :: post).map (·.2.form) := by
+  induction pre with
+  | nil => exact mi.insert_cons_of_precedes hx
+  | cons y pre ih =>
+    rw [List.forall_mem_cons] at hpre
+    rw [List.cons_append, mi.insert_cons_of_not_precedes hpre.1, ih hpre.2]
+    rfl
+
+/-- *mI* follows the last marker of a predicate if it precedes none of them (§11.1.1.5). -/
+theorem mi.insert_of_forall_not_precedes (h : ∀ y ∈ xs, ¬ mi.Precedes y) :
+    mi.insert xs = xs.map (·.2.form) ++ [mi.suffix] := by
+  induction xs with
+  | nil => rfl
+  | cons y xs ih =>
+    rw [List.forall_mem_cons] at h
+    rw [mi.insert_cons_of_not_precedes h.1, ih h.2]
+    rfl
+
 end Turkish.QuestionParticles

Studies/GokselKerslake2005.lean

@@ -2,6 +2,7 @@ module
 
 public import Linglib.Fragments.Turkish.Clause
 public import Linglib.Fragments.Turkish.Possession
+public import Linglib.Fragments.Turkish.QuestionParticles
 public import Linglib.Fragments.Turkish.Verbs
 
 /-!
@@ -23,6 +24,10 @@ The grammar's example words are licensed with their stacked voice suffixes, reve
 not, and the rule that markers of one position cannot co-occur (§8.2.3) holds because the
 template does not repeat the position.
 
+The question clitic *mI* stands before the first clitic among the markers of a predicate and
+after the other markers (§11.1.1.5), as `Turkish.QuestionParticles.mi.insert` places it, so the
+grammar's examples are its surface forms, the markers after it attached to it (§6.3 (5)).
+
 The converbs of §8.5.2.2 are those of `Turkish.Converb` on the grammar's verbs, and
 *-(y)Ip* and *-(y)ArAk* follow every slot before the position-3 marker and none after it
 (§28.2).
@@ -43,11 +48,19 @@ The possessive and locative existential sentences of §12.1.1.2 are those of
 * `causative_stems`, `spelled_stems`: the -DIr causatives of §8.2.1.1 and the Fragment's verbs.
 * `finite_verb`: §8.2 (7), every slot of the finite verb.
 * `same_position_excluded`: §8.2.3 (i), since the template does not repeat position 3.
+* `mi_precedes_clitics`, `mi_follows`: §11.1.1.5, the position of *mI* among the markers of a
+  predicate.
 * `converbs`, `doubled_converbs`: the converbs of §8.5.2.2 and -DIkçA.
 * `conjunctive_converbs`: §28.2, -(y)Ip and -(y)ArAk in place of the position-3 marker.
 * `possessive_existential`, `locative_existential`: §12.1.1.2 (21), (22), (26) and (17).
 * `possessive_obligatory`: §14.4 (117), the possessive suffix on the possessee.
 
+## Errata
+
+Among the examples of §11.1.1.5, *Gittiler mı?* should be *Gittiler mi?*, since fronting
+harmony gives a front vowel after *gittiler* (§3.2.1), and *Baslasın mı?* should be
+*Başlasın mı?*.
+
 ## References
 
 * [A. Göksel and C. Kerslake, *Turkish: A Comprehensive Grammar* (2005)][goksel-kerslake-2005]
@@ -57,7 +70,7 @@ The possessive and locative existential sentences of §12.1.1.2 are those of
 
 namespace GokselKerslake2005
 
-open Turkish Phonology Verb.Exponent Nominal.Exponent
+open Turkish Phonology Verb.Exponent Nominal.Exponent QuestionParticles
 
 /-! ### Vowel harmony (Chapter 3) -/
 
@@ -295,6 +308,69 @@ theorem same_position_excluded (m₁ m₂ : Verb.Exponent .tam) :
     ¬ Verb.template.Licensed [⟨_, m₁⟩, ⟨_, m₂⟩] :=
   show [Verb.Slot.tam, .tam] ∉ Verb.template.language by decide
 
+/-! ### The question clitic (§11.1.1.5) -/
+
+/-- *mI* precedes the copular markers, as in *Gitse miydik?*, *Başlamış mıydınız?* and *Burada
+mıymış?*, the group-2 person markers but the third-person plural, as in *Gidiyor musun?*,
+*İster miyiz?* and *Hazır mısınız?*, and -DIr, as in *Unutmuş mudurlar?*, *Evde midir?* and
+*geçmiş miyimdir?*, and the markers after it attach to it, as in *bil-iyor mu-ydu-nuz*
+(§6.3 (5)). -/
+theorem mi_precedes_clitics :
+    realize [g, i, t]
+        (mi.insert [⟨_, sa⟩, ⟨_, pastCopula⟩, ⟨_, person .one (.personNumber .first .plural)⟩]) =
+      [g, i, t, s, e] ++ [m, i, y, d, i, k] ∧
+    realize [b, a, ş, l, a]
+        (mi.insert [⟨_, miş⟩, ⟨_, pastCopula⟩, ⟨_, person .one (.personNumber .second .plural)⟩]) =
+      [b, a, ş, l, a, m, ı, ş] ++ [m, ı, y, d, ı, n, ı, z] ∧
+    realize [b, u, r, a, d, a] (mi.insert [⟨_, evidentialCopula⟩]) =
+      [b, u, r, a, d, a] ++ [m, ı, y, m, ı, ş] ∧
+    realize [g, i, d] (mi.insert [⟨_, iyor⟩, ⟨_, person .two (.personNumber .second .singular)⟩]) =
+      [g, i, d, i, y, o, r] ++ [m, u, s, u, n] ∧
+    realize [i, s, t, e]
+        (mi.insert [⟨_, aorist⟩, ⟨_, person .two (.personNumber .first .plural)⟩]) =
+      [i, s, t, e, r] ++ [m, i, y, i, z] ∧
+    realize [h, a, z, ı, r] (mi.insert [⟨_, person .two (.personNumber .second .plural)⟩]) =
+      [h, a, z, ı, r] ++ [m, ı, s, ı, n, ı, z] ∧
+    realize [u, n, u, t]
+        (mi.insert [⟨_, miş⟩, ⟨_, dir⟩, ⟨_, person .two (.personNumber .third .plural)⟩]) =
+      [u, n, u, t, m, u, ş] ++ [m, u, d, u, r, l, a, r] ∧
+    realize [e, v, d, e] (mi.insert [⟨_, dir⟩]) = [e, v, d, e] ++ [m, i, d, i, r] ∧
+    realize [g, e, ç]
+        (mi.insert [⟨_, miş⟩, ⟨_, person .two (.personNumber .first .singular)⟩, ⟨_, dir⟩]) =
+      [g, e, ç, m, i, ş] ++ [m, i, y, i, m, d, i, r] ∧
+    realize [b, i, l]
+        (mi.insert [⟨_, iyor⟩, ⟨_, pastCopula⟩, ⟨_, person .one (.personNumber .second .plural)⟩]) =
+      [b, i, l, i, y, o, r] ++ [m, u, y, d, u, n, u, z] := by
+  decide
+
+/-- *mI* follows the group-1 person markers, as in *Gördün mü?*, *Gitsek mi?* and *Yürüdünüz
+mü?*, those of group 3, as in *Kalayım mı?* and *Başlasın mı?*, the third-person plural, as in
+*Gittiler mi?*, *Uyanırlar mı?* and *Okuldalar mı?*, and a subject complement without markers,
+as in *Akıllı mı?* and *Benimki mi?*. -/
+theorem mi_follows :
+    realize [g, ö, r] (mi.insert [⟨_, di⟩, ⟨_, person .one (.personNumber .second .singular)⟩]) =
+      [g, ö, r, d, ü, n] ++ [m, ü] ∧
+    realize [g, i, t] (mi.insert [⟨_, sa⟩, ⟨_, person .one (.personNumber .first .plural)⟩]) =
+      [g, i, t, s, e, k] ++ [m, i] ∧
+    realize [y, ü, r, ü]
+        (mi.insert [⟨_, di⟩, ⟨_, person .one (.personNumber .second .plural)⟩]) =
+      [y, ü, r, ü, d, ü, n, ü, z] ++ [m, ü] ∧
+    realize [k, a, l]
+        (mi.insert [⟨_, optative⟩, ⟨_, person .three (.personNumber .first .singular)⟩]) =
+      [k, a, l, a, y, ı, m] ++ [m, ı] ∧
+    realize [b, a, ş, l, a] (mi.insert [⟨_, person .three (.personNumber .third .singular)⟩]) =
+      [b, a, ş, l, a, s, ı, n] ++ [m, ı] ∧
+    realize [g, i, t] (mi.insert [⟨_, di⟩, ⟨_, person .one (.personNumber .third .plural)⟩]) =
+      [g, i, t, t, i, l, e, r] ++ [m, i] ∧
+    realize [u, y, a, n]
+        (mi.insert [⟨_, aorist⟩, ⟨_, person .two (.personNumber .third .plural)⟩]) =
+      [u, y, a, n, ı, r, l, a, r] ++ [m, ı] ∧
+    realize [o, k, u, l, d, a] (mi.insert [⟨_, person .two (.personNumber .third .plural)⟩]) =
+      [o, k, u, l, d, a, l, a, r] ++ [m, ı] ∧
+    realize [a, k, ı, l, l, ı] (mi.insert []) = [a, k, ı, l, l, ı] ++ [m, ı] ∧
+    realize [b, e, n, i, m, k, i] (mi.insert []) = [b, e, n, i, m, k, i] ++ [m, i] := by
+  decide
+
 /-! ### Converbs (§8.5.2.2) -/
 
 /-- The converbs on the grammar's verbs: on the stem, as in *koş-up*, *kalk-ma-yınca*,

Studies/TurkHirsch2026.lean

@@ -225,4 +225,11 @@ theorem isStrongestTrueAnswer_hamblinCat_compl {p : Set W} {w : W} (hw : w ∉ p
 /-- *=mI* is obligatory in polar questions such as (4), as the fragment records. -/
 example : Turkish.QuestionParticles.mi.distribution .polar .matrix = some .obligatory := rfl
 
+open Turkish.Phonology in
+/-- In its default position in (4), *=mI* follows the markers of the predicate *uyu-du*. -/
+example : ∃ t ∈ Examples.ex_4.glossedTokens,
+    ofSegmented? t.1 = some (Turkish.realize [u, y, u] (Turkish.QuestionParticles.mi.insert
+      [⟨_, .di⟩, ⟨_, .person .one (.personNumber .third .singular)⟩])) := by
+  decide
+
 end TurkHirsch2026

references.bib

@@ -18095,7 +18095,7 @@ @misc{qing-uegaki-2025
   url       = {https://ling.auf.net/lingbuzz/008113},
   subfield  = {semantics/presupposition},
   role      = {cited},
-  sources   = {Fragments/Japanese/Verbs.lean;Fragments/Mandarin/Verbs.lean;Fragments/Turkish/Verbs.lean;Semantics/Attitudes/Distributivity.lean;Semantics/Attitudes/Preference.lean;Studies/QingEtAl2025.lean;Syntax/Category/Verb/Defs.lean}
+  sources   = {Fragments/Japanese/Verbs.lean;Fragments/Mandarin/Verbs.lean;Fragments/Turkish/QuestionParticles.lean;Fragments/Turkish/Verbs.lean;Semantics/Attitudes/Distributivity.lean;Semantics/Attitudes/Preference.lean;Studies/QingEtAl2025.lean;Syntax/Category/Verb/Defs.lean}
 }
 @article{ozyildiz-etal-2025,
   author    = {Özyıldız, Deniz and Qing, Ciyang and Roelofsen, Floris and Uegaki, Wataru and Romero, Maribel},