English version
では，SUCC を具体的に計算してみよう．まず私は数を適用するというので，0 とか 1 を適用しようとして困った．まったくの素人なのでそういうことをする．ここでの数というのは Church 数であるので，0 は (λf x. x) である．
SUCC 0 := (λn f x. f (n f x)) (λf x. x)
(λ f x. f ((λf x. x) f x))
ところでこの中の下線部分，
((λf x. x) f x))
だが，最初に何が f に入っても消えてしまう．1変数で
(λf. 3)
というような場合，
f(x) := 3
と同じなので，x が何になってもこの函数は 3 を返す．こういう x はλに束縛されていない自由な変数と呼ぶ．黄金の心号のマービンみたいなものである．何があっても別に関係がなかったり，ザップホッドには常に忘れれられてしまう．しかし，それならばいらないかというとマービンが出てこないヒッチハイクガイドのように，まったく面白くなくなってしまうので必要なのである．自動販売機gensym3141 ではクレジットカードを入れない限り，どんな入力も無効なのである．クレジットカードが入力されない限り，全ての変数は束縛されないのだ．そういう機能がλ函数にはある．
(λf x. x) f x は最初に f に f が入るがそれは束縛されていない．(このλ式の '.' のあとには x しかない)ので，消えてしまう．ここでは 2 つf があるのでわかりにくいという場合は，(λg x. x) f x でも同じである．gに f が入っても g は束縛されていないので f は消えてしまう．
すると，
(λf x. x) f x
(λx. x) x
となるが，x に x を代入すると，これは x になってしまう．どの x がどの xなのかわからない人もいるかもしれないので，λ式の変数の名前を変えてみよう
(λy. y) x
と書いても同じである．それは
f(x) := x
f(y) := y
が本質的には同じ函数であることと同じである．マービンは日本語ではマービンであり，英語では Marvin であるが，何語で呼んでもマービンはマービンである．ことわっておくが，変数の名前を変えても良いというのは (λx.x) を (λx.y)にしても良いということではない．何が何に対応しているかはきちんとしておかねばならない．そこまで規則をやぶってしまってはボゴン人だっておとなしくなってしまいかねない．