一句话：论文研究 I/O 与可数概率选择程序形成的概率策略，用等式理论的和与张量刻画双相似和迹等价，并在有穷情形证明完备性。
论文研究同时含 I/O 与可数概率选择的程序，在双相似或迹等价下将其视为概率策略。目标是像非确定性情形那样，用等式理论的和公理化双相似，用张量公理化迹等价。结果：双相似确可由理论和刻画；张量对迹等价至少可靠，但一般完备性未决。作者在概率选择或 I/O 有穷时证明完备，并证明“冒充”意义下的完备性：张量理论把迹等价程序视为求解同一方程组，从而得到概率选择消去律下的完备性。还证明概率迹策略是良基程序语义当且仅当它必胜，即与任意部分反策略对局时无限继续概率为零，并将结果与效应 monad 关联。
Programs that combine I/O and countable probabilistic choice, modulo either bisimilarity or trace equivalence, can be seen as describing a probabilistic strategy. For well-founded programs, we might expect to axiomatize bisimilarity via a sum of equational theories and trace equivalence via a tensor of such theories. This is by analogy with similar results for nondeterminism, established previously. While bisimilarity is indeed axiomatized via a sum of theories, and the tensor is indeed at least sound for trace equivalence, completeness in general, remains an open problem. Nevertheless, we show completeness in the case that either the probabilistic choice or the I/O operations used are finitary. We also show completeness up to impersonation, i.e. that the tensor theory regards trace equivalent programs as solving the same system of equations. This entails completeness up to the cancellation law of the probabilistic choice operator.Furthermore, we show that a probabilistic trace strategy arises as the semantics of a well-founded program iff it is victorious. This means that, when the strategy is played against any partial counterstrategy, the probability of play continuing forever is zero.We link our results (and open problem) to particular monads that can be used to model computational effects.