diff --git a/Linglib/Fragments/Turkish/Morphotactics.lean b/Linglib/Fragments/Turkish/Morphotactics.lean index 1d64b663ab..6266f13f43 100644 --- a/Linglib/Fragments/Turkish/Morphotactics.lean +++ b/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 diff --git a/Linglib/Fragments/Turkish/Phonology.lean b/Linglib/Fragments/Turkish/Phonology.lean index a1f4d5ca80..a3a8681b66 100644 --- a/Linglib/Fragments/Turkish/Phonology.lean +++ b/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 diff --git a/Linglib/Fragments/Turkish/QuestionParticles.lean b/Linglib/Fragments/Turkish/QuestionParticles.lean index 7f6b12f4da..241fbe03a3 100644 --- a/Linglib/Fragments/Turkish/QuestionParticles.lean +++ b/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 diff --git a/Studies/GokselKerslake2005.lean b/Studies/GokselKerslake2005.lean index 56530b9ecb..d92e8c63d0 100644 --- a/Studies/GokselKerslake2005.lean +++ b/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*, diff --git a/Studies/TurkHirsch2026.lean b/Studies/TurkHirsch2026.lean index 9b6bb1097d..f5ea312b0d 100644 --- a/Studies/TurkHirsch2026.lean +++ b/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 diff --git a/references.bib b/references.bib index 409717ee15..8570978109 100644 --- a/references.bib +++ b/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},