为何无法良性运行？带约束的直接递归规则的非终止分析
编程语言
2017-01-11 v1 计算机科学中的逻辑
软件工程
摘要
本文关注出错的基于规则的程序。规则应用的不期望行为是计算的非终止或失败。我们提出针对约束处理规则(CHR)语言中递归的非终止问题的静态程序分析。CHR是一种涉及约束推理的高级并发声明式语言。它与许多其他基于规则的方法密切相关，因此结果具有更广泛意义。在此类语言中，非终止源于递归规则的无限应用。失败源于计算期间矛盾约束的累积。我们给出带有所谓误行为条件的定理，用于线性直接递归简化规则的潜在非终止与失败（以及确定终止）。递归规则中约束间的逻辑关系在此类程序分析中起关键作用。我们认为该方法可扩展到其他类型递归和更一般规则类。因此本文可作为基础参考和进一步研究的起点。
引用
@article{arxiv.1701.02648,
title = {Why Can't You Behave? Non-termination Analysis of Direct Recursive Rules with Constraints},
author = {Thom Fruehwirth},
journal= {arXiv preprint arXiv:1701.02648},
year = {2017}
}