Category theory for operational semantics

Category theory for operational semantics
复制标题

DOI：
10.1016/j.tcs.2004.07.024
复制
发表时间：
2004-10
期刊：
Theor. Comput. Sci.
影响因子：
--
通讯作者：
Marina Lenisa;J. Power;Hiroshi Watanabe
Marina Lenisa;J. Power;Hiroshi Watanabe
中科院分区：
其他
文献类型：
--
作者：
Marina Lenisa;J. Power;Hiroshi Watanabe

文献摘要

被引文献

相似文献

我们使用联合内函子上的单子分配律的概念来定义和发展Turi和Plotkin的抽象运算规则概念的重新表述和温和推广。我们给出了抽象的定义，并精确地分析了它与图里和普洛特金的定义之间的关系。遵循Turi和Plotkin，我们的定义（适当地加以限制）与一组gsos规则的概念一致，允许构建一个操作模型和一个规范的、内部完全抽象的指示模型。超越Turi和Plotkin，我们从小步骤操作语义构建了可能被视为大步骤操作语义的东西，我们展示了我们的定义如何允许人们结合分配律，特别是考虑到操作语义与同余的结合。
We use the concept of a distributive law of a monad over a copointed endofunctor to define and develop a reformulation and mild generalisation of Turi and Plotkin's notion of an abstract operational rule. We make our abstract definition and give a precise analysis of the relationship between it and Turi and Plotkin's definition. Following Turi and Plotkin, our definition, suitably restricted, agrees with the notion of a set of GSOS-rules, allowing one to construct both an operational model and a canonical, internally fully abstract denotational model. Going beyond Turi and Plotkin, we construct what might be seen as large-step operational semantics from small-step operational semantics and we show how our definition allows one to combine distributive laws, in particular accounting for the combination of operational semantics with congruences.