问题标签 [unification]

谁能告诉我为什么会失败？

我的假设是 X 首先被实例化为 a，然后被删除，然后是 b，使得 X = b。尝试一下，我发现我错了，但我不知道为什么。

谢谢你。

I am trying to learn Prolog for an exam.

According to my slides arithmetic expressions do not unify with constants. Is there a reason for?

for example

The 0 doesn't unify with (X-1).

So my Question is: Would it be a problem in some case if there was unification between constants and arithmetic expressions?

I'm studying for my final exam and I'm having trouble understanding this FC algorithm:

I understand it up to the part where you standardize each rule. Then I think the next line is saying for each theta that satisfied the Generalized Modus Ponens (p'_iTheta = p_iTheta), do... something. What is that something? I don't really understand what is happening after that part.

Any help is appreciated. Thanks for reading.

可以查询 ghci 的统一类型吗？

例如，如果我想知道之间的统一类型(Int -> Bool)以及(a -> Bool)如何向 ghci 查询？

我要解决的是Haskell 第三版中的练习 13.23：函数式编程的工艺。

如何使用 Haskell 系统检查两个类型表达式是否可统一，如果可以，它们的统一性是什么？提示：您可以在 Haskell 中进行虚拟定义，其中定义的值，例如锆石，等同于自身：

像这样定义的值可以声明为您希望的任何类型。

谢谢，
塞巴斯蒂安。

我试图理解为什么类型：

(flip .) is: (a -> a1 -> b -> c) -> a -> b -> a1 -> c

首先，类型：

flip: is (a -> b -> c) -> b -> a -> c (.): is (b -> c) -> (a -> b) -> a -> c

我将重命名变量以在我的解释中更清楚，所以类型：

flip: is (ax -> bx -> cx) -> bx -> ax -> cx (.): is (by -> cy) -> (ay -> by) -> ay -> cy

然后我尝试像这样替换：

ax = (by -> cy) bx = (ay -> by) cx = ay -> cy

所以得到的类型是：(ay -> by) (by -> cy) -> ay -> cy，与正确的结果不同。

有什么帮助吗？

谢谢，塞巴斯蒂安。

这可以按预期工作...直到您取消注释asFunction!的第二个子句 这实际上只是其他两种模式已经匹配的特殊情况的内联版本，所以我希望它没问题。但是 ( ghc-7.6.2, 或者也ghc-7.4.1)

为什么会发生这种情况，为什么不在其他条款中？在更复杂的应用程序中究竟应该做些什么来防止这种麻烦？

我试图理解为什么类型fun g x = ys where ys = [x] ++ filter (curry g x) ys是((a, a) -> Bool) -> a -> [a].

我明白那个：

filter :: (a -> Bool) -> [a] -> [a]然后curry :: ((a, b) -> c) -> a -> b -> c

但我不明白如何继续。

我想手动导出类型：

f1 x xs = (filter . (<)) x xs

我们第一次看到x，所以：

然后(<)有这种类型：

我们只能说(< x)是否可以统一以下类型：

然后

所以

过滤器有这种类型

第一次看到xs，所以：

我们只能说(filter . (<)) x xs是否可以统一以下类型：

因此，当正确的类型是（询问 GHCi）时，我得到了f1 :: (a2 -> Bool) -> [a2] -> [a2]与 相同的类型。filterOrd a => a -> [a] -> [a]

有什么帮助吗？

我正在尝试手动导出 ((.) foldr) 的类型

然后：

匹配我得到的类型：

但是后来我对如何减少这种表达感到困惑。

有什么帮助吗？

谢谢，
塞巴斯蒂安。

我正在尝试手动导出 (foldr (.)) 的类型

然后：

所以我明白了(foldr (.)) :: (a2 -> b2) -> [(b2 -> c2)] -> (a2 -> b2)

但是 GHCi 返回：:t (foldr (.)) :: (a -> b) -> [b -> b] -> a -> b

为什么 b2 和 c2 是一样的？

谢谢，
塞巴斯蒂安。