An Adequacy Theorem Between Mixed Powerdomains and Probabilistic Concurrency
Renato Neves
TL;DR
The paper addresses adequacy between a concurrent extension of probabilistic GCL and domain-theoretic semantics built from mixed powerdomains. It develops a Smyth-style open-set logic, a final-coalgebra based denotational semantics, and an extensional collapse to establish computational adequacy and full abstraction with respect to an observational preorder $\lesssim$. A central technical achievement is a topological generalisation of König's lemma used to prove must-termination equivalences, enabling semi-decidability results for may and must termination within main fragments of the logic. The framework is then instantiated to a concurrent quantum setting, illustrating the approach's versatility and potential for broader impact. Overall, the work provides a rigorous bridge between operational scheduling, topological observables, and denotational semantics for concurrent probabilistic computation, with concrete implications for semi-decidability and quantum extensions.
Abstract
We present an adequacy theorem for a concurrent extension of probabilistic GCL. The underlying denotational semantics is based on the so-called mixed powerdomains, which combine non-determinism with probabilistic behaviour. The theorem itself is formulated via M. Smyth's idea of treating observable properties as open sets of a topological space. The proof hinges on a 'topological generalisation' of König's lemma in the setting of probabilistic programming (a result that is proved in the paper as well). One application of the theorem is that it entails semi-decidability w.r.t. whether a concurrent program satisfies an observable property (written in a certain form). This is related to M. Escardo's conjecture about semi-decidability w.r.t. may and must probabilistic testing.