Documentation

MIPRE.Foundations.Cost.ManyOne

The many-one reduction of an r.e. language to halting, in polynomial time #

Cost.exists_semidecider turns an r.e. predicate on strings into a well-scoped program S halting on encode z exactly on its members. The reduction to halting on the empty input hard-codes z into S — the s-m-n theorem — and hardcode is linear time, so the map z ↦ M_z is a PolyTimeFun. Halting.exists_code_halts_of_isRE is the same reduction on Mathlib's Nat.Partrec.Code through Code.curry, with no time tracked; the polynomial-time halting reduction (planning/polytime-halting.md) needs this one.

hardcode p d runs p on cons d v where v is the input, so on the empty input nil it runs p on cons d nil; Prog.onLeft p is the program running p on the left component of its input, and M_z = hardcode (onLeft S) (encode z).

source
def MIPRE.Cost.Prog.onLeft (p : Prog) :
Prog

On the input cons d v, run p on d; on nil, halt with nil.

Equations
Instances For
    source
    theorem MIPRE.Cost.Prog.onLeft_wellScoped {p : Prog} (hp : WellScoped 1 p) :
    WellScoped 1 p.onLeft
    source
    noncomputable def MIPRE.Cost.haltingReduction (S : Prog) :
    PolyTimeFun BitStr Prog

    The reduction: z ↦ hardcode (onLeft S) (encode z), in linear time.

    Equations
    Instances For
      source
      @[simp]
      theorem MIPRE.Cost.haltingReduction_apply (S : Prog) (z : BitStr) :
      (haltingReduction S).toFun z = hardcode S.onLeft (encode z)
      source
      theorem MIPRE.Cost.haltingReduction_wellScoped {S : Prog} (hS : Prog.WellScoped 1 S) (z : BitStr) :
      Prog.WellScoped 1 ((haltingReduction S).toFun z)
      source
      theorem MIPRE.Cost.halts_haltingReduction_iff {S : Prog} (hS : Prog.WellScoped 1 S) (z : BitStr) :
      Halts ((haltingReduction S).toFun z) Data.nil ↔ Halts S (encode z)

      The reduction halts on the empty input exactly when S halts on encode z.

      source
      theorem MIPRE.Cost.exists_polyTime_reduction {p : BitStr → Prop} (hp : REPred p) :
      ∃ (R : PolyTimeFun BitStr Prog), (∀ (z : BitStr), Prog.WellScoped 1 (R.toFun z)) ∧ ∀ (z : BitStr), Halts (R.toFun z) Data.nil ↔ p z

      Every r.e. predicate on strings many-one reduces to halting on the empty input, in polynomial time.