The paper provides a mathematical model for the innermost version of the functional logic programming
language BABEL [MR89, MR92] and refines it stepwise towards a mathematical specification of its implementation
by a graph-narrowing machine [KLMR90]. Our description directly reflects the basic intuitions
underlying the language and can thus be used as a primary mathematical definition of innermost BABEL.
For each refinement step a mathematical correctness proof is given, thus paving the way for a correctness
proof of the graph-narrowing machine implementation (a full correctness proof could be achieved by providing
some further refinement steps, leading to the machine's abstraction level). The specification uses evolving
algebras, thus allowing the descriptions to be procedural and nevertheless abstract, readable as `pseudocode
over abstract data'.