CODEWITHSUNDEEP
haskellfunctional-programminglambda-calculus
user158083
user158083

Reputation: 59

Haskell code for one step redex of abstract machine?

What should be the type of a single-step reduction function for an abstract machine? x -> Maybe x or x -> x?

Given such a single-step reduction function, how would one write the multi-step reduction function that gives the normal form of an input term?

Upvotes: 1

Views: 430

Answers (1)

Jonathan Cast
Jonathan Cast

Reputation: 4635

Normally, you want the single-step reduction function to have type T -> Maybe T. Then, for redexes you return a Just, and for normal forms you return Nothing. This follows a general principle that functions should return as much of the information they compute to the caller as possible, which helps reduce re-computation in your program.

If your single-step reduction function is singleStepReduce :: T -> T, it has two choices when given an argument which is already in normal form:

  • Return the argument. This requires the caller to do something like x == singleStepReduce x or isNF x to determine if the argument is in NF; this is information singleStepReduce is already determining, so it's wasted computation; furthermore, x == singleStepReduce x is very computationally expensive, while isNF x still duplicates that determination and allows the rules for reduction and the rules for determining normal forms to fall out of step, which violates basic software engineering principles.
  • Return undefined. This is worse; it means the caller has no way to recover from the normal-form case, forcing the caller to use isNF x before calling singleStepReduce x, and leaving the problem that the definitions of isNF x and singleStepReduce x implement overlapping logic unsolved.

Implementing a multi-step reducer, provided you're ok with the reducer going into an infinite loop on terms that lack a normal form, is then pretty simple:

multiStepReduce :: (a -> Maybe a) -> a
multiStepReduce r x = case r x of
    Nothing -> x
    Just y -> multiStepReduce r y

Upvotes: 2

Related Questions