Transfinite Rewriting Semantics for Term Rewriting Systems
Author
Salvador Lucas
Abstract
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.
Keywords
Declarative programming, semantics,
infinitary rewriting.