A Condensed Goal-Independent Fixpoint Semantics Modeling the Small-Step Behavior of Rewriting

In this paper we present a novel condensed narrowing-like semantics that contains the minimal information which is needed to describe compositionally all possible rewritings of a term rewriting system. We provide its goal-dependent top-down definition and, more importantly, an equivalent goal-independent bottom-up fixpoint characterization.We prove soundness and completeness w.r.t. the small-step behavior of rewriting for the full class of term rewriting systems.