Diagnostic tests

A diagnostic is an abductive test for a latent classification C from an observed outcome Ω: each outcome is consistent with a set of latent values — the values that could have produced it. From that single datum everything else follows:

• the test is conclusive at an outcome when the consistent set is a Set.Subsingleton (it pins the latent value to at most one);
• it is sound against a ground-truth outcome model truth : C → Ω when the true value is always among the consistent ones (the test never rules out the truth);
• it decides C when, on every true value, the outcome's consistent set is exactly that value — sound and conclusive everywhere it matters;
• one test refines another when its consistent sets are pointwise smaller (it rules out at least as much), a preorder under which conclusiveness is monotone.

ofCauses builds a diagnostic from named causes (each entailing a latent value) — the faithful Hankamer–Sag picture, where a test outcome is explained by a set of causes and the consistent latent values are what those causes entail.

The structure is domain-general (any Ω, C); the anaphora specialisation (Anaphor.DepthCause, the ground-truth Depth.testOutcome) instantiates it for Hankamer & Sag depth, and the per-test instances (EIR, extraction) live in the paper that draws the comparison.

structure Diagnostic (Ω : Type u) (C : Type v) : Type (max u v)

An abductive diagnostic: each observed outcome o : Ω is consistent with the set consistent o of latent values in C that could have produced it.

• consistent : Ω → Set C

  The latent values consistent with an outcome (the verdict it licenses).

theorem Diagnostic.ext {Ω : Type u} {C : Type v} {x y : Diagnostic Ω C} (consistent : x.consistent = y.consistent) : x = y

theorem Diagnostic.ext_iff {Ω : Type u} {C : Type v} {x y : Diagnostic Ω C} : x = y ↔ x.consistent = y.consistent

def Diagnostic.IsConclusiveAt {Ω : Type u} {C : Type v} (t : Diagnostic Ω C) (o : Ω) : Prop

t is conclusive at o when the outcome pins the latent value to at most one possibility.

Equations

• t.IsConclusiveAt o = (t.consistent o).Subsingleton

def Diagnostic.Conclusive {Ω : Type u} {C : Type v} (t : Diagnostic Ω C) : Prop

t is conclusive when every outcome is.

Equations

• t.Conclusive = ∀ (o : Ω), t.IsConclusiveAt o

def Diagnostic.SoundFor {Ω : Type u} {C : Type v} (t : Diagnostic Ω C) (truth : C → Ω) : Prop

t is sound for a ground-truth outcome model truth : C → Ω when the true latent value is always among the explanations of the outcome it yields — the test never rules out the truth.

Equations

• t.SoundFor truth = ∀ (c : C), c ∈ t.consistent (truth c)

def Diagnostic.Decides {Ω : Type u} {C : Type v} (t : Diagnostic Ω C) (truth : C → Ω) : Prop

t decides C against truth when, on every true value, the outcome's consistent set is exactly that value: a sound, conclusive verdict everywhere it is exercised.

Equations

• t.Decides truth = ∀ (c : C), t.consistent (truth c) = {c}

def Diagnostic.Refines {Ω : Type u} {C : Type v} (t s : Diagnostic Ω C) : Prop

t refines s when every outcome's consistent set under t is contained in s's — t rules out at least as much. This is the pointwise-⊆ informativeness order on tests; a finer (more informative) test is ≤.

Equations

• t.Refines s = ∀ (o : Ω), t.consistent o ⊆ s.consistent o

theorem Diagnostic.Refines.refl {Ω : Type u} {C : Type v} (t : Diagnostic Ω C) : t.Refines t

theorem Diagnostic.Refines.trans {Ω : Type u} {C : Type v} {t s r : Diagnostic Ω C} (h₁ : t.Refines s) (h₂ : s.Refines r) : t.Refines r

@[implicit_reducible]

instance Diagnostic.instPreorder {Ω : Type u} {C : Type v} : Preorder (Diagnostic Ω C)

Tests are preordered by refinement: t ≤ s iff t.Refines s (t is finer, ruling out at least as much).

Equations

• Diagnostic.instPreorder = { le := Diagnostic.Refines, le_refl := ⋯, le_trans := ⋯, lt_iff_le_not_ge := ⋯ }

theorem Diagnostic.Conclusive.mono {Ω : Type u} {C : Type v} {t s : Diagnostic Ω C} (h : t.Refines s) (hs : s.Conclusive) : t.Conclusive

Refinement is monotone in conclusiveness: a refinement of a conclusive test is conclusive (a subset of a subsingleton is a subsingleton).

theorem Diagnostic.decides_iff {Ω : Type u} {C : Type v} {t : Diagnostic Ω C} {truth : C → Ω} : t.Decides truth ↔ t.SoundFor truth ∧ ∀ (c : C), t.IsConclusiveAt (truth c)

Deciding is exactly soundness plus conclusiveness on the truth outcomes.

theorem Diagnostic.Decides.soundFor {Ω : Type u} {C : Type v} {t : Diagnostic Ω C} {truth : C → Ω} (h : t.Decides truth) : t.SoundFor truth

A deciding test is sound.

Building a diagnostic from causes

def Diagnostic.ofCauses {Ω : Type u} {C : Type v} {γ : Type w} (causes : Ω → Set γ) (entails : γ → C) : Diagnostic Ω C

Build a diagnostic from named causes: each outcome is explained by a set of causes, and the consistent latent values are exactly what those causes entail (Set.image). The verdict is inconclusive at an outcome precisely when its causes entail more than one latent value — so ambiguity is derived from the cause structure, not stipulated.

Equations

• Diagnostic.ofCauses causes entails = { consistent := fun (o : Ω) => entails '' causes o }

@[simp]

theorem Diagnostic.ofCauses_consistent {Ω : Type u} {C : Type v} {γ : Type w} (causes : Ω → Set γ) (entails : γ → C) (o : Ω) : (ofCauses causes entails).consistent o = entails '' causes o

theorem Diagnostic.ofCauses_refines {Ω : Type u} {C : Type v} {γ : Type w} {c₁ c₂ : Ω → Set γ} (entails : γ → C) (h : ∀ (o : Ω), c₁ o ⊆ c₂ o) : (ofCauses c₁ entails).Refines (ofCauses c₂ entails)

Fewer causes ⇒ a refinement: shrinking the cause sets pointwise rules out at least as much.

Anaphoric-depth specialisation

The latent classification for an anaphora diagnostic is Anaphor.Depth; the causes are the Hankamer–Sag / Landau reasons a depth test can pass or fail.

inductive Anaphor.DepthCause : Type

The causes of a depth-test outcome ([HS76], [Lan26], the (42c)/(42d) "two reasons for the star" analysis): a site passes because it hostsVariable (has surface structure for the resumptive or trace); it fails because it is a deepAnaphor (no structure → (42d)), or — for movement-based tests only — because a surface site's dependency is derivationalBleeding (bled by ellipsis timing → (42c)) or islandBlocking (an inherent barrier; resumption is "indifferent to island constraints"). Only deepAnaphor entails deep; the surface-site confounds (derivationalBleeding/islandBlocking) entail surface. The asymmetry between EIR (failure = deepAnaphor only) and extraction (all three) is exactly which confounds each test admits.

• hostsVariable : DepthCause
• deepAnaphor : DepthCause
• derivationalBleeding : DepthCause
• islandBlocking : DepthCause

@[implicit_reducible]

instance Anaphor.instDecidableEqDepthCause : DecidableEq DepthCause

Equations

• Anaphor.instDecidableEqDepthCause x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

def Anaphor.instReprDepthCause.repr : DepthCause → ℕ → Std.Format

Equations

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

@[implicit_reducible]

instance Anaphor.instReprDepthCause : Repr DepthCause

Equations

• Anaphor.instReprDepthCause = { reprPrec := Anaphor.instReprDepthCause.repr }

def Anaphor.DepthCause.entails : DepthCause → Depth

The depth each cause entails.

Equations

• Anaphor.DepthCause.deepAnaphor.entails = Anaphor.Depth.deep
• x✝.entails = Anaphor.Depth.surface

def Anaphor.Depth.testOutcome : Depth → Bool

The ground-truth test outcome on a site of known depth: a surface anaphor passes (it has internal structure to host the variable/trace), a deep one fails. This is the truth model every depth diagnostic is judged against.

Equations

• Anaphor.Depth.surface.testOutcome = true
• Anaphor.Depth.deep.testOutcome = false