Finnish morphotactics

A Finnish nominal takes number, case and possessive endings and clitics, always in that order, as pullo-i-ssa-nne-kin 'in your bottles too' (Karlsson §3.1), and a non-finite verb form puts the function ending of its infinitive before them, as sano-e-ssa-ni 'while I say' (§3.3). The plural is -t in the nominative and -i elsewhere, -j between two vowels, and clitics come last, more than one occasionally, as on-ko-han (§25.6).

Some endings determine more than their own position. The nominative plural -t stands on the border between number and case, so no case ending follows it. The comitative -ine contains a fossilized plural -i, so no number ending precedes it, and on a noun a possessive ending always follows it (§16.4). Infinitives are never marked for number, each takes only its own cases (Finnish.Infinitive.cases), and the translative of the A infinitive takes a possessive ending (§22.2.2).

Before a possessive ending the final consonant of an ending is dropped, so that the nominative and the genitive coincide, as in ove-mme 'our door, of our door', and the illative loses its -n, as in auto-o-ni 'into my car'. The translative is -kse. After a case ending in a short vowel the third person is usually -Vn, as in talo-ssa-an 'in his house', beside the older -nsA, except after a partitive -A that follows a stem-final A, as in kala-a-nsa (§14.1).

Main definitions

• Finnish.Clitic: the common clitics.
• Finnish.Nominal.Slot, Finnish.Nominal.Exponent, Finnish.Nominal.template: the positions, their exponents and their order.
• Finnish.Nominal.WellFormed: the strings of endings that make a word.
• Finnish.Nominal.realize: the surface forms of a stem with a string of endings.

Main results

• Finnish.Nominal.not_wellFormed_nominativePlural_case, Finnish.Nominal.not_wellFormed_comitative: the nominative plural takes no case ending and a comitative needs a possessive ending.
• Finnish.Nominal.continuations_third: the third-person possessive ending after the inessive and after the illative.
• Finnish.Nominal.realize_gen_possessive: with a possessive ending the genitive is the nominative.

Implementation notes

The genitive plural -ten, which follows the consonant stem of the singular without the plural -i, as in nais-ten 'of the women', is not represented, nor the rarer clitics -kA and -s, nor the passive of the E infinitive. Which alternant of an ending a stem takes is not represented either, so a stem has every form its endings allow.

References

• [Kar18]

inductive Finnish.Clitic : Type

The common clitics (§25.6).

• kO : Clitic

  -kO, of yes-no questions.

• kin : Clitic

  -kin 'also, too'.

• kAAn : Clitic

  -kAAn '(not) either', -kin of negative sentences.

• hAn : Clitic

  -hAn, emphasis.

• pA : Clitic

  -pA, emphasis.

@[instance_reducible]

instance Finnish.instDecidableEqClitic : DecidableEq Clitic

Equations

• Finnish.instDecidableEqClitic x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

def Finnish.instReprClitic.repr : Clitic → ℕ → Std.Format

Equations

• Finnish.instReprClitic.repr Finnish.Clitic.kO prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Finnish.Clitic.kO")).group prec✝
• Finnish.instReprClitic.repr Finnish.Clitic.kin prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Finnish.Clitic.kin")).group prec✝
• Finnish.instReprClitic.repr Finnish.Clitic.kAAn prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Finnish.Clitic.kAAn")).group prec✝
• Finnish.instReprClitic.repr Finnish.Clitic.hAn prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Finnish.Clitic.hAn")).group prec✝
• Finnish.instReprClitic.repr Finnish.Clitic.pA prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Finnish.Clitic.pA")).group prec✝

@[instance_reducible]

instance Finnish.instReprClitic : Repr Clitic

Equations

• Finnish.instReprClitic = { reprPrec := Finnish.instReprClitic.repr }

def Finnish.Clitic.form : Clitic → List Phonology.Segment

The form of a clitic.

Equations

• Finnish.Clitic.kO.form = [Finnish.k, Finnish.O]
• Finnish.Clitic.kin.form = [Finnish.k, Finnish.i, Finnish.n]
• Finnish.Clitic.kAAn.form = [Finnish.k, Finnish.A, Finnish.A, Finnish.n]
• Finnish.Clitic.hAn.form = [Finnish.h, Finnish.A, Finnish.n]
• Finnish.Clitic.pA.form = [Finnish.p, Finnish.A]

inductive Finnish.Nominal.Slot : Type

The positions of the endings of a nominal and of a non-finite verb form.

• function : Slot

  The function ending of an infinitive.

• number : Slot

  The plural.

• case : Slot

  The case ending.

• possession : Slot

  The possessive ending.

• clitic : Slot

  The clitics.

@[instance_reducible]

instance Finnish.Nominal.instDecidableEqSlot : DecidableEq Slot

Equations

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

@[instance_reducible]

instance Finnish.Nominal.instReprSlot : Repr Slot

Equations

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

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

Equations

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

inductive Finnish.Nominal.Exponent : Slot → Type

The endings of each position.

• infinitive (i : Infinitive) : Exponent Slot.function

  The function ending of an infinitive.

• nominativePlural : Exponent Slot.number

  The nominative plural -t.

• plural : Exponent Slot.number

  The plural -i of the cases other than the nominative.

• case (c : Case) : Exponent Slot.case

  A case ending.

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

  A possessive ending, a cell of Finnish.Possession.endings.

• clitic (c : Clitic) : Exponent Slot.clitic

  A clitic.

@[instance_reducible]

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

Equations

• Finnish.Nominal.instDecidableEqExponent = Finnish.Nominal.instDecidableEqExponent.decEq

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

Equations

• Finnish.Nominal.instDecidableEqExponent.decEq (Finnish.Nominal.Exponent.infinitive a_1) (Finnish.Nominal.Exponent.infinitive b) = if h : a_1 = b then h ▸ isTrue ⋯ else isFalse ⋯
• Finnish.Nominal.instDecidableEqExponent.decEq Finnish.Nominal.Exponent.nominativePlural Finnish.Nominal.Exponent.nominativePlural = isTrue Finnish.Nominal.instDecidableEqExponent.decEq._proof_2
• Finnish.Nominal.instDecidableEqExponent.decEq Finnish.Nominal.Exponent.nominativePlural Finnish.Nominal.Exponent.plural = isFalse Finnish.Nominal.instDecidableEqExponent.decEq._proof_4
• Finnish.Nominal.instDecidableEqExponent.decEq Finnish.Nominal.Exponent.plural Finnish.Nominal.Exponent.nominativePlural = isFalse Finnish.Nominal.instDecidableEqExponent.decEq._proof_5
• Finnish.Nominal.instDecidableEqExponent.decEq Finnish.Nominal.Exponent.plural Finnish.Nominal.Exponent.plural = isTrue Finnish.Nominal.instDecidableEqExponent.decEq._proof_9
• Finnish.Nominal.instDecidableEqExponent.decEq (Finnish.Nominal.Exponent.case a_1) (Finnish.Nominal.Exponent.case b) = if h : a_1 = b then h ▸ isTrue ⋯ else isFalse ⋯
• Finnish.Nominal.instDecidableEqExponent.decEq (Finnish.Nominal.Exponent.possessive a_1) (Finnish.Nominal.Exponent.possessive b) = if h : a_1 = b then h ▸ isTrue ⋯ else isFalse ⋯
• Finnish.Nominal.instDecidableEqExponent.decEq (Finnish.Nominal.Exponent.clitic a_1) (Finnish.Nominal.Exponent.clitic b) = if h : a_1 = b then h ▸ isTrue ⋯ else isFalse ⋯

def Finnish.Nominal.template : RegularExpression Slot

The endings come in the order function, number, case and possessive, each of which a word may lack, and are followed by any number of clitics (§3.1, §3.3).

Equations

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

def Finnish.Nominal.Exponent.fills {σ : Slot} : Exponent σ → List Slot

An ending determines the value of its own position, and the nominative plural also determines the case, the comitative the number, and an infinitive the number, which is never marked. A clitic determines none.

Equations

• (Finnish.Nominal.Exponent.infinitive i).fills = [Finnish.Nominal.Slot.function, Finnish.Nominal.Slot.number]
• Finnish.Nominal.Exponent.nominativePlural.fills = [Finnish.Nominal.Slot.number, Finnish.Nominal.Slot.case]
• Finnish.Nominal.Exponent.plural.fills = [Finnish.Nominal.Slot.number]
• (Finnish.Nominal.Exponent.case Finnish.Case.com).fills = [Finnish.Nominal.Slot.case, Finnish.Nominal.Slot.number]
• (Finnish.Nominal.Exponent.case c).fills = [Finnish.Nominal.Slot.case]
• (Finnish.Nominal.Exponent.possessive p).fills = [Finnish.Nominal.Slot.possession]
• (Finnish.Nominal.Exponent.clitic c).fills = []

def Finnish.Nominal.Exponent.case? {σ : Slot} : Exponent σ → Option Case

The case an ending realizes.

Equations

• Finnish.Nominal.Exponent.nominativePlural.case? = some Finnish.Case.nom
• (Finnish.Nominal.Exponent.case c).case? = some c
• x✝.case? = none

def Finnish.Nominal.Exponent.infinitive? {σ : Slot} : Exponent σ → Option Infinitive

The infinitive an ending is the function ending of.

Equations

• (Finnish.Nominal.Exponent.infinitive i).infinitive? = some i
• x✝.infinitive? = none

def Finnish.Nominal.caseOf (es : List ((σ : Slot) × Exponent σ)) : Case

The case of a string of endings, the nominative if none realizes one.

Equations

• Finnish.Nominal.caseOf es = (List.findSome? (fun (x : (σ : Finnish.Nominal.Slot) × Finnish.Nominal.Exponent σ) => x.snd.case?) es).getD Finnish.Case.nom

def Finnish.Nominal.HasPossessive (es : List ((σ : Slot) × Exponent σ)) : Prop

The string of endings has a possessive ending.

Equations

• Finnish.Nominal.HasPossessive es = ∃ e ∈ es, e.fst = Finnish.Nominal.Slot.possession

@[instance_reducible]

instance Finnish.Nominal.instDecidableHasPossessive (es : List ((σ : Slot) × Exponent σ)) : Decidable (HasPossessive es)

Equations

• Finnish.Nominal.instDecidableHasPossessive es = Finnish.Nominal.instDecidableHasPossessive._aux_1 es

def Finnish.Nominal.WellFormed (es : List ((σ : Slot) × Exponent σ)) : Prop

A string of endings makes a word when they are in the order of the template, no position is determined twice, a comitative is followed by a possessive ending, and an infinitive is in one of its cases, its translative with a possessive ending.

Equations

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

@[instance_reducible]

instance Finnish.Nominal.instDecidablePredListSigmaSlotExponentWellFormed : DecidablePred WellFormed

Equations

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

theorem Finnish.Nominal.not_wellFormed_nominativePlural_case (c : Case) : ¬WellFormed [⟨Slot.number, Exponent.nominativePlural⟩, ⟨Slot.case, Exponent.case c⟩]

The nominative plural takes no case ending: pullo-t but not pullo-t-ssa.

theorem Finnish.Nominal.not_wellFormed_comitative : ¬WellFormed [⟨Slot.case, Exponent.case Case.com⟩]

A comitative needs a possessive ending: vaimo-ine-ni but not vaimo-ine.

Realization

def Finnish.Nominal.caseEndings (plural : Bool) (c : Case) : List (List Phonology.Segment)

The endings of the case c, after the plural when plural holds, where the genitive is -en, or -den or -tten (§13.1.2), the partitive -A or -tA and the illative -hVn or -siin.

Equations

• One or more equations did not get rendered due to their size.
• Finnish.Nominal.caseEndings plural Finnish.Case.part = if plural = true then [[Finnish.A], [Finnish.t, Finnish.A]] else Finnish.Declension.endings Finnish.Case.part
• Finnish.Nominal.caseEndings plural c = if plural = true then Finnish.Declension.endings c else Finnish.Declension.endings c

def Finnish.Nominal.beforePossessive (x : List Phonology.Segment) : List Phonology.Segment

Before a possessive ending the translative -ksi is -kse, and a final consonant is dropped.

Equations

• Finnish.Nominal.beforePossessive x = if x = [Finnish.k, Finnish.s, Finnish.i] then [Finnish.k, Finnish.s, Finnish.e] else if ∀ y ∈ x.getLast?, y.IsVowel then x else x.dropLast

def Finnish.Nominal.EndsInVowel (c : Case) : Prop

Every ending of the case ends in a vowel, as those of the local cases, the partitive, the essive, the translative, the abessive and the comitative do.

Equations

• Finnish.Nominal.EndsInVowel c = ∀ x ∈ Finnish.Declension.endings c, ∃ y ∈ x.getLast?, y.IsVowel

@[instance_reducible]

instance Finnish.Nominal.instDecidableEndsInVowel (c : Case) : Decidable (EndsInVowel c)

Equations

• Finnish.Nominal.instDecidableEndsInVowel c = Finnish.Nominal.instDecidableEndsInVowel._aux_1 c

def Finnish.Nominal.possessiveForms (p : Agreement.Bundle) (c : Option Case) (w : List Phonology.Segment) : List (List Phonology.Segment)

The forms of the possessive ending of the cell p after the word w, whose last case ending is of the case c: after a case ending in a short vowel the third person is -Vn or -nsA, except after a partitive -A that follows a stem-final A.

Equations

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

def Finnish.Nominal.BeforePossessive (es : List ((σ : Slot) × Exponent σ)) : Prop

The next ending is a possessive ending.

Equations

• Finnish.Nominal.BeforePossessive es = ∃ e ∈ es.head?, e.fst = Finnish.Nominal.Slot.possession

@[instance_reducible]

instance Finnish.Nominal.instDecidableBeforePossessive (es : List ((σ : Slot) × Exponent σ)) : Decidable (BeforePossessive es)

Equations

• Finnish.Nominal.instDecidableBeforePossessive es = Finnish.Nominal.instDecidableBeforePossessive._aux_1 es

def Finnish.Nominal.continuations (w : List Phonology.Segment) (plural : Bool) (c : Option Case) : List ((σ : Slot) × Exponent σ) → List (List Phonology.Segment)

The underlying forms of the word w followed by the endings es, where plural records a preceding plural and c the case of the last case ending. The plural -i is -j between two vowels (§5.4).

Equations

• One or more equations did not get rendered due to their size.
• Finnish.Nominal.continuations w plural c [] = [w]
• Finnish.Nominal.continuations w plural c (⟨Finnish.Nominal.Slot.function, Finnish.Nominal.Exponent.infinitive i⟩ :: es) = Finnish.Nominal.continuations (i.base w) plural c es
• Finnish.Nominal.continuations w plural c (⟨Finnish.Nominal.Slot.clitic, Finnish.Nominal.Exponent.clitic k⟩ :: es) = Finnish.Nominal.continuations (w ++ k.form) plural c es

def Finnish.Nominal.realize (w : List Phonology.Segment) (es : List ((σ : Slot) × Exponent σ)) : List (List Phonology.Segment)

The surface forms of the stem w with the endings es.

Equations

• Finnish.Nominal.realize w es = List.map Finnish.surface (Finnish.Nominal.continuations w false none es)

theorem Finnish.Nominal.continuations_third : continuations [] false none [⟨Slot.case, Exponent.case Case.ine⟩, ⟨Slot.possession, Exponent.possessive (Agreement.Bundle.personNumber Person.third Number.singular)⟩] = [[s, s, A, V, n], [s, s, A, n, s, A]] ∧ continuations [] false none [⟨Slot.case, Exponent.case Case.ill⟩, ⟨Slot.possession, Exponent.possessive (Agreement.Bundle.personNumber Person.third Number.singular)⟩] = [[V, n, s, A], [h, V, n, s, A], [s, e, e, n, s, A]]

The third person is -Vn or -nsA after the inessive, as in talo-ssa-an 'in his house', and -nsA alone after the illative, whose endings end in a consonant, as in talo-o-nsa 'into his house'.

theorem Finnish.Nominal.realize_gen_possessive (w : List Phonology.Segment) (p : Agreement.Bundle) : realize w [⟨Slot.case, Exponent.case Case.gen⟩, ⟨Slot.possession, Exponent.possessive p⟩] = realize w [⟨Slot.possession, Exponent.possessive p⟩]

With a possessive ending the genitive is the nominative, as in ove-mme 'our door, of our door'.