A Proof Method for Local Sufficient Completeness of Term Rewriting Systems
A Proof Method for Local Sufficient Completeness of Term Rewriting Systems
复制标题
术语重写系统局部充分完备性的证明方法
DOI：
10.1007/978-3-030-85315-0_22
复制
发表时间：
2021
期刊：
影响因子：
--
通讯作者：
Takahito Aoto
中科院分区：
文献类型：
--
作者：
Tomoki Shiraishi;Kentaro Kikuchi;Takahito Aoto
当每个函数对任何输入都产生一定的值时，术语重写系统（TRS）被认为是足够完整的。本文给出了trs的局部充分完备性的一种证明方法，它是充分完备性概念的推广，对于证明非终止trs的归纳定理是有用的。该证明方法基于由自然数和（可能无限）自然数列表上的函数组成的trs的局部充分完备性的一个充分条件。我们还比较了这两种方法在充分条件下的证明能力和在以前的工作中引入的一个推导系统的证明能力。
A term rewriting system (TRS) is said to be sufficiently complete when each function yields some value for any input. In this paper, we present a proof method for local sufficient completeness of TRSs, which is a generalised notion of sufficient completeness and is useful for proving inductive theorems of non-terminating TRSs. The proof method is based on a sufficient condition for local sufficient completeness of TRSs that consist of functions on natural numbers and (possibly infinite) lists of natural numbers. We also make a comparison between the proof abilities of the methods by the sufficient condition and by a derivation system introduced in previous work.