Transfinite Rewriting Semantics for Term Rewriting Systems


Salvador Lucas


We provide some new results concerning the use of transfinite rewriting for giving semantics to rewrite systems. We especially (but not only) consider the computation of possibly infinite constructor terms by transfinite rewriting due to their interest in many programming languages. We reconsider the problem of compressing transfinite rewrite sequences into shorter (possibly finite) ones. We also investigate the role that (finitary) confluence plays in transfinite rewriting. We consider different (quite standard) rewriting semantics (mappings from input terms to sets of reducts obtained by --transfinite-- rewriting) in a unified framework and investigate their algebraic structure. Such a framework is used to formulate, connect, and approximate different properties of TRSs.


Declarative programming, semantics, infinitary rewriting.