Total native computability

The unbounded model and its witness characterization are moved unchanged from the higher halting calculus. This module imports only machine semantics, not a resource-calculus implementation.

def Turing.MultiTapeTM.IsComputable {α : Type u_1} {β : Type u_2} (f : α → β) (encIn : α ↪ List Bool) (encOut : β ↪ List Bool) : Prop

f is computable: some machine with a binary alphabet and finitely many states computes it with respect to the encodings encIn and encOut within some time and space bounds.

theorem Turing.MultiTapeTM.isComputable_iff {α : Type u_1} {β : Type u_2} {encIn : α ↪ List Bool} {encMid : β ↪ List Bool} {f : α → β} : IsComputable f encIn encMid ↔ ∃ (k : ℕ) (State : Type) (_ : Finite State) (tm : MultiTapeTM k Bool State), ∀ (a : α), tm.Computes (encIn a) (encMid (f a))

Computability is computability by a total machine: some machine with a binary alphabet and finitely many states halts on every encoded input with the encoded value.

theorem Turing.MultiTapeTM.ComputableInTimeAndSpace.isComputable {α : Type u_1} {β : Type u_2} {encIn : α ↪ List Bool} {encMid : β ↪ List Bool} {f : α → β} {t s : α → ℕ} (h : ComputableInTimeAndSpace f encIn encMid t s) : IsComputable f encIn encMid

Functions computable within bounds are computable.