The Functional Machine Calculus (FMC) was recently introduced as a generalization of the lambda-calculus to include higher-order global state, probabilistic and non-deterministic choice, and input and output, while retaining confluence. The calculus can encode both the call-by-name and call-by-value semantics of these effects. This is enabled by two independent generalisations, both natural from the perspective of the FMC's operational semantics, which is given by a simple multi-stack machine. The first generalization decomposes the syntax of the lambda-calculus in a way that allows for sequential composition of terms and the encoding of reduction strategies. Specifically, there exist translations of the call-by-name and call-by-value lambda-calculus which preserve operational semantics. The second parameterizes application and abstraction in terms of 'locations' (corresponding to the multiple stacks of the machine), which gives a unification of the operational semantics, syntax, and reduction rules of the given effects with those of the lambda-calculus. The FMC further comes equipped with a simple type system which restricts and captures the behaviour of effects. This thesis makes two main contributions, showing that two fundamental properties of the lambda-calculus are preserved by the FMC. The first is to show that the categorical semantics of the FMC, modulo an appropriate equational theory, is given by the free Cartesian closed category. The equational theory is validated by a notion of observational equivalence. The second contribution is a proof that typed FMC-terms are strongly normalising. This is an extension (and small simplification) of Gandy's proof for the lambda-calculus, which additionally emphasizes its latent operational intuition.

翻译：函数机器演算（FMC）是近期被引入的，作为lambda演算的推广，它囊括了高阶全局状态、概率与非确定性选择、以及输入输出，同时保留了合流性。该演算能够编码这些效应的按名调用与按值调用语义。这得益于两种独立的推广，二者从FMC操作语义（由简单的多栈机器给出）的角度来看都很自然。第一种推广以允许项的顺序组合与归约策略编码的方式分解了lambda演算的语法。具体而言，存在保持操作语义的按名调用与按值调用lambda演算的翻译。第二种推广则根据“位置”（对应于机器的多个栈）对应用与抽象进行参数化，从而统一了给定效应的操作语义、语法和归约规则与lambda演算的相应部分。FMC还配备了简单的类型系统，用以限制并捕捉效应的行为。本论文做出了两项主要贡献，证明了lambda演算的两个基本性质在FMC中得以保持。第一项贡献是展示了FMC的范畴语义（模适当的等式理论）由自由笛卡尔闭范畴给出。该等式理论通过某种观察等价概念而得到验证。第二项贡献是证明了类型化的FMC项是强规范化的。这是对Gandy的lambda演算证明的扩展（及小幅简化），并额外强调了其潜在的操作直觉。