Coinductive Proof Principles for Stochastic Processes

TL;DR

This paper introduces a coinductive proof principle for recursively-defined stochastic processes that enables high-level reasoning about properties beyond equality, even with non-unique solutions.

Contribution

It presents an explicit coinduction rule applicable to any closed property of stochastic processes, simplifying complex analytic arguments.

Findings

The rule applies to non-unique solutions.

It facilitates reasoning about properties beyond equality.

Demonstrated on a coin-flip process.

Abstract

We give an explicit coinduction principle for recursively-defined stochastic processes. The principle applies to any closed property, not just equality, and works even when solutions are not unique. The rule encapsulates low-level analytic arguments, allowing reasoning about such processes at a higher algebraic level. We illustrate the use of the rule in deriving properties of a simple coin-flip process.