我有一個有趣的問題，但我不知道如何將其短語...如何找到最佳處理順序？
考慮lambda演算。對於給定的lambda表達式，有幾種可能的縮減順序。但其中一些不會終止，而有些則不會。
在λ演算中，事實證明存在一個特定的縮減順序，即保證如果實際存在，總是以不可約的解決方案終止。這叫做正常訂單。
我寫了一個簡單的邏輯求解器。但麻煩在於，它處理約束的順序似乎對它是否找到解決方案產生巨大影響。基本上，我想知道我的邏輯編程語言是否存在像正常順序那樣的東西。 （或者，單純的機器不可能確定地解決這個問題。）
所以這就是我所追求的。據推測，答案在很大程度上取決於「簡單邏輯解算器」是什麼。所以我會試着簡要地來形容它。
我的計劃是在編程（傑里米·吉本斯& Oege德穆爾）的樂趣第9章密切基於組合子系統。語言具有以下結構：
輸入到解算是單謂詞。謂詞可能涉及變量。求解器的輸出爲零或更多解決方案。解決方案是一組變量賦值，它使謂詞變爲真。
變量保存表達式。表達式是整數，變量名或子表達式的元組。
存在一個相等謂詞，它比較表達式（而不是謂詞）是否相等。如果用它的值代替每個（界限）變量使得兩個表達式相同，那麼它是滿意的。 （特別是，每個變量都等於它本身，綁定與否）。這個謂詞是用統一來解決的。
還有AND和OR的運算符，它們以明顯的方式工作。沒有NOT操作符。
有一個「存在」運算符，它本質上創建局部變量。
定義命名謂詞的工具啓用了遞歸循環。
其中的「有趣的事情」關於邏輯編程是，一旦你寫了一個名爲謂詞，它通常適用fowards 和向後（有時甚至側身）。規範示例：也可以使用謂詞來協調兩個列表，以將列表分割爲所有可能的對。
但是，有時向後運行謂詞會導致無限的搜索，除非您重新排列條件的順序。 （例如，交換一個AND或OR的LHS和RHS somehwere。）我想知道是否有一些自動化的方式來檢測最佳命令來運行謂詞，以確保在所有情況下立即終止解決方案設置是準確的有限。
有什麼建議嗎？
它，如果你發佈的程序在你的語言的幾個例子，並展示削減戰略有什麼不同導致可能會幫助不同的結果。 –
@ n.m。好主意。我會試着想出一個最簡單的例子... – MathematicalOrchid
另請參見[Presburger算術]（http://en.wikipedia.org/wiki/Presburger_arithmetic）如果你以前沒有見過它 - 有效性是可確定的，它允許和/或不適用，歸納和歸納（雖然也許歸納並不像你描述的遞歸那麼強大）。 –