Colimit-Based Composition of High-Level Computing Devices

TL;DR

A variation of the computon model is provided to enable functional computing devices, a new branching operator is introduced, how to define synchronous parallelising out of sequencing and asynchronous parallelising is discussed, concrete operational semantics for computon execution are described and the first implementation of the model is provided.

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.

Figures (3)

• Figure 1: Partial and total sequencing. Control ports are not $0$-labelled for clarity.
• Figure 2: Examples of asynchronous and synchronous parallelising.
• Figure 3: Open and closed branching. Here, the wavy arrow is not a morphism, but it expresses the operation ${\lambda_3+_{\lambda_0+\lambda_1}\lambda_5}$ to form the closed branching computon ${\lambda_3??_{\rho_2}\lambda_5}$ from the b-diagram $\rho_2$ shown on the left of (b). The open branching computon ${\lambda_3?_{\rho_1}\lambda_4}$ is just the pushout of the span $\rho_1$ of in-markers ${\lambda_3^+}$ and ${\lambda_4^+}$.

Theorems & Definitions (63)

• definition 1
• definition 2: Computon Interface
• definition 3: Connected Computon
• proposition 1
• proof
• definition 4
• definition 5
• proposition 2
• proof
• definition 6: Computon Morphism