関数型プログラミング-ラムダ計算

ラムダ計算は、関数を使用した計算を研究するために1930年代にアロンゾ教会によって開発されたフレームワークです。

関数の作成-教会は、「x」が正式な引数であり、「E」が関数体である関数を示す表記*λx.E*を導入しました。これらの関数は、名前と単一の引数なしで作成できます。
関数アプリケーション-教会は* E〜1〜.E〜2〜という表記を使用して、実際の引数 E〜2〜への関数 E〜1〜*の適用を示しました。そして、すべての関数は単一の引数に基づいています。

ラムダ計算の構文

Lamdba Calculusには、3種類の式が含まれます。

| E₁ E₂(function application)

| λx.E(function creation)

ここで、*λx.E*はLambda抽象化と呼ばれ、Eはλ式と呼ばれます。

純粋なラムダ計算には組み込み関数はありません。私たちは次の式を評価しましょう-

(+ (* 5 6) (* 8 3))

ここでは、数字のみで動作するため、「+」から始めることはできません。（* 5 6）と（* 8 3）の2つの縮小可能な式があります。

最初にどちらかを減らすことができます。たとえば-

(+ (* 5 6) (* 8 3))
(+ 30 ( *8 3))
(+ 30 24)
= 54

λsを処理する削減ルールが必要です

(λx .* 2 x) 4
(* 2 4)
= 8

これはβ還元と呼ばれます。

正式なパラメータは数回使用される場合があります-

(λx . + x x) 4
(+ 4 4)
= 8

複数の用語がある場合、次のように処理できます-

(λx . (λx . + (− x 1)) x 3) 9

内側の x は内側の*λ*に属し、外側のxは外側のものに属します。

(λx . + (− x 1)) 9 3
+ (− 9 1) 3
+ 8 3
= 11

式では、変数の各出現は「自由」（λ）または「結合」（λ）のいずれかです。

（λxのβ還元 E） yは、 E で発生するすべての x を y に置き換えます。例-

アルファ削減は非常に簡単で、ラムダ式の意味を変更せずに実行できます。

λx . (λx . x) (+ 1 x) ↔ α λx . (λy . y) (+ 1 x)

たとえば-

(λx . (λx . + (− x 1)) x 3) 9
(λx . (λy . + (− y 1)) x 3) 9
(λy . + (− y 1)) 9 3
+ (− 9 1) 3
+ 8 3
11

チャーチ・ロッサーの定理は次のことを述べています-