Contextual Equivalence fo probabilistic languages

Kód výsledku v IS VaVaI

<a href="https://www.isvavai.cz/riv?ss=detail&h=RIV%2F68407700%3A21240%2F18%3A00329965" target="_blank" >RIV/68407700:21240/18:00329965 - isvavai.cz</a>

Výsledek na webu

<a href="http://dx.doi.org/10.1145/3236782" target="_blank" >http://dx.doi.org/10.1145/3236782</a>

DOI - Digital Object Identifier

<a href="http://dx.doi.org/10.1145/3236782" target="_blank" >10.1145/3236782</a>

Jazyk výsledku

angličtina

Název v původním jazyce

Contextual Equivalence fo probabilistic languages

Popis výsledku v původním jazyce

We present a complete reasoning principle for contextual equivalence in an untyped probabilistic language. The language includes continuous (real-valued) random variables, conditionals, and scoring. It also includes recursion, since the standard call-by-value fixpoint combinator is expressible. We demonstrate the usability of our characterization by proving several equivalence schemas, including familiar facts from lambda calculus as well as results specific to probabilistic programming. In particular, we use it to prove that reordering the random draws in a probabilistic program preserves contextual equivalence. This allows us to show, for example, that (let x = e1 in let y = e2 in e0) =ctx (let y = e2 in let x = e1 in e0) (provided x does not occur free in e2 and y does not occur free in e1) despite the fact that e1 and e2 may have sampling and scoring effects.

Název v anglickém jazyce

Contextual Equivalence fo probabilistic languages

Popis výsledku anglicky

We present a complete reasoning principle for contextual equivalence in an untyped probabilistic language. The language includes continuous (real-valued) random variables, conditionals, and scoring. It also includes recursion, since the standard call-by-value fixpoint combinator is expressible. We demonstrate the usability of our characterization by proving several equivalence schemas, including familiar facts from lambda calculus as well as results specific to probabilistic programming. In particular, we use it to prove that reordering the random draws in a probabilistic program preserves contextual equivalence. This allows us to show, for example, that (let x = e1 in let y = e2 in e0) =ctx (let y = e2 in let x = e1 in e0) (provided x does not occur free in e2 and y does not occur free in e1) despite the fact that e1 and e2 may have sampling and scoring effects.

Druh

D - Stať ve sborníku

CEP obor

—

OECD FORD obor

10201 - Computer sciences, information science, bioinformathics (hardware development to be 2.2, social aspect to be 5.8)

Projekt

—

Návaznosti

R - Projekt Ramcoveho programu EK

Rok uplatnění

2018

Kód důvěrnosti údajů

S - Úplné a pravdivé údaje o projektu nepodléhají ochraně podle zvláštních právních předpisů

Název statě ve sborníku

Journal Proceedings of the ACM on Programming Languages,Volume 2, Issue ICFP

ISBN

—

ISSN

2475-1421

e-ISSN

2475-1421

Počet stran výsledku

38

Strana od-do

—

Název nakladatele

ACM

Místo vydání

New York

Místo konání akce

St. Louis

Datum konání akce

23. 9. 2018

Typ akce podle státní příslušnosti

WRD - Celosvětová akce

Kód UT WoS článku

—