一句话：在高阶数学操作语义框架中提出抽象大步 SOS，并由高阶 GSOS 推导，证明二者等价。
小步与大步操作语义是结构操作语义的两种基本风格。前者更细粒度，通常视为原始；后者以自包含方式直接关联程序与求值净结果。二者的一致性在程序操作推理中极为关键，但通常只能逐例从头证明，缺少一般抽象论证。本文在高阶数学操作语义框架下处理该问题：给出抽象范畴意义下的大步 SOS 概念，用以补充已有的抽象高阶 GSOS；同时提出从后者推导前者的通用构造，并证明两种语义之间的抽象等价结果。
Small-step and big-step operational semantics are two fundamental styles of structural operational semantics (SOS), extensively used in practice. The former one is more fine-grained and is usually regarded as primitive, as it only defines a one-step reduction relation between a given program and its direct descendant under an ambient evaluation strategy . The latter one implements, in a self-contained manner, such a strategy directly by relating a program to the net result of the evaluation process. The agreement between these two styles of semantics is one of the key pillars in operational reasoning on programs; however, such agreement is typically proven from scratch every time on a case-by-case basis. A general, abstract mathematical argument behind this agreement is up till now missing. We cope with this issue within the framework of higher-order mathematical operational semantics by providing an abstract categorical notion of big-step SOS, complementing the existing notion of abstract higher-order GSOS. Moreover, we introduce a general construction for deriving the former from the latter, and prove an abstract equivalence result between the two.
@article{paperbot3060,
title = {Big Steps in Higher-Order Mathematical Operational Semantics},
author = {Sergey Goncharov and Pouya Partow and Stelios Tsampas},
journal = {Proceedings of the ACM on Programming Languages},
volume = {9},
number = {ICFP},
year = {2025},
doi = {10.1145/3747540}
}