haskell - 为什么这个的第二个版本在指数时间内运行？

Question

我正在编写一个程序来确定两个字符串之间的 Levenshtein 距离是否在线性时间内正好是 2。
我有一个算法可以做到这一点。我使用简单的递归方法来扫描字符串，当它发现差异时，它会分支为 3 个选项，尝试删除、插入或替换。但是我做了一个修改，如果我们的总数超过 2，我们就放弃那个分支。这将分支的总数限制为 9，并使算法线性化。
这是我的初始实现:

diffIs2 x y =
  2 == go 0 x y
  where
    go total xs@(x1:xs') ys@(y1:ys')
      | x1 == y1
      =
        go total xs' ys'
      | total < 2
      =
        minimum $ zipWith (go $ total + 1)
          [ xs', xs , xs' ]
          [ ys , ys', ys' ]
    go total xs ys =
      total + length xs + length ys

测试证实这在线性时间内运行。
我还有第二个类似的程序，据我所知，它也应该是线性的。
这里的想法是使用短路和惰性评估来限制评估的分支数量。但是，我们总是允许分支，当我们分支时，我们取每个和 3 的结果中的最小值。这样，如果分支总数超过 3，短路应该会阻止进一步的评估。
我们必须实现一个自然数类型来进行部分评估。

data Nat
  = Zero
  | Succ Nat
  deriving
    ( Eq
    , Ord
    )

natLength :: [a] -> Nat
natLength [] =
  Zero
natLength (a : b) =
  Succ (natLength b)

nat3 =
  Succ $ Succ $ Succ Zero

diffIs2 x y =
  Succ (Succ Zero) == go x y
  where
    go xs@(x1:xs') ys@(y1:ys')
      | x1 == y1
      =
        go xs' ys'
      | otherwise
      =
        Succ $
          minimum $
            map (min nat3) $
              zipWith go
                [ xs', xs , xs' ]
                [ ys , ys', ys' ]
    go xs ys =
      natLength $ xs ++ ys

对此进行测试表明它不会在线性时间内运行。有些东西使它成指数，但我不知道是什么。短路确实按预期工作。我们可以用下面的程序来证明这一点，该程序由于 min 的短路而在有限时间内停止。 :

f = Succ f

main =
  print $ (Succ Zero) == min (Succ Zero) f

但是当放在算法中时，它似乎并没有像我预期的那样工作。
为什么第二个代码是指数的？我的误解是什么？

Answer 1

而默认 min对于问题末尾的简单示例来说足够懒惰，它并不像我们希望的那样懒惰:

ghci> let inf = Succ inf
ghci> inf `min` inf `min` Zero == Zero
^CInterrupted.

要修复它，我们需要一个懒惰的 min :

min' :: Nat -> Nat -> Nat
min' Zero _ = Zero
min' _ Zero = Zero
min' (Succ x) (Succ y) = Succ (min' x y)

最大的不同是现在我们可以在完全评估参数之前得到部分结果:

min (Succ undefined) (Succ undefined) === undefined
min' (Succ undefined) (Succ undefined) === Succ (min' undefined undefined)

现在我们可以按如下方式使用它:

diffIs2 :: Eq a => [a] -> [a] -> Bool
diffIs2 x y = Succ (Succ Zero) == go x y
  where
    go xs@(x1:xs') ys@(y1:ys')
      | x1 == y1 = go xs' ys'
      | otherwise = Succ $ go xs' ys `min'` go xs ys' `min'` go xs' ys'
    go xs ys = natLength $ xs ++ ys

请注意，您甚至不需要额外的 min' nat3 , 因为顶级比较只会强制前三个 Succ无论如何。