{-# LANGUAGE GADTs #-} data Foo x y where Composition :: Foo b c -> Foo a b -> Foo a c FMap :: Functor f => (a->b) -> Foo (f a)...

假设我有以下理论：a(X) :- \+ b(X). b(X) :- \+ c(X). c(a). 它只是简单地说真，这当然是正确的，a(X)是真的，因为没有b(X)（否定作为有限失败）。由于只有在没有c(X) 的情况下才会有一个b(X)，并且我们有c(a)，因此可以将其说明为真。然而，我想...

我正在尝试实现统一，但遇到了问题。虽然已经有了许多例子，但它们只是使问题更加混乱。我感到越来越困惑而不是受到启发： http://www.cs.trincoll.edu/~ram/cpsc352/notes/unification.html https://www.doc.ic.ac.uk...

我正在使用这种类型来推理可进行可决定解析的字符串： data Every : (a -> Type) -> List a -> Type where Nil : {P : a -> Type} -> Every P [] (::) : {P : a -&...

我正在实现Hindley-Milner类型推断算法，参考了Mark Jones和Oleg Kiselyov的教程。这两个教程都有一个“应用绑定”（apply bindings）操作，其类型大致为：applyBindings :: TyEnv -> Type -> Type 该函数将...

问题 什么是最高效的MGU算法？它的时间复杂度是多少？它是否简单到足以在Stack Overflow回答中描述？ 我一直在Google上寻找答案，但只找到了通过ACM订阅才能访问的私人PDF。 我在SICP中找到了一个讨论: 这里 说明“最一般的统一算法”是什么： e1 = (+ x? (...

在ISO Prolog中，一致性仅针对那些不受出现检查限制的情况（NSTO）进行定义。其背后的思想是覆盖程序中大多数使用的一致性情况，并且所有Prolog系统都实际支持这些情况。更具体地，ISO/IEC 13211-1:1995如下所述： 7.3.3 受出现检查（STO）和不受出现检查（NS...

请问有人知道如何在Prolog中访问列表的特定成员吗？例如，如果我需要访问传递到规则中的列表的第三个或第四个元素怎么办？

给定Haskell函数：head . filter fst 现在的问题是如何手动查找类型。如果我让 Haskell 告诉我类型，我会得到： 现在问题是手动如何找到类型。如果我让 Haskell 告诉我类型，那么我会得到：head . filter fst :: [(Bool, b)] -&g...

我正在开发一个高阶定理证明器，其中单一化似乎是最困难的子问题。 如果Huet算法仍被认为是最先进的，有没有任何可以让程序员理解的解释它的链接？ 或者哪些例子可以说明在哪些情况下它可以工作而通常的一阶算法不行？