Documentation

Complexity.Computability.Probabilistic.PPT

Uniform strict probabilistic polynomial time #

IsPPTOn input output program identifies the encoded result distribution with one finite-control fair-coin machine, clocked by a polynomial in the encoded input length. The machine and polynomial are fixed before quantifying over inputs. Only fair bits are supplied to the machine, and it has no oracle channels. Thus arbitrary Lean computation, nonuniform advice, and arbitrary distribution samplers are not free operations.

The clock bounds every execution, rather than its expectation. The witness is forcibly stopped at its clock; this definition does not require that its control state has already halted. PPT.Clock compiles every such witness to an intrinsically halting finite machine, charging preparation and consumption of a unary budget to its polynomial bound. In particular, this definition does not certify exact uniform sampling from every finite type.

The public input and output encodings reuse the tidy calculus. A deterministic certificate lifts directly to IsPPTOn without another deterministic computability predicate. PPT.Composition certifies monadic bind, deterministic preprocessing and postprocessing. PPT.Capture permits captured inputs and efficient conditionals. Adaptive certifies bounded probabilistic loops from supported state-size invariants. Tactic.PPT automates the closed program rules and constant-growth loops; oracle PPT requires further certified constructions.

Adapted from the cslib crypto branch's Computability/Probabilistic/PPT.lean at 5ff69ca93402e7c947208dc56396d6d86203ccd8. The witness uses the common machine and any finite control type, as the upstream tidy calculus does, instead of imposing a separate Fin presentation.

Main definitions #

Main results #

source
theorem Cslib.ProbComp.probability_not (program : ProbComp Bool) :
((not <$> program).eval true).toReal = 1 - (program.eval true).toReal

Complementing a Boolean program's answer replaces the real probability of true by its complement.

source
def Cslib.Probability.IsPPTOn {α β : Type} (input : α ↪ List Bool) (output : β ↪ List Bool) (program : α → ProbComp β) :
Prop

One finite fair-coin machine realizes the program, with a uniform polynomial clock. The clock is strict on every execution and includes the cost of writing the encoded output.

Instances For
    source
    theorem Cslib.Probability.IsPPTOn.congr {α β : Type} {input : α ↪ List Bool} {output : β ↪ List Bool} {program program' : α → ProbComp β} (h : IsPPTOn input output program) (heq : ∀ (a : α), (program a).eval = (program' a).eval) :
    IsPPTOn input output program'

    Distributional equality reuses the same finite machine and clock.

    source
    theorem Cslib.Probability.IsPPTOn.length_le {α β : Type} {input : α ↪ List Bool} {output : β ↪ List Bool} {program : α → ProbComp β} (h : IsPPTOn input output program) :
    ∃ (c : ℕ) (d : ℕ), ∀ (a : α), ∀ result ∈ (program a).eval.support, (output result).length ≤ c * ((input a).length + 1) ^ d

    A typed certificate bounds the encoded length of every supported result.

    source
    theorem Cslib.Probability.isPPTOn_iff_encoded {α β : Type} {input : α ↪ List Bool} {output : β ↪ List Bool} {program : α → ProbComp β} :
    IsPPTOn input output program ↔ IsPPTOn input Turing.MultiTapeTM.encBits fun (a : α) => ⇑output <$> program a

    A program returning its declared encoding has the same machine-level contract.

    source
    theorem Turing.MultiTapeTM.ComputableTidilyInPolyTime.isPPTOn {α β : Type} {input : α ↪ List Bool} {output : β ↪ List Bool} {f : α → β} (h : ComputableTidilyInPolyTime f input output) :
    Cslib.Probability.IsPPTOn input output fun (a : α) => pure (f a)

    Reuse a tidy deterministic machine as a fair-coin machine that ignores its sampled bits.