关于状态变换语义与谓词变换语义的等价性
计算机科学中的逻辑
2014-10-30 v1
摘要
G. Plotkin 与作者已在域理论框架下,针对结合非确定性与概率的程序,推导出了状态变换语义与谓词变换语义之间的等价性。C. Morgan 及其合作者,以及 Keimel、Rosenbusch 和 Streicher 的工作,仅使用离散状态空间也已朝同一方向迈进。本文旨在展示一个通用框架,在其中有望实现状态变换语义与谓词变换语义的等价。我们使用了借用于通用代数的熵性(entropicity)概念,以及一种适应于域理论情境的松弛设定。
引用
@article{arxiv.1410.7930,
title = {On the equivalence of state transformer semantics and predicate transformer semantics},
author = {Klaus Keimel},
journal= {arXiv preprint arXiv:1410.7930},
year = {2014}
}