Lambda微積分表達式

Question

對於lambda表達式(x (λx y. x y) z h)，我不明白自由變量x (outer x),z和h可以在C代碼中進行轉換嗎？

問候， darkie

Answer 1

自由變量是Lambda微積分中的一個特殊情況 - 它們不能被「轉換」爲任何東西，所以通常它們只被視爲符號。顯然

mk_app(mk_app(mk_app(mk_sym("x"), 
        mk_lam("x", 
          mk_lam("y", 
            mk_app(mk_var("x"), 
              mk_var("y"))))), 
       mk_sym("z")), 
     mk_sym("h")); 

，您可以使用mk_var()那些：在你的榜樣，並給出了lambda表達式一些虛構的構造函數，你把它翻譯爲以下（包括對付隱鑽營）C類的表達符號也是如此，但這會誤導，因爲它們不是真正的變量，因爲它們沒有綁定。換句話說，如果你對錶達式進行了任何alpha轉換，他們將不得不保持不變。

（順便說一下，這裏的相關部分是Barendregt的自由變量假設。）

Answer 2

轉換演算爲C代碼是不平凡的。通常你會寫一個解釋器，逐步評估。也就是說，將表達式轉換爲樹，並找到最接近根節點的節點，該節點是左側爲lambda的應用程序。現在替換在右側。重複，直到你不能再申請，並且你有結果。

請注意，這裏沒有直接等價於自由變量;我們只是用它們來知道在哪裏取代東西。

請記住，圖靈等價不需要精確兩個圖靈完備語言中的任何概念之間的等價性。它只是要求你能夠與另一個模擬一個，反之亦然。