Vyhodnocování lambda výrazů se provádí na základě pravidel, které označujeme jako konverze. Tyto konverze jsou založené na pojmu substituce.

Substituce e1[e2/x] vyjadřuje náhradu všech volných výskytů proměnné x ve výrazu e1 za výraz e2. Pro tuto substituci se vyžaduje, aby byla platná, což znamená, že se žádná volná proměnná z výrazu e2 nesmí po substituci stát vázanou.

	Příklad 2.2.
	Příkladem substituce, která není platná, je (\f->f x)[f y / x]. Volná proměnná f z výrazu f y by se totiž po dosazení za x v těle lambda abstrakce (\f->f x) stala vázanou. Příkladem platné substituce je (\f->f x)[y/x], která vede na výraz (\f->f y).

Nejjednodušším typem konverze je alfa konverze, představující předjmenování proměnných. Máme-li abstrakci (\x->e), můžeme ji nahradit abstrakcí (\x'->e[x'/x]), ovšem pouze za předpokladu, že je uvedená substituce platná. Přejmenování vázaných proměnných v lambda výrazu je užitečné tehdy, pokud by při substituci mohlo dojít ke konfliktu volných a vázaných proměnných - vhodným přejmenováním můžeme dosáhnout toho, že takto zobecněná substituce je vždy platná.

	Příklad 2.3.
	Lambda výraz \f->(\x -> f x) můžeme po přejmenování proměnné f na gnahradit výrazem \g->(\x -> g x), aniž se jeho význam změní. Nemůžeme ale proměnnou x přejmenovat na f, neboť by se tím volná proměnná f z výrazu f x stala vázanou.

Základní konverzí, na které je postaveno vyhodnocování lambda výrazů, je beta konverze. Představuje dosazení hodnoty argumentu za parametr abstrakce, která je použita v aplikaci na místě funkce. Konkrétně máme-li výraz ((\x->e1) e2), můžeme místo něj psát e1[e2 / x], samozřejmě opět za předpokladu, že naznačená substituce je platná. Pomocí beta konverze můžeme zjednodušovat lambda výrazy a tím je i vyhodnocovat.

	Příklad 2.4.
	Výraz (\f->(\x-> f x)) (g y) můžeme s využitím beta konverze přepsat na (\x-> (g y) x).

Cílem vyhodnocování lambda výrazu je obvykle dosažení stavu, kdy se již žádná další aplikace nedá pomocí beta konverze realizovat. Potom říkáme, že je výraz v normální formě. Není-li výraz v normální formě, pak musí obsahovat podvýraz, který je redukovatelný pomocí beta konverze. Takový podvýraz nazýváme beta redex (reducible expression, redukovatelný výraz). Podobně bychom mohli definovat i alfa redex.

Musí mít každý výraz normální formu? Pokud má výraz normální formu, existuje postup, jak se k ní vhodnou volbou pořadí provádění redukcí dostat? Na uvedené otázky lze odpovědět na základě tzv. Church-Rosserova normalizačního teorému. Najděte si jeho přesné znění v literatuře nebo na Internetu a pokuste se jej vlastními slovy interpretovat.