次のようなプログラムを考えます。2*x + 3 を計算する関数の本体部です。代入の記号は「:=」を使いました。
a := 2;
y := a*x;
y := y + 3;
return y;
この例では、変数yへの代入が二回あるので、最初の値は上書きされて消えています。つまり、破壊的な代入が実行されています。
このプログラムを、ラムダ計算で書いてみます。ラムダ計算は、純粋に記号的な計算体系なので、プログラム変数や破壊的代入はありません。それでも、破壊的代入と同じ効果を表現することはできます。
まず、let式を次のような形として導入します。
- (let x1 := E1, x2 := E2; F)
x1, x2は、ラムダ計算の意味での変数（単なる記号）、E1, E2, Fはラムダ式です。このlet式の意味は次のとおり。
- (λ(x1, x2).F)(E1, E2)
つまりlet式は、変数x1, x2に関するラムダ抽象と適用を簡略に書いただけのシンタックスシュガーに過ぎません。
ここで、次のように入れ子になったlet式を考えます。
(let a := 2;
(let y := a*x;
(let y := y + 3; y)))
先の定義に基づいて、普通のラムダ式に展開します。外から順にやってみます。
(let a := 2;
(let y := a*x;
(let y := y + 3; y)))↓
(λa.
(let y := a*x;
(let y := y + 3; y))
)(2)↓
(λa.
(λy.
(let y := y + 3; y)
)(a*x)
)(2)↓
(λa.
(λy.
(λy.y)(y + 3)
)(a*x)
)(2)
ポイントは、(λy.y)(y + 3) という式の評価方法です。ラムダ記号λで束縛された変数は一斉に置き換え（アルファ変換）してもいいので、束縛変数yをzにリネームします。すると、(λz.z)(y + 3)、部分式は等価な式に置き換えてもいいので次の形になります。
- (λa.(λy.(λz.z)(y + 3))(a*x))(2)
xを引数とする関数としては、さらに外側に λx が付きますが、ともかくxを具体化して適用を順に計算（ベータ変換）していくと、代入計算がちゃんと出来ているのがわかるでしょう。
最初のlet式に戻って、let式のスコープが明らかなら外側を囲む丸括弧を省略していいことにすると：
let a := 2;
let y := a*x;
let y := y + 3;
y
これって、見た感じは破壊的代入を伴う手続き的コードでしょ。でもラムダ式なんです。
