.png){kind=icon}
返回
Computation-Tree Semantics: An Algorithmic Approach to Structurally Defined Relations
.png){kind=icon}
PRE
AI
DOI：10.1145/3779209.3779534.png)
.png){kind=icon}
原文求助.png){kind=icon}
分享.png){kind=icon}
收藏
摘要
En 中文
结构操作语义（SOS）是描述语言语义的最常用形式化方法之一。人们已对如何自动从大步定义推导出小步SOS定义（反之亦然）以及如何从这些归纳性、声明性定义外推语言实现表现出浓厚兴趣。本研究提出计算树语义（CTS），其中语义配置为树状结构，而不同于标准SOS配置的扁平结构。这种树状结构是实现我们算法化方法的关键，意味着它能描述如何产生转换，这与SOS所采取的传统声明性方法相反。我们展示了如何从大步语义（简单算术语言、简单while语言以及由Launchbury给出的需调用λ演算）中直接获得CTS，并从得到的CTS中获取这些语言的小步理解。算术语言示例已在Coq/Rocq中形式化。
Keyword:
Structural operational semantics
structural relations
algorithmic
big-step semantics
small-step semantics
lambda calculus
.png){kind=icon}
查看更多内容