我有一个有趣的问题，但我不知道如何将其短语...如何找到最佳处理顺序？
考虑lambda演算。对于给定的lambda表达式，有几种可能的缩减顺序。但其中一些不会终止，而有些则不会。
在λ演算中，事实证明存在一个特定的缩减顺序，即保证如果实际存在，总是以不可约的解决方案终止。这叫做正常订单。
我写了一个简单的逻辑求解器。但麻烦在于，它处理约束的顺序似乎对它是否找到解决方案产生巨大影响。基本上，我想知道我的逻辑编程语言是否存在像正常顺序那样的东西。 （或者，单纯的机器不可能确定地解决这个问题。）
所以这就是我所追求的。据推测，答案在很大程度上取决于“简单逻辑解算器”是什么。所以我会试着简要地来形容它。
我的计划是在编程（杰里米·吉本斯& Oege德穆尔）的乐趣第9章密切基于组合子系统。语言具有以下结构：
输入到解算是单谓词。谓词可能涉及变量。求解器的输出为零或更多解决方案。解决方案是一组变量赋值，它使谓词变为真。
变量保存表达式。表达式是整数，变量名或子表达式的元组。
存在一个相等谓词，它比较表达式（而不是谓词）是否相等。如果用它的值代替每个（界限）变量使得两个表达式相同，那么它是满意的。 （特别是，每个变量都等于它本身，绑定与否）。这个谓词是用统一来解决的。
还有AND和OR的运算符，它们以明显的方式工作。没有NOT操作符。
有一个“存在”运算符，它本质上创建局部变量。
定义命名谓词的工具启用了递归循环。
其中的“有趣的事情”关于逻辑编程是，一旦你写了一个名为谓词，它通常适用fowards 和向后（有时甚至侧身）。规范示例：也可以使用谓词来协调两个列表，以将列表分割为所有可能的对。
但是，有时向后运行谓词会导致无限的搜索，除非您重新排列条件的顺序。 （例如，交换一个AND或OR的LHS和RHS somehwere。）我想知道是否有一些自动化的方式来检测最佳命令来运行谓词，以确保在所有情况下立即终止解决方案设置是准确的有限。
有什么建议吗？
它，如果你发布的程序在你的语言的几个例子，并展示削减战略有什么不同导致可能会帮助不同的结果。 –
@ n.m。好主意。我会试着想出一个最简单的例子... – MathematicalOrchid
另请参见[Presburger算术]（http://en.wikipedia.org/wiki/Presburger_arithmetic）如果你以前没有见过它 - 有效性是可确定的，它允许和/或不适用，归纳和归纳（虽然也许归纳并不像你描述的递归那么强大）。 –