The Fundamental Theorem of Perfect Simulation

TL;DR

The paper introduces the Fundamental Theorem of Perfect Simulation (FTPS), unifying various perfect simulation algorithms under a common framework and providing criteria for their correctness.

Contribution

It presents the FTPS, a simple yet powerful criterion that verifies the correctness of a wide range of perfect simulation algorithms.

Findings

FTPS unifies multiple perfect simulation algorithms.

The criteria ensure finite termination and local correctness.

The theorem verifies correctness of protocols like Acceptance Rejection and Coupling From the Past.

Abstract

Here several perfect simulation algorithms are brought under a single framework, and shown to derive from the same probabilistic result, called here the Fundamental Theorem of Perfect Simulation (FTPS). An exact simulation algorithm has output according to an input distribution $\pi$. Perfect simulations are a subclass of exact simulations where recursion is used either explicitly or implicitly. The FTPS gives two simple criteria that, when satisfied, give a correct perfect simulation algorithm. First the algorithm must terminate in finite time with probability 1. Second, the algorithm must be locally correct in the sense that the algorithm can be proved correct given the assumption that any recursive call used returns an output from the correct distribution. This simple idea is surprisingly powerful. Like other general techniques such as Metropolis-Hastings for approximate simulation, the FTPS allows for the flexible construction of existing and new perfect simulation protocols. This theorem can be used to verify the correctness of many perfect simulation protocols, including Acceptance Rejection, Coupling From the Past, and Recursive Bernoulli factories.