如何将 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 方式是什么？

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 的递归调用没有产生结果，我们目前不会尝试不同的匹配。 我假设您确实想尝试不同的方法，因此我们可以通过 set 函数使用封装来检查递归调用是否有解决方案。

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  

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

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