论文标题
功能机积分
The Functional Machine Calculus
论文作者
论文摘要
本文将功能机演算（FMC）作为一个简单的高阶计算模型，具有“读取器/作者”效果：高阶可突变存储，输入/输出以及概率和非确定性计算。 FMC通过将呼叫堆栈机的标准操作视角作为主要的，并引入了两种自然概括，从而源自Lambda-Calculus。一个“位置”引入了多个堆栈，每个堆栈都可能代表一种效果，因此可以将效果运算符编码为conculus的抽象和应用结构。第二个“测序”是从kappa-calculus和串联编程语言中知道的，并介绍了“跳过”和“序列”的命令。这使得可以编码还原策略，包括逐个价值的lambda-calculus和monadic构造。 将效应的编码在广义抽象中和应用中表示，lambda-calculus的标准结果可能会延续到效果上。主要结果是汇合，这是可能的，因为编码效应会减少代数而不是操作。还原生成了熟悉的状态代数定律，并且与Monadic环境不同，读者/作者效果无缝地结合在一起。简单类型的系统赋予了机器的终止。
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.
