Haskell组合子逻辑step函数未返回全部一步归约结果问题

你的step函数存在两个核心问题，导致无法生成所有合法的一步归约结果：

1. 完全应用组合子的处理不完整 #

对于I、K、S的完全应用（即形成可归约式redex的情况），你只处理了顶层归约，没有包含子表达式内部的redex归约。例如：

• 对于K :@ x :@ y，除了顶层归约为x，还应该允许归约x或y内部的redex，生成K :@ x' :@ y或K :@ x :@ y'；
• 对于S :@ x :@ y :@ z，除了顶层归约为x :@ z :@ (y :@ z)，还需要处理x、y、z内部的redex归约。

2. 错误的同时归约逻辑 #

在处理普通应用式c :@ d时，你加入了同时归约c和d的情况（[c' :@ d' | c' <- step c, d' <- step d]），但一步归约的定义是仅归约一个redex，同时修改两个redex不属于一步归约的范畴，这部分需要删除。

修正后的代码 #

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]
-- I的一步归约：顶层归约 + x内部归约
step (I :@ x) = [x] ++ [I :@ x' | x' <- step x]
-- K的一步归约：顶层归约 + x内部归约 + y内部归约
step (K :@ x :@ y) = [x] ++ [K :@ x' :@ y | x' <- step x] ++ [K :@ x :@ y' | y' <- step y]
-- S的一步归约：顶层归约 + x/y/z内部归约
step (S :@ x :@ y :@ z) = [x :@ z :@ (y :@ z)] ++ 
                          [S :@ x' :@ y :@ z | x' <- step x] ++ 
                          [S :@ x :@ y' :@ z | y' <- step y] ++ 
                          [S :@ x :@ y :@ z' | z' <- step z]
-- 普通应用式：仅归约c内部 或 d内部
step (c :@ d) = [c' :@ d | c' <- step c] ++ [c :@ d' | 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"

测试验证 #

修正后在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]

结果与你的预期完全一致。

内容的提问来源于stack exchange，提问作者idkDude