Fast Left Kan Extensions Using The Chase

TL;DR

This paper introduces an optimized chase algorithm for computing left Kan extensions by reducing the problem to free model computation of cartesian theories, demonstrating significant performance improvements.

Contribution

It presents a novel chase-based method for efficiently computing left Kan extensions, with theoretical guarantees and practical performance enhancements.

Findings

Standard and parallel chase are complete algorithms under fairness.

The optimized parallel chase outperforms existing algorithms by an order of magnitude.

The approach bridges category theory and database theory concepts.

Abstract

We show how computation of left Kan extensions can be reduced to computation of free models of cartesian (finite-limit) theories. We discuss how the standard and parallel chase compute weakly free models of regular theories and free models of cartesian theories, and compare the concept of "free model" with a similar concept from database theory known as "universal model". We prove that, as algorithms for computing finite free models of cartesian theories, the standard and parallel chase are complete under fairness assumptions. Finally, we describe an optimized implementation of the parallel chase specialized to left Kan extensions that achieves an order of magnitude improvement in our performance benchmarks compared to the next fastest left Kan extension algorithm we are aware of.