On probabilistic term rewriting
Martin Avanzini, Ugo Dal Lago, Akihisa Yamada · Science of Computer Programming · 2019
Almost sure termination Interpretation methodWe study the termination problem for probabilistic term rewrite systems.We prove that the interpretation method is sound and complete for a strengthening of positive almost sure termination, when abstract reduction systems and term rewrite systems are considered.Two instances of the interpretation method-polynomial and matrix interpretations-are analyzed and shown to capture interesting and nontrivial examples when automated.We capture probabilistic computation in a novel way by means of multidistribution reduction sequences, thus accounting for both the nondeterminism in the choice of the redex and the probabilism intrinsic in firing each rule.