Consensus-Free Spreadsheet Integration

TL;DR

This paper introduces a category theory-based method for merging multiple spreadsheets without requiring consensus among authors, ensuring semantics preservation and enabling scalable engineering model integration.

Contribution

It presents a novel, formal approach using algebraic theories and category theory to merge spreadsheets without consensus, demonstrated through a real-world engineering case study.

Findings

Successfully integrated two engineering spreadsheets preserving semantics.

Automated theorem proving verified the correctness of the integration.

Method enables scalable, consensus-free engineering model merging.

Abstract

We describe a method for merging multiple spreadsheets into one sheet, and/or exchanging data among the sheets, by expressing each sheet's formulae as an algebraic (equational) theory and each sheet's values as a model of its theory, expressing the overlap between the sheets as theory and model morphisms, and then performing colimit, lifting, and Kan-extension constructions from category theory to compute a canonically universal integrated theory and model, which can then be expressed as a spreadsheet. Our motivation is to find methods of merging engineering models that do not require consensus (agreement) among the authors of the models being merged, a condition fulfilled by our method because theory and model morphisms are semantics-preserving. We describe a case study of this methodology on a real-world oil and gas calculation at a major energy company, describing the theories and models that arise when integrating two different casing pressure test (MASP) calculation spreadsheets constructed by two non-interacting engineers. We also describe the automated theorem proving burden associated with both verifying the semantics preservation of the overlap mappings as well as verifying the conservativity/consistency of the resulting integrated sheet. We conclude with thoughts on how to apply the methodology to scale engineering efforts across the enterprise.