Deciding Equations in the Time Warp Algebra
Fuente:
arXiv
Saved in:
| Main Authors: | , , , |
|---|---|
| Format: | Preprint |
| Published: |
2023
|
| Subjects: | |
| Online Access: | |
| Tags: |
Add Tag
No Tags, Be the first to tag this record!
|
| _version_ | 1866916347512881152 |
|---|---|
| author | van Gool, Sam Guatto, Adrien Metcalfe, George Santschi, Simon |
| author_facet | van Gool, Sam Guatto, Adrien Metcalfe, George Santschi, Simon |
| contents | 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. |
| format | Preprint |
| id |
arxiv_https___arxiv_org_abs_2302_04668 |
| institution | arXiv |
| publishDate | 2023 |
| record_format | arxiv |
| spellingShingle | Deciding Equations in the Time Warp Algebra van Gool, Sam Guatto, Adrien Metcalfe, George Santschi, Simon Logic in Computer Science Logic 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. |
| title | Deciding Equations in the Time Warp Algebra |
| topic | Logic in Computer Science Logic |
| url | https://arxiv.org/abs/2302.04668 |