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.

翻译：函数式机器演算（FMC）是作者最近提出的一种λ演算的泛化，能够忠实地编码高阶可变存储、输入/输出以及概率/非确定性输入等效应。值得注意的是，该演算在存在这些效应时仍保持合流性且可简单类型化。本文探究了FMC的指称语义。我们有三项主要贡献：首先，论证其语法——其中效应与λ演算均通过相同的句法构造实现——在语义上具有自然性，与Scott风格域论语义的结构紧密对应。其次，通过扩展Gandy对λ演算的证明（包含对该技术的一点简化），证明简单类型确保了强规范化性质。最后，表明经过适当等式理论处理的类型化FMC（不考虑编码效应的具体细节）是笛卡尔闭范畴的完备语言。