逻辑程序自动终止分析的一般框架
编程语言
2020-06-11 v1
摘要
本文描述一个逻辑程序自动终止分析的一般框架，其中我们将“终止”理解为针对程序与给定查询所构造的 LD 树的有限性。证明了从无限 LD 树的某个分支子集到有限集的映射的一般性质。由此结果出发，通过使用不同有限集推导出若干终止定理。前两个针对谓词依赖与原子依赖图表述。随后证明关于程序相关的查询-映射对的一般结果（参见 \cite{Sagiv,Lindenstrauss:Sagiv}）。\cite{Lindenstrauss:Sagiv:Serebrenik} 中描述的 {\em TermiLog} 系统的正确性由此得出。该系统无法证明涉及算术谓词程序的终止，因为整数的通常序非良基。本文提出一种可轻易纳入 {\em TermiLog} 或类似系统的新方法，使涉及算术谓词程序的终止得以证明。它基于将整数的有限抽象与查询-映射对技术相结合，本质上能将终止证明分为若干情形，使每情形仅需简单终止函数。最后概述若干可能扩展。
引用
@article{arxiv.cs/0012008,
title = {A General Framework for Automatic Termination Analysis of Logic Programs},
author = {Nachum Dershowitz and Naomi Lindenstrauss and Yehoshua Sagiv and Alexander Serebrenik},
journal= {arXiv preprint arXiv:cs/0012008},
year = {2020}
}