在lambda微積分中，如果將表達式應用於非函數表達式會怎樣？

我是Lambda Calculus的新用戶。我已閱讀約definition of lambda expression on Wikipedia。在lambda微積分中，如果將表達式應用於非函數表達式會怎樣？

該組lambda表達式，Λ，可以感應地定義：

如果x是一個變數，則x∈Λ

如果x是一個變量和M∈Λ，則（ λx.M）∈Λ

如果M，N∈Λ，則（MN）∈Λ規則2的

實例被稱爲抽象和規則3的情況下，被稱爲應用程序。

我知道規則2的含義時中號是一個函數的抽象，即在（λx.E）形式。

但是什麼意思M不是函數？如，只是一個可變X或無功能表達X + Y

2017-04-02 yuxingdubai

'x + y'不是lambda表達式，所以不會發生。 – melpomene

請參閱https://en.wikipedia.org/wiki/Lambda_calculus_definition#Reduction。如果M是一個變量，那麼表達式不能進一步減少（除非另一個beta減少用抽象替代變量）。 – melpomene

LAMBDA演算在於一種上下文無關文法

E ::= v  Variable 
    | λ v. E Abstraction 
    | E E  Application

其中v範圍以上的變量，與所述β-一起 - 和ETA還原規則

(λ x. B) E => B where every occurrence of x in B in substituted by E 
    λ x. E x => E if x doesn't occur free in E

a是免費，但不在λ a. λ b. b a。兩個縮減規則均不適用的表達式是正常形式。

所以，如果M N不是一種β-歸約(λ x. B) E，都M和N是在正常的形式，然後M N整體處於束縛範式。

來源

2017-04-06 02:30:33 suchtgott

因此，當M是一個函數時，（M N）的含義對你很清楚。爲簡單起見，我們考慮身份的情況，即M = I = \ x.x。

      (*) (\x.x) N

減少到N. 假設現在你想使你的程序更通用一些。您不想僅將身份應用於N，而是應用您輸入的通用功能。所以，你用\ f替換\ x.x然後抽取整個術語w.r.t. f：

        \f.f N

必須理解爲\ f。（f N）。很簡單。

您現在可以養活身份參數上一屆，獲得相當於一個術語，（*）：

     (\f.f N) \x.x = \x.x N

爲了讓事情更加複雜，你可能想象到處理您的輸入例如，如果你期待一個二進制的（currified）函數作爲輸入，你可能希望將f應用到參數「N」（N，N）的「對」上，因爲f被修正了，等於通過N作爲參數兩次：

     (**) \f. f N N

\ f。

被理解爲\ f。（（f N）N）。所以，您清楚地看到了讓應用程序處於其他應用程序的功能位置上的重要性。

要查看上一個示例，請使用術語K = \ x。\ y.x而不是標識。 K有兩個參數 ad返回第一個。如果你給K作爲輸入到上一屆你仍然可以獲得相當於一個術語，（*）

     (\f.f N N) K = K N N = N

一般而言，編程語言都提供抽象的一種方式。要想抽象出一個概念，首先需要給一個名稱給這個概念的實例。例如，在命令式語言中，變量本質上是存儲單元的抽象。要對功能進行抽象，您需要使用功能名稱。第二步，它允許概念是「可表達的」，即提供了一種表達式的語言，允許動態合成給定概念的新實例（在我們的例子中是新函數）。 lambda演算只是一個核心演算，其功能是（直接）可表達的。

來源

2017-04-06 07:02:59

在lambda微積分中，如果將表達式應用於非函數表達式會怎樣？

回答

相關問題