论文标题
功能机演算II：语义
The Functional Machine Calculus II: Semantics
论文作者
论文摘要
作者最近引入的功能机积分（FMC）是lambda-calculus的概括，它可能忠实地编码高阶可突变存储，I/O和概率/非确定性输入的效果。值得注意的是，它保持汇合，可以简单地在存在这些效果的情况下键入。在本文中，我们探讨了FMC的典型语义。我们有三个主要贡献：首先，我们认为它的语法 - 使用相同的句法构造可以实现效果和lambda-calculus-在语义上是自然的，与Scott-Style型域理论语义的结构紧密相对应。其次，我们表明，简单类型通过扩展Gandy的lambda-Calculus证明，包括对技术的少量简化，从而赋予了强大的归一化。最后，我们表明键入的FMC（不考虑编码效果的细节），Modulo是适当的方程理论，是笛卡尔封闭类别的完整语言。
The Functional Machine Calculus (FMC), recently introduced by the authors, is a generalization of the lambda-calculus which may faithfully encode the effects of higher-order mutable store, I/O and probabilistic/non-deterministic input. Significantly, it remains confluent and can be simply typed in the presence of these effects. In this paper, we explore the denotational semantics of the FMC. We have three main contributions: first, we argue that its syntax -- in which both effects and lambda-calculus are realised using the same syntactic constructs -- is semantically natural, corresponding closely to the structure of a Scott-style domain theoretic semantics. Second, we show that simple types confer strong normalization by extending Gandy's proof for the lambda-calculus, including a small simplification of the technique. Finally, we show that the typed FMC (without considering the specifics of encoded effects), modulo an appropriate equational theory, is a complete language for Cartesian closed categories.
