CPO Models for Infinite Term Rewriting

Infinite terms in universal algebras are a well-known topic since the seminal work of the ADJ group. The recent interest in the field of term rewriting (TR) for infinite terms is due to the use of term graph rewriting to implement TR, where terms are represented by graphs: so, a cyclic graph is a finitary description of a possibly infinite term. In this paper we introduce infinite rewriting logic, working on the framework of rewriting logic proposed by Jose Meseguer. We provide a simple algebraic presentation of infinite computations, recovering the infinite parallel term rewriting, originally presented by one of the authors to extend the classical, set-theoretical approach to TR with infinite terms. Moreover, we put all the formalism on firm theoretical bases, providing (for the first time, to the best of our knowledge, for infinitary rewriting systems) a clean algebraic semantics by means of (internal) 2-categories.