How to realize LSE narrowing

Narrowing is a complete unification procedure for equational theories defined by canonical term rewriting systems. It is also the operational semantics of various logic and functional programming languages. In Ref. 3), we introduced the LSE narrowing strategy, which is complete for arbitrary canonical rewriting systems and optimal in the sense that two different LSE narrowing derivations cannot generate the same narrowing substitution. LSE narrowing improves all previously known strategies for the class of arbitrary canonical systems. LSE narrowing detects redundant derivations by reducibility tests. According to their definition, LSE narrowing steps seem to be very expensive, because a large number of subterms has to be tested. In this paper, we show that many of these subterms are identical. We describe how left-to-right basic occurrences can be used to identify and exclude these identical subterms. This way, we can drastically reduce the number of subterms that have to be tested. Based on these theoretical results, we develop an efficient implementation of LSE narrowing.