Not returning all possible one-step reductions for combinatory expressions

Question

I'm trying to implement combinatory logic in Haskell, and am currently writing a function step, which returns a list of all possible one step reductions using the standard reduction rules. When running the step function on the variable S (S I) (K I) (S I K) I, it returns the correct expression for the first reduction, but when I reduce it again with step (head it) it returns only one of the possible reductions.

This is my code

module Main where

 data Combinator
  = I
  | K
  | S
  | V String
  | Combinator :@ Combinator
  deriving (Eq, Ord)

instance Show Combinator where
  show = f 0
    where
      f _ I = "I"
      f _ K = "K"
      f _ S = "S"
      f _ (V s) = s
      f i (c :@ d) = if i == 1 then "(" ++ s ++ ")" else s where s = f 0 c ++ " " ++ f 1 d

step :: Combinator -> [Combinator]
step (I :@ x) = [x]
step (K :@ x :@ y) = [x]
step (S :@ x :@ y :@ z) = [x :@ z :@ (y :@ z)]
step (c :@ d) = [c' :@ d | c' <- step c] ++ [c :@ d' | d' <- step d] ++ 
[c' :@ d' | c' <- step            c, d' <- step d]
step _ = []

parse :: String -> Combinator
parse s = down [] s
  where
    down [] (' ' : str) = down [] str
    down cs ('(' : str) = down (Nothing : cs) str
    down cs ('I' : str) = up cs I str
    down cs ('K' : str) = up cs K str
    down cs ('S' : str) = up cs S str
    down cs (c : str) = up cs (V [c]) str
    up [] c [] = c
    up (Just c : cs) d str = up cs (c :@ d) str
    up (Nothing : cs) d (')' : str) = up cs d str
    up cs d str = down (Just d : cs) str

main :: IO ()
main = do
  putStrLn $ "Combinatory Logic in Haskell"

I am aiming for this when running in GHCi-

*Main> parse "S(SI)(KI)(SIK)I"
S (S I) (K I) (S I K) I
*Main> step it
[S I (S I K) (K I (S I K)) I]
*Main> step (head it)
[ I (K I (S I K)) (S I K (K I (S I K))) I, S I (S I K) I I ]

I am getting -

ghci> parse "S(SI)(KI)(SIK)I"
S (S I) (K I) (S I K) I
ghci> step it
[S I (S I K) (K I (S I K)) I]
ghci> step (head it)
[I (K I (S I K)) (S I K (K I (S I K))) I]

Answer 1

The cases

step (I :@ x) = [x]
step (K :@ x :@ y) = [x]
step (S :@ x :@ y :@ z) = [x :@ z :@ (y :@ z)]

do not allow reductions within x, y, or z.

Note that the more general equation step (c :@ d) is not considered when we fall in one of the above cases.

Finally, I'm not sure if you really want [c' :@ d' | c' <- step c, d' <- step d] since that will perform two parallel steps.

Answer 2

[ I (K I (S I K)) (S I K (K I (S I K))) I, S I (S I K) I I ]

This implies step ((S :@ x :@ y :@ z) :@ I) should produce [s :@ I | s <- step (S :@ x :@ y :@ z)], which it does, by the last equation of step. However, if you want to explore only one step at a time, you should skip the [c' :@ d' | …] part of this equation, since it makes two steps in parallel.

It also implies step (S :@ x :@ y :@ z) should produce [S :@ x :@ y :@ z' | z' <- step z], yet it doesn’t, because this is already matched by the third (S) equation of step.

In other words, your evaluator is slightly too lazy: it omits some of the steps that would be done by eager evaluation of arguments, since it only evaluates arguments if a call isn’t fully saturated.

One possible solution is to always visit each subexpression, even if reducing the whole application is possible; and separately consider whether the whole expression is reducible. This is perhaps easier to get right if we make step always step exactly once, returning an empty list if there is no single-step reduction.

step (f :@ z) = outer ++ left ++ right
  where

    --       I   z ~> z
    -- (  K   y) z ~> y
    -- ((S x) y) z ~> xz(yz)
    outer = case f of
      I -> [z]
      K :@ y -> [y]
      S :@ x :@ y -> [(x :@ z) :@ (y :@ z)]
      _ -> []

    --   f ~> f'
    -- -----------
    -- f z ~> f' z
    left = [f' :@ z | f' <- step f]

    --   z ~> z'
    -- -----------
    -- f z ~> f z'
    right = [f :@ z' | z' <- step z]    

step _ = []

Now step returns the result you expected, and you can compute the sequence of reductions using iterate and concatMap (or =<<).

λ import Data.List (nub)

λ reductions input = iterate (nub . concatMap step) [parse input]

λ import Data.Foldable (traverse_)

λ traverse_ print $ takeWhile (not . null) $ reductions "K(I(K(Ia)))bc"

[K (I (K (I a))) b c]
[I (K (I a)) c,K (K (I a)) b c,K (I (K a)) b c]
[K (I a) c,I (K a) c,K (K a) b c]
[I a,K a c]
[a]

I use nub here for illustration, to filter out duplicate solutions (confluent reductions), but I should point out that it’s very inefficient—not only because of nub itself, but also because of generating terms that will be discarded.