0

我正在使用 PAKCS Curry 编译器，版本 3.3.0。

这是 Curry 中的一个简单的列表反转功能（它也适用于 Haskell）：

rev :: [a] -> [a]
rev [] = []
rev (x : xs) = (rev xs) ++ [x]

让我们尝试反转函数，即找到一个反转为 [1..5] 的列表 l：

> rev l =:= [1 .. 5] where l free
{l=[5,4,3,2,1]} True
...hang...

库里能解方程真是太好了。然而，它进入了一个无限循环，寻找更多的解决方案。

这是 Prolog 中的等价谓词：

rev([], []).
rev([X | L], M) :- rev(L, LR), append(LR, [X], M).

Prolog 谓词也无法以相反的方向终止：

?- rev(L, [1, 2, 3, 4, 5]).
L = [5, 4, 3, 2, 1] ;
...hang...

在 Prolog 中，我可以通过添加 L 及其倒数具有相同长度的约束来帮助终止：

rev([], []).
rev([X | L], M) :- same_length([X | L], M), rev(L, LR), append(LR, [X], M).

有了这个额外的约束，谓词在两个方向上都终止。

在 Curry 中，是否可以添加类似的约束，或者以其他方式帮助查询终止？

我尝试定义一个具有类似 same_length 约束的反函数：

same_length :: [a] -> [b] -> Bool
same_length [] [] = True
same_length (_ : _) [] = False
same_length [] (_ : _) = False
same_length (_ : xs) (_ : ys) = same_length xs ys

rev :: [a] -> [a]
rev [] = []
rev (x : xs) = (rev xs) ++ [x]

rev2 :: Data a => [a] -> [a]
rev2 b@(rev a) | same_length a b = a

但是它没有帮助：'rev2 [1 .. 5]' 也找到了一个解决方案，然后无法终止。

4

1 回答 1

1

您考虑列表长度的想法非常好。但是，在您的定义中rev2，功能模式b@(rev a)仍会在检查防护之前进行评估same_length a b，因此，您的评估不会在找到第一个解决方案后终止。

我能想到的最简单的解决方案是same_length在保护的开头移动约束，而在结尾处有统一约束 - 结合使用(&&).

revInv xs | same_length xs ys && rev ys =:= xs = ys where ys free

为了进一步改进关于列表元素的非严格性的逆定义（例如，如果元素之一失败，则上述定义失败），您甚至可以使用非严格统一运算符=:<=而不是严格的统一运算符=:=。

revInv' xs | same_length xs ys && rev ys =:<= xs = ys where ys free

为了比较，请考虑以下两个表达式。

> head (revInv [1, failed, 2])
*** No value found!
> head (revInv' [1, failed, 2])
2
于 2021-03-19T11:25:30.393 回答