Generic Trace Theory |
| |
Authors: | Ichiro Hasuo Bart Jacobs Ana Sokolova |
| |
Affiliation: | aInstitute for Computing and Information Sciences, Radboud University Nijmegen, the Netherlands |
| |
Abstract: | Trace semantics has been defined for various non-deterministic systems with different input/output types, or with different types of “non-determinism” such as classical non-determinism (with a set of possible choices) vs. probabilistic non-determinism. In this paper we claim that these various forms of “trace semantics” are instances of a single categorical construction, namely coinduction in a Kleisli category. This claim is based on our main technical result that an initial algebra in the category of sets and functions yields a final coalgebra in the Kleisli category, for monads with a suitable order structure. The proof relies on coincidence of limits and colimits, like in the work of Smyth and Plotkin. |
| |
Keywords: | coalgebra trace semantics linear time semantics monad Kleisli category non-determinism probability |
本文献已被 ScienceDirect 等数据库收录! |
|