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.

CPO Models for Infinite Term Rewriting

CORRADINI, ANDREA;GADDUCCI, FABIO
1995-01-01

Abstract

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.
1995
3540600434
File in questo prodotto:
Non ci sono file associati a questo prodotto.

I documenti in IRIS sono protetti da copyright e tutti i diritti sono riservati, salvo diversa indicazione.

Utilizza questo identificativo per citare o creare un link a questo documento: https://hdl.handle.net/11568/182440
 Attenzione

Attenzione! I dati visualizzati non sono stati sottoposti a validazione da parte dell'ateneo

Citazioni
  • ???jsp.display-item.citation.pmc??? ND
  • Scopus 10
  • ???jsp.display-item.citation.isi??? 6
social impact