Confluence and Convergence Modulo Equivalence in Probabilistically Terminating Reduction Systems

Convergence of an abstract reduction system is the property that the possible derivations from a given initial state all end in the same final state. Relaxing this by “modulo equivalence” means that these final states need not be identical, only equivalent wrt. a specified equivalence relation.

We generalize this notion for probabilistic abstract reduction systems, naming it almost-sure convergence modulo equivalence, such that the final states are reached with probability 1. We relate it to the well-studied properties of almost-sure termination and confluence/convergence of probabilistic and non-probabilistic systems. In addition, we provide a transformational approach for proving – or disproving – almost-sure convergence modulo equivalence of given systems.