論文

査読有り 責任著者
2020年12月24日

Stability of termination and sufficient-completeness under pushouts via amalgamation

Theoretical Computer Science
  • Daniel Găină
  • ,
  • Masaki Nakamura
  • ,
  • Kazuhiro Ogata
  • ,
  • Kokichi Futatsugi

848
開始ページ
82
終了ページ
105
記述言語
掲載種別
研究論文(学術雑誌)
DOI
10.1016/j.tcs.2020.09.024

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.

リンク情報
DOI
https://doi.org/10.1016/j.tcs.2020.09.024
DBLP
https://dblp.uni-trier.de/rec/journals/tcs/GainaNOF20
URL
https://dblp.uni-trier.de/db/journals/tcs/tcs848.html#GainaNOF20
Scopus
https://www.scopus.com/inward/record.uri?partnerID=HzOxMe3b&scp=85091071875&origin=inward
Scopus Citedby
https://www.scopus.com/inward/citedby.uri?partnerID=HzOxMe3b&scp=85091071875&origin=inward
ID情報
  • DOI : 10.1016/j.tcs.2020.09.024
  • ISSN : 0304-3975
  • DBLP ID : journals/tcs/GainaNOF20
  • SCOPUS ID : 85091071875

エクスポート
BibTeX RIS