Time Warps, from Algebra to Algorithms

TL;DR

This paper explores the algebraic structure of time warps, a concept used to measure information growth in programs, proving their algebraic properties and decidability, and linking universal algebra to verification techniques.

Contribution

It provides a detailed algebraic analysis of time warps, proves the decidability of their equational theory, and introduces a universal-algebraic approach to verification.

Findings

Time warps form a complete residuated lattice.

The equational theory of time warps is decidable.

A new link between universal algebra and verification is established.

Abstract

Graded modalities have been proposed in recent work on programming languages as a general framework for refining type systems with intensional properties. In particular, continuous endomaps of the discrete time scale, or time warps, can be used to quantify the growth of information in the course of program execution. Time warps form a complete residuated lattice, with the residuals playing an important role in potential programming applications. In this paper, we study the algebraic structure of time warps, and prove that their equational theory is decidable, a necessary condition for their use in real-world compilers. We also describe how our universal-algebraic proof technique lends itself to a constraint-based implementation, establishing a new link between universal algebra and verification technology.