Download PDFOpen PDF in browserProgram Equivalence in a Typed Probabilistic Call-by-Need Functional LanguageEasyChair Preprint 838510 pages•Date: July 5, 2022AbstractWe introduce a call-by-need variant of PCF with a binary probabilistic fair choice operator. We define its operational semantics and contextual equivalence as program equivalence, where the expected convergence is only observed on numbers. We investigate another program equivalence that views two closed expressions as distribution-equivalent if evaluation generates the same distribution on the natural numbers. We show that contextual equivalence implies distribution-equivalence. Future work is to provide a full proof of the opposite direction. Keyphrases: lambda calculus, probabilistic programming, program equivalence, semantics
|