Partial order infinitary term rewriting

TY - JOUR

T1 - Partial order infinitary term rewriting

AU - Bahr, Patrick

PY - 2014/6/3

Y1 - 2014/6/3

N2 - We study an alternative model of infinitary term rewriting. Instead of a metric on terms, a partial order on partial terms is employed to formalise convergence of reductions. We consider both a weak and a strong notion of convergence and show that the metric model of convergence coincides with the partial order model restricted to total terms. Hence, partial order convergence constitutes a conservative extension of metric convergence, which additionally offers a fine-grained distinction between different levels of divergence. In the second part, we focus our investigation on strong convergence of orthogonal systems. The main result is that the gap between the metric model and the partial order model can be bridged by extending the term rewriting system by additional rules. These extensions are the well-known Böhm extensions. Based on this result, we are able to establish that - contrary to the metric setting - orthogonal systems are both infinitarily confluent and infinitarily normalising in the partial order setting. The unique infinitary normal forms that the partial order model admits are Böhm trees.

AB - We study an alternative model of infinitary term rewriting. Instead of a metric on terms, a partial order on partial terms is employed to formalise convergence of reductions. We consider both a weak and a strong notion of convergence and show that the metric model of convergence coincides with the partial order model restricted to total terms. Hence, partial order convergence constitutes a conservative extension of metric convergence, which additionally offers a fine-grained distinction between different levels of divergence. In the second part, we focus our investigation on strong convergence of orthogonal systems. The main result is that the gap between the metric model and the partial order model can be bridged by extending the term rewriting system by additional rules. These extensions are the well-known Böhm extensions. Based on this result, we are able to establish that - contrary to the metric setting - orthogonal systems are both infinitarily confluent and infinitarily normalising in the partial order setting. The unique infinitary normal forms that the partial order model admits are Böhm trees.

U2 - 10.2168/LMCS-10(2:6)2014

DO - 10.2168/LMCS-10(2:6)2014

M3 - Journal article

SN - 1860-5974

VL - 10

JO - Logical Methods in Computer Science

JF - Logical Methods in Computer Science

IS - 2

M1 - 6

ER -