This paper presents the Functional Machine Calculus (FMC) as a simple model of higher-order computation with "reader/writer" effects: higher-order mutable store, input/output, and probabilistic and non-deterministic computation. The FMC derives from the lambda-calculus by taking the standard operational perspective of a call-by-name stack machine as primary, and introducing two natural generalizations. One, "locations", introduces multiple stacks, which each may represent an effect and so enable effect operators to be encoded into the abstraction and application constructs of the calculus. The second, "sequencing", is known from kappa-calculus and concatenative programming languages, and introduces the imperative notions of "skip" and "sequence". This enables the encoding of reduction strategies, including call-by-value lambda-calculus and monadic constructs. The encoding of effects into generalized abstraction and application means that standard results from the lambda-calculus may carry over to effects. The main result is confluence, which is possible because encoded effects reduce algebraically rather than operationally. Reduction generates the familiar algebraic laws for state, and unlike in the monadic setting, reader/writer effects combine seamlessly. A system of simple types confers termination of the machine.

翻译：本文提出函数式机器演算（Functional Machine Calculus, FMC），作为一种包含"读/写"效应的高阶计算简单模型，涵盖高阶可变存储、输入/输出以及概率与非确定性计算。FMC源于λ演算，其核心思路是将按名调用栈机器的标准操作视角作为首要出发点，并引入两种自然泛化。其一为"位置"（locations），引入多个栈，每个栈可代表一种效应，从而使效应算子能够被编码到演算的抽象与应用构造中。其二为"序列化"（sequencing），该概念源自kappa演算与串联式编程语言，引入了命令式概念"跳过"（skip）与"序列"（sequence），从而支持对归约策略（包括按值调用λ演算与单子构造）的编码。将效应编码到泛化抽象与应用中意味着λ演算的标准结果可迁移至效应领域。主要结果为汇合性，其可行性源于编码效应以代数方式而非操作方式进行归约。归约过程生成了关于状态的常见代数定律，且与单子设定不同，读/写效应能够无缝结合。一个简单类型系统保证了机器的终止性。