Computable functions and decidable sets

A function is computable (Turing.MultiTapeTM.IsComputable) when it is computable within some bounds in the sense of cslib's Turing.MultiTapeTM.ComputableInTimeAndSpace: some machine with a binary alphabet and finitely many states halts on every encoded input with the encoded value. The bounds are arbitrary, so this is computability by a total machine (Turing.MultiTapeTM.isComputable_iff). A set is decidable (Turing.MultiTapeTM.IsDecidable) when it is decidable within some bounds in the sense of Turing.MultiTapeTM.DecidableInTimeAndSpace, that is, when its Boolean indicator is computable.

Computable functions compose (Turing.MultiTapeTM.IsComputable.comp): both machines are first put into the tidy normal form (Turing.MultiTapeTM.ComputableInTimeAndSpace.exists_computableTidilyInTimeAndSpace), whose machines compose. Functions computable within bounds in the senses of Turing.MultiTapeTM.ComputableInTimeAndSpace, Turing.MultiTapeTM.ComputableTidilyInTimeAndSpace, Turing.MultiTapeTM.ComputableTidilyInO, Turing.MultiTapeTM.ComputableTidilyInDegree and Turing.MultiTapeTM.ComputableTidilyInPolyTime are computable (their .isComputable lemmas), and decidable sets are closed under complement.

These are the decidable sets of Sipser, Definition 3.6, for the library's native multi-tape machines. Mathlib's ComputablePred is the analogous notion for its partial recursive functions; Turing.MultiTapeTM.IsComputable.computable and Turing.MultiTapeTM.IsDecidable.computablePred in MultiTape.Halting.Partrec connect the two models.

Main definitions

• Turing.MultiTapeTM.IsComputable: computability by a total machine.
• Turing.MultiTapeTM.IsDecidable: decidability by a total machine.

Main results

• Turing.MultiTapeTM.isComputable_iff: computability is the existence of a machine computing the function without bounds.
• Turing.MultiTapeTM.IsComputable.comp, .prod, Turing.MultiTapeTM.isComputable_id, Turing.MultiTapeTM.IsComputable.of_finite: closure properties.
• Turing.MultiTapeTM.isDecidable_iff: decidability through any computable Boolean function.
• Turing.MultiTapeTM.IsDecidable.compl: decidable sets are closed under complement.

References

• M. Sipser, Introduction to the Theory of Computation

Computable functions

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.

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

Functions tidily computable within bounds are computable.

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

Functions tidily computable up to constants are computable.

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

Functions tidily computable within bounds of given degrees are computable.

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

Functions tidily computable in polynomial time are computable.

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

A computable function is tidily computable within some bounds.

theorem Turing.MultiTapeTM.IsComputable.comp {α : Type u_1} {β : Type u_2} {γ : Type u_3} {encIn : α ↪ List Bool} {encMid : β ↪ List Bool} {encOut : γ ↪ List Bool} {f : β → γ} {g : α → β} (hf : IsComputable f encMid encOut) (hg : IsComputable g encIn encMid) : IsComputable (f ∘ g) encIn encOut

Computable functions compose.

theorem Turing.MultiTapeTM.isComputable_id {α : Type u_1} (enc : α ↪ List Bool) : IsComputable id enc enc

The identity is computable.

theorem Turing.MultiTapeTM.IsComputable.of_finite {α : Type u_1} {β : Type u_2} {encIn : α ↪ List Bool} {encMid : β ↪ List Bool} [Finite α] (f : α → β) : IsComputable f encIn encMid

Functions on finite types are computable.

theorem Turing.MultiTapeTM.IsComputable.prod {α β₁ β₂ : Type u} {encIn : α ↪ List Bool} {enc₁ : β₁ ↪ List Bool} {enc₂ : β₂ ↪ List Bool} {enc : β₁ × β₂ ↪ List Bool} [PairEncoding enc₁ enc₂ enc] {f : α → β₁} {g : α → β₂} (hf : IsComputable f encIn enc₁) (hg : IsComputable g encIn enc₂) : IsComputable (fun (a : α) => (f a, g a)) encIn enc

Pairs of computable functions are computable.

Decidable sets

def Turing.MultiTapeTM.IsDecidable {α : Type u_1} (L : Set α) (enc : α ↪ List Bool) : Prop

L is decidable with respect to the encoding enc: its Boolean indicator is computable, by a machine with a binary alphabet and finitely many states within some time and space bounds.

theorem Turing.MultiTapeTM.isDecidable_iff_isComputable_indicator {α : Type u_1} {L : Set α} {enc : α ↪ List Bool} : IsDecidable L enc ↔ IsComputable (indicator L) enc encBool

A set is decidable exactly when its Boolean indicator is computable.

theorem Turing.MultiTapeTM.isDecidable_iff {α : Type u_1} {L : Set α} {enc : α ↪ List Bool} : IsDecidable L enc ↔ ∃ (f : α → Bool), IsComputable f enc encBool ∧ ∀ (a : α), a ∈ L ↔ f a = true

A set is decidable exactly when some computable Boolean function decides membership.

theorem Turing.MultiTapeTM.IsDecidable.exists_isComputable {α : Type u_1} {L : Set α} {enc : α ↪ List Bool} (h : IsDecidable L enc) : ∃ (f : α → Bool), IsComputable f enc encBool ∧ ∀ (a : α), a ∈ L ↔ f a = true

Membership in a decidable set is decided by a computable Boolean function.

theorem Turing.MultiTapeTM.IsDecidable.compl {α : Type u_1} {L : Set α} {enc : α ↪ List Bool} (h : IsDecidable L enc) : IsDecidable Lᶜ enc

Decidable sets are closed under complement.

@[simp]

theorem Turing.MultiTapeTM.isDecidable_compl_iff {α : Type u_1} {L : Set α} {enc : α ↪ List Bool} : IsDecidable Lᶜ enc ↔ IsDecidable L enc