Case assignment

import Linglib.Syntax.Case.Assignment

The state of a derivation gives each nominal the slot of its case: unvalued until a value is assigned, valued once one is, and absent for a nominal that bears no case, such as PRO. A nominal is caseless when its slot has no value, so PRO is caseless and competes for dependent case without receiving one. A case rule says what an unvalued nominal takes, given how many caseless nominals of its domain stand above it and how many below, and a pass applies a rule across a domain at once. A rule's cells for one and two nominals are a marking of S, A and P, and on a chain the values of a pass are a case array. A pass extends the state, so it is inflationary, but it is not monotone: valuing one nominal can bleed the case of another, so no order-theoretic closure applies.

Implementation notes

The nominals are a type ι, whatever identifies them in a study: positions Fin n, labels, or the tokens of a tree. What stands above what is a relation the study supplies: c-command in a tree, the hierarchy of functions in a lexical account. It is not an LT instance because a grammar may vary it domain by domain. A domain is a Finset, so restricting a pass to what a rule sees is restricting the domain. The values are of any type, since a language's cases are its own categories.

References

Marantz 1991, Case and Licensing formalized
Zaenen et al. 1985, Case and Grammatical Functions: The Icelandic Passive formalized
Kalin 2018, Licensing and Differential Object Marking: The View from Neo-Aramaic formalized

What valued a case

L53–64

L68–71

L73–75

The state

t extends s by values in S: each slot is as in s, or was unvalued there and is valued in t with a value in S.

def FeatureSlot.Extends L108–111

{ι : Type u_1} {κ : Type u_2} (S : Set κ) (s t : ι → FeatureSlot κ) :

Prop

FeatureSlot.Extends S s t = ∀ (x : ι), s x = t x ∨ s x = FeatureSlot.unvalued ∧ ∃ v ∈ S, t x = FeatureSlot.valued v

Used by FeatureSlot.Extends.refl, FeatureSlot.Extends.mono, FeatureSlot.Extends.trans, FeatureSlot.Extends.le, FeatureSlot.Extends.eq_absent_iff, FeatureSlot.Extends.valued, FeatureSlot.Extends.unvalued, FeatureSlot.Extends.of_valued, FeatureSlot.Extends.foldl, CaseRule.extends_pass, CaseRule.extends_passUnvalued, CaseRule.extends_inOrder

Used in Syntax/Case/Dependent, Syntax/Minimalist/Case/Assignment, Kalin2018, ZaenenMalingThrainsson1985

Case rules

L169–171

L179–180

L182–184

The marking a rule gives the core roles, three of its cells: S alone in its domain, and A above P in theirs.

def CaseRule.marking L186–192

{κ : Type u_2} (r : CaseRule κ) :

ArgumentRole → Option κ

Built from

Used in Syntax/Case/Dependent

L194–197

A pass of the rule r over the domain D, lt y x saying that y stands above x: each unvalued nominal of D takes what r says of the caseless nominals of D above and below it, all of them at once.

def CaseRule.pass L203–209

{ι : Type u_1} {κ : Type u_2} [DecidableEq ι] (lt : ι → ι → Prop) [DecidableRel lt] (r : CaseRule κ) (D : Finset ι) (s : ι → FeatureSlot κ) :

ι → FeatureSlot κ

The definition is too large to print here; read it in the source.

Built from

Used by CaseRule.passUnvalued, CaseRule.pass_of_mem, CaseRule.pass_of_notMem, CaseRule.pass_of_ne_unvalued, CaseRule.pass_of_forall_eq_none, CaseRule.extends_pass, CaseRule.le_pass, CaseRule.map_pass, CaseRule.not_monotone_pass

Used in Syntax/Case/Dependent, Marantz1991, Poole2024

Chains

L277–295

L297–316

L318–324

On a chain, the values of a pass over the unvalued nominals are the rule's case array.

theorem CaseRule.map_value?_passUnvalued L326–332

{ι : Type u_1} {κ : Type u_2} {D : Finset ι} {s : ι → FeatureSlot κ} [DecidableEq ι] {lt : ι → ι → Prop} [DecidableRel lt] [Std.Asymm lt] (r : CaseRule κ) {G : List ι} (hG : List.Pairwise lt G) (hD : FeatureSlot.unvaluedIn D s = G.toFinset) :

List.map (fun (x : ι) => (passUnvalued lt r D s x).value?) G = r.caseArray G.length

Built from , , ,

A pass is not monotone in the state whenever the rule offers something to a nominal with a caseless nominal above it that it does not offer one alone: valuing the higher nominal bleeds the lower one's case.

theorem CaseRule.not_monotone_pass L336–365

{κ : Type u_2} {r : CaseRule κ} {c : κ} (h₁ : r 1 0 = some c) (h₀ : r 0 0 = none) :

¬Monotone (pass (fun (x1 x2 : Fin 2) => x1 < x2) r Finset.univ)

Built from ,