Monoidal computer I: Basic computability by string diagrams

TL;DR

This paper introduces a categorical model of computation using monoidal categories and string diagrams, aligning with Church-Turing Thesis and offering an intuitive graphical formalism for reasoning about computability.

Contribution

It presents a new monoidal categorical framework for modeling computation, providing a high-level, implementation-agnostic interface supported by a complete graphical formalism.

Findings

Model conforms to Church-Turing Thesis

Provides a sound and complete graphical formalism

Lays groundwork for high-level programming of computational resources

Abstract

We present a new model of computation, described in terms of monoidal categories. It conforms the Church-Turing Thesis, and captures the same computable functions as the standard models. It provides a succinct categorical interface to most of them, free of their diverse implementation details, using the ideas and structures that in the meantime emerged from research in semantics of computation and programming. The salient feature of the language of monoidal categories is that it is supported by a sound and complete graphical formalism, string diagrams, which provide a concrete and intuitive interface for abstract reasoning about computation. The original motivation and the ultimate goal of this effort is to provide a convenient high level programming language for a theory of computational resources, such as one-way functions, and trapdoor functions, by adopting the methods for hiding the low level implementation details that emerged from practice. In the present paper, we make a first step towards this ambitious goal, and sketch a path to reach it. This path is pursued in three sequel papers, that are in preparation.