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

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

Function creation −教会は表記法を導入しました λx.E'x'が正式な引数であり、 'E'が関数本体である関数を示します。これらの関数は、名前や単一の引数なしで使用できます。
Function application −教会は表記法を使用しました E₁.E₂ 機能の適用を示すため E₁ 実際の議論に E₂。そして、すべての関数は単一の引数にあります。

ラムダ計算の構文

ラムダ計算には、3つの異なるタイプの式が含まれています。

E :: = x （変数）

| E ₁ E ₂（機能適用）

| λx.E （関数作成）

どこ λx.E ラムダ抽象化と呼ばれ、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 . + (− x 1)) 9 3 
+ (− 9 1) 3 
+ 8 3 
= 11

式では、変数の各出現は「自由」（λへ）または「バインド」（λへ）のいずれかです。

のβ還元 (λx . E) yはすべてを置き換えます x それは無料で発生します E と 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

チャーチ・ロッサーの定理は次のように述べています-