| Summary: | Join-preserving maps on the discrete time scale $\omega^+$, referred to as
time warps, have been proposed as graded modalities that can be used to
quantify the growth of information in the course of program execution. The set
of time warps forms a simple distributive involutive residuated lattice --
called the time warp algebra -- that is equipped with residual operations
relevant to potential applications. In this paper, we show that although the
time warp algebra generates a variety that lacks the finite model property, it
nevertheless has a decidable equational theory. We also describe an
implementation of a procedure for deciding equations in this algebra, written
in the OCaml programming language, that makes use of the Z3 theorem prover.
|
|---|