Termination

Difficulty: moderate — 3 definitions, 0 abbreviations, 2 lemmas, 5 theorems, 0 examples.

definition lemma theorem
legend

A relation on a universe may be read as a machine: from \(a\) it moves to any \(v\) related to it. Two questions about such a machine are worth keeping apart. Does every run from \(a\) come to a stop, and does every run from \(a\) stay within finitely many elements?

Stopping is the stronger of the two. A run that comes to a stop visits finitely many elements, so halting implies termination whenever each element has at most one move. Termination is the weaker reading, and it is the useful one for a model of arithmetic: a run that circles forever through a handful of elements terminates in this sense while it never stops.

Inside a model, termination is bounded growth. What a run reaches stays below some element exactly when it is finite in number, since everything up to an element is finite and a finite orbit has a greatest element. So a measure that never grows already gives termination, and a measure that strictly shrinks gives the stronger halting.

The relation \(R\) halts at \(a\): every run from \(a\) comes to a stop.

halting
def Structure.Arithmetic.Halts.{u_1} {L : Type u_1} (R : L → L → Prop) (a : L) : Prop
Show details 
| Structure.Arithmetic.Halts R a = Acc (fun x y => R y x) a

Complexity: 25 (size of the value term)

Outer dependencies: (none)

Lean core dependencies: Acc

Used by: Structure.Arithmetic.halts_of_measure, Structure.Arithmetic.terminates_of_halts

What \(a\) reaches by \(R\), in zero or more moves.

def Structure.Arithmetic.Orbit.{u_1} {L : Type u_1} (R : L → L → Prop) (a : L) : Set L
Show details 
| Structure.Arithmetic.Orbit R a = {v | Relation.ReflTransGen R a v}

Complexity: 25 (size of the value term)

Outer dependencies: (none)

Mathlib dependencies: Relation.ReflTransGen, Set, setOf

Used by: Structure.Arithmetic.Terminates, Structure.Arithmetic.orbit_le, Structure.Arithmetic.orbit_subset, Structure.Arithmetic.terminates_iff_bounded, Structure.Arithmetic.terminates_of_finite, Structure.Arithmetic.terminates_of_halts, Structure.Arithmetic.terminates_of_le

The relation \(R\) terminates at \(a\): only finitely many elements are reached from \(a\), so a run either stops or circles.

termination
def Structure.Arithmetic.Terminates.{u_1} {L : Type u_1} (R : L → L → Prop) (a : L) : Prop
Show details 
| Structure.Arithmetic.Terminates R a = (Structure.Arithmetic.Orbit R a).Finite

Complexity: 21 (size of the value term)

Outer dependencies: (none)

Inner dependencies: Structure.Arithmetic.Orbit

Mathlib dependencies: Set.Finite

Used by: Structure.Arithmetic.terminates_iff_bounded, Structure.Arithmetic.terminates_of_finite, Structure.Arithmetic.terminates_of_halts, Structure.Arithmetic.terminates_of_le

Where each element has at most one move, what a successor reaches is all that is reached, apart from the starting point.

theorem Structure.Arithmetic.orbit_subset.{u_1} {L : Type u_1} {R : L → L → Prop}
  [Structure.Arithmetic.Univalent R] {a v : L} (h : R a v) :
  Structure.Arithmetic.Orbit R a ⊆ insert a (Structure.Arithmetic.Orbit R v)
Show details 
fun {L} {R} [Structure.Arithmetic.Univalent R] {a v} h ⦃x⦄ hx =>
  Or.casesOn (Relation.ReflTransGen.cases_head hx)
    (fun h =>
      Eq.ndrec (motive := fun ⦃x⦄ =>
        x ∈ Structure.Arithmetic.Orbit R a → x ∈ insert a (Structure.Arithmetic.Orbit R v))
        (fun hx => Set.mem_insert a (Structure.Arithmetic.Orbit R v)) h hx)
    fun h_1 =>
    Exists.casesOn h_1 fun b h_2 =>
      And.casesOn h_2 fun hb hbx =>
        Set.mem_insert_of_mem a
          (Eq.mp
            (congrArg (fun _a => Relation.ReflTransGen R _a x)
              (Structure.Arithmetic.Univalent.uniq a b v hb h))
            hbx)

Complexity: 583 (size of the value term)

Dependencies: Structure.Arithmetic.Orbit, Structure.Arithmetic.Univalent

Mathlib dependencies: Relation.ReflTransGen, Relation.ReflTransGen.cases_head, Set, Set.mem_insert, Set.mem_insert_of_mem

Lean core dependencies: And, Eq, Eq.mp, Exists, Or, congrArg

Used by: Structure.Arithmetic.terminates_of_halts

Halting is the stronger property: where each element has at most one move, a run that comes to a stop reaches finitely many elements.

theorem Structure.Arithmetic.terminates_of_halts.{u_1} {L : Type u_1} {R : L → L → Prop}
  [Structure.Arithmetic.Univalent R] {a : L} (h : Structure.Arithmetic.Halts R a) :
  Structure.Arithmetic.Terminates R a
Show details 
fun {L} {R} [Structure.Arithmetic.Univalent R] {a} h =>
  Acc.rec
    (fun a h ih =>
      if hex : ∃ v, R a v then
        Exists.casesOn hex fun v hv =>
          Set.Finite.subset (Set.Finite.insert a (ih v hv)) (Structure.Arithmetic.orbit_subset hv)
      else
        Set.Finite.subset (Set.finite_singleton a) fun x hx =>
          Or.casesOn (Relation.ReflTransGen.cases_head hx)
            (fun h =>
              Eq.ndrec (motive := fun x => x ∈ Structure.Arithmetic.Orbit R a → x ∈ {a})
                (fun hx => Eq.refl a) h hx)
            fun h =>
            Exists.casesOn h fun b h =>
              And.casesOn h fun hb right => absurd (Exists.intro b hb) hex)
    h

Complexity: 803 (size of the value term)

Dependencies: Structure.Arithmetic.Halts, Structure.Arithmetic.Terminates, Structure.Arithmetic.Univalent

Proof dependencies: Structure.Arithmetic.Orbit, Structure.Arithmetic.orbit_subset

Mathlib dependencies: Relation.ReflTransGen, Relation.ReflTransGen.cases_head, Set, Set.Finite.insert, Set.Finite.subset, Set.finite_singleton

Lean core dependencies: Acc, And, Eq, Exists, Not, Or, absurd, dite

Used by: (none)

A measure that never grows along \(R\) bounds what a run reaches.

theorem Structure.Arithmetic.orbit_le.{u_1, u_2} {L : Type u_1} {U : Type u_2}
  [Structure.Arithmetic.Arith U] {R : L → L → Prop} (μ : L → U) (h : ∀ (a v : L), R a v → μ v ≤ μ a)
  {a x : L} (hx : x ∈ Structure.Arithmetic.Orbit R a) : μ x ≤ μ a
Show details 
fun {L} {U} [Structure.Arithmetic.Arith U] {R} μ h {a x} hx =>
  Relation.ReflTransGen.rec le_rfl (fun {b c} a_1 hbv ih => LE.le.trans (h b c hbv) ih) hx

Complexity: 321 (size of the value term)

Dependencies: Structure.Arithmetic.Arith, Structure.Arithmetic.Orbit

Mathlib dependencies: Relation.ReflTransGen, Set, le_rfl

Used by: Structure.Arithmetic.terminates_of_le

On a model, a relation that never moves upwards terminates: what it reaches stays up to the starting point, and that is finite in number.

theorem Structure.Arithmetic.terminates_of_le.{u_2} {U : Type u_2} [Structure.Arithmetic.Arith U]
  {R : U → U → Prop} (h : ∀ (a v : U), R a v → v ≤ a) (a : U) : Structure.Arithmetic.Terminates R a
Show details 
fun {U} [Structure.Arithmetic.Arith U] {R} h a =>
  Set.Finite.subset (Structure.Arithmetic.Arith.reach a) fun x hx =>
    Structure.Arithmetic.orbit_le id h hx

Complexity: 147 (size of the value term)

Dependencies: Structure.Arithmetic.Arith, Structure.Arithmetic.Terminates

Proof dependencies: Structure.Arithmetic.Orbit, Structure.Arithmetic.orbit_le

Mathlib dependencies: Set, Set.Finite.subset, Set.Iic

Lean core dependencies: id

Used by: (none)

On a model, terminating is being bounded. What stays up to some element is finite in number, and a finite orbit has a greatest element to serve as a bound.

theorem Structure.Arithmetic.terminates_iff_bounded.{u_2} {U : Type u_2} [Structure.Arithmetic.Arith U]
  (R : U → U → Prop) (a : U) :
  Structure.Arithmetic.Terminates R a ↔ ∃ b, ∀ x ∈ Structure.Arithmetic.Orbit R a, x ≤ b
Show details 
fun {U} [Structure.Arithmetic.Arith U] R a =>
  {
    mp := fun h =>
      Exists.casesOn
        (Set.exists_max_image (Structure.Arithmetic.Orbit R a) id h
          (Exists.intro a Relation.ReflTransGen.refl))
        fun b h => And.casesOn h fun left hb => Exists.intro b hb,
    mpr := fun a_1 =>
      Exists.casesOn a_1 fun b hb => Set.Finite.subset (Structure.Arithmetic.Arith.reach b) hb }

Complexity: 1269 (size of the value term)

Dependencies: Structure.Arithmetic.Arith, Structure.Arithmetic.Orbit, Structure.Arithmetic.Terminates

Mathlib dependencies: Set, Set.Finite.subset, Set.Iic, Set.exists_max_image

Lean core dependencies: And, Exists, Iff, id

Used by: (none)

On a finite universe everything terminates.

theorem Structure.Arithmetic.terminates_of_finite.{u_1} {L : Type u_1} [Finite L] (R : L → L → Prop)
  (a : L) : Structure.Arithmetic.Terminates R a
Show details 
fun {L} [Finite L] R a => Set.toFinite (Structure.Arithmetic.Orbit R a)

Complexity: 51 (size of the value term)

Dependencies: Structure.Arithmetic.Terminates

Proof dependencies: Structure.Arithmetic.Orbit

Mathlib dependencies: Finite, Set, Set.toFinite

Used by: (none)

The general halting argument. A measure into a model of arithmetic that strictly shrinks along \(R\) makes every run stop, since the order of a model is well founded.

theorem Structure.Arithmetic.halts_of_measure.{u_1, u_2} {L : Type u_1} {U : Type u_2}
  [Structure.Arithmetic.Arith U] {R : L → L → Prop} (μ : L → U) (h : ∀ (a v : L), R a v → μ v < μ a)
  (a : L) : Structure.Arithmetic.Halts R a
Show details 
fun {L} {U} [Structure.Arithmetic.Arith U] {R} μ h a =>
  WellFounded.apply
    (Subrelation.wf (fun {x y} hxy => h y x hxy) (InvImage.wf μ Structure.Arithmetic.lt_wf)) a

Complexity: 213 (size of the value term)

Dependencies: Structure.Arithmetic.Arith, Structure.Arithmetic.Halts

Proof dependencies: Structure.Arithmetic.lt_wf

Lean core dependencies: InvImage.wf, Subrelation.wf, WellFounded.apply

Used by: (none)

Dependency diagram

Drag to pan, Ctrl+scroll (or Cmd+scroll, or pinch on a touch screen) to zoom, click a node to jump to it.

definitionlemmatheoremdeclared elsewheredependencyproof dependency
legend