haskell - 如何找到最优的加工顺序？

Question

我有一个有趣的问题，但我不确定如何表达它......

考虑 lambda 演算。对于给定的 lambda 表达式，有几种可能的归约顺序。但其中一些不会终止，而另一些则会终止。

在 lambda 演算中，事实证明存在一个特定的约简顺序，如果实际存在的话，它保证始终以不可约解终止。这称为正常顺序。

我编写了一个简单的逻辑求解器。但问题是，它处理约束的顺序似乎对它是否找到解决方案有很大影响。基本上，我想知道我的逻辑编程语言是否存在类似正常顺序的东西。 (或者单纯的机器是否不可能确定性地解决这个问题。)

<小时/>

这就是我所追求的。想必答案很大程度上取决于“简单逻辑求解器”到底是什么。因此，我将尝试简要描述它。

我的程序紧密基于编程的乐趣(Jeremy Gibbons 和 Oege de Moor)第 9 章中的组合器系统。该语言具有以下结构:

• 求解器的输入是单个谓词。谓词可能涉及变量。求解器的输出是零个或多个解。解决方案是一组使谓词变为 true 的变量赋值。

• 变量保存表达式。表达式可以是整数、变量名或子表达式的元组。

• 有一个相等谓词，它比较表达式(而不是谓词)是否相等。如果用每个(绑定(bind))变量的值替换每个(绑定(bind))变量使得两个表达式相同，则满足。 (特别是，每个变量都等于自身，无论是否绑定(bind)。)这个谓词是使用统一来解决的。

• 还有 AND 和 OR 运算符，其工作方式很明显。没有 NOT 运算符。

• 有一个“exists”运算符，它本质上创建局部变量。

• 定义命名谓词的工具可实现递归循环。

关于逻辑编程的“有趣的事情”之一是，一旦编写了命名谓词，它通常会向前和向后工作(有时甚至横向)。规范示例:连接两个列表的谓词也可用于将列表拆分为所有可能的对。

但有时向后运行谓词会导致无限搜索，除非您重新排列术语的顺序。 (例如，交换 AND 或 OR 的 LHS 和 RHS。)我想知道是否有某种自动方法来检测运行谓词的最佳顺序，以确保在解决方案集完全正确的所有情况下都能立即终止有限。

有什么建议吗？

Answer 1

相关论文，我认为:http://www.cs.technion.ac.il/~shaulm/papers/abstracts/Ledeniov-1998-DCS.html

另请看一下:http://en.wikipedia.org/wiki/Constraint_logic_programming#Bottom-up_evaluation