The Functional Machine Calculus (Heijltjes 2022) is a new approach to unifying the imperative and functional programming paradigms. It extends the lambda-calculus, preserving the key features of confluent reduction and typed termination, to embed computational effects, evaluation strategies, and control flow operations. The first instalment modelled sequential higher-order computation with global store, input/output, probabilities, and non-determinism, and embedded both the call-by-name and call-by-value lambda-calculus, as well as Moggi's computational metalanguage and Levy's call-by-push-value. The present paper extends the calculus from sequential to branching and looping control flow. This allows the faithful embedding of a minimal but complete imperative language, including conditionals, exception handling, and iteration, as well as constants and algebraic data types. The calculus is defined through a simple operational semantics, extending the (simplified) Krivine machine for the lambda-calculus with multiple operand stacks to model effects and a continuation stack to model sequential, branching, and looping computation. It features a confluent reduction relation and a system of simple types that guarantees termination of the machine and strong normalization of reduction (in the absence of iteration). These properties carry over to the embedded imperative language, providing a unified functional-imperative model of computation that supports simple types, a direct and intuitive operational semantics, and a confluent reduction semantics.
翻译:函数式机器演算(Heijltjes 2022)是一种统一命令式与函数式编程范式的新方法。它扩展了λ演算,保留了合流归约和类型化终止的关键特性,以嵌入计算效应、求值策略和控制流操作。第一部分通过全局存储、输入/输出、概率和非确定性对顺序高阶计算进行了建模,并同时嵌入了按名调用与按值调用的λ演算,以及Moggi的计算元语言和Levy的按推送值调用。本文将该演算从顺序控制流扩展到分支与循环控制流。这使得能够忠实嵌入一个最小但完整的命令式语言,包括条件语句、异常处理和迭代,以及常量和代数数据类型。该演算通过简单的操作语义定义,它扩展了用于λ演算的(简化)Krivine机,通过多个操作数栈来建模效应,并通过一个延续栈来建模顺序、分支和循环计算。它具有一个合流的归约关系和一个简单类型系统,该系统保证了机器的终止性以及归约的强正规化(在无迭代的情况下)。这些性质延续到被嵌入的命令式语言中,从而提供了一个支持简单类型、直接直观的操作语义以及合流归约语义的统一函数式-命令式计算模型。