Download PDFOpen PDF in browser

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

EasyChair Preprint 8385

10 pagesDate: July 5, 2022

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

BibTeX entry
BibTeX does not have the right entry for preprints. This is a hack for producing the correct reference:
@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}}
Download PDFOpen PDF in browser