Context-Sensitive Computations in Confluent Programs

摘要

Context-sensitive rewriting is a refined form of rewriting which explores a smaller reduction space by imposing some fixed restrictions on the replacements. Any Term Rewriting System (TRS) can be given a context-sensitive rewrite relation. In this paper, we formulate conditions to guarantee the confluence of this relation. Moreover, for a confluent TRS, we are able to give sufficient conditions to ensure that the (eventually obtained) computed value of a given expression can be reached by using context-sensitive rewriting, thus leading to more efficient and still complete computations.