Conversion to tail recursion in term rewriting

•We present a transformation of (first-order) rewrite systems to tail recursive form.•This is the first direct, first-order transformation that achieves this conversion.•The transformation can be useful when tail recursive form is required (and also for improving efficiency).

Tail recursive functions are a special kind of recursive functions where the last action in their body is the recursive call. Tail recursion is important for a number of reasons (e.g., they are usually more efficient). In this article, we introduce an automatic transformation of first-order functions into tail recursive form. Functions are defined using a (first-order) term rewrite system. We prove the correctness of the transformation for constructor-based reduction over constructor systems (i.e., typical first-order functional programs).