A Condensed Goal-Independent Fixpoint Semantics Modeling the Small-Step Behavior of Rewriting
Marco Comini, Luca Torella · EPiC series in computing · 2018
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.