时间扭曲代数中方程的可判定性
Deciding Equations in the Time Warp Algebra
AI总结：
本文证明时间扭曲代数虽缺乏有限模型性质，但其等式理论可判定，并给出了基于 OCaml 和 Z3 的判定过程实现。
摘要：
离散时间尺度 $ω^+$ 上的保并映射被称为时间扭曲（time warps），已被提出作为分级模态，可用于量化程序执行过程中信息的增长。时间扭曲的集合构成一个简单的分配对合剩余格——称为时间扭曲代数——并配备有与潜在应用相关的剩余运算。在本文中，我们证明，尽管时间扭曲代数生成的簇缺乏有限模型性质，但它仍然具有可判定的等式理论。我们还描述了该代数中方程判定过程的一个实现，该实现使用 OCaml 编程语言编写，并利用了 Z3 定理证明器。
英文摘要：
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.
机构、总结、中文摘要均由AI分析而来，可能存在错误，请以论文正文为准。
