Colimit-Based Composition of High-Level Computing Devices

TL;DR

This paper introduces a colimit-based compositional framework for high-level computation models that explicitly separates data and control, enabling the construction of complex, correct-by-construction computing devices.

Contribution

It presents a variation of the computon model with new operators, operational semantics, and the first implementation, advancing formal reasoning about large-scale computation.

Findings

Developed a concrete implementation of the computon model

Introduced a new branching operator for the model

Provided operational semantics and an open-source environment

Abstract

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.