performance - 我如何将 Prolog 的剪辑翻译成 Curry？

Question

这是 Curry 中的一个算法，它接受 n 并匹配彼此在 n 编辑距离内的两个字符串。

lev :: Eq a => Int -> [a] -> [a] -> ()
lev n (a : b) (a : c) =
  lev n b c
lev n (_ : b) (_ : c) | n > 0 =
  lev (n - 1) b c
lev n (_ : b) c | n > 0 =
  lev (n - 1) b c
lev n b (_ : c) | n > 0 =
  lev (n - 1) b c
lev n [] [] =
  ()

这修改了朴素的递归算法，因此我们限制了我们可以尝试的编辑次数。一旦我们尝试了 n 次编辑，我们就放弃了。

如果我们将其翻译成 Prolog，我们会得到

p(_, [], []).
p(N, [A|B], [A|C]) :-
  p(N, B, C).
p(N, [_|B], C) :-
  N>0,
  p(N-1, B, C).
p(N, B, [_|C]) :-
  N>0,
  p(N-1, B, C).
p(N, [_|B], [_|C]) :-
  N>0,
  p(N-1, B, C).

虽然这些确实限制了他们可以尝试的编辑次数，但对分支因子没有限制。因此它的运行时间与输入的大小成指数关系。在 Prolog 中，我可以通过剪切来解决这个问题:

p(_, [], []).
p(N, [A|B], [A|C]) :-
  !, p(N, B, C).
p(N, [_|B], C) :-
  N>0,
  p(N-1, B, C).
p(N, B, [_|C]) :-
  N>0,
  p(N-1, B, C).
p(N, [_|B], [_|C]) :-
  N>0,
  p(N-1, B, C).

现在分支因子被限制了，并且在线性时间内运行。但是我不能对 Curry 做同样的改变，因为 Curry 没有削减。

实现这个的惯用 Curry 方法是什么？

Answer 1

不幸的是，库里没有“惯用”的方式来实现切入，这取决于你想做什么。然而，大多数时候，最好将相应的非确定性、灵活的模式匹配转换为刚性匹配。这是我想出的:

在您的情况下，我们希望第一条规则和第二条规则之间的决定是确定性的(不完全是，我会谈到这一点)。

因此，我们可以将决策转移到 if 中。由于我们仍然希望在 n > 0 规则之间灵活选择，我们可以移动将匹配的那部分放入 else 分支中的灵活大小写。

lev2 _ []         []         = ()
lev2 n xs@(x : b) ys@(y : c) = 
  if x == y 
    then lev2 n b c 
    else case (xs, ys) of 
      (_ : b, _ : c) | n > 0 -> lev2 (n - 1) b c
      (_ : b, c    ) | n > 0 -> lev2 (n - 1) b c
      (b    , _ : c) | n > 0 -> lev2 (n - 1) b c    

编辑:以下是我原回答的一部分。对于具有不同位置切入点的修订后问题，此答案的较早部分就足够了。其余部分不是必需的，但可以作为如何翻译不同位置的剪切的示例 (p(N, [A|B], [A|C]) :- p(N,B,C) , !.).

然而，这个解决方案并不是对剪辑的忠实翻译。如果在 then 分支中对 lev2 的递归调用没有产生结果，我们目前不会尝试不同的匹配。我假设您确实想尝试不同的方法，因此我们可以通过集合函数使用封装来检查递归调用是否有解决方案。

lev2 _ []         []         = ()
lev2 n xs@(x : b) ys@(y : c) = 
  if x == y 
   then let allSols = set0 (lev2 n b c) -- get set of all solutions
        in if notEmpty allSols         
             then selectValue allSols   -- choose (non-det) any value 
             else lev2' (xs, ys)        -- try the other matches in case of failure
   else lev2' (xs, ys)    
  where 
    lev2' (_ : b, _ : c) | n > 0 = lev2 (n - 1) b c
    lev2' (_ : b, c    ) | n > 0 = lev2 (n - 1) b c
    lev2' (b    , _ : c) | n > 0 = lev2 (n - 1) b c  

我知道这不再那么优雅了......

请注意，我没有测试性能是否真的更好，因为我没有时间去做。但以我的理解，它应该更好。