Semantics of sub-probabilistic programs |
| |
Authors: | Yixiang Chen and Hengyang Wu |
| |
Affiliation: | (1) Institute of Theoretical Computing, Shanghai Key Laboratory of Trustworthy Computing, East China Normal University, Shanghai, 200062, China;(2) Information Engineering College, Hangzhou Dianzi University, Hangzhou, 310037, China |
| |
Abstract: | The aim of this paper is to extend the probabilistic choice in probabilistic programs to sub-probabilistic choice, i.e., of
the form (p)P
⋈(q)Q where p + q ⩽ 1. It means that program P is executed with probability p and program Q is executed with probability q. Then, starting from an initial state, the execution of a sub-probabilistic program results in a sub-probability distribution.
This paper presents two equivalent semantics for a sub-probabilistic while-programming language. One of these interprets programs as sub-probabilistic distributions on state spaces via denotational
semantics. The other interprets programs as bounded expectation transformers via wp-semantics. This paper proposes an axiomatic systems for total logic, and proves its soundness and completeness in a classical
pattern on the structure of programs. |
| |
Keywords: | sub-probabilistic programs total correctness wp-calculus |
本文献已被 万方数据 SpringerLink 等数据库收录! |
|