  We introduce a method for proving almost sure termination in the context of
lambda calculus with continuous random sampling and explicit recursion, based
on ranking supermartingales. This result is extended in three ways. Antitone
ranking functions have weaker restrictions on how fast they must decrease, and
are applicable to a wider range of programs. Sparse ranking functions take
values only at a subset of the program's reachable states, so they are simpler
to define and more flexible. Ranking functions with respect to alternative
reduction strategies give yet more flexibility, and significantly increase the
applicability of the ranking supermartingale approach to proving almost sure
termination, thanks to a novel (restricted) confluence result which is of
independent interest. The notion of antitone ranking function was inspired by
similar work by McIver, Morgan, Kaminski and Katoen in the setting of a
first-order imperative language, but adapted to a higher-order functional
language. The sparse ranking function and confluent semantics extensions are
unique to the higher-order setting. Our methods can be used to prove almost
sure termination of programs that are beyond the reach of methods in the
literature, including higher-order and non-affine recursion.
