Dependency pairs for proving termination properties of conditional term rewriting systems

详细信息    查看全文

• 作者：Salvador Lucas^a ; ^{slucas@dsic.upv.es} ; José ; Meseguer^b
• 关键词：Conditional term rewriting ; Dependency pairs ; Program analysis ; Operational termination
• 刊名：Journal of Logical and Algebraic Methods in Programming
• 出版年：2017
• 出版时间：January 2017
• 年：2017
• 卷：86
• 期：1
• 页码：236-268
• 全文大小：847 K
• 卷排序：86

文摘

We characterize operational termination of CTRSs as the conjunction of termination and a new termination property of CTRSs that we call V-termination. We identify termination and V-termination as two sources (or dimensions) of operational termination of CTRSs. We introduce several notions of dependency pairs that make the bidimensional nature of operational termination explicit. We provide a characterization of termination, V-termination, and operational termination of CTRSs using our dependency pairs and appropriate notions of chains of such dependency pairs. We show that termination, V-termination and operational termination can be (dis)proved using our dependency pairs and a single kind of chains.