Completeness of Continuation Models for λ μ-Calculus
Completeness of Continuation Models for λ μ-Calculus
复制标题
λ μ 微积分的延拓模型的完备性
DOI：
--
复制
发表时间：
2002
期刊：
影响因子：
--
通讯作者：
M. Hofmann
中科院分区：
文献类型：
--
作者：
M. Hofmann
我们证明了Parigot λμ-演算的一个简单的按名调用延续语义是完备的。更确切地说，对于每个λμ-理论，我们构造一个carnival闭范畴，使得随后的λμ的延拓式解释（它将项映射到函数，将抽象延拓发送到响应）是完整和忠实的。因此，任何λμ-范畴在L. Ong（1996，在“Proceedings of LICS '96”，IEEE Press，纽约）同构于连续模型（Y.拉丰，B。雷乌斯和T. Streicher，“Continuous Semantics or Expressing Implication by Negation，”Technical Report 93-21，University of慕尼黑）从一个笛卡尔闭的延续范畴中导出。我们还将这个结果扩展到后来由C. H. L. Ong和C. A. Stewart（1997，in“Proceedings of ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages，巴黎，January 1997，”Assoc.马赫Press，纽约）。C © 2002 Elsevier Science（美国）
We show that a certain simple call-by-name continuation semantics of Parigot’s λμ-calculus is complete. More precisely, for every λμ-theory we construct a cartesian closed category such that the ensuing continuation-style interpretation of λμ, which maps terms to functions sending abstract continuations to responses, is full and faithful. Thus, any λμ-category in the sense of L. Ong (1996, in “Proceedings of LICS ’96,” IEEE Press, New York) is isomorphic to a continuation model (Y. Lafont, B. Reus, and T. Streicher, “Continuous Semantics or Expressing Implication by Negation,” Technical Report 93-21, University of Munich) derived from a cartesian-closed category of continuations. We also extend this result to a later call-by-value version of λμ developed by C.-H. L. Ong and C. A. Stewart (1997, in “Proceedings of ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, Paris, January 1997,” Assoc. Comput. Mach. Press, New York). C © 2002 Elsevier Science (USA)