ラムダ計算では、非関数式に式を適用するとどうなりますか？

Question

私はLambda Calculusを初めて使う人です。 私はdefinition of lambda expression on Wikipediaについて読んだことがあります。

ラムダ式のセット、Λ、帰納的に定義することができる。

1. xが変数である場合、X∈Λ
2. xは変数、次いでM∈Λ、（ある場合λx.M）∈Λ
3. 場合M、N∈Λ、次いで（MN）∈Λルール2の

インスタンスがアプリケーションとして知られている抽象化とルール3のインスタンスとして知られています。

Mは、それが（λx.E）の形態であり、機能の抽象化である場合、私はルール2の意味を知っています。

しかし、意味は何ですか？Mは機能ではありません？そのようなだけX可変または非機能発現X + Y

Answer 1

ラムダ計算は、文脈自由文法で

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

v範囲一緒にベータを持つ変数、上に構成され、として - およびイータ削減ルール

(λ 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にはありません。 2つの削減ルールのどちらも適用されない式は、正規形式です。 M Nは、β-可約式(λ x. B) E、両方MとNない場合

ので、通常の形態である、そしてM N全体が既約標準形です。

Answer 2

したがって、Mが関数であるとき、（M N）の意味はあなたには明らかです。 簡単のために、同一性の場合、すなわちM = I = \ x.xを考える。 N. に減少し

      (*) (\x.x) N 

は今、あなたはあなたのプログラムが、もう少し一般的なようにしたいとします。 NにIDを適用するだけではなく、入力として受け取る汎用関数 fを適用します。したがって、\ x.xをfに置き換えて、 の全項w.r.tを抽象化します。 f：

        \f.f N 

これは\ f。（f N）と理解する必要があります。ものすごく単純。あなたは今、（*）に 用語相当を取得するために、前期に引数としてのアイデンティティを養うことができ

：物事をさらに複雑にするために

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

、あなたの入力を処理するために想像して 関数fを入力してからNにします。たとえば、バイナリの文字列が入力として期待される場合は、引数f（N、N）の "pair"にfを適用することができます。引数をNとして2回渡すことができます。

     (**) \f. f N N 

は\ fと理解してください。 （（f N）N）。したがって、他のアプリケーションの機能的な位置にアプリケーションがあることが明確に分かります。

前の例を見るには、アイデンティティの代わりに、K = \ x。\ y.xという用語を使用してください。 Kは2つの引数を受け取ります 広告が最初に返します。あなたは前期への入力としてKを供給した場合、一般的に

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

（*）と同等の用語を取得し、あなたはまだ、プログラミング言語は、抽象化を提供する方法です。 概念に関して抽象化するには、まず、 にその概念のインスタンス名を付ける必要があります。例えば、命令的言語では、変数は本質的にメモリセルの抽象化である。 関数に関して抽象化するには、関数の名前を にする必要があります。 2番目のステップでは、概念を「表現可能」にすること、すなわち は与えられた概念（ここでは新しい関数）の新しいインスタンスを動的に合成することを可能にする表現の言語を提供します。ラムダ計算は、機能が（直接的に）表現可能なコア計算です。