高阶LCTRS及其终止
摘要：逻辑约束的术语重写系统（LCTRSs）是一种程序分析形式化工具，具有本机对非（协同）归纳定义的数据类型的支持。作为一种一阶形式，LCTRSs目前仅适用于对命令式程序进行分析。在本文中，我们提出了一种LCTRS形式化工具的高阶变种，可用于分析函数式程序。然后，我们研究了终止问题，并为这个新形式化工具定义了一个高阶递归路径排序（HORPO）。
作者：Liye Guo and Cynthia Kop
论文ID：2307.13519
分类：Logic in Computer Science
分类简称：cs.LO
提交时间：2023-07-26