eng
Schloss Dagstuhl – Leibniz-Zentrum für Informatik
Leibniz International Proceedings in Informatics
1868-8969
2021-11-29
49:1
49:15
10.4230/LIPIcs.FSTTCS.2021.49
article
Simple Derivation Systems for Proving Sufficient Completeness of Non-Terminating Term Rewriting Systems
Kikuchi, Kentaro
1
Aoto, Takahito
2
Tohoku University, Sendai, Japan
Niigata University, Niigata, Japan
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.
https://drops.dagstuhl.de/storage/00lipics/lipics-vol213-fsttcs2021/LIPIcs.FSTTCS.2021.49/LIPIcs.FSTTCS.2021.49.pdf
Term rewriting
Sufficient completeness
Local sufficient completeness
Non-termination
Derivation rule
Well-founded induction schema