Simple Derivation Systems for Proving Sufficient Completeness of Non-Terminating Term Rewriting Systems

Kentaro Kikuchi, Takahito Aoto

Research output: Chapter in Book/Report/Conference proceedingConference contributionpeer-review

2 Citations (Scopus)

Abstract

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.

Original languageEnglish
Title of host publication41st IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science, FSTTCS 2021
EditorsMikolaj Bojanczyk, Chandra Chekuri
PublisherSchloss Dagstuhl- Leibniz-Zentrum fur Informatik GmbH, Dagstuhl Publishing
ISBN (Electronic)9783959772150
DOIs
Publication statusPublished - 2021 Dec 1
Event41st IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science, FSTTCS 2021 - Virtual, Online
Duration: 2021 Dec 152021 Dec 17

Publication series

NameLeibniz International Proceedings in Informatics, LIPIcs
Volume213
ISSN (Print)1868-8969

Conference

Conference41st IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science, FSTTCS 2021
CityVirtual, Online
Period21/12/1521/12/17

Keywords

  • Derivation rule
  • Local sufficient completeness
  • Non-termination
  • Sufficient completeness
  • Term rewriting
  • Well-founded induction schema

Fingerprint

Dive into the research topics of 'Simple Derivation Systems for Proving Sufficient Completeness of Non-Terminating Term Rewriting Systems'. Together they form a unique fingerprint.

Cite this