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源于λ演算，通过将标准按名调用栈机器的操作视角作为首要原则，并引入两种自然推广。其一为“位置”，引入多个栈，每个栈可表示一种效应，从而使效应操作符能够编码到演算的抽象与应用构造中。其二为“序列化”，源自kappa演算和拼接式编程语言，并引入了“跳过”和“序列”等命令式概念。这允许对归约策略（包括按值调用λ演算和单子构造）进行编码。将效应编码到广义抽象与应用中，意味着λ演算的标准结果可迁移至效应场景。主要结果是汇合性，这之所以可能，是因为编码后的效应以代数方式而非操作方式归约。归约生成了熟悉的状态代数律，并且与单子设置不同，读/写效应能够无缝结合。一个简单类型系统确保了机器的终止性。