Jungle Rewriting: an Abstract Description of a Lazy Narrowing Machine

We propose to use Jungle Rewriting, a graph rewriting formalism, as a formal specification tool for the LANAM, an abstract machine implementing lazy narrowing. Three jungle rewriting systems which model a narrowing program at different levels of abstraction are presented. The first system is proved to be essentially equivalent (from an operational point of view) to the given program. The second one contains only rules which correspond to elementary actions of a narrowing interpreter, while the third one also models the control issues of the abstract machine. We formally prove the equivalence of the first and second systems, while the relationship between the second and the third one is sketched. The last system provides an abstract description of the compiled code of the LANAM, which is outlined