2020年12月24日
Stability of termination and sufficient-completeness under pushouts via amalgamation
Theoretical Computer Science
- ,
- ,
- ,
- 巻
- 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