Abstract

Skew confluence was introduced as a characterization of non-confluent
term rewriting systems that had unique infinite normal forms or Böhm
like trees. This notion however is not expressive enough to deal with
all possible sources of non-confluence in the context of infinite terms
or terms extended with letrec. We present a new notion called
ω-skew confluence which constitutes a sufficient and necessary
condition for uniqueness. We also present a theory that can lift
uniqueness results from term rewriting systems to rewriting systems on
terms with letrec. We present our results in the setting of Abstract
Böhm Semantics, which is a generalization of Böhm like trees to
abstract reduction systems.

BibTeX

@inproceedings{AB-JWK60,
  author      = "Zena M.\ Ariola and Stefan Blom",
  title       = "Skew and {$\omega$}-Skew Confluence and Abstract B{\"o}hm
                 Semantics",
  booktitle   = "Processes, Terms and Cycles: Steps on the Road to
                 Infinity; Essays Dedicated to Jan Willem Klop, on the
                 Occasion of his 60th Birthday",
  series      = "Lecture Notes in Computer Science",
  volume      = 3838,
  pages       = "368-403",
  publisher   = "Springer-Verlag",
  year        = 2005
}