Turkish morphotactics

This file defines the inflectional suffixes of the Turkish finite verb and nominal and the order in which they appear, following the reference grammar of Göksel and Kerslake.

Turkish is suffixing. Derivational suffixes precede inflectional ones, and clitics follow both (§6.3). The inflectional suffixes of a finite verb appear in the order root, voice, negation, tense/aspect/modality, copular marker, person marker, -DIr (§8.2). The tense/aspect/modality markers themselves fall into five positions (§8.2.3): the possibility suffix -(y)A (1), which precedes the negative (§8.2.3.1), the bound auxiliaries (2), the markers of tense, aspect and modality proper (3), the copular markers (4) and -DIr (5). Markers of one position cannot co-occur, and every finite verb but the imperative and the third-person optative carries one of position 3. The voice slot alone admits a sequence of suffixes, as the four of döğ-üş-tür-t-ül- in (7) (§8.2, §8.2.1.1). The person marker alone may leave its place: a group-1 marker after -DI and the third-person plural may precede the copular marker, and the third-person plural may follow -DIr (§8.3.3, §8.4). The inflectional suffixes of a nominal appear in the order number, possession, case (§8.1).

The finite verb and the nominal each have a slot inventory, the exponents of each slot, and a template of suffix positions, each of which a word may skip, the voice position of the verb stacking. The person markers (§8.4) and the possessives (§8.1.2) are Agreement.Paradigms.

Vowels do not occur next to each other in Turkish, and the grammar brackets in a suffix's citation form the initial segment whose presence depends on the stem (§6.1.3). The vowel of -(I)m is lost after a vowel, as in araba-m, and the consonant of -(y)A, -(n)In and -(s)I appears only after one, as in masa-ya. Both cases are one rule: a bracketed segment appears exactly when it differs from the last segment of the stem in being a vowel.

Main definitions

• Turkish.Verb.Slot, Turkish.Verb.Exponent, Turkish.Verb.template: the slots, exponents and template of the finite verb, the slots ordered as the template lists them.
• Turkish.Nominal.Slot, Turkish.Nominal.Exponent, Turkish.Nominal.template: the same for the nominal.
• Turkish.Suffix, Suffix.attach: a suffix in citation form, with its bracketed initial segment, and its attachment to a stem.
• 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.forms: the citation forms of a string of exponents of the finite verb.
• Verb.Exponent.IsClitic: the copular markers, -DIr and the group-2 person markers, which are clitics (§11.1).
• Verb.Licensed: the strings of exponents of the finite verb, in the order of its template or with the person marker moved as §8.4 allows.
• Nominal.forms: the forms of a string of nominal exponents, with the final n of a third-person possessive before a case suffix.

Main results

• Suffix.attach_concat_alternates: a bracketed suffix attaches with vowels and consonants alternating across the juncture.
• Suffix.attach_eq_elideV2, Suffix.attach_eq_epenthesize, Suffix.attach_concat_eq_repair: after a vowel-final stem, attachment is one of the repairs of Phonology.Hiatus, elision of the suffix's vowel or insertion of its bracketed consonant.
• realize_singleton_ne_self: a suffix with fixed segments changes every stem it attaches to.
• Verb.pairwise_lt_suffixSlots: the template lists the slots of the finite verb in order.

Implementation notes

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

• A. Göksel and C. Kerslake, Turkish: A Comprehensive Grammar (2005)

Suffixes and their attachment

structure Turkish.Suffix : Type

A suffix in citation form consists of the segments that always appear, preceded by a bracketed initial segment if it has one, as the y of -(y)A and the I of -(I)m (§6.1.3).

• bracketed : Option Phonology.Segment

  The bracketed initial segment.

• segments : List Phonology.Segment

  The segments that always appear.

def Turkish.instDecidableEqSuffix.decEq (x✝ x✝¹ : Suffix) : Decidable (x✝ = x✝¹)

Equations

• Turkish.instDecidableEqSuffix.decEq { bracketed := a, segments := a_1 } { bracketed := b, segments := b_1 } = if h : a = b then h ▸ if h : a_1 = b_1 then h ▸ isTrue ⋯ else isFalse ⋯ else isFalse ⋯

@[instance_reducible]

instance Turkish.instDecidableEqSuffix : DecidableEq Suffix

Equations

• Turkish.instDecidableEqSuffix = Turkish.instDecidableEqSuffix.decEq

def Turkish.Suffix.initial (s : Suffix) (w : List Phonology.Segment) : List Phonology.Segment

s.initial w is what the bracketed segment of s contributes after the stem w. The segment appears exactly when it keeps vowels and consonants apart, a vowel after a consonant and a consonant after a vowel (§6.1.3).

Equations

• s.initial w = (Option.filter (fun (b : Phonology.Segment) => decide (∀ l ∈ w.getLast?, ¬(b.IsVowel ↔ l.IsVowel))) s.bracketed).toList

def Turkish.Suffix.attach (w : List Phonology.Segment) (s : Suffix) : List Phonology.Segment

s.attach w is the stem w with the suffix s attached.

Equations

• Turkish.Suffix.attach w s = w ++ s.initial w ++ s.segments

@[simp]

theorem Turkish.Suffix.initial_of_bracketed_eq_none {s : Suffix} (h : s.bracketed = none) (w : List Phonology.Segment) : s.initial w = []

theorem Turkish.Suffix.initial_concat {s : Suffix} {b : Phonology.Segment} (h : s.bracketed = some b) (w : List Phonology.Segment) (l : Phonology.Segment) : s.initial (w ++ [l]) = if b.IsVowel ↔ l.IsVowel then [] else [b]

theorem Turkish.Suffix.attach_concat_alternates {s : Suffix} {b h : Phonology.Segment} {t : List Phonology.Segment} (hb : s.bracketed = some b) (hs : s.segments = h :: t) (hbh : ¬(b.IsVowel ↔ h.IsVowel)) (w : List Phonology.Segment) (l : Phonology.Segment) : ∃ (x : Phonology.Segment) (r : List Phonology.Segment), attach (w ++ [l]) s = w ++ l :: x :: r ∧ ¬(l.IsVowel ↔ x.IsVowel)

A suffix whose bracketed segment differs from its first fixed segment in being a vowel, as every bracketed suffix of the grammar does, attaches with vowels and consonants alternating across the juncture, so the segment after the stem-final l differs from l in being a vowel.

theorem Turkish.Suffix.attach_eq_elideV2 (j : Phonology.Hiatus.Juncture) {s : Suffix} (hb : s.bracketed = some j.v2) (hs : s.segments = j.rightBody) : attach j.left s = j.elideV2

After a vowel-final stem a bracketed vowel is lost, so attachment is the elision of the second vowel of the juncture.

theorem Turkish.Suffix.attach_eq_epenthesize (j : Phonology.Hiatus.Juncture) {s : Suffix} {c : Phonology.Segment} (hb : s.bracketed = some c) (hc : ¬c.IsVowel) (hs : s.segments = j.right) : attach j.left s = j.epenthesize c

After a vowel-final stem a bracketed consonant appears before the vowel of the suffix, so attachment is the insertion of that consonant at the juncture.

theorem Turkish.Suffix.attach_concat_eq_repair {s : Suffix} {b h : Phonology.Segment} {t : List Phonology.Segment} (hb : s.bracketed = some b) (hs : s.segments = h :: t) (hbh : ¬(b.IsVowel ↔ h.IsVowel)) (w : List Phonology.Segment) {l : Phonology.Segment} (hl : l.IsVowel) : (∃ (j : Phonology.Hiatus.Juncture), j.left = w ++ [l] ∧ attach (w ++ [l]) s = j.elideV2) ∨ ∃ (j : Phonology.Hiatus.Juncture), j.left = w ++ [l] ∧ attach (w ++ [l]) s = j.epenthesize b

After a vowel-final stem the attachment of a bracketed suffix is a repair of hiatus. If the bracketed segment is a vowel it is elided, and if it is a consonant it is inserted before the suffix's vowel.

def Turkish.underlying (w : List Phonology.Segment) (sfxs : List Suffix) : List Phonology.Segment

underlying w sfxs is the underlying form of the stem w with the suffixes sfxs attached in turn.

Equations

• Turkish.underlying w sfxs = List.foldl Turkish.Suffix.attach w sfxs

@[simp]

theorem Turkish.underlying_nil (w : List Phonology.Segment) : underlying w [] = w

@[simp]

theorem Turkish.underlying_cons (w : List Phonology.Segment) (s : Suffix) (sfxs : List Suffix) : underlying w (s :: sfxs) = underlying (Suffix.attach w s) sfxs

theorem Turkish.underlying_append (w : List Phonology.Segment) (sfxs sfxs' : List Suffix) : underlying w (sfxs ++ sfxs') = underlying (underlying w sfxs) sfxs'

def Turkish.realize (w : List Phonology.Segment) (sfxs : List Suffix) : List Phonology.Segment

realize w sfxs is the surface form of the stem w with the suffixes sfxs.

Equations

• Turkish.realize w sfxs = Turkish.Phonology.surface (Turkish.underlying w sfxs)

@[simp]

theorem Turkish.length_realize (w : List Phonology.Segment) (sfxs : List Suffix) : (realize w sfxs).length = (underlying w sfxs).length

theorem Turkish.realize_singleton_ne_self {s : Suffix} (hs : s.segments ≠ []) (w : List Phonology.Segment) : realize w [s] ≠ w

A suffix whose fixed segments are not empty changes every stem it attaches to.

The finite verb

inductive Turkish.Verb.Slot : Type

The suffix slots of a finite verb (§8.2, §8.2.3).

• voice : Slot

  Causative, passive, reflexive and reciprocal (§8.2.1).

• possibility : Slot

  The possibility suffix -(y)A of negative forms, position 1 (§8.2.3.1).

• negation : Slot

  -mA (§8.2.2).

• auxiliary : Slot

  The bound auxiliaries -(y)Abil, -(y)Iver, -(y)Agel, -(y)Ayaz, -(y)Akal and -(y)Adur, position 2 (§8.2.3.2).

• tam : Slot

  The position 3 markers -DI, -mIş, -sA, the aorist, -(y)AcAK, -(I)yor, -mAlI, -mAktA and the optative -(y)A (§8.2.3.3).

• copula : Slot

  The copular markers -(y)DI, -(y)mIş and -(y)sA, position 4 (§8.3.2).

• person : Slot

  Person markers (§8.4).

• generalizing : Slot

  The generalizing-modality marker -DIr, position 5 (§8.3.3).

@[instance_reducible]

instance Turkish.Verb.instDecidableEqSlot : DecidableEq Slot

Equations

• Turkish.Verb.instDecidableEqSlot x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

@[instance_reducible]

instance Turkish.Verb.instReprSlot : Repr Slot

Equations

• Turkish.Verb.instReprSlot = { reprPrec := Turkish.Verb.instReprSlot.repr }

def Turkish.Verb.instReprSlot.repr : Slot → ℕ → Std.Format

Equations

• One or more equations did not get rendered due to their size.
• Turkish.Verb.instReprSlot.repr Turkish.Verb.Slot.voice prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Turkish.Verb.Slot.voice")).group prec✝
• Turkish.Verb.instReprSlot.repr Turkish.Verb.Slot.negation prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Turkish.Verb.Slot.negation")).group prec✝
• Turkish.Verb.instReprSlot.repr Turkish.Verb.Slot.auxiliary prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Turkish.Verb.Slot.auxiliary")).group prec✝
• Turkish.Verb.instReprSlot.repr Turkish.Verb.Slot.tam prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Turkish.Verb.Slot.tam")).group prec✝
• Turkish.Verb.instReprSlot.repr Turkish.Verb.Slot.copula prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Turkish.Verb.Slot.copula")).group prec✝
• Turkish.Verb.instReprSlot.repr Turkish.Verb.Slot.person prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Turkish.Verb.Slot.person")).group prec✝

@[instance_reducible]

instance Turkish.Verb.instFintypeSlot : Fintype Slot

Equations

• Turkish.Verb.instFintypeSlot = { elems := { val := ↑Turkish.Verb.Slot.enumList, nodup := Turkish.Verb.Slot.enumList_nodup }, complete := Turkish.Verb.instFintypeSlot._proof_1 }

@[instance_reducible]

instance Turkish.Verb.instLinearOrderSlot : LinearOrder Slot

The slots in the order of the template.

Equations

• Turkish.Verb.instLinearOrderSlot = LinearOrder.lift' Turkish.Verb.Slot.ctorIdx Turkish.Verb.instLinearOrderSlot._proof_1

inductive Turkish.Verb.PersonGroup : Type

A person-marker group of §8.4. Group 1 follows -DI, -sA and the copular markers -(y)DI and -(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.

• one : PersonGroup
• two : PersonGroup
• three : PersonGroup

@[instance_reducible]

instance Turkish.Verb.instDecidableEqPersonGroup : DecidableEq PersonGroup

Equations

• Turkish.Verb.instDecidableEqPersonGroup x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

@[instance_reducible]

instance Turkish.Verb.instReprPersonGroup : Repr PersonGroup

Equations

• Turkish.Verb.instReprPersonGroup = { reprPrec := Turkish.Verb.instReprPersonGroup.repr }

def Turkish.Verb.instReprPersonGroup.repr : PersonGroup → ℕ → Std.Format

Equations

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

def Turkish.Verb.PersonGroup.one.paradigm : Agreement.Paradigm Suffix

The person markers of group 1 (§8.4). The second-person plural is also the formal singular, and the third-person singular is zero.

Equations

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

def Turkish.Verb.PersonGroup.two.paradigm : Agreement.Paradigm Suffix

The person markers of group 2 (§8.4), whose first-person markers -(y)Im and -(y)Iz take the buffer y.

Equations

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

def Turkish.Verb.PersonGroup.three.paradigm : Agreement.Paradigm Suffix

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.

Equations

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

def Turkish.Verb.PersonGroup.paradigm : PersonGroup → Agreement.Paradigm Suffix

The paradigm of a person-marker group.

Equations

• Turkish.Verb.PersonGroup.one.paradigm = Turkish.Verb.PersonGroup.one.paradigm
• Turkish.Verb.PersonGroup.two.paradigm = Turkish.Verb.PersonGroup.two.paradigm
• Turkish.Verb.PersonGroup.three.paradigm = Turkish.Verb.PersonGroup.three.paradigm

inductive Turkish.Verb.Exponent : Slot → Type

The exponents of each slot (§8.2.1 to §8.4).

• reciprocal : Exponent Slot.voice

  -(I)ş (§8.2.1.4).

• reflexive : Exponent Slot.voice

  -(I)n (§8.2.1.3).

• causative : Exponent Slot.voice

  -DIr, with the stem-conditioned allomorphs -t, -It, -Ir, -Ar and -Art (§8.2.1.1).

• passive : Exponent Slot.voice

  -Il, with -In after l and -n after a vowel (§8.2.1.2).

• possibility : Exponent Slot.possibility

  -(y)A, possibility; negative forms only (§8.2.3.1).

• negative : Exponent Slot.negation

  -mA (§8.2.2).

• abil : Exponent Slot.auxiliary

  -(y)Abil, possibility (§8.2.3.2).

• iver : Exponent Slot.auxiliary

  -(y)Iver, non-premeditative.

• agel : Exponent Slot.auxiliary
• ayaz : Exponent Slot.auxiliary
• akal : Exponent Slot.auxiliary
• adur : Exponent Slot.auxiliary
• di : Exponent Slot.tam

  -DI, perfective (§8.2.3.3).

• miş : Exponent Slot.tam

  -mIş, perfective/evidential.

• sa : Exponent Slot.tam

  -sA, conditional.

• aorist : Exponent Slot.tam

  -(A/I)r, negative -z.

• acak : Exponent Slot.tam

  -(y)AcAK, future.

• iyor : Exponent Slot.tam

  -(I)yor, imperfective.

• mali : Exponent Slot.tam

  -mAlI, obligative.

• makta : Exponent Slot.tam

  -mAktA, imperfective.

• optative : Exponent Slot.tam

  -(y)A, optative.

• pastCopula : Exponent Slot.copula

  -(y)DI, past copula (§8.3.2).

• evidentialCopula : Exponent Slot.copula

  -(y)mIş, evidential copula.

• conditionalCopula : Exponent Slot.copula

  -(y)sA, conditional copula.

• person (group : PersonGroup) (cell : Agreement.Bundle) : Exponent Slot.person

  A person marker, the cell of a group's paradigm (§8.4).

• dir : Exponent Slot.generalizing

  -DIr, generalizing modality (§8.3.3).

@[instance_reducible]

instance Turkish.Verb.instDecidableEqExponent {a✝ : Slot} : DecidableEq (Exponent a✝)

Equations

• Turkish.Verb.instDecidableEqExponent = Turkish.Verb.instDecidableEqExponent.decEq

def Turkish.Verb.instDecidableEqExponent.decEq {a✝ : Slot} (x✝ x✝¹ : Exponent a✝) : Decidable (x✝ = x✝¹)

Equations

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

def Turkish.Verb.Exponent.form {σ : Slot} : Exponent σ → Suffix

The citation form of an exponent. The stem-conditioned allomorphs of the causative and the passive (§8.2.1) and the A of the aorist -(A/I)r are not represented, and a person cell outside its group's paradigm has the empty form.

Equations

• Turkish.Verb.Exponent.reciprocal.form = { bracketed := some Turkish.Phonology.I, segments := [Turkish.Phonology.ş] }
• Turkish.Verb.Exponent.reflexive.form = { bracketed := some Turkish.Phonology.I, segments := [Turkish.Phonology.n] }
• Turkish.Verb.Exponent.causative.form = { segments := [Turkish.Phonology.D, Turkish.Phonology.I, Turkish.Phonology.r] }
• Turkish.Verb.Exponent.passive.form = { segments := [Turkish.Phonology.I, Turkish.Phonology.l] }
• Turkish.Verb.Exponent.possibility.form = { bracketed := some Turkish.Phonology.y, segments := [Turkish.Phonology.A] }
• Turkish.Verb.Exponent.negative.form = { segments := [Turkish.Phonology.m, Turkish.Phonology.A] }
• Turkish.Verb.Exponent.abil.form = { bracketed := some Turkish.Phonology.y, segments := [Turkish.Phonology.A, Turkish.Phonology.b, Turkish.Phonology.i, Turkish.Phonology.l] }
• Turkish.Verb.Exponent.iver.form = { bracketed := some Turkish.Phonology.y, segments := [Turkish.Phonology.I, Turkish.Phonology.v, Turkish.Phonology.e, Turkish.Phonology.r] }
• Turkish.Verb.Exponent.agel.form = { bracketed := some Turkish.Phonology.y, segments := [Turkish.Phonology.A, Turkish.Phonology.g, Turkish.Phonology.e, Turkish.Phonology.l] }
• Turkish.Verb.Exponent.ayaz.form = { bracketed := some Turkish.Phonology.y, segments := [Turkish.Phonology.A, Turkish.Phonology.y, Turkish.Phonology.a, Turkish.Phonology.z] }
• Turkish.Verb.Exponent.akal.form = { bracketed := some Turkish.Phonology.y, segments := [Turkish.Phonology.A, Turkish.Phonology.k, Turkish.Phonology.a, Turkish.Phonology.l] }
• Turkish.Verb.Exponent.adur.form = { bracketed := some Turkish.Phonology.y, segments := [Turkish.Phonology.A, Turkish.Phonology.d, Turkish.Phonology.u, Turkish.Phonology.r] }
• Turkish.Verb.Exponent.di.form = { segments := [Turkish.Phonology.D, Turkish.Phonology.I] }
• Turkish.Verb.Exponent.miş.form = { segments := [Turkish.Phonology.m, Turkish.Phonology.I, Turkish.Phonology.ş] }
• Turkish.Verb.Exponent.sa.form = { segments := [Turkish.Phonology.s, Turkish.Phonology.A] }
• Turkish.Verb.Exponent.aorist.form = { bracketed := some Turkish.Phonology.I, segments := [Turkish.Phonology.r] }
• Turkish.Verb.Exponent.acak.form = { bracketed := some Turkish.Phonology.y, segments := [Turkish.Phonology.A, Turkish.Phonology.c, Turkish.Phonology.A, Turkish.Phonology.K] }
• Turkish.Verb.Exponent.iyor.form = { bracketed := some Turkish.Phonology.I, segments := [Turkish.Phonology.y, Turkish.Phonology.o, Turkish.Phonology.r] }
• Turkish.Verb.Exponent.mali.form = { segments := [Turkish.Phonology.m, Turkish.Phonology.A, Turkish.Phonology.l, Turkish.Phonology.I] }
• Turkish.Verb.Exponent.makta.form = { segments := [Turkish.Phonology.m, Turkish.Phonology.A, Turkish.Phonology.k, Turkish.Phonology.t, Turkish.Phonology.A] }
• Turkish.Verb.Exponent.optative.form = { bracketed := some Turkish.Phonology.y, segments := [Turkish.Phonology.A] }
• Turkish.Verb.Exponent.pastCopula.form = { bracketed := some Turkish.Phonology.y, segments := [Turkish.Phonology.D, Turkish.Phonology.I] }
• Turkish.Verb.Exponent.evidentialCopula.form = { bracketed := some Turkish.Phonology.y, segments := [Turkish.Phonology.m, Turkish.Phonology.I, Turkish.Phonology.ş] }
• Turkish.Verb.Exponent.conditionalCopula.form = { bracketed := some Turkish.Phonology.y, segments := [Turkish.Phonology.s, Turkish.Phonology.A] }
• (Turkish.Verb.Exponent.person g c).form = (g.paradigm.realize c).getD { segments := [] }
• Turkish.Verb.Exponent.dir.form = { segments := [Turkish.Phonology.D, Turkish.Phonology.I, Turkish.Phonology.r] }

def Turkish.Verb.forms (xs : List ((σ : Slot) × Exponent σ)) : List Suffix

The citation forms of a string of exponents.

Equations

• Turkish.Verb.forms xs = List.map (fun (x : (σ : Turkish.Verb.Slot) × Turkish.Verb.Exponent σ) => x.snd.form) xs

@[simp]

theorem Turkish.Verb.forms_nil : forms [] = []

@[simp]

theorem Turkish.Verb.forms_cons (x : (σ : Slot) × Exponent σ) (xs : List ((σ : Slot) × Exponent σ)) : forms (x :: xs) = x.snd.form :: forms xs

@[simp]

theorem Turkish.Verb.forms_append (xs ys : List ((σ : Slot) × Exponent σ)) : forms (xs ++ ys) = forms xs ++ forms ys

def Turkish.Verb.Exponent.group? {σ : Slot} : Exponent σ → Option PersonGroup

The group of a person marker.

Equations

• (Turkish.Verb.Exponent.person g cell).group? = some g
• x✝.group? = none

def Turkish.Verb.Exponent.IsClitic {σ : Slot} : Exponent σ → Prop

The exponents that are clitics, those of the copula and -DIr positions and the person markers of group 2 (§11.1).

Equations

• (Turkish.Verb.Exponent.person g cell).IsClitic = (g = Turkish.Verb.PersonGroup.two)
• x✝.IsClitic = (σ = Turkish.Verb.Slot.copula ∨ σ = Turkish.Verb.Slot.generalizing)

@[instance_reducible]

instance Turkish.Verb.instDecidablePredExponentIsClitic {σ : Slot} : DecidablePred Exponent.IsClitic

Equations

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

def Turkish.Verb.Exponent.IsThirdPlural {σ : Slot} : Exponent σ → Prop

The third-person plural -lAr of groups 1 and 2, the one person marker whose place varies (§8.3.3, §8.4).

Equations

• (Turkish.Verb.Exponent.person g cell).IsThirdPlural = (g ≠ Turkish.Verb.PersonGroup.three ∧ cell = Agreement.Bundle.personNumber Person.third Number.plural)
• x✝.IsThirdPlural = False

@[instance_reducible]

instance Turkish.Verb.instDecidablePredExponentIsThirdPlural {σ : Slot} : DecidablePred Exponent.IsThirdPlural

Equations

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

def Turkish.Verb.template : Morphology.AffixTemplate Slot

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.

Equations

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

theorem Turkish.Verb.pairwise_lt_suffixSlots : List.Pairwise (fun (x1 x2 : Slot) => x1 < x2) template.suffixSlots

def Turkish.Verb.Licensed (xs : List ((σ : Slot) × Exponent σ)) : Prop

A string of exponents is licensed in the order of the template, or with its person marker before the copular marker when that is a group-1 marker after -DI or the third-person plural, or after -DIr when it is the third-person plural (§8.3.2, §8.3.3, §8.4).

Equations

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

@[instance_reducible]

instance Turkish.Verb.instDecidablePredListSigmaSlotExponentLicensed : DecidablePred Licensed

Equations

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

The nominal

inductive Turkish.Nominal.Slot : Type

The inflectional suffix slots of a nominal (§8.1).

• number : Slot
• possession : Slot
• case : Slot

@[instance_reducible]

instance Turkish.Nominal.instDecidableEqSlot : DecidableEq Slot

Equations

• Turkish.Nominal.instDecidableEqSlot x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

@[instance_reducible]

instance Turkish.Nominal.instReprSlot : Repr Slot

Equations

• Turkish.Nominal.instReprSlot = { reprPrec := Turkish.Nominal.instReprSlot.repr }

def Turkish.Nominal.instReprSlot.repr : Slot → ℕ → Std.Format

Equations

• One or more equations did not get rendered due to their size.
• Turkish.Nominal.instReprSlot.repr Turkish.Nominal.Slot.case prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Turkish.Nominal.Slot.case")).group prec✝

def Turkish.Nominal.possessives : Agreement.Paradigm Suffix

The possessive suffixes (§8.1.2). The second-person plural is also the formal singular, and the final n that the third-person forms take before a case suffix is supplied by forms.

Equations

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

inductive Turkish.Nominal.Exponent : Slot → Type

The exponents of each slot (§8.1.1 to §8.1.3).

• plural : Exponent Slot.number

  -lAr (§8.1.1).

• possessive (cell : Agreement.Bundle) : Exponent Slot.possession

  A possessive suffix, a cell of possessives (§8.1.2).

• accusative : Exponent Slot.case

  -(y)I.

• dative : Exponent Slot.case

  -(y)A.

• locative : Exponent Slot.case

  -DA.

• ablative : Exponent Slot.case

  -DAn.

• genitive : Exponent Slot.case

  -(n)In.

@[instance_reducible]

instance Turkish.Nominal.instDecidableEqExponent {a✝ : Slot} : DecidableEq (Exponent a✝)

Equations

• Turkish.Nominal.instDecidableEqExponent = Turkish.Nominal.instDecidableEqExponent.decEq

def Turkish.Nominal.instDecidableEqExponent.decEq {a✝ : Slot} (x✝ x✝¹ : Exponent a✝) : Decidable (x✝ = x✝¹)

Equations

• Turkish.Nominal.instDecidableEqExponent.decEq Turkish.Nominal.Exponent.plural Turkish.Nominal.Exponent.plural = isTrue Turkish.Nominal.instDecidableEqExponent.decEq._proof_1
• Turkish.Nominal.instDecidableEqExponent.decEq (Turkish.Nominal.Exponent.possessive a_1) (Turkish.Nominal.Exponent.possessive b) = if h : a_1 = b then h ▸ isTrue ⋯ else isFalse ⋯
• Turkish.Nominal.instDecidableEqExponent.decEq Turkish.Nominal.Exponent.accusative Turkish.Nominal.Exponent.accusative = isTrue Turkish.Nominal.instDecidableEqExponent.decEq._proof_24
• Turkish.Nominal.instDecidableEqExponent.decEq Turkish.Nominal.Exponent.accusative Turkish.Nominal.Exponent.dative = isFalse Turkish.Nominal.instDecidableEqExponent.decEq._proof_4
• Turkish.Nominal.instDecidableEqExponent.decEq Turkish.Nominal.Exponent.accusative Turkish.Nominal.Exponent.locative = isFalse Turkish.Nominal.instDecidableEqExponent.decEq._proof_5
• Turkish.Nominal.instDecidableEqExponent.decEq Turkish.Nominal.Exponent.accusative Turkish.Nominal.Exponent.ablative = isFalse Turkish.Nominal.instDecidableEqExponent.decEq._proof_6
• Turkish.Nominal.instDecidableEqExponent.decEq Turkish.Nominal.Exponent.accusative Turkish.Nominal.Exponent.genitive = isFalse Turkish.Nominal.instDecidableEqExponent.decEq._proof_7
• Turkish.Nominal.instDecidableEqExponent.decEq Turkish.Nominal.Exponent.dative Turkish.Nominal.Exponent.accusative = isFalse Turkish.Nominal.instDecidableEqExponent.decEq._proof_8
• Turkish.Nominal.instDecidableEqExponent.decEq Turkish.Nominal.Exponent.dative Turkish.Nominal.Exponent.dative = isTrue Turkish.Nominal.instDecidableEqExponent.decEq._proof_25
• Turkish.Nominal.instDecidableEqExponent.decEq Turkish.Nominal.Exponent.dative Turkish.Nominal.Exponent.locative = isFalse Turkish.Nominal.instDecidableEqExponent.decEq._proof_9
• Turkish.Nominal.instDecidableEqExponent.decEq Turkish.Nominal.Exponent.dative Turkish.Nominal.Exponent.ablative = isFalse Turkish.Nominal.instDecidableEqExponent.decEq._proof_10
• Turkish.Nominal.instDecidableEqExponent.decEq Turkish.Nominal.Exponent.dative Turkish.Nominal.Exponent.genitive = isFalse Turkish.Nominal.instDecidableEqExponent.decEq._proof_11
• Turkish.Nominal.instDecidableEqExponent.decEq Turkish.Nominal.Exponent.locative Turkish.Nominal.Exponent.accusative = isFalse Turkish.Nominal.instDecidableEqExponent.decEq._proof_12
• Turkish.Nominal.instDecidableEqExponent.decEq Turkish.Nominal.Exponent.locative Turkish.Nominal.Exponent.dative = isFalse Turkish.Nominal.instDecidableEqExponent.decEq._proof_13
• Turkish.Nominal.instDecidableEqExponent.decEq Turkish.Nominal.Exponent.locative Turkish.Nominal.Exponent.locative = isTrue Turkish.Nominal.instDecidableEqExponent.decEq._proof_26
• Turkish.Nominal.instDecidableEqExponent.decEq Turkish.Nominal.Exponent.locative Turkish.Nominal.Exponent.ablative = isFalse Turkish.Nominal.instDecidableEqExponent.decEq._proof_14
• Turkish.Nominal.instDecidableEqExponent.decEq Turkish.Nominal.Exponent.locative Turkish.Nominal.Exponent.genitive = isFalse Turkish.Nominal.instDecidableEqExponent.decEq._proof_15
• Turkish.Nominal.instDecidableEqExponent.decEq Turkish.Nominal.Exponent.ablative Turkish.Nominal.Exponent.accusative = isFalse Turkish.Nominal.instDecidableEqExponent.decEq._proof_16
• Turkish.Nominal.instDecidableEqExponent.decEq Turkish.Nominal.Exponent.ablative Turkish.Nominal.Exponent.dative = isFalse Turkish.Nominal.instDecidableEqExponent.decEq._proof_17
• Turkish.Nominal.instDecidableEqExponent.decEq Turkish.Nominal.Exponent.ablative Turkish.Nominal.Exponent.locative = isFalse Turkish.Nominal.instDecidableEqExponent.decEq._proof_18
• Turkish.Nominal.instDecidableEqExponent.decEq Turkish.Nominal.Exponent.ablative Turkish.Nominal.Exponent.ablative = isTrue Turkish.Nominal.instDecidableEqExponent.decEq._proof_27
• Turkish.Nominal.instDecidableEqExponent.decEq Turkish.Nominal.Exponent.ablative Turkish.Nominal.Exponent.genitive = isFalse Turkish.Nominal.instDecidableEqExponent.decEq._proof_19
• Turkish.Nominal.instDecidableEqExponent.decEq Turkish.Nominal.Exponent.genitive Turkish.Nominal.Exponent.accusative = isFalse Turkish.Nominal.instDecidableEqExponent.decEq._proof_20
• Turkish.Nominal.instDecidableEqExponent.decEq Turkish.Nominal.Exponent.genitive Turkish.Nominal.Exponent.dative = isFalse Turkish.Nominal.instDecidableEqExponent.decEq._proof_21
• Turkish.Nominal.instDecidableEqExponent.decEq Turkish.Nominal.Exponent.genitive Turkish.Nominal.Exponent.locative = isFalse Turkish.Nominal.instDecidableEqExponent.decEq._proof_22
• Turkish.Nominal.instDecidableEqExponent.decEq Turkish.Nominal.Exponent.genitive Turkish.Nominal.Exponent.ablative = isFalse Turkish.Nominal.instDecidableEqExponent.decEq._proof_23
• Turkish.Nominal.instDecidableEqExponent.decEq Turkish.Nominal.Exponent.genitive Turkish.Nominal.Exponent.genitive = isTrue Turkish.Nominal.instDecidableEqExponent.decEq._proof_28

def Turkish.Nominal.Exponent.form {σ : Slot} : Exponent σ → Suffix

The citation form of an exponent.

Equations

• Turkish.Nominal.Exponent.plural.form = { segments := [Turkish.Phonology.l, Turkish.Phonology.A, Turkish.Phonology.r] }
• (Turkish.Nominal.Exponent.possessive c).form = (Turkish.Nominal.possessives.realize c).getD { segments := [] }
• Turkish.Nominal.Exponent.accusative.form = { bracketed := some Turkish.Phonology.y, segments := [Turkish.Phonology.I] }
• Turkish.Nominal.Exponent.dative.form = { bracketed := some Turkish.Phonology.y, segments := [Turkish.Phonology.A] }
• Turkish.Nominal.Exponent.locative.form = { segments := [Turkish.Phonology.D, Turkish.Phonology.A] }
• Turkish.Nominal.Exponent.ablative.form = { segments := [Turkish.Phonology.D, Turkish.Phonology.A, Turkish.Phonology.n] }
• Turkish.Nominal.Exponent.genitive.form = { bracketed := some Turkish.Phonology.n, segments := [Turkish.Phonology.I, Turkish.Phonology.n] }

def Turkish.Nominal.Exponent.IsThirdPossessive : (σ : Slot) × Exponent σ → Prop

The third-person possessives are the exponents that take a final n before a case suffix (§6.2 (iib), §8.1.2).

Equations

• One or more equations did not get rendered due to their size.
• Turkish.Nominal.Exponent.IsThirdPossessive x✝ = False

@[instance_reducible]

instance Turkish.Nominal.instDecidablePredSigmaSlotExponentIsThirdPossessive : DecidablePred Exponent.IsThirdPossessive

Equations

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

def Turkish.Nominal.forms : List ((σ : Slot) × Exponent σ) → List Suffix

forms es lists the citation forms of a string of exponents, a third-person possessive taking its final n when a case suffix follows, as in tepe-si-n-de (§8.1.2).

Equations

• One or more equations did not get rendered due to their size.
• Turkish.Nominal.forms [] = []

def Turkish.Nominal.template : Morphology.AffixTemplate Slot

The template of the nominal lists the slots number, possession and case, in that order, each of which a nominal may skip (§8.1).

Equations

• Turkish.Nominal.template = { suffixSlots := [Turkish.Nominal.Slot.number, Turkish.Nominal.Slot.possession, Turkish.Nominal.Slot.case] }

def Turkish.Nominal.Exponent.toCase : Exponent Slot.case → Case

The case a case exponent realizes.

Equations

• Turkish.Nominal.Exponent.accusative.toCase = Turkish.Case.acc
• Turkish.Nominal.Exponent.dative.toCase = Turkish.Case.dat
• Turkish.Nominal.Exponent.locative.toCase = Turkish.Case.loc
• Turkish.Nominal.Exponent.ablative.toCase = Turkish.Case.abl
• Turkish.Nominal.Exponent.genitive.toCase = Turkish.Case.gen

theorem Turkish.Nominal.Exponent.toCase_injective : Function.Injective toCase

The five case exponents realize five distinct cases.

theorem Turkish.Nominal.exists_toCase_eq_iff (c : Case) : (∃ (e : Exponent Slot.case), e.toCase = c) ↔ c ≠ Case.nom

The case exponents realize every case but the nominative, which is unmarked.