Applicative diagnostics

@cite{pylkkanen-2008}

Cluster-based diagnostic classifier for the high/low applicative distinction (@cite{pylkkanen-2008}, Table 2.1). Three diagnostics:

1. Can unergative verbs be applicativized? (Ch. 2 §2.1.2)
2. Can static verbs be applicativized? (Ch. 2 §2.1.2)
3. If the language has English-style depictive secondary predicates, is the applied argument available for depictive modification? (Ch. 2 §2.1.3)

The diagnostic infrastructure lives in Theories/ because it is reusable: any applicative-typology paper using Pylkkänen's framework (Wood 2015, Bruening 2021, Cuervo 2003 extensions) consumes the same classifier. Per-paper instantiation lives in Studies files.

Cluster-based classification

A high applicative passes all tests; a low applicative fails all tests. Test 3 is conditional — when a language lacks English-style depictives (e.g., Korean) or has too-broad depictives (Venda, Albanian), the test is inapplicable (.inapplicable), not "fails." The classifier ignores inapplicable tests and classifies on the cluster of applicable ones.

This is stricter than an OR-based classifier (which would misclassify a language passing one test by accident). Languages that don't pattern cleanly with either cluster yield none, requiring further investigation rather than a forced classification.

inductive Minimalist.ApplDiagnosticResult : Type

The result of running a single Pylkkänen diagnostic on a language.

• passes : ApplDiagnosticResult

  The diagnostic is applicable and the language passes (the construction in question is grammatical).

• fails : ApplDiagnosticResult

  The diagnostic is applicable and the language fails (the construction is ungrammatical).

• inapplicable : ApplDiagnosticResult

  The diagnostic is inapplicable in this language — e.g., Korean lacks English-style depictives entirely, so Test 3 cannot be run. Distinct from .fails: an inapplicable test contributes no classification evidence.

@[implicit_reducible]

instance Minimalist.instDecidableEqApplDiagnosticResult : DecidableEq ApplDiagnosticResult

Equations

• Minimalist.instDecidableEqApplDiagnosticResult x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

@[implicit_reducible]

instance Minimalist.instReprApplDiagnosticResult : Repr ApplDiagnosticResult

Equations

• Minimalist.instReprApplDiagnosticResult = { reprPrec := Minimalist.instReprApplDiagnosticResult.repr }

def Minimalist.instReprApplDiagnosticResult.repr : ApplDiagnosticResult → ℕ → Std.Format

Equations

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

structure Minimalist.ApplDiagnosticBundle : Type

A bundle of Pylkkänen Table 2.1's three diagnostic results for a given language. Test 3's inapplicable value handles the language-conditional cases (Korean lacks depictives; Venda and Albanian have too-broad depictives to test).

• unergative : ApplDiagnosticResult

  Test 1: can unergative verbs be applicativized?

• staticVerb : ApplDiagnosticResult

  Test 2: can static verbs be applicativized?

• depictive : ApplDiagnosticResult

  Test 3: depictive modification of applied argument (conditional on language having English-style depictives).

@[implicit_reducible]

instance Minimalist.instReprApplDiagnosticBundle : Repr ApplDiagnosticBundle

Equations

• Minimalist.instReprApplDiagnosticBundle = { reprPrec := Minimalist.instReprApplDiagnosticBundle.repr }

def Minimalist.instReprApplDiagnosticBundle.repr : ApplDiagnosticBundle → ℕ → Std.Format

Equations

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

def Minimalist.ApplDiagnosticBundle.results (b : ApplDiagnosticBundle) : List ApplDiagnosticResult

The list of diagnostic results in a bundle, for cluster checks.

Equations

• b.results = [b.unergative, b.staticVerb, b.depictive]

def Minimalist.ApplDiagnosticBundle.applicableResults (b : ApplDiagnosticBundle) : List ApplDiagnosticResult

The applicable (non-.inapplicable) results in a bundle.

Equations

• b.applicableResults = List.filter (fun (x : Minimalist.ApplDiagnosticResult) => decide (x ≠ Minimalist.ApplDiagnosticResult.inapplicable)) b.results

def Minimalist.classifyByDiagnostics (b : ApplDiagnosticBundle) : Option ApplType

Cluster-based classification (@cite{pylkkanen-2008}, Table 2.1): a language has high applicatives iff every applicable diagnostic passes; low iff every applicable diagnostic fails; otherwise the pattern is mixed and the classifier returns none, requiring further investigation rather than forcing a classification.

Note: this returns Option ApplType collapsed to .high or .lowRecipient — distinguishing recipient from source low applicatives requires additional diagnostics (transfer directionality, §2.2 + §2.3) not in Table 2.1.

Equations

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

Soundness theorems

The classifier returns .high only on all-pass bundles, .lowRecipient only on all-fail bundles. Mixed bundles and empty/all-inapplicable bundles yield none. Soundness is checked structurally on the four canonical bundle shapes below.

theorem Minimalist.all_pass_classifies_high : classifyByDiagnostics { unergative := ApplDiagnosticResult.passes, staticVerb := ApplDiagnosticResult.passes, depictive := ApplDiagnosticResult.passes } = some ApplType.high

A bundle with all three results .passes classifies as high.

theorem Minimalist.all_fail_classifies_low : classifyByDiagnostics { unergative := ApplDiagnosticResult.fails, staticVerb := ApplDiagnosticResult.fails, depictive := ApplDiagnosticResult.fails } = some ApplType.lowRecipient

A bundle with all three results .fails classifies as low.

theorem Minimalist.mixed_does_not_classify : classifyByDiagnostics { unergative := ApplDiagnosticResult.passes, staticVerb := ApplDiagnosticResult.fails, depictive := ApplDiagnosticResult.fails } = none

A bundle with mixed results does not classify.

theorem Minimalist.all_inapplicable_does_not_classify : classifyByDiagnostics { unergative := ApplDiagnosticResult.inapplicable, staticVerb := ApplDiagnosticResult.inapplicable, depictive := ApplDiagnosticResult.inapplicable } = none

An all-inapplicable bundle does not classify.

theorem Minimalist.inapplicable_excluded : classifyByDiagnostics { unergative := ApplDiagnosticResult.passes, staticVerb := ApplDiagnosticResult.passes, depictive := ApplDiagnosticResult.inapplicable } = some ApplType.high

Inapplicable tests are excluded from the cluster: a bundle with one .inapplicable and two .passes still classifies as high.

theorem Minimalist.inapplicable_with_fails_classifies_low : classifyByDiagnostics { unergative := ApplDiagnosticResult.fails, staticVerb := ApplDiagnosticResult.fails, depictive := ApplDiagnosticResult.inapplicable } = some ApplType.lowRecipient

Inapplicable + all-fails still classifies as low.