Models of High-level Computation (MHCs) provide effective means to describe complex real-world computing systems because they offer formal foundations for the specification of interacting computing devices, as opposed to describing individual ones, which has been the focus of classical models such as Turing machines or the lambda calculus. Despite numerous proposals over the past half century, there is still no canonical MHC akin to Turing machines for (compositionally) reasoning about computation in the large. One of the major drawbacks of current MHCs is that they extensively neglect control flow, a well-know semantic property that defines computation order. Only a few MHCs treat control explicitly at the expense of assuming that data follows control. Mixing such dimensions within the same framework leads to inefficient methods for formal analysis and verification. To address this, the computon model has recently emerged as a category-theoretic MHC that separates data and control and makes control explicit by supporting composition operators characterised as finite colimit constructions. Such constructions allow the formation of sequential, parallel, branching and iterative computing devices. Unfortunately, the computon model is still a generic reference rather than a concrete realisation. In this paper, we provide a variation of it to enable functional computing devices, introduce a new branching operator, discuss how to define synchronous parallelising out of sequencing and asynchronous parallelising, describe concrete operational semantics for computon execution and provide the first implementation of the model. The implementation yields an open-source programming environment that realises the underlying categorical semantics. This tool is publicly available and ready to build complex computing devices that are structurally correct by construction.

翻译：高层计算模型为描述复杂的现实世界计算系统提供了有效手段，因为它们为交互计算设备的规范提供了形式化基础，而非像图灵机或λ演算等经典模型那样侧重于描述单个设备。尽管过去半个世纪提出了众多方案，目前仍缺乏类似于图灵机的标准高层计算模型来（组合式地）推理宏观计算。现有高层计算模型的主要缺陷在于普遍忽视了控制流——这一定义计算顺序的经典语义属性。仅有少数模型以假定数据跟随控制为代价显式处理控制。将这两个维度混合在同一框架中会导致形式化分析与验证方法的低效。为此，计算子模型近期作为一种范畴论高层计算模型应运而生，它通过支持以有限余极限构造为特征的组合算子，实现了数据与控制的分离，并使控制显式化。此类构造支持形成顺序、并行、分支及迭代的计算设备。然而计算子模型目前仍是通用参考框架而非具体实现。本文提出其变体以实现函数式计算设备，引入新的分支算子，阐述如何从顺序化与异步并行化中定义同步并行化，描述计算子执行的具体操作语义，并提供该模型的首次实现。该实现产生了一个实现底层范畴语义的开源编程环境。该工具已公开可用，能够直接构建结构正确的复杂计算设备。