Case assigners — one signature for comparing rival theories

[Mar91] [Kal18]

The rival accounts of case assignment (Dependent.lean, Licensing.lean) each run on their own input type and produce their own result type, so they cannot be applied to a common stimulus — which is exactly what comparing them requires. This file gives them one shared signature.

• The shared stimulus is List LicensedNP — the richest of the rivals' inputs (LicensedNP extends NPInDomain), so a configural account reads its NPInDomain projection and ignores needsLicensing, while a licensing account reads the whole thing.
• An Assigner maps that stimulus to a per-label Verdict (a surface case plus its neutral Case.Source provenance). This is the Predict-style function signature, not a typeclass: rivals are ordinary defs, so two accounts with the same input/output types coexist (which a typeclass could not host).
• AgreesOnCase / AgreesOnSource compare two accounts per projection. Divergence is the negation, witnessed by a stimulus — generalizing the agree_on_…/diverge_on_… pattern of Studies/Woolford1997.lean and Studies/Baker2015.lean.

The Chomskyan Case Filter (Syntax/Case/Filter.lean) is a checker, not an assigner, and is bridged separately. The paper-anchored dependent-case ⟺ licensing DOM divergence belongs in the later paper's study file (Studies/Kalin2018.lean); the examples here only validate that the harness is non-vacuous.

structure Syntax.Case.Verdict : Type

What a case account predicts for one nominal: its surface case (none exactly when the provenance is the crash uncased) and its neutral Case.Source provenance.

• source : Case.Source
• surfaceCase : Option Case

@[implicit_reducible]

instance Syntax.Case.instDecidableEqVerdict : DecidableEq Verdict

Equations

• Syntax.Case.instDecidableEqVerdict = Syntax.Case.instDecidableEqVerdict.decEq

def Syntax.Case.instDecidableEqVerdict.decEq (x✝ x✝¹ : Verdict) : Decidable (x✝ = x✝¹)

Equations

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

def Syntax.Case.instReprVerdict.repr : Verdict → ℕ → Std.Format

Equations

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

@[implicit_reducible]

instance Syntax.Case.instReprVerdict : Repr Verdict

Equations

• Syntax.Case.instReprVerdict = { reprPrec := Syntax.Case.instReprVerdict.repr }

@[reducible, inline]

abbrev Syntax.Case.Assigner : Type

A case-assignment account as a function from the shared stimulus to a per-label verdict (none = no nominal with that label). The signature that makes rival theories runnable on one input.

Equations

• Syntax.Case.Assigner = (List Syntax.Case.Licensing.LicensedNP → String → Option Syntax.Case.Verdict)

def Syntax.Case.dependentAssigner (lang : CaseLanguageType) : Assigner

Marantz dependent case as an Assigner: it reads the configural projection (needsLicensing ignored) and is total, so it never produces the crash uncased.

Equations

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

def Syntax.Case.kalinAssigner (cl : Licensing.ClauseLicensers) : Assigner

Kalin hybrid licensing as an Assigner: an unlicensed nominal crashes to ⟨uncased, none⟩.

Equations

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

def Syntax.Case.AgreesOnCase (a b : Assigner) (nps : List Licensing.LicensedNP) : Prop

Two accounts agree on the surface case of every nominal in the stimulus.

Equations

• Syntax.Case.AgreesOnCase a b nps = ∀ np ∈ nps, Option.map Syntax.Case.Verdict.surfaceCase (a nps np.label) = Option.map Syntax.Case.Verdict.surfaceCase (b nps np.label)

def Syntax.Case.AgreesOnSource (a b : Assigner) (nps : List Licensing.LicensedNP) : Prop

Two accounts agree on the provenance of every nominal in the stimulus. Two accounts can agree on case yet diverge here.

Equations

• Syntax.Case.AgreesOnSource a b nps = ∀ np ∈ nps, Option.map Syntax.Case.Verdict.source (a nps np.label) = Option.map Syntax.Case.Verdict.source (b nps np.label)

@[implicit_reducible]

instance Syntax.Case.instDecidableAgreesOnCase (a b : Assigner) (nps : List Licensing.LicensedNP) : Decidable (AgreesOnCase a b nps)

Equations

• Syntax.Case.instDecidableAgreesOnCase a b nps = id inferInstance

@[implicit_reducible]

instance Syntax.Case.instDecidableAgreesOnSource (a b : Assigner) (nps : List Licensing.LicensedNP) : Decidable (AgreesOnSource a b nps)

Equations

• Syntax.Case.instDecidableAgreesOnSource a b nps = id inferInstance

Non-vacuity: the harness on a transitive clause

A [subj, obj] transitive (both nominals active, no lexical case) in an accusative language with a Turkish-style primary-T / secondary-AGRO clause. Dependent case and hybrid licensing agree on the surface case (subj NOM, obj ACC) but diverge on the provenance of the subject — dependent case calls it default (unmarked last resort), licensing calls it structural (valued by primary T). The shape of the eventual Studies/Kalin2018.lean divergence, here only to confirm the harness is not vacuous.