Compositional Computational Systems

Abstract

We propose a collection of formal definitions for problems and solutions, and study the relationships between the two. Problems and solutions can be represented as morphisms in two categories, and the structure of problem reduction and problem-solving has the properties of a heteromorphic twisted arrow category (a generalization of the twisted arrow category) defined on them. Lagado, a compositional computational system built on a type-theoretic foundation that accounts for the resources required for computation is provided as an example. This thesis furthermore provides the universal conditions for defining any compositional computational system. We argue that any problem can be represented as a function from the product of hom-sets of two semicategories to a rig (a kinded function) and that any procedure can also be represented as a similar kinded function. Combining all problems and procedures defined over the same subcategory of SemiCat via a solution judgment map results in a heteromorphic twisted arrow category called Laputa, which automatically provides problem-reducing and problem-solving properties. The thesis illustrates the practical application of the theory of compositional computations systems by studying the representation of co-design problems from the theory of mathematical co-design as part of several different compositional computations systems. In the process, new results on the conditions for the solvability of co-design problems and their compositional category-theoretical properties are also presented.