math - 左側の抽象化なしのアプリケーションの意味は何ですか？

Question

ラムダ用語は次のようになります。

• 変数
• ラムダ抽象化（たとえば\x.t）
• 応用。tとsがラムダ項の場合、tsはアプリケーションです。

したがって、左側の部分（たとえば(\x.t)a）に抽象化されたアプリケーションは見栄えがします。関数呼び出しのように見えます。しかし、左側が可変または他のアプリケーションである場合、アプリケーションはどういう意味ですか？はどういう意味ですかab、((\x.x)a)bまたは変数であるa(\x.x)場合はどうaなりますか？b

Answer 1

((\x.x)b)c関数適用です。ここではに適用さbれcます。

((\x.x)b)c
= bc

a(\x.y)は関数適用であり、関数aをその唯一の引数に適用します。これはたまたま関数、つまりy（自由変数）を返す関数です。

lamdba微積分の特徴の1つは、関数を関数に適用しやすく、関数が他の関数を引数として取ることができることです。2つの例は、両方のケースをうまく示しています。

編集ラムダ計算には（少なくとも）2つのバージョンがあります：型なしと型付きです。ここで使用している型なし微積分では、何でも何にでも適用できます。型付きラムダ計算法には、命題の種類や「個人」の種類など、関数ではない基本型が存在します。したがって、の型が型を何かにマッピングする関数型abである場合にのみ、書き込むことができます。ab