我有一个有趣的问题，但我不确定如何表达它......
考虑 lambda 演算。对于给定的 lambda 表达式，有几种可能的归约顺序。但其中一些不会终止，而另一些会终止。
在 lambda 演算中，事实证明存在一个特定的归约顺序，如果确实存在一个不可约解，则它保证总是以不可约解结束。它被称为正常订单。
我写了一个简单的逻辑求解器。但问题是，它处理约束的顺序似乎对它是否找到任何解决方案有巨大的影响。基本上，我想知道我的逻辑编程语言是否存在类似正常顺序的东西。（或者仅仅是一台机器不可能确定性地解决这个问题。）
所以这就是我所追求的。据推测，答案主要取决于“简单逻辑求解器”究竟是什么。因此，我将尝试简要描述它。
我的程序非常基于The Fun of Programming (Jeremy Gibbons & Oege de Moor) 第 9 章中的组合器系统。该语言具有以下结构：
求解器的输入是单个谓词。谓词可能涉及变量。求解器的输出是零个或多个解。解决方案是一组使谓词变为真的变量赋值。
变量包含表达式。表达式是整数、变量名或子表达式的元组。
有一个相等谓词，它比较表达式（不是谓词）是否相等。如果用它的值替换每个（绑定的）变量使两个表达式相同，则满足。（特别是，每个变量都等于它自己，无论是否绑定。）这个谓词是使用统一来解决的。
还有用于 AND 和 OR 的运算符，它们以明显的方式工作。没有 NOT 运算符。
有一个“存在”运算符，它本质上是创建局部变量。
定义命名谓词的工具支持递归循环。
关于逻辑编程的“有趣的事情”之一是，一旦你编写了一个命名谓词，它通常会向前和向后工作（有时甚至是横向工作）。典型示例：连接两个列表的谓词也可用于将列表拆分为所有可能的对。
但有时向后运行谓词会导致无限搜索，除非您重新排列术语的顺序。（例如，交换 AND 或 OR somehwere 的 LHS 和 RHS。）我想知道是否有一些自动方法来检测运行谓词的最佳顺序，以确保在解决方案集完全正确的所有情况下立即终止有限。
有什么建议么？