Productivity of Non-Orthogonal Term Rewrite Systems

TL;DR

This paper extends the concept of productivity in term rewrite systems to non-orthogonal systems, showing that context-sensitive termination implies productivity and applying this to digital circuit stabilization.

Contribution

It introduces techniques to prove productivity in non-orthogonal systems, linking it to context-sensitive termination, which was previously only considered for orthogonal systems.

Findings

Productivity can be proved for non-orthogonal systems using context-sensitive termination.

Any outermost-fair reduction computes an infinite constructor term in the limit.

Application to stabilization of digital circuits demonstrated.

Abstract

Productivity is the property that finite prefixes of an infinite constructor term can be computed using a given term rewrite system. Hitherto, productivity has only been considered for orthogonal systems, where non-determinism is not allowed. This paper presents techniques to also prove productivity of non-orthogonal term rewrite systems. For such systems, it is desired that one does not have to guess the reduction steps to perform, instead any outermost-fair reduction should compute an infinite constructor term in the limit. As a main result, it is shown that for possibly non-orthogonal term rewrite systems this kind of productivity can be concluded from context-sensitive termination. This result can be applied to prove stabilization of digital circuits, as will be illustrated by means of an example.