Haskell algorithm to find all possible Beta reductions

Question

I'm trying to come up with an algorithm that would print all available beta reductions for a given expression.

I know I will need a matching pattern cases to see if item is reducible and if not then the three cases cases for variable, lambda and application. I have custom type for these defined as follows:

data Term =
    Variable Var
  | Lambda   Var  Term
  | Apply    Term Term
  deriving Show

Previously I've implemented following methods:

the functionality of the given methods is as follows:

• Merge
• Rename renames to avoid variable capturing
• Substitution reducing the expression
• fresh gives a new variable to which was not previously used
• used returns all used variables for given expression

So far everything works well, however, the function for returning all possible beta reductions is where I'm lost. I've tried to define the four case matching pattern as shown below, however I'm struggling with the definition of the redex case (especially looking into redex for other redex) and the operations which need to take place in the beta method.:

beta :: Term -> [Term]
beta (Variable var) = 
beta (Lambda var term) = 
beta (Apply term1 term2)

I now don't know how to proceed here in order to get all available reductions. The outcome should be:

*Main> Apply (x y)
(\a. \x. (\y. a) x b) (\f. \x. f x)
*Main> beta it
[\c. (\b. \f. \x. f x) c b,(\a. \x. a b) (\f. \x. f x)]

Answer 1

Here's an informal description, as a hint.

beta :: Term -> [Term]
beta (Variable var) = ...

Variables don't beta-reduce, so this case should be easy.

beta (Lambda var term) = ...

Lambdas only reduce if their body reduces. Start with recursing on term.

beta (Apply term1 term2) = ...

This is the complex part: we have three subcases here.

• If term1 reduces, the whole application reduces accordingly.
• If term2 reduces, the whole application reduces accordingly.
• If term1 happens to be a lambda, you have found a redex. You can substitute the abstracted variables in the lambda body with term2.

The whole code could follow this shape:

beta :: Term -> [Term]
beta (Variable var) = ...
beta (Lambda var term) = ...
beta (Apply term1 term2) = term1Moves ++ term2Moves ++ redexMoves
   where
   term1Moves = ...
   term2Moves = ...
   redexMoves = case term1 of
      Lambda var term -> ...
      _               -> []        -- no further moves

List comprehensions could be convenient to use.

---

Taking a part of the code the OP posted, and adding a few more hints, we get:

beta :: Term -> [Term]
beta (Variable var) = ...
beta (Lambda var term) = ...
beta (Apply term1 term2) = term1Moves ++ term2Moves ++ redexMoves
   where
   term1Moves = [ Apply term1' term2 | term1' <- beta term1 ]
   term2Moves = ...
   redexMoves = case term1 of
      Lambda var body -> [substitute var term2 body]  -- don't recurse here
      _               -> []        -- no further moves