Stepwise Refinement of an Abstract State Machine for WHNF-Reduction of LambdaTerms

摘要

In this paper the authors present a series consisting of three abstract statemachines (ASMs) for the problem of finding the weak head normal form (WHNF) of an arbitrary term of the pure lambda-calculus. The authors use a method of stepwise refinement in which three stages of refinement are clearly distinguished. In the first stage an ASM is constructed which is a high-level specification of the problem. From this ASM a second ASM is derived by refinement of static functions. Finally, the third ASM is obtained from the second by a refinement replacing static universes by dynamic ones. The adequacy of each refinement is assessed. Both kinds of refinement provide further experience with hierarchical ASM design by stepwise refinement.