我有一个有趣的问题，但我不确定如何准确地表述它...
考虑λ演算。对于给定的λ表达式，存在多种可能的约简顺序。但其中一些不终止，而其他一些则会。
在λ演算中，事实证明有一种特定的约简顺序，如果实际上存在一个不可约解，则此顺序保证始终终止。这被称为正则序。
我写了一个简单的逻辑求解器。但问题是，它处理约束条件的顺序似乎对是否找到任何解决方案有很大影响。基本上，我想知道是否存在类似于我的逻辑编程语言的正则序。（或者说，仅靠机器就无法确定性地解决这个问题。）
所以这就是我想要的。答案可能关键取决于“简单逻辑求解器”的具体内容。因此，我将尝试简要描述它。
我的程序密切基于《编程的乐趣》（Jeremy Gibbons＆Oege de Moor）第9章中的组合子系统。该语言具有以下结构：
求解器的输入是单个谓词。谓词可以涉及变量。求解器的输出是零个或多个解决方案。一个解决方案是一组使谓词成为真的变量分配。
变量保存表达式。表达式是整数、变量名或子表达式元组。
有一个相等性谓词，用于比较等式（而不是谓词）是否相等。如果将每个（绑定的）变量替换为其值，使两个表达式完全相同，则满足它。 （特别地，每个变量都等于自身，无论是否绑定。）这个谓词使用统一解决。
还有AND和OR运算符，它们按照明显的方式工作。没有NOT运算符。
存在“exists”运算符，基本上创建本地变量。
定义命名谓词的功能使得递归循环成为可能。
逻辑编程的一个“有趣之处”在于，一旦编写了一个命名谓词，它通常可以向前和向后工作（有时甚至可以向侧面工作）。典型例子：连接两个列表的谓词也可用于将列表拆分为所有可能的对。
但是，有时候反向运行谓词会导致无限搜索，除非你重新排列术语的顺序。（例如，在AND或OR的左右交换某个地方）。我想知道是否有自动检测最佳运行谓词顺序的方法，以确保在解集完全有限的所有情况下及时终止。
有什么建议吗？