非表示:
キーワード:
-
要旨:
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 an earlier paper, 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.
