Zaenen, Maling and Thráinsson (1985): Case and grammatical functions

This file formalizes [ZMT85]'s account of Icelandic case. A verb's arguments are thematic roles, some of which the verb marks with an idiosyncratic case (Arg); the association principles map the roles onto the grammatical functions SUBJ, OBJ and 2OBJ, agents to SUBJ and case-marked themes to the lowest function available, and the functions are the linear positions (associations). The passive is an operation on functions, not on cases or roles: SUBJ is suppressed and OBJ becomes SUBJ (GF.passive). Only afterwards does default case marking give the highest function without a case the nominative and the next the accusative (surfaceCase), so idiosyncratic case survives the passive (surfaceCase_lexical) while the accusative of an object does not.

The consequences the paper draws are theorems over the fragment. Every case array of Fragments.Icelandic.Verbs that the paper discusses is derived from its thematic structure (fragment_cases). A dative subject leaves the nominative to its object (þykja), and the passive of hjálpa has a dative subject and no nominative at all. A dative–accusative verb gives its theme and its goal either function, so gefa has two passives, the dative subject with a nominative retained object and the nominative subject with a dative object (gefa_passives), where the other ditransitives have one (lofa_passive); and a genitive theme passivizes exactly when it is the only object, since with a goal beside it the lowest function is 2OBJ (oska_passive). The seven subjecthood tests of §2 target SUBJ, whatever its case: each of the paper's judgments on raising, reflexivization, inversion, extraction, postposing, ellipsis and control is acceptable exactly when the argument tested is assigned SUBJ (rows_subject), and each attested case array is one the principles derive (rows_cases).

Implementation notes

The paper names the roles Agent, Theme, Goal and Source; the dative and accusative subjects of þykja, finnast, sakna and vanta it calls oblique subjects without a role, and experiencer is the label under which principle (61a) assigns them their function. Principle (61a) is read as assigning the first role SUBJ and leaving the object functions to the remaining roles in either order unless (61c) fixes them, which is the paper's dual association for gefa and keeps the nominative theme of þykja an object, as the tests of §2 require. A third function without idiosyncratic case receives no default case; the paper's ditransitives never present one.

References

• [ZMT85]

Thematic structure and grammatical functions

inductive ZaenenMalingThrainsson1985.Role : Type

The thematic roles.

• agent : Role
• theme : Role
• goal : Role
• source : Role
• experiencer : Role

@[instance_reducible]

instance ZaenenMalingThrainsson1985.instDecidableEqRole : DecidableEq Role

Equations

• ZaenenMalingThrainsson1985.instDecidableEqRole x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

def ZaenenMalingThrainsson1985.instReprRole.repr : Role → ℕ → Std.Format

Equations

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

@[instance_reducible]

instance ZaenenMalingThrainsson1985.instReprRole : Repr Role

Equations

• ZaenenMalingThrainsson1985.instReprRole = { reprPrec := ZaenenMalingThrainsson1985.instReprRole.repr }

structure ZaenenMalingThrainsson1985.Arg : Type

An argument at thematic structure: its role and the idiosyncratic case the verb assigns it, if any, as in the paper's (60).

• role : Role
• lexicalCase : Option Icelandic.Case

@[instance_reducible]

instance ZaenenMalingThrainsson1985.instDecidableEqArg : DecidableEq Arg

Equations

• ZaenenMalingThrainsson1985.instDecidableEqArg = ZaenenMalingThrainsson1985.instDecidableEqArg.decEq

def ZaenenMalingThrainsson1985.instDecidableEqArg.decEq (x✝ x✝¹ : Arg) : Decidable (x✝ = x✝¹)

Equations

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

def ZaenenMalingThrainsson1985.instReprArg.repr : Arg → ℕ → Std.Format

Equations

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

@[instance_reducible]

instance ZaenenMalingThrainsson1985.instReprArg : Repr Arg

Equations

• ZaenenMalingThrainsson1985.instReprArg = { reprPrec := ZaenenMalingThrainsson1985.instReprArg.repr }

inductive ZaenenMalingThrainsson1985.GF : Type

The grammatical functions a bare NP argument may bear.

• subj : GF
• obj : GF
• obj2 : GF

@[instance_reducible]

instance ZaenenMalingThrainsson1985.instDecidableEqGF : DecidableEq GF

Equations

• ZaenenMalingThrainsson1985.instDecidableEqGF x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

@[instance_reducible]

instance ZaenenMalingThrainsson1985.instReprGF : Repr GF

Equations

• ZaenenMalingThrainsson1985.instReprGF = { reprPrec := ZaenenMalingThrainsson1985.instReprGF.repr }

def ZaenenMalingThrainsson1985.instReprGF.repr : GF → ℕ → Std.Format

Equations

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

def ZaenenMalingThrainsson1985.GF.available (n : ℕ) : List GF

The functions available to n arguments, highest first, (61a).

Equations

• ZaenenMalingThrainsson1985.GF.available n = List.take n [ZaenenMalingThrainsson1985.GF.subj, ZaenenMalingThrainsson1985.GF.obj, ZaenenMalingThrainsson1985.GF.obj2]

def ZaenenMalingThrainsson1985.GF.rank : GF → ℕ

The position of a function in the hierarchy.

Equations

• ZaenenMalingThrainsson1985.GF.subj.rank = 0
• ZaenenMalingThrainsson1985.GF.obj.rank = 1
• ZaenenMalingThrainsson1985.GF.obj2.rank = 2

def ZaenenMalingThrainsson1985.GF.lowest (n : ℕ) : Option GF

The lowest function available to n arguments.

Equations

• ZaenenMalingThrainsson1985.GF.lowest n = (ZaenenMalingThrainsson1985.GF.available n).getLast?

@[reducible, inline]

abbrev ZaenenMalingThrainsson1985.Association : Type

An association of the arguments, in order, with functions.

Equations

• ZaenenMalingThrainsson1985.Association = List ZaenenMalingThrainsson1985.GF

def ZaenenMalingThrainsson1985.Association.Valid (t : List Arg) (a : Association) : Prop

The association satisfies the principles: the first role bears SUBJ (61a), agents bear SUBJ (61b), and a case-marked theme the lowest function available (61c).

Equations

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

@[instance_reducible]

instance ZaenenMalingThrainsson1985.instDecidableValid (t : List Arg) (a : Association) : Decidable (Association.Valid t a)

Equations

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

def ZaenenMalingThrainsson1985.insertions (x : GF) : List GF → List (List GF)

x inserted at each position of a list.

Equations

• ZaenenMalingThrainsson1985.insertions x [] = [[x]]
• ZaenenMalingThrainsson1985.insertions x (y :: ys) = (x :: y :: ys) :: List.map (fun (x : List ZaenenMalingThrainsson1985.GF) => y :: x) (ZaenenMalingThrainsson1985.insertions x ys)

def ZaenenMalingThrainsson1985.perms : List GF → List (List GF)

The permutations of a list, by structural recursion so that decide can run them.

Equations

• ZaenenMalingThrainsson1985.perms [] = [[]]
• ZaenenMalingThrainsson1985.perms (y :: ys) = List.flatMap (ZaenenMalingThrainsson1985.insertions y) (ZaenenMalingThrainsson1985.perms ys)

def ZaenenMalingThrainsson1985.associations (t : List Arg) : List Association

The associations the principles allow: the assignments of the available functions to the arguments, one each (61a), that satisfy (61b) and (61c).

Equations

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

Passive and default case

inductive ZaenenMalingThrainsson1985.Voice : Type

The voices.

• active : Voice
• passive : Voice

@[instance_reducible]

instance ZaenenMalingThrainsson1985.instDecidableEqVoice : DecidableEq Voice

Equations

• ZaenenMalingThrainsson1985.instDecidableEqVoice x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

def ZaenenMalingThrainsson1985.instReprVoice.repr : Voice → ℕ → Std.Format

Equations

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

@[instance_reducible]

instance ZaenenMalingThrainsson1985.instReprVoice : Repr Voice

Equations

• ZaenenMalingThrainsson1985.instReprVoice = { reprPrec := ZaenenMalingThrainsson1985.instReprVoice.repr }

def ZaenenMalingThrainsson1985.GF.passive : GF → Option GF

The passive on functions, (53): SUBJ is suppressed and OBJ becomes SUBJ.

Equations

• ZaenenMalingThrainsson1985.GF.subj.passive = none
• ZaenenMalingThrainsson1985.GF.obj.passive = some ZaenenMalingThrainsson1985.GF.subj
• ZaenenMalingThrainsson1985.GF.obj2.passive = some ZaenenMalingThrainsson1985.GF.obj2

def ZaenenMalingThrainsson1985.GF.inVoice (g : GF) : Voice → Option GF

The function an argument bears in a voice.

Equations

• g.inVoice ZaenenMalingThrainsson1985.Voice.active = some g
• g.inVoice ZaenenMalingThrainsson1985.Voice.passive = g.passive

def ZaenenMalingThrainsson1985.realize (t : List Arg) (a : Association) (v : Voice) : List (Arg × Option GF)

The arguments with the functions they bear in a voice.

Equations

• ZaenenMalingThrainsson1985.realize t a v = List.map (fun (p : ZaenenMalingThrainsson1985.Arg × ZaenenMalingThrainsson1985.GF) => (p.1, p.2.inVoice v)) (t.zip a)

def ZaenenMalingThrainsson1985.unmarkedAbove (r : List (Arg × Option GF)) (g : GF) : ℕ

The functions without idiosyncratic case that outrank g.

Equations

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

def ZaenenMalingThrainsson1985.surfaceCase (r : List (Arg × Option GF)) (p : Arg × Option GF) : Option Icelandic.Case

The surface case of an argument bearing a function: its idiosyncratic case if it has one, else by default the nominative if no unmarked function outranks it and the accusative if one does, (61d).

Equations

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

theorem ZaenenMalingThrainsson1985.surfaceCase_lexical {r : List (Arg × Option GF)} {x : Arg} {g : GF} {c : Icelandic.Case} (h : x.lexicalCase = some c) : surfaceCase r (x, some g) = some c

Idiosyncratic case is preserved under passive and raising: an argument bearing a function surfaces in its idiosyncratic case.

def ZaenenMalingThrainsson1985.cases (r : List (Arg × Option GF)) : List Icelandic.Case

The case array: the subject's case and then the objects' in the order of their functions, the immediately postverbal NP the OBJ.

Equations

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

def ZaenenMalingThrainsson1985.arrays (t : List Arg) (v : Voice) : List (List Icelandic.Case)

The case arrays a thematic structure yields in a voice, one per association.

Equations

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

def ZaenenMalingThrainsson1985.IsSubject (t : List Arg) (v : Voice) (ρ : Role) : Prop

The argument with a role bears SUBJ under some association in the voice.

Equations

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

@[instance_reducible]

instance ZaenenMalingThrainsson1985.instDecidableIsSubject (t : List Arg) (v : Voice) (ρ : Role) : Decidable (IsSubject t v ρ)

Equations

• ZaenenMalingThrainsson1985.instDecidableIsSubject t v ρ = ZaenenMalingThrainsson1985.instDecidableIsSubject._aux_1 t v ρ

The verbs

The thematic structures of the paper's verbs: (58), (60), (63), (67), (76) and Table I.

def ZaenenMalingThrainsson1985.Thematic.dansa : List Arg

Equations

• ZaenenMalingThrainsson1985.Thematic.dansa = [{ role := ZaenenMalingThrainsson1985.Role.agent }]

def ZaenenMalingThrainsson1985.Thematic.kyssa : List Arg

Equations

• ZaenenMalingThrainsson1985.Thematic.kyssa = [{ role := ZaenenMalingThrainsson1985.Role.agent }, { role := ZaenenMalingThrainsson1985.Role.theme }]

def ZaenenMalingThrainsson1985.Thematic.hjalpa : List Arg

Equations

• ZaenenMalingThrainsson1985.Thematic.hjalpa = [{ role := ZaenenMalingThrainsson1985.Role.agent }, { role := ZaenenMalingThrainsson1985.Role.theme, lexicalCase := some Icelandic.Case.dat }]

def ZaenenMalingThrainsson1985.Thematic.sakna : List Arg

Equations

• ZaenenMalingThrainsson1985.Thematic.sakna = [{ role := ZaenenMalingThrainsson1985.Role.experiencer }, { role := ZaenenMalingThrainsson1985.Role.theme, lexicalCase := some Icelandic.Case.gen }]

def ZaenenMalingThrainsson1985.Thematic.thykja : List Arg

Equations

• ZaenenMalingThrainsson1985.Thematic.thykja = [{ role := ZaenenMalingThrainsson1985.Role.experiencer, lexicalCase := some Icelandic.Case.dat }, { role := ZaenenMalingThrainsson1985.Role.theme }]

def ZaenenMalingThrainsson1985.Thematic.vanta : List Arg

Equations

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

def ZaenenMalingThrainsson1985.Thematic.gefa : List Arg

Equations

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

def ZaenenMalingThrainsson1985.Thematic.leyna : List Arg

Equations

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

def ZaenenMalingThrainsson1985.Thematic.bidja : List Arg

Equations

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

def ZaenenMalingThrainsson1985.Thematic.lofa : List Arg

Equations

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

def ZaenenMalingThrainsson1985.Thematic.oska : List Arg

Equations

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

def ZaenenMalingThrainsson1985.Thematic.oskaTransitive : List Arg

óska as a simple transitive, its goal absent, (67).

Equations

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

def ZaenenMalingThrainsson1985.entries : List (List Arg × Icelandic.Verbs.Verb)

The paper's verbs with the fragment entries they realize.

Equations

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

theorem ZaenenMalingThrainsson1985.fragment_cases (e : List Arg × Icelandic.Verbs.Verb) : e ∈ entries → e.2.cases ∈ arrays e.1 Voice.active

Every case array of the fragment is derived from its thematic structure.

theorem ZaenenMalingThrainsson1985.thykja_arrays : arrays Thematic.thykja Voice.active = [[Icelandic.Case.dat, Icelandic.Case.nom]]

A dative experiencer subject leaves the nominative to the theme, (62b).

theorem ZaenenMalingThrainsson1985.hjalpa_passive : arrays Thematic.hjalpa Voice.passive = [[Icelandic.Case.dat]]

The passive of hjálpa has a dative subject and no nominative, (11a).

theorem ZaenenMalingThrainsson1985.gefa_passives : have ps := arrays Thematic.gefa Voice.passive; [Icelandic.Case.dat, Icelandic.Case.nom] ∈ ps ∧ [Icelandic.Case.nom, Icelandic.Case.dat] ∈ ps ∧ ps.length = 2

A dative–accusative verb has two passives: the goal as dative subject with the theme a nominative retained object, and the theme as nominative subject, (44).

theorem ZaenenMalingThrainsson1985.lofa_passive : arrays Thematic.lofa Voice.passive = [[Icelandic.Case.dat, Icelandic.Case.dat]]

A dative–dative verb has one passive, its goal the subject, (42).

theorem ZaenenMalingThrainsson1985.oska_passive : IsSubject Thematic.oskaTransitive Voice.passive Role.theme ∧ ¬IsSubject Thematic.oska Voice.passive Role.theme

The genitive theme of óska passivizes as the only object and not beside a goal, (68).

theorem ZaenenMalingThrainsson1985.dansa_passive : arrays Thematic.dansa Voice.passive = [[]]

The impersonal passive of an intransitive has no NP, (9a).

The rows

def ZaenenMalingThrainsson1985.verbTable : List (String × List Arg)

The verbs as the rows name them.

Equations

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

def ZaenenMalingThrainsson1985.voiceTable : List (String × Voice)

The voices as the rows name them.

Equations

• ZaenenMalingThrainsson1985.voiceTable = [("active", ZaenenMalingThrainsson1985.Voice.active), ("passive", ZaenenMalingThrainsson1985.Voice.passive)]

def ZaenenMalingThrainsson1985.roleTable : List (String × Role)

The roles as the rows name them.

Equations

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

def ZaenenMalingThrainsson1985.casesTable : List (String × List Icelandic.Case)

The case arrays as the rows write them.

Equations

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

def ZaenenMalingThrainsson1985.ofCasesRow (ex : Datum) : Option (List Arg × Voice × List Icelandic.Case)

A row attesting a case array, as the thematic structure, the voice and the array.

Equations

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

def ZaenenMalingThrainsson1985.ofTestRow (ex : Datum) : Option (List Arg × Voice × Role)

A row applying a subjecthood test to an argument, as the thematic structure, the voice and the role tested.

Equations

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

theorem ZaenenMalingThrainsson1985.ofCasesRow_isSome (ex : Datum) : ex ∈ Examples.all → (ex.feature? "cases").isSome = true → (ofCasesRow ex).isSome = true

theorem ZaenenMalingThrainsson1985.ofTestRow_isSome (ex : Datum) : ex ∈ Examples.all → (ex.feature? "tested").isSome = true → (ofTestRow ex).isSome = true

theorem ZaenenMalingThrainsson1985.rows_cases (ex : Datum) : ex ∈ Examples.all → ∀ r ∈ ofCasesRow ex, r.2.2 ∈ arrays r.1 r.2.1

Every case array the paper attests, active or passive, is one the principles derive.

theorem ZaenenMalingThrainsson1985.rows_subject (ex : Datum) : ex ∈ Examples.all → ∀ r ∈ ofTestRow ex, ex.judgment = Judgment.acceptable ↔ IsSubject r.1 r.2.1 r.2.2

The subjecthood tests target SUBJ: the paper's judgment is acceptable exactly when the argument tested bears SUBJ under some association in that voice.