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.

翻译：本文提出函数机器演算（FMC），作为高阶计算与"读/写"效应的简洁模型：涵盖高阶可变存储、输入/输出、概率与非确定性计算。FMC源自λ演算，以按名调用栈机的标准操作视角为基础，引入两种自然推广：其一为"位置"机制，通过引入多栈结构，每个栈可表征一种效应，从而将效应操作符编码到演算的抽象与应用构造中；其二为"排序"机制（源自κ演算与拼接式编程语言），引入"跳过"与"顺序"等命令式概念。这使得包括按值调用λ演算与单子构造在内的归约策略均可被编码。由于效应被编码为广义抽象与应用，λ演算的标准结论得以迁移至效应系统。核心成果是合流性——归约过程以代数方式（而非操作方式）进行使得该性质成立。归约生成熟悉的状态代数律，且与单子框架不同，读/写效应可无缝结合。简单类型系统保证机器停机。