Control categories and duality: on the categorical semantics of the lambda-mu calculus
Control categories and duality: on the categorical semantics of the lambda-mu calculus
复制标题
控制类别和对偶性：关于 lambda-mu 演算的分类语义
DOI：
10.1017/s096012950000311x
复制
发表时间：
2001
影响因子：
0.5
通讯作者：
P. Selinger
中科院分区：
文献类型：
--
作者：
P. Selinger
我们为具有析取类型的 Parigot 的 λμ 演算的按名称调用和按值调用版本提供了分类语义。我们引入了控制范畴的类，它结合了笛卡尔封闭结构和 Power 和 Robinson 意义上的预幺半群结构。我们通过分类结构定理证明分类语义相当于 Hofmann 和 Streicher 风格的 CPS 语义。我们证明，按名称调用 λμ 演算形成了控制类别的内部语言，而按值调用 λμ 演算形成了对偶协同控制类别的内部语言。作为推论，我们得到了句法二元性结果：按名称调用和按值调用之间存在相互逆并保留操作语义的句法翻译。这回答了 Streicher 和 Reus 的问题。
We give a categorical semantics to the call-by-name and call-by-value versions of Parigot's λμ-calculus with disjunction types. We introduce the class of control categories, which combine a cartesian-closed structure with a premonoidal structure in the sense of Power and Robinson. We prove, via a categorical structure theorem, that the categorical semantics is equivalent to a CPS semantics in the style of Hofmann and Streicher. We show that the call-by-name λμ-calculus forms an internal language for control categories, and that the call-by-value λμ-calculus forms an internal language for the dual co-control categories. As a corollary, we obtain a syntactic duality result: there exist syntactic translations between call-by-name and call-by-value that are mutually inverse and preserve the operational semantics. This answers a question of Streicher and Reus.