5

我有这个特殊的问题，我还没有解决方案。我认为如果我知道它存在相关算法会有所帮助。

我正在寻找的算法是一种有助于找到满足函数返回目标的参数的算法。

例如，a works for b表示为(a,b)

Given: [ (a,b); (b,c) ]

函数works将确保它们与布尔值的关系

let works a b -> true
let works b c -> true

现在给了我

[ (a, "x"); ("x", c) ]

如果我希望这两个绑定是真的，那么这个函数必须是真的

let works a "x" -> true
let works "x" c -> true

现在我正在尝试编写一个函数/算法来帮助我实现这样的"x" = b

我正在考虑回溯，但还不知道如何实现它。如果有人能给我一个提示，我将不胜感激。

作为旁注，我正在使用函数式编程范例在 F# 中实现该算法。

4

2 回答 2

4

你是正确的，你需要反向链接，杰克是正确的，你需要统一，但特别是你需要反向链接的句法统一。

您的问题并不新鲜，但在CS:StackExchange上得到了更彻底的回答，即如何以纯函数式语言实现序言解释器？

虽然这将使您走上正确的道路，但根据您要解决的问题，您可能会发现这可能并不像看起来那么容易。

编辑

我在我拥有的一些工作 F# 代码上测试了你的示例，它确实有效，但是我无法向公众发布代码，抱歉。

对于您给定的示例，可以仅通过统一来完成，而无需反向链接。

您需要为

works(a,b).
works(b,c).

和一个查询

works(a,X),works(X,c).

答案是

X = b

如果您想将其扩展到中间的多个人，那么您将需要使用反向链接，因为您必须创建一个递归从属规则。

您需要为

works(a,b).
works(b,c).
works(c,d).

和规则

subordinate(X,Z) :- works(X,Z).
subordinate(X,Z) :- works(X,Y), subordinate(Y,Z).

和一个查询

subordinate(a,X),subordinate(X,d).

答案是

X = b,c

您将必须创建类型、统一和反向链接算法。您可以选择在 REPL 上创建解析器和漂亮的打印机和层，但这不是必需的。

事实、规则和查询以人工方式显示，但如果您跳过解析器和漂亮的打印机，您将不得不将它们编码为 AST。IE

("works", [Const "a", Const "b"])

大写字母代表 Prolog 变量。即 XYZ
小写字母代表 Prolog 常量。即美国广播公司

您的作品问题只是经典祖先示例的变体。请参阅：Prolog/递归规则

于 2013-10-09T20:05:59.687 回答
3

您描述的算法是统一——它是 Prolog 的基础，在 F# 中实现起来并不难。

我建议阅读John Harrison的《实用逻辑和自动推理手册》（亚马逊、Safari 书籍）；第 3.9 节介绍了统一算法。如果你想看看的话，我和另外两个 F# 人员去年将代码从书中移植到了 F#：fsharp-logic-examples。

鉴于您对问题的描述，您可能可以通过一些简单的约束逻辑编程 (CLP) 来解决它，但据我所知，还没有人为 F# 实现 CLP 库。miniKanren和cKanren是此类系统的两个流行的简单示例，如果您有兴趣将它们移植到 F#，我怀疑它们会花费很多时间。

于 2013-10-09T18:47:55.893 回答