Saved in:
| Main Authors: | , , |
|---|---|
| Format: | Preprint |
| Published: |
2025
|
| Subjects: | |
| Online Access: | https://arxiv.org/abs/2504.09392 |
| Tags: |
Add Tag
No Tags, Be the first to tag this record!
|
| _version_ | 1866916911292350464 |
|---|---|
| author | Bowler, Nathan Goncharov, Sergey Levy, Paul Blain |
| author_facet | Bowler, Nathan Goncharov, Sergey Levy, Paul Blain |
| contents | 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. |
| format | Preprint |
| id |
arxiv_https___arxiv_org_abs_2504_09392 |
| institution | arXiv |
| publishDate | 2025 |
| record_format | arxiv |
| spellingShingle | Probabilistic Strategies: Definability and the Tensor Completeness Problem Bowler, Nathan Goncharov, Sergey Levy, Paul Blain Logic in Computer Science 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. |
| title | Probabilistic Strategies: Definability and the Tensor Completeness Problem |
| topic | Logic in Computer Science |
| url | https://arxiv.org/abs/2504.09392 |