不返回组合表达式的所有可能的一步缩减-解网

问：

我正在尝试在 Haskell 中实现组合逻辑，目前正在编写一个函数步骤，它使用标准简化规则返回所有可能的一步缩减的列表。当在变量 S （S I）（K I）（S I K） I 上运行 step 函数时，它返回第一个约简的正确表达式，但是当我使用 step （head it）再次约简它时，它只返回一个可能的约简。

这是我的代码

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"

在 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]

Haskell lambda-calculus 组合逻辑

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 _ = []

现在返回您期望的结果，您可以使用和（或）计算约简序列。stepiterateconcatMap=<<

λ 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]

我在这里用来说明，过滤掉重复的解决方案（汇合约简），但我应该指出，它非常低效——不仅因为它本身，还因为生成将被丢弃的项。nubnub

上一个：如何使用 coq 证明定理 euclid_gcd ： forall a b z， euclid a b z -> gcd a b z？

下一个：lambda 演算和函数式编程中的异常处理

不返回组合表达式的所有可能的一步缩减

Not returning all possible one-step reductions for combinatory expressions

评论