Priority records and their stabilization

A priority construction keeps, at each stage, a finite list of records indexed by priority, with smaller index meaning higher priority. When requirement e receives attention it installs a new record at position e and resets every record of lower priority: the list is truncated after position e. This is the initialization of lower-priority requirements. It is bookkeeping about records only; whether a reset is accompanied by an injury, an entry into a protected oracle interval, is a separate question that this file does not address.

The update is guarded: attention at a priority beyond the end of the list leaves the records unchanged. Without the guard, truncating and appending would place the new record at the end of the list, a position of higher priority than the attending requirement.

Main definitions

• TauCeti.Priority.Update: a priority together with the record to install there.
• TauCeti.Priority.Update.apply: the guarded update of a list of records.
• TauCeti.Priority.run: the records after n stages of a schedule of updates.
• TauCeti.Priority.attentionStages: for a priority schedule ℕ → Option ℕ, the run indices s + 1 after which an update of priority e, scheduled at stage s, has been applied.

Main results

• TauCeti.Priority.Update.getElem?_apply_of_lt: locality. An update at priority e leaves every record of strictly higher priority unchanged.
• TauCeti.Priority.Update.getElem?_apply_of_gt: after an update, no record of strictly lower priority remains.
• TauCeti.Priority.disjoint_attentionStages: distinct requirements have disjoint attention stages.
• TauCeti.Priority.finite_attentionStages_of_local: if each requirement receives attention finitely often whenever every higher-priority requirement does, then every requirement receives attention finitely often.
• TauCeti.Priority.exists_forall_getElem?_run_eq_of_finite: if requirements 0, …, e each receive attention finitely often, the record at position e eventually stops changing.
• TauCeti.Priority.exists_forall_getElem?_run_eq_of_local: under the conditional local finiteness hypothesis, every record eventually stops changing.

The stabilization theorem assumes only the conditional local finiteness of attention: no scheduling discipline, no bound on how often a requirement receives attention, and no effective stabilization stage. Stabilization of a record is not satisfaction of its requirement.

References

• R. I. Soare, Recursively Enumerable Sets and Degrees, Springer, 1987, Chapter VII.
• Ported from cameronfreer/computable-model-theory at commit a1fe76155a98f03933f7de0811e03b2473dd2e21: ComputableModelTheory/Computability/FiniteInjury.lean and its audit FiniteInjuryAudit.lean.
• Divergences from that source: records are a plain List rather than a wrapper structure; truncation of lower-priority records is called a reset (initialization), not an injury; attention is counted by the sets attentionStages of a priority schedule ℕ → Option ℕ, and local finiteness is stated as finiteness of these sets; the separate goodness predicate is not included.

structure TauCeti.Priority.Update (α : Type u_2) : Type u_2

An update: install value at priority prio, resetting every record of strictly lower priority.

• prio : ℕ

  The priority receiving attention.

• value : α

  The record installed at that priority.

def TauCeti.Priority.Update.apply {α : Type u_1} (u : Update α) (s : List α) : List α

The guarded update. In range, keep the records of higher priority, install the new record, and reset the rest; out of range, change nothing.

theorem TauCeti.Priority.Update.apply_of_le {α : Type u_1} {u : Update α} {s : List α} (h : u.prio ≤ s.length) : u.apply s = List.take u.prio s ++ [u.value]

In range, an update keeps the records of higher priority and installs the new record last.

@[simp]

theorem TauCeti.Priority.Update.apply_of_lt {α : Type u_1} {u : Update α} {s : List α} (h : s.length < u.prio) : u.apply s = s

Out of range, an update changes nothing.

@[simp]

theorem TauCeti.Priority.Update.getElem?_apply_of_lt {α : Type u_1} (u : Update α) (s : List α) {i : ℕ} (h : i < u.prio) : (u.apply s)[i]? = s[i]?

Locality. An update at priority e leaves every record of strictly higher priority unchanged.

@[simp]

theorem TauCeti.Priority.Update.getElem?_apply_self {α : Type u_1} {u : Update α} {s : List α} (h : u.prio ≤ s.length) : (u.apply s)[u.prio]? = some u.value

An update in range installs its record at its own priority.

@[simp]

theorem TauCeti.Priority.Update.getElem?_apply_of_gt {α : Type u_1} {u : Update α} {s : List α} {i : ℕ} (hi : u.prio < i) : (u.apply s)[i]? = none

Reset. After an update, no record of strictly lower priority remains: in range they are reset, and out of range there were none.

@[simp]

theorem TauCeti.Priority.Update.take_apply_of_le {α : Type u_1} (u : Update α) (s : List α) {n : ℕ} (h : n ≤ u.prio) : List.take n (u.apply s) = List.take n s

An update at priority e keeps the first n ≤ e records.

Runs

def TauCeti.Priority.run {α : Type u_1} (sched : ℕ → Option (Update α)) (init : List α) : ℕ → List α

The records after n stages: starting from init, at each stage s < n the update sched s scheduled at that stage, if any, is applied.

@[simp]

theorem TauCeti.Priority.run_zero {α : Type u_1} (sched : ℕ → Option (Update α)) (init : List α) : run sched init 0 = init

A run starts at the initial records.

theorem TauCeti.Priority.run_succ {α : Type u_1} (sched : ℕ → Option (Update α)) (init : List α) (n : ℕ) : run sched init (n + 1) = (sched n).elim (run sched init n) fun (u : Update α) => u.apply (run sched init n)

A run applies the update scheduled at stage n, if any, to the records after n stages.

@[simp]

theorem TauCeti.Priority.run_succ_of_eq_none {α : Type u_1} {sched : ℕ → Option (Update α)} {init : List α} {n : ℕ} (h : sched n = none) : run sched init (n + 1) = run sched init n

A stage with no scheduled update leaves the records unchanged.

@[simp]

theorem TauCeti.Priority.run_succ_of_eq_some {α : Type u_1} {sched : ℕ → Option (Update α)} {init : List α} {n : ℕ} {u : Update α} (h : sched n = some u) : run sched init (n + 1) = u.apply (run sched init n)

A stage with a scheduled update applies it.

Attention and stabilization

A priority schedule action : ℕ → Option ℕ records which requirement, if any, receives attention at each stage. The update scheduled at stage s has been applied in the records run sched init (s + 1), so attention is counted by these run indices s + 1. A schedule of updates gives the priority schedule fun s => (sched s).map Update.prio.

def TauCeti.Priority.attentionStages (action : ℕ → Option ℕ) (e : ℕ) : Set ℕ

The run indices s + 1 after which an update of priority e, scheduled at stage s, has been applied.

@[simp]

theorem TauCeti.Priority.mem_attentionStages {action : ℕ → Option ℕ} {e t : ℕ} : t ∈ attentionStages action e ↔ ∃ (s : ℕ), t = s + 1 ∧ action s = some e

Membership in attentionStages.

theorem TauCeti.Priority.disjoint_attentionStages {action : ℕ → Option ℕ} {d e : ℕ} (h : d ≠ e) : Disjoint (attentionStages action d) (attentionStages action e)

Distinct requirements have disjoint attention stages.

theorem TauCeti.Priority.finite_attentionStages_of_local (action : ℕ → Option ℕ) (hlocal : ∀ (e : ℕ), (∀ i < e, (attentionStages action i).Finite) → (attentionStages action e).Finite) (e : ℕ) : (attentionStages action e).Finite

Priority induction. If each requirement receives attention finitely often whenever every higher-priority requirement does, then every requirement receives attention finitely often.

theorem TauCeti.Priority.exists_forall_lt_of_finite {action : ℕ → Option ℕ} {e : ℕ} (h : ∀ i ≤ e, (attentionStages action i).Finite) : ∃ (N : ℕ), ∀ (s : ℕ), N ≤ s → ∀ (i : ℕ), action s = some i → e < i

If requirements 0, …, e each receive attention finitely often, then from some stage on every requirement receiving attention has priority beyond e.

theorem TauCeti.Priority.getElem?_run_eq_of_forall_lt_prio {α : Type u_1} {sched : ℕ → Option (Update α)} {init : List α} {e N : ℕ} (h : ∀ (s : ℕ), N ≤ s → ∀ (u : Update α), sched s = some u → e < u.prio) {n : ℕ} (hn : N ≤ n) : (run sched init n)[e]? = (run sched init N)[e]?

From a stage after which only updates of priority beyond e are scheduled, the record at position e never changes.

theorem TauCeti.Priority.exists_forall_getElem?_run_eq_of_finite {α : Type u_1} {sched : ℕ → Option (Update α)} {init : List α} {e : ℕ} (h : ∀ i ≤ e, (attentionStages (fun (s : ℕ) => Option.map Update.prio (sched s)) i).Finite) : ∃ (N : ℕ), ∀ (n : ℕ), N ≤ n → (run sched init n)[e]? = (run sched init N)[e]?

Stabilization of one record. If requirements 0, …, e each receive attention finitely often, then the record at position e eventually stops changing.

theorem TauCeti.Priority.exists_forall_getElem?_run_eq_of_local {α : Type u_1} (sched : ℕ → Option (Update α)) (init : List α) (hlocal : ∀ (e : ℕ), (∀ i < e, (attentionStages (fun (s : ℕ) => Option.map Update.prio (sched s)) i).Finite) → (attentionStages (fun (s : ℕ) => Option.map Update.prio (sched s)) e).Finite) (e : ℕ) : ∃ (N : ℕ), ∀ (n : ℕ), N ≤ n → (run sched init n)[e]? = (run sched init N)[e]?

Stabilization. If each requirement receives attention finitely often whenever every higher-priority requirement does, then every record eventually stops changing.