pith. machine review for the scientific record. sign in
structure definition def or abbrev

TuringModel

show as:
view Lean formalization →

No prose has been written for this declaration yet. The Lean source and graph data below render without it.

generate prose now

formal statement (Lean)

  67structure TuringModel where
  68  /-- Turing time complexity -/
  69  T : ℕ → ℕ
  70  /-- Recognition complexity is zero in the Turing model. -/
  71  recognition_complexity : ℕ → ℕ
  72  recognition_free : ∀ n, recognition_complexity n = 0
  73
  74/-- Ledger-based computational model with explicit observation cost -/
  75

used by (2)

From the project-wide theorem graph. These declarations reference this one in their body.

depends on (9)

Lean names referenced from this declaration's body.