Stability of termination and sufficient-completeness under pushouts via amalgamation

Daniel Găină, Masaki Nakamura, Kazuhiro Ogata, Kokichi Futatsugi

Research output: Contribution to journalArticlepeer-review

Abstract

In the present study, we provide conditions for the existence of pushouts of signature morphisms in constructor-based order-sorted algebra, and then we prove that reducibility and termination of term rewriting systems are closed under pushouts. Under the termination assumption, reducibility is equivalent to sufficient-completeness, which is crucial for proving several important properties in computing for constructor-based logics such as completeness, existence of initial models and interpolation. In logic frameworks that are not based on constructors, sufficient-completeness is essential to establish the soundness of the induction schemes which are based on some methodological constructor operators. We discuss the application of our results to the instantiation of parameterized specifications.

Original languageEnglish
Pages (from-to)82-105
Number of pages24
JournalTheoretical Computer Science
Volume848
DOIs
Publication statusPublished - Dec 24 2020

All Science Journal Classification (ASJC) codes

  • Theoretical Computer Science
  • Computer Science(all)

Fingerprint Dive into the research topics of 'Stability of termination and sufficient-completeness under pushouts via amalgamation'. Together they form a unique fingerprint.

Cite this