Stability of termination and sufficient-completeness under pushouts via amalgamation

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

研究成果: ジャーナルへの寄稿学術誌査読

1 被引用数 (Scopus)

抄録

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.

本文言語英語
ページ(範囲)82-105
ページ数24
ジャーナルTheoretical Computer Science
848
DOI
出版ステータス出版済み - 12月 24 2020

!!!All Science Journal Classification (ASJC) codes

  • 理論的コンピュータサイエンス
  • コンピュータ サイエンス(全般)

フィンガープリント

「Stability of termination and sufficient-completeness under pushouts via amalgamation」の研究トピックを掘り下げます。これらがまとまってユニークなフィンガープリントを構成します。

引用スタイル