Karlsson (2017): Finnish: A Comprehensive Grammar

This file formalizes the object-case rules of [Kar18], the alternation between the partitive and the total object in Finnish. The grammar orders the rules: the object is partitive if the sentence is negative, the action irresultative, or the quantity indefinite (section 12.2.2); only otherwise does it take a total-object case, the accusative for a personal pronoun, the nominative for a plural nominal or a numeral head, and for a singular nominal the genitive, or the nominative under an imperative, a passive, an obligation, or an infinitive phrase acting as subject (section 13.3.2). Object.case is that procedure, and the grammar's examples, as rows, agree with it (rows_agree).

The partitive is the stronger object case (case_eq_part_iff), and in an affirmative sentence about a definite quantity the object is partitive exactly when the action is irresultative (part_iff_atelic), the case marking of aspect the grammar describes.

The word forms of the grammar's tables of endings are words of the Finnish Fragment's morphotactics (wellFormed_forms) and derived by it (forms_derived). A form is its stem followed by the function ending of an infinitive, a number, a case and a possessive ending and a clitic, in the order of the grammar's diagrams and in the archiphonemic spelling of its tables, and vowel copy and palatal harmony give its surface. The tables are those of the cases, the possessive endings and the structure of nominals and of non-finite forms (section 3), of the plural (section 5.4), of the partitive and genitive plural (section 13.1.2), of the possessive endings after a case ending (section 14.1), of the A infinitive translative (section 22.2.2) and of the MA infinitive (section 22.4.1).

Implementation notes

Resultative and irresultative action are read as the telic and atelic values of Aspect.Telicity. The grammar lists the constructions under which a singular total object drops its ending rather than unifying them; Clause lists them likewise.

The forms of the tables are those whose genitive plural, if any, follows the plural -i, since the Fragment does not represent -ten on the consonant stem, as in nais-ten 'of the women'. A nominative form has no case ending.

References

• [Kar18]

inductive Karlsson2017.Nominal : Type

The kind of nominal serving as object, as the total-object endings of section 13.3.2 read it.

• personalPronoun : Nominal
• plural : Nominal
• numeral : Nominal
• singular : Nominal

@[instance_reducible]

instance Karlsson2017.instDecidableEqNominal : DecidableEq Nominal

Equations

• Karlsson2017.instDecidableEqNominal x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

def Karlsson2017.instReprNominal.repr : Nominal → ℕ → Std.Format

Equations

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

@[instance_reducible]

instance Karlsson2017.instReprNominal : Repr Nominal

Equations

• Karlsson2017.instReprNominal = { reprPrec := Karlsson2017.instReprNominal.repr }

inductive Karlsson2017.Clause : Type

The clause types, the last four being those under which a singular total object is in the nominative (section 13.3.2, rule 4).

• finite : Clause
• imperative : Clause
• passive : Clause
• obligation : Clause
• infinitival : Clause

@[instance_reducible]

instance Karlsson2017.instDecidableEqClause : DecidableEq Clause

Equations

• Karlsson2017.instDecidableEqClause x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

def Karlsson2017.instReprClause.repr : Clause → ℕ → Std.Format

Equations

• One or more equations did not get rendered due to their size.
• Karlsson2017.instReprClause.repr Karlsson2017.Clause.finite prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Karlsson2017.Clause.finite")).group prec✝

@[instance_reducible]

instance Karlsson2017.instReprClause : Repr Clause

Equations

• Karlsson2017.instReprClause = { reprPrec := Karlsson2017.instReprClause.repr }

structure Karlsson2017.Object : Type

An object comes with the factors the grammar's rules read, namely the polarity of the sentence, the resultativity of the action, the definiteness of the quantity, the kind of nominal, and the clause type.

• negated : Bool
• telicity : Aspect.Telicity
• definite : Bool
• nominal : Nominal
• clause : Clause

def Karlsson2017.instDecidableEqObject.decEq (x✝ x✝¹ : Object) : Decidable (x✝ = x✝¹)

Equations

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

@[instance_reducible]

instance Karlsson2017.instDecidableEqObject : DecidableEq Object

Equations

• Karlsson2017.instDecidableEqObject = Karlsson2017.instDecidableEqObject.decEq

def Karlsson2017.instReprObject.repr : Object → ℕ → Std.Format

Equations

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

@[instance_reducible]

instance Karlsson2017.instReprObject : Repr Object

Equations

• Karlsson2017.instReprObject = { reprPrec := Karlsson2017.instReprObject.repr }

def Karlsson2017.Object.IsPartitive (o : Object) : Prop

The partitive conditions of section 12.2.2 are negation, irresultative action and indefinite quantity.

Equations

• o.IsPartitive = (o.negated = true ∨ o.telicity = Aspect.Telicity.atelic ∨ ¬o.definite = true)

@[instance_reducible]

instance Karlsson2017.Object.instDecidablePredIsPartitive : DecidablePred IsPartitive

Equations

• x✝.instDecidablePredIsPartitive = { decide := decide (x✝.negated = true) || decide (x✝.telicity = Aspect.Telicity.atelic ∨ ¬x✝.definite = true), reflects_decide := ⋯ }

def Karlsson2017.Object.totalCase (o : Object) : Case

The total-object ending of section 13.3.2.

Equations

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

def Karlsson2017.Object.case (o : Object) : Case

The case of the object is the partitive under any partitive condition, and otherwise the total-object ending (section 13.3.1).

Equations

• o.case = if o.IsPartitive then Case.part else o.totalCase

theorem Karlsson2017.Object.totalCase_ne_part (o : Object) : o.totalCase ≠ Case.part

theorem Karlsson2017.Object.case_eq_part_iff (o : Object) : o.case = Case.part ↔ o.IsPartitive

The partitive is the stronger object case: the object is partitive exactly under a partitive condition.

theorem Karlsson2017.Object.part_iff_atelic {o : Object} (hn : ¬o.negated = true) (hd : o.definite = true) : o.case = Case.part ↔ o.telicity = Aspect.Telicity.atelic

In an affirmative sentence about a definite quantity, the object is partitive exactly when the action is irresultative: the case marks the aspect.

theorem Karlsson2017.Object.case_eq_part_of_negated {o : Object} (h : o.negated = true) : o.case = Case.part

A negated sentence has a partitive object whatever the nominal.

theorem Karlsson2017.Object.case_of_personalPronoun {o : Object} (h : o.nominal = Nominal.personalPronoun) (hp : ¬o.IsPartitive) : o.case = Case.acc

A personal pronoun is a total object in the accusative alone.

structure Karlsson2017.Row : Type

A row pairs an object with the case the grammar gives it.

• object : Object
• case : Case

def Karlsson2017.nominalOf : List (String × Nominal)

Equations

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

def Karlsson2017.clauseOf : List (String × Clause)

Equations

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

def Karlsson2017.caseOf : List (String × Case)

Equations

• Karlsson2017.caseOf = [("part", Case.part), ("acc", Case.acc), ("nom", Case.nom), ("gen", Case.gen)]

def Karlsson2017.Row.ofDatum (e : Datum) : Option Row

A row from the grammar's features.

Equations

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

def Karlsson2017.rows : List Row

The object-case examples of sections 12.2.2 and 13.3.

Equations

• Karlsson2017.rows = List.filterMap Karlsson2017.Row.ofDatum Karlsson2017.Examples.all

theorem Karlsson2017.rows_agree (r : Row) : r ∈ rows → r.object.case = r.case

The grammar's examples take the case its rules assign.

Word structure

structure Karlsson2017.Word : Type

A word of the tables is given by its stem and its endings.

• stem : List Phonology.Segment
• endings : List ((σ : Finnish.Nominal.Slot) × Finnish.Nominal.Exponent σ)

def Karlsson2017.caseEnding : UD.Case → Option (Option Finnish.Case)

The case ending of a case, the nominative having none.

Equations

• Karlsson2017.caseEnding UD.Case.Nom = some none
• Karlsson2017.caseEnding UD.Case.Gen = some (some Finnish.Case.gen)
• Karlsson2017.caseEnding UD.Case.Acc = some (some Finnish.Case.acc)
• Karlsson2017.caseEnding UD.Case.Par = some (some Finnish.Case.part)
• Karlsson2017.caseEnding UD.Case.Ine = some (some Finnish.Case.ine)
• Karlsson2017.caseEnding UD.Case.Ela = some (some Finnish.Case.ela)
• Karlsson2017.caseEnding UD.Case.Ill = some (some Finnish.Case.ill)
• Karlsson2017.caseEnding UD.Case.Ade = some (some Finnish.Case.ade)
• Karlsson2017.caseEnding UD.Case.Abl = some (some Finnish.Case.abl)
• Karlsson2017.caseEnding UD.Case.All = some (some Finnish.Case.all)
• Karlsson2017.caseEnding UD.Case.Ess = some (some Finnish.Case.ess)
• Karlsson2017.caseEnding UD.Case.Tra = some (some Finnish.Case.transl)
• Karlsson2017.caseEnding UD.Case.Com = some (some Finnish.Case.com)
• Karlsson2017.caseEnding UD.Case.Abe = some (some Finnish.Case.abess)
• Karlsson2017.caseEnding UD.Case.Ins = some (some Finnish.Case.instr)
• Karlsson2017.caseEnding x✝ = none

def Karlsson2017.possessorOf : Forms.Possessor → Agreement.Bundle

The agreement of a possessive suffix.

Equations

• Karlsson2017.possessorOf Karlsson2017.Forms.Possessor.sg1 = Agreement.Bundle.personNumber Person.first Number.singular
• Karlsson2017.possessorOf Karlsson2017.Forms.Possessor.sg2 = Agreement.Bundle.personNumber Person.second Number.singular
• Karlsson2017.possessorOf Karlsson2017.Forms.Possessor.sg3 = Agreement.Bundle.personNumber Person.third Number.singular
• Karlsson2017.possessorOf Karlsson2017.Forms.Possessor.pl1 = Agreement.Bundle.personNumber Person.first Number.plural
• Karlsson2017.possessorOf Karlsson2017.Forms.Possessor.pl2 = Agreement.Bundle.personNumber Person.second Number.plural
• Karlsson2017.possessorOf Karlsson2017.Forms.Possessor.pl3 = Agreement.Bundle.personNumber Person.third Number.plural

def Karlsson2017.infinitiveOf : Forms.Infinitive → Finnish.Infinitive

The infinitive of the tables' label.

Equations

• Karlsson2017.infinitiveOf Karlsson2017.Forms.Infinitive.a = Finnish.Infinitive.a
• Karlsson2017.infinitiveOf Karlsson2017.Forms.Infinitive.e = Finnish.Infinitive.e
• Karlsson2017.infinitiveOf Karlsson2017.Forms.Infinitive.ma = Finnish.Infinitive.ma

def Karlsson2017.cliticOf : Forms.Clitic → Finnish.Clitic

The clitic of the tables' label.

Equations

• Karlsson2017.cliticOf Karlsson2017.Forms.Clitic.kO = Finnish.Clitic.kO
• Karlsson2017.cliticOf Karlsson2017.Forms.Clitic.kin = Finnish.Clitic.kin
• Karlsson2017.cliticOf Karlsson2017.Forms.Clitic.hAn = Finnish.Clitic.hAn
• Karlsson2017.cliticOf Karlsson2017.Forms.Clitic.kAAn = Finnish.Clitic.kAAn

def Karlsson2017.numberOf (c : Forms.Cell) : Option (Finnish.Nominal.Exponent Finnish.Nominal.Slot.number)

The plural exponent of a cell, -t in the nominative and -i- in the other cases.

Equations

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

def Karlsson2017.spell (w : String) : Option (List Phonology.Segment)

The phonemes a word writes, a capital as its small letter.

Equations

• Karlsson2017.spell w = List.mapM Finnish.ofChar (List.map Char.toLower w.toList)

def Karlsson2017.Word.ofForm (f : Data.Forms.Form Forms.Cell) : Option Word

A word from a form's segmentation and cell.

Equations

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

theorem Karlsson2017.isSome_ofForm (f : Data.Forms.Form Forms.Cell) : f ∈ Forms.all → (Word.ofForm f).isSome = true

Every form of the tables is a word.

theorem Karlsson2017.wellFormed_forms (f : Data.Forms.Form Forms.Cell) : f ∈ Forms.all → ∀ w ∈ Word.ofForm f, Finnish.Nominal.WellFormed w.endings

The endings of each form make a word.

theorem Karlsson2017.forms_derived (f : Data.Forms.Form Forms.Cell) : f ∈ Forms.all → ∀ w ∈ Word.ofForm f, ∃ x ∈ spell f.form, x ∈ Finnish.Nominal.realize w.stem w.endings

The Fragment gives each form of the tables.