TY - GEN
T1 - Simple Derivation Systems for Proving Sufficient Completeness of Non-Terminating Term Rewriting Systems
AU - Kikuchi, Kentaro
AU - Aoto, Takahito
N1 - Funding Information:
This work was partially supported by JSPS KAKENHI Grant Numbers JP17K00005, JP19K11891, JP20H04164 and JP21K11750.
Funding Information:
Funding This work was partially supported by JSPS KAKENHI Grant JP19K11891, JP20H04164 and JP21K11750.
Publisher Copyright:
© Kentaro Kikuchi and Takahito Aoto.
PY - 2021/12/1
Y1 - 2021/12/1
N2 - A term rewriting system (TRS) is said to be sufficiently complete when each function yields some value for any input. Proof methods for sufficient completeness of terminating TRSs have been well studied. In this paper, we introduce a simple derivation system for proving sufficient completeness of possibly non-terminating TRSs. The derivation system consists of rules to manipulate a set of guarded terms, and sufficient completeness of a TRS holds if there exists a successful derivation for each function symbol. We also show that variations of the derivation system are useful for proving special cases of local sufficient completeness of TRSs, which is a generalised notion of sufficient completeness.
AB - A term rewriting system (TRS) is said to be sufficiently complete when each function yields some value for any input. Proof methods for sufficient completeness of terminating TRSs have been well studied. In this paper, we introduce a simple derivation system for proving sufficient completeness of possibly non-terminating TRSs. The derivation system consists of rules to manipulate a set of guarded terms, and sufficient completeness of a TRS holds if there exists a successful derivation for each function symbol. We also show that variations of the derivation system are useful for proving special cases of local sufficient completeness of TRSs, which is a generalised notion of sufficient completeness.
KW - Derivation rule
KW - Local sufficient completeness
KW - Non-termination
KW - Sufficient completeness
KW - Term rewriting
KW - Well-founded induction schema
UR - http://www.scopus.com/inward/record.url?scp=85122422604&partnerID=8YFLogxK
UR - http://www.scopus.com/inward/citedby.url?scp=85122422604&partnerID=8YFLogxK
U2 - 10.4230/LIPIcs.FSTTCS.2021.49
DO - 10.4230/LIPIcs.FSTTCS.2021.49
M3 - Conference contribution
AN - SCOPUS:85122422604
T3 - Leibniz International Proceedings in Informatics, LIPIcs
BT - 41st IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science, FSTTCS 2021
A2 - Bojanczyk, Mikolaj
A2 - Chekuri, Chandra
PB - Schloss Dagstuhl- Leibniz-Zentrum fur Informatik GmbH, Dagstuhl Publishing
T2 - 41st IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science, FSTTCS 2021
Y2 - 15 December 2021 through 17 December 2021
ER -