Abstract
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.
This is a preview of subscription content, log in via an institution to check access.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Similar content being viewed by others
References
Baader, F., Nipkow, T.: Term Rewriting and All That. Cambridge University Press, Cambridge (1998)
Comon, H., Jacquemard, F.: Ground reducibility is EXPTIME-complete. Inf. Comput. 187(1), 123–153 (2003)
Geser, A.: Relative termination. Ph.D. thesis, Universität Passau (1990). Available as technical report 91–03
Gnaedig, I., Kirchner, H.: Computing constructor forms with non terminating rewrite programs. In: Proceedings of the 8th PPDP, pp. 121–132. ACM (2006)
Gnaedig, I., Kirchner, H.: Proving weak properties of rewriting. Theoret. Comput. Sci. 412(34), 4405–4438 (2011)
Guttag, J.V.: The specification and application to programming of abstract data types. Ph.D. thesis, University of Toronto (1975)
Guttag, J.V., Horning, J.J.: The algebraic specification of abstract data types. Acta Inf. 10(1), 27–52 (1978)
Hirokawa, N., Middeldorp, A.: Decreasing diagrams and relative termination. J. Autom. Reason. 47(4), 481–501 (2011)
Kapur, D., Narendran, P., Zhang, H.: On sufficient-completeness and related properties of term rewriting systems. Acta Inf. 24(4), 395–415 (1987)
Kikuchi, K., Aoto, T., Sasano, I.: Inductive theorem proving in non-terminating rewriting systems and its application to program transformation. In: Proceedings of the 21st PPDP, pp. 13:1–13:14. ACM (2019)
Lazrek, A., Lescanne, P., Thiel, J.J.: Tools for proving inductive equalities, relative completeness, and \(\omega \)-completeness. Inf. Comput. 84(1), 47–70 (1990)
Lucas, S.: Context-sensitive computations in functional and functional logic programs. J. Funct. Log. Programm. 1998(1) (1998)
Nakamura, M., Ogata, K., Futatsugi, K.: Reducibility of operation symbols in term rewriting systems and its application to behavioral specifications. J. Symb. Comput. 45(5), 551–573 (2010)
Terese: Term Rewriting Systems. Cambridge University Press (2003)
Toyama, Y.: How to prove equivalence of term rewriting systems without induction. Theoret. Comput. Sci. 90(2), 369–390 (1991)
Acknowledgements
We are grateful to the anonymous referees for valuable comments. This work was partly supported by JSPS KAKENHI Grant Numbers JP19K11891, JP20H04164 and JP21K11750.
Author information
Authors and Affiliations
Corresponding author
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2021 Springer Nature Switzerland AG
About this paper
Cite this paper
Shiraishi, T., Kikuchi, K., Aoto, T. (2021). A Proof Method for Local Sufficient Completeness of Term Rewriting Systems. In: Cerone, A., Ölveczky, P.C. (eds) Theoretical Aspects of Computing – ICTAC 2021. ICTAC 2021. Lecture Notes in Computer Science(), vol 12819. Springer, Cham. https://doi.org/10.1007/978-3-030-85315-0_22
Download citation
DOI: https://doi.org/10.1007/978-3-030-85315-0_22
Published:
Publisher Name: Springer, Cham
Print ISBN: 978-3-030-85314-3
Online ISBN: 978-3-030-85315-0
eBook Packages: Computer ScienceComputer Science (R0)