时间扭曲，从代数到算法
Time Warps, from Algebra to Algorithms
摘要：
分级模态在最近的编程语言工作中被提出来作为改进具有内涵属性的类型系统的一般框架。特别地，离散时间尺度的连续内映射或时间扭曲可以用于量化程序执行过程中的信息增长。时间扭曲形成了一个完整的剩余格，在潜在的编程应用中发挥着重要作用的残差。本文研究了时间扭曲的代数结构，并证明了它们的方程理论是可判定的，这是它们在实际编译器中使用的一个必要条件。我们还描述了我们的通用代数证明技术如何适用于一个基于约束的实现，建立一个新的联系之间的泛代数和验证技术。
英文摘要：
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.
机构、总结、中文摘要均由AI分析而来，可能存在错误，请以论文正文为准。
