类型为 Mercury 等逻辑编程语言带来啥好处？

Posted 2023-05-08

【中文标题】类型为 Mercury 等逻辑编程语言带来啥好处？

【英文标题】：What benefit does types bring in logic programming languages like Mercury?类型为 Mercury 等逻辑编程语言带来什么好处？

【发布时间】：2014-05-25 11:43:12

【问题描述】：

我开始研究 Mercury 语言，这似乎很有趣。我是逻辑编程的新手，但对 Scala 和 Haskell 的函数式编程非常有经验。我一直在思考的一件事是，当您已经拥有至少应该与类型一样具有表达力的谓词时，为什么在逻辑编程中还需要类型。

例如，在以下 sn-p 中使用类型有什么好处（取自 Mercury 教程）：

:- type list(T) ---> [] ; [T | list(T)].

:- pred fib(int::in, int::out) is det.
fib(N, X) :-
  ( if N =< 2
  then X = 1
  else fib(N - 1, A), fib(N - 2, B), X = A + B
  ).

与仅使用谓词编写相比：

list(T, []).
list(T, [H | X]) :- T(H), list(T, X).

int(X) :- .... (builtin predicate)

fib(N, X) :-
  int(N),
  int(X),
  ( if N =< 2
  then X = 1
  else fib(N - 1, A), fib(N - 2, B), X = A + B
  ).

请随意指出涵盖该主题的介绍性材料。

编辑： 我可能在问题的表述上有点不清楚。实际上，我是在研究了 Idris 等依赖类型语言之后才开始研究 Mercury 的，就像在依赖类型中可以在类型中使用值一样，也可以在编译时使用谓词来验证逻辑程序的正确性。如果程序需要很长时间来评估，我可以看到出于编译时性能原因使用类型的好处（但前提是类型不如“实现”复杂，在谈论依赖类型时不一定是这种情况）。我的问题是除了编译时性能之外，使用类型是否还有其他好处。

【问题讨论】：

您是说逻辑编程语言中的运行时类型断言比函数式或过程语言中的运行时类型断言更能替代静态类型吗？

不，我有点不清楚，请参阅我对问题的编辑。

我认为我正在寻找一种具有自动定理证明的语言，例如 Why3 或 Astrée。缺点是这些解决方案（如 SMT 求解器）是有限的和/或不可预测的，而类型系统是健壮的（但也是有限的）。不过，这似乎是一个活跃的研究领域，甚至还有一些项目使用 SMT 求解器扩展 Haskell。

【参考方案1】：

与您的替代方案相比，一个直接的好处是声明像

:- pred fib(int::in, int::out) is det.

可以与子句分开放在模块的接口中。这样，模块的用户就可以获得关于 fib 谓词的建设性的、经过编译器验证的信息，而无需了解实现细节。

更一般地说，Mercury 的类型系统是静态可判定的。这意味着它比使用谓词严格地表达更少，但好处是代码的作者确切地知道在编译时将捕获哪些错误。用户当然仍然可以使用谓词添加运行时检查，以涵盖类型系统无法捕获的情况。

Mercury 支持类型推断，因此在静态检查方面，依赖类型会遇到与谓词相同的问题。有关信息和更多链接，请参阅this answer。

【讨论】：

感谢您的回复。关于您的第一个论点，在我看来，也可以用接口中的隐含替换类型（在本例中为 fib(N, X) :- int(N), int(X)）。

@JesperNordenberg 这暗示是错误的方式 - 你的意思是说如果 fib(N, X) 为真，那么 N 和 X 是整数。但是，是的，可以按照您的建议进行操作。问题是，它是否可取？从语言设计的角度来看，模块作者的更多表现力意味着它的用户更复杂。

是的，暗示的方向很有趣。在函数式语言中，fib 将具有 (N: Int) -> (X: Int) 类型，这意味着您可以给 fib 任何 Int，它总是会给您一个 Int。但它不能为每个结果X 给你一个N，所以这个命题应该类似于forall N. (int(N) -> exists X. (int(X) & fib(N, X)))。也许这就是 fib(int::in, int::out) 在 Mercury 类型系统中的解释方式。

是的，该命题是is det 含义的一部分，另一部分是X 对于每个N 都是唯一的。在Mercury 中，模式和确定性提供除了类型之外的信息。然而，就这个问题而言，模式和确定性提供了与类型大致相同的好处。