Program Equivalence in a Typed Probabilistic Call-by-Need Functional Language

EasyChair Preprint 8385

Abstract

We 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

@booklet{EasyChair:8385,
  author    = {David Sabel and Manfred Schmidt-Schauss},
  title     = {Program Equivalence in a Typed Probabilistic Call-by-Need Functional Language},
  howpublished = {EasyChair Preprint 8385},
  year      = {EasyChair, 2022}}