Confluence by Critical Pair Analysis Revisited (Extended Version)
classification
💻 cs.LO
cs.SC
keywords
confluencesubsystemterminatingallowinganalysisboilclosednesscombining
read the original abstract
We present two methods for proving confluence of left-linear term rewrite systems. One is hot-decreasingness, combining the parallel/development closedness theorems with rule labelling based on a terminating subsystem. The other is critical-pair-closing system, allowing to boil down the confluence problem to confluence of a special subsystem whose duplicating rules are relatively terminating.
This paper has not been read by Pith yet.
discussion (0)
Sign in with ORCID, Apple, or X to comment. Anyone can read and Pith papers without signing in.