Documentation

Complexity.Computability.Machines.Turing.MultiTape.Halting.Reduction

Mapping reductions #

MappingReducible encA encB A B: a computable function (Turing.MultiTapeTM.IsComputable) with respect to the encodings encA and encB maps the instances of A to instances of B and the other instances to instances outside B Sipser, Definition 5.20. Mapping reducibility is a preorder, and decidability transfers backwards along reductions (Turing.MultiTapeTM.IsDecidable.of_mappingReducible), so undecidability transfers forwards (Turing.MultiTapeTM.MappingReducible.not_isDecidable).

A polynomial-time reduction (Cslib.Complexity.PolyTimeReducible) is a mapping reduction, its function being computable (Turing.MultiTapeTM.ComputableTidilyInPolyTime.isComputable). Mathlib's ManyOneReducible is the analogous notion for Mathlib's partial recursive functions on Primcodable types; Turing.MultiTapeTM.MappingReducible.manyOneReducible in MultiTape.Halting.Partrec connects the two notions.

Main definitions #

Main results #

References #

source
def Turing.MultiTapeTM.MappingReducible {α : Type u_1} {β : Type u_2} (encA : α ↪ List Bool) (encB : β ↪ List Bool) (A : Set α) (B : Set β) :
Prop

A is mapping reducible to B: some function f, computable with respect to encA and encB, satisfies a ∈ A ↔ f a ∈ B. This is ManyOneReducibleBy for the computable maps (mappingReducible_iff_manyOneReducibleBy).

Instances For
    source
    theorem Turing.MultiTapeTM.mappingReducible_iff_manyOneReducibleBy {α : Type u_1} {β : Type u_2} {encA : α ↪ List Bool} {encB : β ↪ List Bool} {A : Set α} {B : Set β} :
    MappingReducible encA encB A B ↔ Cslib.Complexity.ManyOneReducibleBy (fun (x : α → β) => IsComputable x encA encB) A B

    Mapping reducibility is many-one reducibility by computable maps.

    source
    theorem Turing.MultiTapeTM.MappingReducible.refl {α : Type u_1} (encA : α ↪ List Bool) (A : Set α) :
    MappingReducible encA encA A A

    Every set reduces to itself by the identity.

    source
    theorem Turing.MultiTapeTM.MappingReducible.trans {α : Type u_1} {β : Type u_2} {γ : Type u_3} {encA : α ↪ List Bool} {encB : β ↪ List Bool} {encC : γ ↪ List Bool} {A : Set α} {B : Set β} {C : Set γ} (hAB : MappingReducible encA encB A B) (hBC : MappingReducible encB encC B C) :
    MappingReducible encA encC A C

    Mapping reductions compose.

    source
    theorem Turing.MultiTapeTM.MappingReducible.compl {α : Type u_1} {β : Type u_2} {encA : α ↪ List Bool} {encB : β ↪ List Bool} {A : Set α} {B : Set β} (h : MappingReducible encA encB A B) :
    MappingReducible encA encB Aᶜ Bᶜ

    A reduction from A to B is also a reduction from Aᶜ to Bᶜ.

    source
    theorem Turing.MultiTapeTM.IsDecidable.of_mappingReducible {α : Type u_1} {β : Type u_2} {encA : α ↪ List Bool} {encB : β ↪ List Bool} {A : Set α} {B : Set β} (hB : IsDecidable B encB) (h : MappingReducible encA encB A B) :
    IsDecidable A encA

    Decidability transfers backwards along mapping reductions.

    source
    theorem Turing.MultiTapeTM.MappingReducible.not_isDecidable {α : Type u_1} {β : Type u_2} {encA : α ↪ List Bool} {encB : β ↪ List Bool} {A : Set α} {B : Set β} (h : MappingReducible encA encB A B) (hA : ¬IsDecidable A encA) :
    ¬IsDecidable B encB

    Undecidability transfers forwards along mapping reductions.