非表示:
キーワード:
-
要旨:
Narrowing is a universal unification procedure for equational theories given by a canonical term rewrite system. In this paper we introduce conditional narrowing modulo a set of conditional equations and give a full proof of its correctness and completeness for equational conditional rewrite systems R,E without extravariables where E is regular and R,E is Church‐Rosser modulo E and decrasing modulo E. This result can be seen as the theoretical foundation of a special form of constraint logic and functional programming.
