首页 | 本学科首页   官方微博 | 高级检索  
     


On modularity in infinitary term rewriting
Affiliation:Department of Computer Science, University of Copenhagen (DIKU), Universitetsparken 1, DK-2100 Copenhagen Ø, Denmark
Abstract:We study modular properties in strongly convergent infinitary term rewriting. In particular, we show that:
  • •Confluence is not preserved across direct sum of a finite number of systems, even when these are non-collapsing.
  • •Confluence modulo equality of hypercollapsing subterms is not preserved across direct sum of a finite number of systems.
  • •Normalization is not preserved across direct sum of an infinite number of left-linear systems.
  • •Unique normalization with respect to reduction is not preserved across direct sum of a finite number of left-linear systems.
Together, these facts constitute a radical departure from the situation in finitary term rewriting. Positive results are:
  • •Confluence is preserved under the direct sum of an infinite number of left-linear systems iff at most one system contains a collapsing rule.
  • •Confluence is preserved under the direct sum of a finite number of non-collapsing systems if only terms of finite rank are considered.
  • •Top-termination is preserved under the direct sum of a finite number of left-linear systems.
  • •Normalization is preserved under the direct sum of a finite number of left-linear systems.
All of the negative results above hold in the setting of weakly convergent rewriting as well, as do the positive results concerning modularity of top-termination and normalization for left-linear systems.
Keywords:
本文献已被 ScienceDirect 等数据库收录!
设为首页 | 免责声明 | 关于勤云 | 加入收藏

Copyright©北京勤云科技发展有限公司  京ICP备09084417号