Logo
ScienceStack
Table of Contents
Fetching ...
Sign In

Deciding Equations in the Time Warp Algebra

Sam van Gool, Adrien Guatto, George Metcalfe, Simon Santschi

TL;DR

This work establishes the decidability of the equational theory of the time warp algebra $\\mathbf W$, the involutive residuated lattice of join-preserving maps on $\\omega^+$. By introducing an elegant normal form using the predecessor operator $p$ and associating $\\mathbf W$ with an involutive residuated lattice via $f^\\star = f\\backslash p$, the authors reduce equation satisfaction to finite "diagrams" and a first-order satisfiability problem over $\\omega^+$. They further show the equational theory of $\\mathbf W$ coincides with that of a regular subalgebra $\\mathbf R$, enabling a practical decision procedure implemented in OCaml that leverages Z3. The results enable reliable reasoning about graded modalities in programming languages and suggest extensions to definable constants and relational semantics for these algebras.

Abstract

Join-preserving maps on the discrete time scale $ω^+$, 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.

Deciding Equations in the Time Warp Algebra

TL;DR

This work establishes the decidability of the equational theory of the time warp algebra , the involutive residuated lattice of join-preserving maps on . By introducing an elegant normal form using the predecessor operator and associating with an involutive residuated lattice via , the authors reduce equation satisfaction to finite "diagrams" and a first-order satisfiability problem over . They further show the equational theory of coincides with that of a regular subalgebra , enabling a practical decision procedure implemented in OCaml that leverages Z3. The results enable reliable reasoning about graded modalities in programming languages and suggest extensions to definable constants and relational semantics for these algebras.

Abstract

Join-preserving maps on the discrete time scale , 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.
Paper Structure (5 sections, 19 theorems, 44 equations, 3 figures)

This paper contains 5 sections, 19 theorems, 44 equations, 3 figures.

Table of Contents

  1. Introduction
  2. The Time Warp Algebra
  3. Decidability via Diagrams
  4. Implementation
  5. Concluding Remarks

Key Result

Lemma 2.1

[lem]lem:normal There exists an algorithm that produces for any term $t\in{\rm Tm}$ positive integers $m,n_1,\dots,n_m$ and basic terms $t_{i,j}$ for each $i\in\{1,\dots,m\}$ and $j\in\{1,\dots,n_i\}$ such that for any fully distributive involutive residuated lattice ${\bf {L}}$,

Figures (3)

  • Figure 1: Visualization of the saturation of $\{{x{x}'}[{\kappa}] \}$
  • Figure 2: Visualization of the extension of $\lfloor {x} \rfloor_{\delta}$
  • Figure 3: SMT query whose models correspond to diagrams for $\textrm{e}\le x$

Theorems & Definitions (34)

  • Lemma 2.1
  • proof
  • Proposition 2.2
  • proof
  • Lemma 2.3
  • proof
  • Proposition 2.4
  • proof
  • Proposition 2.5
  • proof
  • ...and 24 more