This paper formalizes term rewriting systems (TRSs), called
scoped, in which a rewrite rule can be nested within another
rewrite rule.  The right-hand side and/or the condition of a
nested rule can refer to any variable in the left-hand side of a
nesting rule.  Nesting of rewrite rules is intended to define a
lexical scope with static binding.  Our work is applicable to
programming languages in which programs are modeled by TRSs and
computations are executed by rewriting or narrowing.  In
particular, we consider a class of non-confluent and
non-terminating TRSs well suited for modeling modern functional
logic programs.  We describe an abstract implementation of
rewriting and narrowing for scoped TRSs to show that scopes can be
easily handled irrespective of the evaluation strategy.  The
efficiency of rewriting within a scoped TRS, measured using a
narrowing virtual machine, is comparable to the efficiency of
rewriting for non-scoped TRSs.