Captured inputs in efficient probabilistic programs

Ordinary monadic continuations and callbacks may use both the caller's input and a sampled result. These operations specialize the strict oracle calculus to empty external channels. Its clean-realization compiler charges copying, framing and preparation; the existing pair encoding makes the retained data a typed value for the next computation. Prefixing is pairing followed by efficient deterministic concatenation.

Main results

• Cslib.Probability.IsPPTOn.pair: retain efficiently computed data alongside a sampled result.
• Cslib.Probability.IsPPTOn.bind_with: a monadic continuation may capture the original input.
• Cslib.Probability.IsPPTOn.map_with: a deterministic callback may capture the original input.
• Cslib.Probability.IsPPTOn.cond, Cslib.Probability.IsPPTOn.ite: efficient branch selection.

References

Adapted from Computability/Probabilistic/{Realization/Composition,Composition}.lean on the cslib crypto branch at 5ff69ca93402e7c947208dc56396d6d86203ccd8, using the existing tidy calculus and framed pair encoding.

theorem Cslib.Probability.IsPPTOn.prefix {α : Type} {input : α ↪ List Bool} {pre : α → List Bool} {program : α → ProbComp (List Bool)} (hprogram : IsPPTOn input Turing.MultiTapeTM.encBits program) (hprefix : Turing.MultiTapeTM.ComputableTidilyInPolyTime pre input Turing.MultiTapeTM.encBits) : IsPPTOn input Turing.MultiTapeTM.encBits fun (a : α) => (fun (x : List Bool) => pre a ++ x) <$> program a

Write efficiently computed input data before a probabilistic output, charging preparation.

theorem Cslib.Probability.IsPPTOn.pair {α β γ : Type} {input : α ↪ List Bool} {left : β ↪ List Bool} {right : γ ↪ List Bool} {program : α → ProbComp γ} {f : α → β} (hprogram : IsPPTOn input right program) (hf : Turing.MultiTapeTM.ComputableTidilyInPolyTime f input left) : IsPPTOn input (Turing.MultiTapeTM.encPair left right) fun (a : α) => (fun (b : γ) => (f a, b)) <$> program a

Retain efficiently computed input data beside a sampled result, using the existing encoding.

theorem Cslib.Probability.IsPPTOn.keep_input {α β : Type} {input : α ↪ List Bool} {left : β ↪ List Bool} {program : α → ProbComp β} (hprogram : IsPPTOn input left program) : IsPPTOn input (Turing.MultiTapeTM.encPair input left) fun (a : α) => (fun (b : β) => (a, b)) <$> program a

Keep the original argument available to a later computation, charging its encoded copy.

theorem Cslib.Probability.IsPPTOn.bind_with {α β γ : Type} {input : α ↪ List Bool} {left : β ↪ List Bool} {right : γ ↪ List Bool} {first : α → ProbComp β} {second : α → β → ProbComp γ} (hfirst : IsPPTOn input left first) (hsecond : IsPPTOn (Turing.MultiTapeTM.encPair input left) right fun (pair : α × β) => second pair.1 pair.2) : IsPPTOn input right fun (a : α) => do let b ← first a second a b

A monadic continuation may use both the caller's input and the sampled result.

theorem Cslib.Probability.IsPPTOn.map_with {α β γ : Type} {input : α ↪ List Bool} {left : β ↪ List Bool} {right : γ ↪ List Bool} {program : α → ProbComp β} {f : α → β → γ} (hprogram : IsPPTOn input left program) (hf : Turing.MultiTapeTM.ComputableTidilyInPolyTime (fun (pair : α × β) => f pair.1 pair.2) (Turing.MultiTapeTM.encPair input left) right) : IsPPTOn input right fun (a : α) => f a <$> program a

A deterministic callback may capture the original argument.

theorem Cslib.Probability.IsPPTOn.cond {α β : Type} {input : α ↪ List Bool} {left : β ↪ List Bool} {condition : α → Bool} {yes no : α → ProbComp β} (hcondition : Turing.MultiTapeTM.ComputableTidilyInPolyTime condition input Turing.MultiTapeTM.encBool) (hyes : IsPPTOn input left yes) (hno : IsPPTOn input left no) : IsPPTOn input left fun (a : α) => if condition a = true then yes a else no a

Select a closed probabilistic branch with an efficient Boolean condition, using the empty-channel specialization of oracle branch selection.

theorem Cslib.Probability.IsPPTOn.ite {α β : Type} {input : α ↪ List Bool} {left : β ↪ List Bool} {condition : α → Prop} [(a : α) → Decidable (condition a)] {yes no : α → ProbComp β} (hcondition : Turing.MultiTapeTM.ComputableTidilyInPolyTime (fun (a : α) => decide (condition a)) input Turing.MultiTapeTM.encBool) (hyes : IsPPTOn input left yes) (hno : IsPPTOn input left no) : IsPPTOn input left fun (a : α) => if condition a then yes a else no a

Select a closed probabilistic branch with an efficiently decidable condition.