Control Diagnostics and Profiles

The observable diagnostic battery of control — the antecedence and reading tests every framework's account is answerable to. A Profile ι records which of an analysis's licensing clauses hold of a construction, over an arbitrary clause index ι; an Excludes ι instance says which clause's failure admits each diagnostic, and Profile.admits computes the admitted diagnostics as a preimage: admits is antitone, obligatory control is the empty fiber, non-obligatory control the full one, and the battery encodes the profile faithfully (Profile.admits_injective). 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.Profile: clause profiles over an index, with Profile.admits
• Control.Excludes: the clause each diagnostic is excluded by

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 ⋯

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

Equations

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

@[instance_reducible]

instance Control.instReprDiagnostic : Repr Diagnostic

Equations

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

@[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.

@[reducible, inline]

abbrev Control.Profile (ι : Type u_1) : Type u_1

A profile over an index of licensing clauses: which clauses hold of a construction.

Equations

• Control.Profile ι = (ι → Bool)

def Control.Profile.IsObligatory {ι : Type u_1} (p : Profile ι) : Prop

Obligatory control: every licensing clause holds.

Equations

• p.IsObligatory = ∀ (c : ι), p c = true

def Control.Profile.IsNonObligatory {ι : Type u_1} (p : Profile ι) : Prop

Non-obligatory control: no licensing clause holds.

Equations

• p.IsNonObligatory = ∀ (c : ι), ¬p c = true

@[instance_reducible]

instance Control.Profile.instDecidablePredIsObligatoryOfFintype {ι : Type u_1} [Fintype ι] : DecidablePred IsObligatory

Equations

• x✝.instDecidablePredIsObligatoryOfFintype = Control.Profile.instDecidablePredIsObligatoryOfFintype._aux_1 x✝

@[instance_reducible]

instance Control.Profile.instDecidablePredIsNonObligatoryOfFintype {ι : Type u_1} [Fintype ι] : DecidablePred IsNonObligatory

Equations

• x✝.instDecidablePredIsNonObligatoryOfFintype = Control.Profile.instDecidablePredIsNonObligatoryOfFintype._aux_1 x✝

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

The diagnostics a profile admits: those whose excluding clause fails.

Equations

• p.admits = Control.excludedBy ⁻¹' {c : ι | ¬p c = true}

@[instance_reducible]

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

Equations

• Control.Profile.instDecidablePredDiagnosticMemSetAdmits x✝ = Control.Profile.instDecidablePredDiagnosticMemSetAdmits._aux_1 x✝

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

The more clauses hold, the fewer diagnostics are admitted.

theorem Control.Profile.isObligatory_iff_admits_eq_empty {ι : Type u_1} [Excludes ι] {p : Profile ι} : p.IsObligatory ↔ p.admits = ∅

A profile is obligatory control iff it admits nothing.

theorem Control.Profile.isNonObligatory_iff_admits_eq_univ {ι : Type u_1} [Excludes ι] {p : Profile ι} : p.IsNonObligatory ↔ p.admits = Set.univ

A profile is non-obligatory control iff it admits everything.

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

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