一句话：提出概率PCF的并发博弈语义，证明其内涵完全抽象并给出有限可定义性。
本文为概率PCF（PPCF）提出一种新的博弈语义。作者在Castellan等人最近引入的带对称性的thin concurrent games上加入概率，得到支持PPCF的顺序与并行两种解释的并发博弈模型。通过利用概率并发策略的因果结构，论文证明PPCF程序所得策略的交互无死锁，并构造一个保持解释的函子，从该模型映射到Ehrhard等人已证明完全抽象的概率关系模型，由此推出该模型是内涵完全抽象的。作者还定义了概率innocence，并证明有限可定义性，从而给出完全抽象性的第二个独立证明。
We define a new games model of Probabilistic PCF (PPCF) by enriching thin concurrent games with symmetry, recently introduced by Castellan et al, with probability. This model supports two interpretations of PPCF, one sequential and one parallel. We make the case for this model by exploiting the causal structure of probabilistic concurrent strategies. First, we show that the strategies obtained from PPCF programs have a deadlock-free interaction, and therefore deduce that there is an interpretation-preserving functor from our games to the probabilistic relational model recently proved fully abstract by Ehrhard et al. It follows that our model is intensionally fully abstract. Finally, we propose a definition of probabilistic innocence and prove a finite definability result, leading to a second (independent) proof of full abstraction.