离散程序搜索的Haskell实现优化验证：是否存在更优方案？

我正在研究如何通过最优评估优化离散程序搜索，目前得到一个看似高效的简单方案。基于以下测试用例：

f 1001101110 = 1010100110
f 0100010100 = 1001101001

搜索得到目标函数xor_xnor：

xor_xnor (0:0:xs) = 0 : 1 : xor_xnor xs
xor_xnor (0:1:xs) = 1 : 0 : xor_xnor xs
xor_xnor (1:0:xs) = 1 : 0 : xor_xnor xs
xor_xnor (1:1:xs) = 0 : 1 : xor_xnor xs

我用Omega Monad实现的Haskell搜索器需要4700万次猜测，耗时约2.8秒；而基于SUP节点的HVM搜索器仅需170万次交互，耗时约0.0085秒，且每次猜测仅对应0.03次交互。如此巨大的性能差异让我怀疑Haskell实现存在疏漏，特寻求验证。

我的问题是：

• 我是否遗漏了关键实现细节？
• 在不改变核心算法的前提下，该Haskell搜索器是否有明显的优化空间？
• 最优评估版本是否确实比Haskell能实现的方案更快？

以下是完整的Haskell代码：

-- A demo, minimal Program Search in Haskell

-- Given a test (input/output) pairs, it will find a function that passes it.
-- This file is for demo purposes, so, it is restricted to just simple, single
-- pass recursive functions. The idea is to use HVM superpositions to try many
-- functions "at once". Obviously, Haskell does not have them, so, we just use
-- the Omega Monad to convert to a list of functions, and try each separately.

import Control.Monad (forM_)

-- PRELUDE
----------

newtype Omega a = Omega { runOmega :: [a] }

instance Functor Omega where
  fmap f (Omega xs) = Omega (map f xs)

instance Applicative Omega where
  pure x                = Omega [x]
  Omega fs <*> Omega xs = Omega [f x | f <- fs, x <- xs]

instance Monad Omega where
  Omega xs >>= f = Omega $ diagonal $ map (\x -> runOmega (f x)) xs

diagonal :: [[a]] -> [a]
diagonal xs = concat (stripe xs) where
  stripe []             = []
  stripe ([]     : xss) = stripe xss
  stripe ((x:xs) : xss) = [x] : zipCons xs (stripe xss)
  zipCons []     ys     = ys
  zipCons xs     []     = map (:[]) xs
  zipCons (x:xs) (y:ys) = (x:y) : zipCons xs ys

-- ENUMERATOR
-------------

-- A bit-string
data Bin
  = O Bin
  | I Bin
  | E

-- A simple DSL for `Bin -> Bin` terms
data Term
  = MkO Term      -- emits the bit 0
  | MkI Term      -- emits the bit 1
  | Mat Term Term -- pattern-matches on the argument
  | Rec           -- recurses on the argument
  | Ret           -- returns the argument
  | Sup Term Term -- a superposition of two functions

-- Checks if two Bins are equal
bin_eq :: Bin -> Bin -> Bool
bin_eq (O xs) (O ys) = bin_eq xs ys
bin_eq (I xs) (I ys) = bin_eq xs ys
bin_eq E      E      = True
bin_eq _      _      = False

-- Stringifies a Bin
bin_show :: Bin -> String
bin_show (O xs) = "O" ++ bin_show xs
bin_show (I xs) = "I" ++ bin_show xs
bin_show E      = "E"

-- Checks if two term are equal
term_eq :: Term -> Term -> Bool
term_eq (Mat l0 r0) (Mat l1 r1) = term_eq l0 l1 && term_eq r0 r1
term_eq (MkO t0)    (MkO t1)    = term_eq t0 t1
term_eq (MkI t0)    (MkI t1)    = term_eq t0 t1
term_eq Rec         Rec         = True
term_eq Ret         Ret         = True
term_eq _           _           = False

-- Stringifies a term
term_show :: Term -> String
term_show (MkO t)    = "(O " ++ term_show t ++ ")"
term_show (MkI t)    = "(I " ++ term_show t ++ ")"
term_show (Mat l r)  = "{O:" ++ term_show l ++ "|I:" ++ term_show r ++ "}"
term_show (Sup a b)  = "{" ++ term_show a ++ "|" ++ term_show b ++ "}"
term_show Rec        = "@"
term_show Ret        = "*"

-- Enumerates all terms
enum :: Bool -> Term
enum s = (if s then Sup Rec else id) $ Sup Ret $ Sup (intr s) (elim s) where
  intr s = Sup (MkO (enum s)) (MkI (enum s))
  elim s = Mat (enum True) (enum True)

-- Converts a Term into a native function
make :: Term -> (Bin -> Bin) -> Bin -> Bin
make Ret       _ x = x
make Rec       f x = f x
make (MkO trm) f x = O (make trm f x)
make (MkI trm) f x = I (make trm f x)
make (Mat l r) f x = case x of
  O xs -> make l f xs
  I xs -> make r f xs
  E    -> E

-- Finds a program that satisfies a test
search :: Int -> (Term -> Bool) -> [Term] -> IO ()
search n test (tm:tms) = do
  if test tm then
    putStrLn $ "FOUND " ++ term_show tm ++ " (after " ++ show n ++ " guesses)"
  else
    search (n+1) test tms

-- Collapses a superposed term to a list of terms, diagonalizing
collapse :: Term -> Omega Term
collapse (MkO t) = do
  t' <- collapse t
  return $ MkO t'
collapse (MkI t) = do
  t' <- collapse t
  return $ MkI t'
collapse (Mat l r) = do
  l' <- collapse l
  r' <- collapse r
  return $ Mat l' r'
collapse (Sup a b) =
  let a' = runOmega (collapse a) in
  let b' = runOmega (collapse b) in
  Omega (diagonal [a',b'])
collapse Rec = return Rec
collapse Ret = return Ret

-- Some test cases:
-- ----------------

test_not :: Term -> Bool
test_not tm = e0 && e1 where
  fn = make tm fn
  x0 = (O (I (O (O (O (I (O (O E))))))))
  y0 = (I (O (I (I (I (O (I (I E))))))))
  e0 = (bin_eq (fn x0) y0)
  x1 = (I (I (I (O (O (I (I (I E))))))))
  y1 = (O (O (O (I (I (O (O (O E))))))))
  e1 = (bin_eq (fn x1) y1)

test_inc :: Term -> Bool
test_inc tm = e0 && e1 where
  fn = make tm fn
  x0 = (O (I (O (O (O (I (O (O E))))))))
  y0 = (I (I (O (O (O (I (O (O E))))))))
  e0 = (bin_eq (fn x0) y0)
  x1 = (I (I (I (O (O (I (I (I E))))))))
  y1 = (O (O (O (I (O (I (I (I E))))))))
  e1 = (bin_eq (fn x1) y1)

test_mix :: Term -> Bool
test_mix tm = e0 && e1 where
  fn = make tm fn
  x0 = (O (I (O (O (O (I (O (O E))))))))
  y0 = (I (O (I (I (I (O (I (O (I (O (I (I (I (O (I (O E))))))))))))))))
  e0 = (bin_eq (fn x0) y0)
  x1 = (I (I (I (O (O (I (I (I E))))))))
  y1 = (I (I (I (I (I (I (I (O (I (O (I (I (I (I (I (I E))))))))))))))))
  e1 = (bin_eq (fn x1) y1)

test_xors :: Term -> Bool
test_xors tm = e0 && e1 where
  fn = make tm fn
  x0 = (I (I (O (O (O (I (O (O E))))))))
  y0 = (I (I (O (I E))))
  e0 = (bin_eq (fn x0) y0)
  x1 = (I (O (O (I (I (I (O (I E))))))))
  y1 = (O (O (I (O E))))
  e1 = (bin_eq (fn x1) y1)

test_xor_xnor :: Term -> Bool
test_xor_xnor tm = e0 && e1 where
  fn = make tm fn
  x0 = (I (O (O (I (I (O (I (I (I (O E))))))))))
  y0 = (I (O (I (O (I (O (O (I (I (O E))))))))))
  e0 = (bin_eq (fn x0) y0)
  x1 = (O (I (O (O (O (I (O (I (O (O E))))))))))
  y1 = (I (O (O (I (I (O (I (O (O (I E)))))))))) 
  e1 = (bin_eq (fn x1) y1)

main :: IO ()
main = search 0 test_xor_xnor $ runOmega $ collapse $ enum False

优化分析与验证 #

1. 潜在的实现疏漏

• 枚举冗余：enum生成的Sup结构展开后会产生大量行为等价但结构不同的Term，导致无效猜测次数暴增；而HVM的SUP节点可通过最优评估自动合并等价分支，避免重复计算。
• 递归计算效率：Haskell版本中make处理递归Term时需反复构建闭包，每次测试都要重新计算函数行为；HVM的最优评估会缓存中间计算结果，复用共享状态。

2. 不改变算法的优化空间

• Term去重缓存：通过term_eq或哈希值识别等价Term，缓存测试结果，避免重复测试相同行为的Term。
• 惰性生成Term：当前collapse会提前展开所有Term，改为惰性生成列表，仅在需要测试时才展开下一个Term，减少内存占用和预计算开销。
• 数据结构优化：将Bin类型改为更高效的表示（如[Bool]或Word64数组），减少递归比较和构造的开销；对make函数启用严格求值，降低闭包创建成本。
• 提前终止测试：测试用例时，一旦第一个输入不匹配就立即返回False，无需完成所有输入的计算。

3. 最优评估的固有优势

最优评估（如HVM采用的机制）通过共享计算图、合并等价分支、按需计算等特性，可同时探索多个函数分支并自动剪枝无效路径；而Haskell的Omega Monad本质是枚举所有可能的Term并逐个测试，无法利用分支间的计算共享。因此，最优评估版本的性能优势是本质性的，确实比当前Haskell实现的方案更快。

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