用基本術語解釋Church-Rosser定理

Question

我想知道在編程中如何使用Church-Rosser定理，特別是函數式編程。我查閱了信息，但只能找到提及lambda微積分（有限知識）和beta減少的來源。

如果任何人都可以解釋lambda微積分在什麼地方出現，以及什麼是縮減，我認爲這樣可以解決問題。

我對Church-Rosser定理的初步想法是，它是關於評估和執行功能的順序，但我不完全確定這是否是準確的信息。

謝謝。

注意：我目前正在學習標準ML

Answer 1

您的初步想法很好。

• lambda微積分函數是構建函數式編程的正式基礎。
• lambda演算是一個術語重寫系統，而reduction意味着遵循重寫規則。

• 拉姆達演算並不規定特定的評估順序，所以給定一個可以多次減少的lambda表達式，Church-Rosser定理說你可以選擇其中一個。這使得函數式編程語言設計人員在設計評估語義時有很大的自由度。例如，在f（g x）中，假設兩者都是純函數，則無論您是減少f還是g首先都是等效的。

  的Church-Rosser theorem的Wikipedia的描述是：

  [I F的有兩個不同的減少量或可施加到相同術語削減序列，則存在一個術語，是從兩個結果可達，通過應用（可能是空的）額外減少的序列。

  示例F（GX）其中˚F是X 2和克是2X：

  (λx.x*x) ((λy.y+y) 2) ~β~> ((λy.y+y) 2)*((λy.y+y) 2) 
           ~β~> (2+2)*((λy.y+y) 2) 
           ~β~> (2+2)*(2+2) 
  
  (λx.x*x) ((λy.y+y) 2) ~β~> (λx.x*x) (2+2) 
           ~β~> (2+2)*(2+2) 
  

  在這個例子中，兩個不同的減少是β-還原在兩個lambda中的任一個上，並且可以從兩個縮減中獲得的一個術語是(2+2)*(2+2)。