问题标签 [lambda-prolog]

我想问你从头开始/逆向工程实现什么正式系统会更有趣。

我浏览了一些现有的和开源的逻辑/声明式编程系统项目。我决定在空闲时间编造一些类似的东西，或者至少要掌握实施的总体思路。

如果其中一些系统能够提供现代学术研究逻辑及其与计算模型的关系的大部分表达能力和简洁性，那就太好了。

你会建议至少在概念层面学习什么？例如，Lambda-Prolog 很有趣，特别是因为它允许更高阶的关系，但 AFAIK 是基于直觉主义逻辑的，因此缺乏排中原则；这对我来说通常是一个缺点。

我也欢迎任何关于不太流行但更具表现力/功能强大的现代逻辑编程系统的建议。

I'm trying to install OMake so I can install Teyjus so I can start writing a bit of Lambda Prolog but I'm getting I'm getting a bunch of errors on OS X 10.10.5. The most current one, that I can't figure out, is:

Has anyone run into this? Does anyone know of a fix? Would love to be able to get started.

我正在使用缺少findall.

在这里实现我们自己的还有另一个问题findall：在 Prolog 中获取解决方案列表。

低效的实现是：

有效率的

需要一个“解决方案”的高阶谓词：

是什么solutions？我可以solutions在高阶 lambda Prolog 中实现我自己的谓词吗？

我正在使用 Teyjus 在 Lambda Prolog 中进行编程。我有这个简单的列表生成器：

我需要创建一个谓词，该谓词返回一个列表，该列表由 islist 在一定范围内生成的所有列表组成。

我想继续失败驱动循环。目前我只能打印使用以下代码生成的列表：

我需要的是收集这些列表而不是打印它们（所以我需要列表理解之类的东西）。我该怎么做？

λProlog是 Prolog 的高阶方言。另一方面，据说 HiLog使用具有一阶模型理论的高阶语法。换句话说，它们都具有高阶语法，但只有 λProlog 具有高阶语义。

高阶语义在 λProlog 中给了你什么（除了你已经通过高阶语法得到的）？λProlog 中有什么简单的例子可以说明这些收益？

我怀疑 λProlog 的主要实现 teyjus 可能有点废弃软件，但 λProlog 是一个迷人的 Prolog，它应该让你使用高阶逻辑、假设推理和其他东西，这就是为什么我试图用它。

文件“example.sig”：

文件“example.mod”：

但是，当我编译和加载它时，虽然它似乎可以工作，但假设的推理查询被拒绝：

我期待在最后一个“是”。我究竟做错了什么？

我怀疑 λProlog 需要一个类型系统来使它们的
高阶统一听起来不错。否则通过自我应用
可能会出现一些罗素型异常。

是否有不需要 .sig 文件的替代高阶 Prolog？
也许通过一个更简单的类型系统，不需要那么多
声明但仍然有某种形式的高阶统一？

这个困境能解决吗？

想做以下从 SKI 表达式到 lambda 表达式的反向转换：

转换不需要涉及任何β-减少。但我仍然想做一个特殊的 beta-reduction。每当有线性 redex 或单位 redex 时：

我想把它减少到：

从某种意义上说，这似乎是一种安全的减少，它不会使 redex 变得更大，它只会移动 E₂ 的位置，甚至在 x 不出现的情况下消除 E₂。分别进行重命名。例子：

周围有任何Prolog实现吗？

Curry与它的表亲 Haskell 不同，它允许您为函数赋予多个值：

它会回溯（或其他一些搜索）来探索这种非确定性的含义。

这使得它类似于 Prolog（尤其是λProlog，由于类型系统和语法），您可以在其中声明

从语义上讲， N元 Curry 函数和N+1元 Prolog 关系之间有什么区别吗？

荷兰数学家 Nicolaas Govert de Bruijn 发明了这些索引来表示 lambda 演算的项，而无需命名绑定变量。让我们来看看这个 lambda 表达式：

使用 de Bruijn 索引时，当我们使用约定时，如here，零 de Bruijn 索引指的是第一个封闭的 lambda binder：

de Bruijn 指数 1 是指包含 de Bruijn 指数的第二个 lambda 粘合剂。如何为替换编写 Prolog 代码，以便我们可以计算 beta 减少，例如：