Control Diagnostics and Profiles

The observable diagnostic battery of control — the antecedence and reading tests every framework's account is answerable to. A profile is the set of an analysis's licensing clauses that hold of a construction, over an arbitrary clause index ι; an Excludes ι instance says which clause's failure admits each diagnostic, and admits computes the admitted diagnostics as the preimage of the failing clauses: admits is antitone, obligatory control (every clause holds) is the empty fiber, non-obligatory control the full one, and the battery encodes the profile faithfully (admits_injective). ofAttested goes the other way, from the diagnostics a construction is observed to admit to the clauses none of them refutes. Which configurations admit which diagnostics varies by theory — [Lan13] (75)–(79) derives the five from the two clauses of its OC signature (Studies/Landau2013.lean).

Main definitions

• Control.Diagnostic: the observable battery
• Control.Excludes: the clause each diagnostic is excluded by
• Control.admits, Control.ofAttested: from a profile to its admitted diagnostics and back from attested diagnostics to a profile

inductive Control.Diagnostic : Type

The observable control diagnostics: the antecedence and reading tests any account of a control construction is answerable to.

• arbitraryControl : Diagnostic

  Arbitrary control: a free reading of the controlled element

• longDistanceControl : Diagnostic

  Long-distance control: a non-local antecedent

• nonCCommandingControl : Diagnostic

  A non-c-commanding antecedent

• strictEllipsis : Diagnostic

  A strict reading under VP-ellipsis

• strictUnderOnly : Diagnostic

  A strict (non-bound-variable) reading under only

@[instance_reducible]

instance Control.instDecidableEqDiagnostic : DecidableEq Diagnostic

Equations

• Control.instDecidableEqDiagnostic x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

@[instance_reducible]

instance Control.instReprDiagnostic : Repr Diagnostic

Equations

• Control.instReprDiagnostic = { reprPrec := Control.instReprDiagnostic.repr }

def Control.instReprDiagnostic.repr : Diagnostic → ℕ → Std.Format

Equations

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

@[instance_reducible]

instance Control.instFintypeDiagnostic : Fintype Diagnostic

Equations

• Control.instFintypeDiagnostic = { elems := { val := ↑Control.Diagnostic.enumList, nodup := Control.Diagnostic.enumList_nodup }, complete := Control.instFintypeDiagnostic._proof_1 }

class Control.Excludes (ι : Type u_1) : Type u_1

An index of licensing clauses, together with the clause whose failure admits each diagnostic. Surjectivity says every clause is witnessed by some diagnostic — what makes the battery a faithful encoding of the profile.

• excludedBy : Diagnostic → ι

  The clause whose failure admits each diagnostic.

• surjective : Function.Surjective excludedBy

  Every clause is witnessed by some diagnostic.

def Control.admits {ι : Type u_1} [Excludes ι] (p : Set ι) : Set Diagnostic

The diagnostics a profile — the set of clauses holding of a construction — admits: those whose excluding clause fails.

Equations

• Control.admits p = Control.excludedBy ⁻¹' pᶜ

@[instance_reducible]

instance Control.instDecidablePredDiagnosticMemSetAdmits {ι : Type u_1} [Excludes ι] {p : Set ι} [DecidablePred fun (x : ι) => x ∈ p] : DecidablePred fun (x : Diagnostic) => x ∈ admits p

Equations

• Control.instDecidablePredDiagnosticMemSetAdmits d = decidable_of_iff (Control.excludedBy d ∉ p) ⋯

theorem Control.admits_anti {ι : Type u_1} [Excludes ι] : Antitone admits

The more clauses hold, the fewer diagnostics are admitted.

theorem Control.admits_eq_empty_iff {ι : Type u_1} [Excludes ι] {p : Set ι} : admits p = ∅ ↔ p = Set.univ

Obligatory control, every clause holding, admits no diagnostic.

theorem Control.admits_eq_univ_iff {ι : Type u_1} [Excludes ι] {p : Set ι} : admits p = Set.univ ↔ p = ∅

Non-obligatory control, no clause holding, admits every diagnostic.

theorem Control.admits_injective {ι : Type u_1} [Excludes ι] : Function.Injective admits

The battery encodes the profile faithfully: distinct profiles admit distinct diagnostic sets.

def Control.ofAttested {ι : Type u_1} [Excludes ι] (A : Set Diagnostic) : Set ι

The profile a set of attested diagnostics determines: the clauses none of them refutes.

Equations

• Control.ofAttested A = (Control.excludedBy '' A)ᶜ

@[instance_reducible]

instance Control.instDecidablePredMemSetOfAttestedOfDecidableEqOfDiagnostic {ι : Type u_1} [Excludes ι] {A : Set Diagnostic} [DecidableEq ι] [DecidablePred fun (x : Diagnostic) => x ∈ A] : DecidablePred fun (x : ι) => x ∈ ofAttested A

Equations

• Control.instDecidablePredMemSetOfAttestedOfDecidableEqOfDiagnostic c = decidable_of_iff (∀ d ∈ A, Control.excludedBy d ≠ c) ⋯

theorem Control.subset_admits_ofAttested {ι : Type u_1} [Excludes ι] {A : Set Diagnostic} : A ⊆ admits (ofAttested A)

Attested diagnostics are admitted.

@[simp]

theorem Control.ofAttested_eq_univ_iff {ι : Type u_1} [Excludes ι] {A : Set Diagnostic} : ofAttested A = Set.univ ↔ A = ∅

With nothing attested every clause holds.