Composing uniformly efficient probabilistic programs

Encoded probabilistic programs compose through ordinary monadic bind. Each certificate gives one finite machine for every input. The output-length bound controls the continuation's clock, and the machine compiler charges every instruction needed to prepare its fresh input.

This module also registers deterministic preprocessing and postprocessing with fun_prop. Closed composition specializes the strict oracle calculus to the empty external-operation type. The embedding preserves sampling and monadic sequencing, so the shared clean-realization compiler supplies the machine and its resource bound. Continuations here consume the sampled result; PPT.Capture retains the caller's input through the same calculus.

Main results

• Cslib.Probability.IsPPTOn.bind: monadic composition preserves uniform strict PPT.
• Cslib.Probability.IsPPTOn.map: polynomial-time deterministic postprocessing preserves PPT.
• Cslib.Probability.IsPPTOn.preprocess: efficiently prepare a probabilistic program's input.

References

Adapted from Computability/Probabilistic/Realization/Composition.lean and Computability/Probabilistic/Composition.lean on the cslib crypto branch at 5ff69ca93402e7c947208dc56396d6d86203ccd8, reusing the common machine and tidy deterministic calculus.

theorem Cslib.Probability.IsPPTOn.bind {α β γ : Type} {input : α ↪ List Bool} {middle : β ↪ List Bool} {output : γ ↪ List Bool} {first : α → ProbComp β} {second : β → ProbComp γ} (hfirst : IsPPTOn input middle first) (hsecond : IsPPTOn middle output second) : IsPPTOn input output fun (a : α) => do let b ← first a second b

Sequence two uniformly efficient encoded programs. The intermediate output length bounds the continuation's time, and input preparation is included in the compiled polynomial clock.

theorem Cslib.Probability.IsPPTOn.preprocess {α β γ : Type} {input : α ↪ List Bool} {middle : β ↪ List Bool} {output : γ ↪ List Bool} {program : β → ProbComp γ} {prepare : α → β} (hprogram : IsPPTOn middle output program) (hprepare : Turing.MultiTapeTM.ComputableTidilyInPolyTime prepare input middle) : IsPPTOn input output fun (a : α) => program (prepare a)

Prepare the encoded argument of a uniformly efficient probabilistic program.

theorem Cslib.Probability.IsPPTOn.map {α β γ : Type} {input : α ↪ List Bool} {middle : β ↪ List Bool} {output : γ ↪ List Bool} {program : α → ProbComp β} {f : β → γ} (hprogram : IsPPTOn input middle program) (hf : Turing.MultiTapeTM.ComputableTidilyInPolyTime f middle output) : IsPPTOn input output fun (a : α) => f <$> program a

Polynomial-time deterministic processing of each sampled result preserves PPT.