1: \begin{abstract}

2: We study the first-order probabilistic programming language introduced by \citet{SWY+:16}, but with an additional language construct, $\Stationary$, that, 

3: like the fixpoint operator of \citet{AYC:18}, converts the description of the Markov kernel of an ergodic Markov chain 

4: into a sample from its unique stationary distribution.

5: Up to minor changes in how certain error conditions are handled,

6: we show that $\Normalize$ and $\Score$ are eliminable from the extended language, in the sense of \citet{Fel:91}.

7: We do so by giving an explicit program transformation and proof of correctness. 

8: In fact, our program transformation implements a Markov chain Monte Carlo algorithm, 

9: in the spirit of the ``Trace-MH'' algorithm of \citet{WSG:11} and \citet{GMR+:08}, but less sophisticated to enable analysis. 

10: We then explore the problem of approximately implementing the semantics of the language with potentially nested $\Stationary$ expressions,

11: in a language without $\Stationary$.

12: For a single $\Stationary$ term, the error introduced by the finite unrolling 

13: proposed by Atkinson et al.\ vanishes only asymptotically.

14: In the general case, no guarantees exist.

15: Under uniform ergodicity assumptions, we are able to give quantitative error bounds and convergence results for the approximate implementation of the extended first-order language.

16: %

17: \end{abstract}

18: