Изменения

<tex>\beta</tex>-редукция олицетворяет идею счёта значения функции. Выражение вида это наименьшее соотношение на <tex>(\lambda x\ .\ f)\ yLambda</tex> можно заменить на такое что:<tex>f[(\lambda x := y]</tex>, где <tex>f.P)Q\to _\beta P[x:=yQ]</tex>, как и ранее, означаетзамкнуто относительно следующих правилзамену всех свободных вхождений :<tex>P\to _\beta P' \Rightarrow \forall x\in V:\lambda x.P\to _\beta \lambda x.P'\\P\to _\beta P' \Rightarrow \forall Z\in \Lambda : P\ Z\to _\beta P'\ Z\\P\to _\beta P' \Rightarrow \forall Z\in \Lambda : Z\ P\to _\beta Z\ P'</tex> в <tex>f</tex> на <tex>y</tex>.