We study the implementation of four reduction strategies for the untyped λ-calculus in the logic programming language λProlog and restricted sublanguages. The higher-order features of these languages provide very natural methods for manipulating and substituting bound variables. Starting from clear and concise specifications of reduction in the full language we demonstrate how to make certain details in the implementations explicit as we restrict ourselves to the weaker sublanguages. We also show how to translate specifications in a higher-order language to a first-order one, such as Prolog, introducing closures as a replacement for substitutions. This process illustrates how a very high-level description of an implementation can be translated to lower-level ones by reasoning about the logic in which the descriptions are given. It also illustrates some basic methods for manipulating functional languages represented in a higher-order abstract syntax.