Developing denotational models for higher-order languages that combine
probabilistic and nondeterministic choice is known to be very
challenging. In this paper, we propose an alternative approach based
on operational techniques. We study a higher-order language combining
parametric polymorphism, recursive types, discrete probabilistic choice
and countable nondeterminism. We define probabilistic generalizations
of may- and must-termination as the optimal and pessimal probabilities
of termination. Then we define step-indexed logical relations and show
that they are sound and complete with respect to the induced contextual
preorders. For may-equivalence we use step-indexing over the natural
numbers whereas for must-equivalence we index over the countable
ordinals. We then show than the probabilities of may- and
must-termination coincide with the maximal and minimal probabilities of
termination under all schedulers. Finally we derive the equational
theory induced by contextual equivalence and show that it validates the
distributive combination of the algebraic theories for probabilistic
and nondeterministic choice.