Лямбда исчисление

http://akoub.narod.ru/funcbook/chapter3/c3.htm

Глава 3. Лямбда-исчисление

3.1. Формальные  теории в программировании

Функциональные языки  программирования появились в качестве средства для написания программ, не содержащих в явном виде понятий  ячеек памяти для хранения значений (переменных) и последовательности вычислений как процесса изменения  состояния памяти. Тем не менее, основа для создания таких языков была предложена еще в середине 30-х годов 20-го века Алонзо Черчем (Alonzo Church) и Стефаном Клини (Stephen Kleene). Мы рассмотрим теорию Черча, названную им лямбда-исчислением, в  качестве теоретической основы и "минимального" функционального языка программирования. В конечном итоге любую программу, написанную на языке Haskell или любом другом функциональном языке программирования, можно сравнительно несложными преобразованиями свести к формуле лямбда-исчисления.

Разумеется, ни Черч, ни Клини  не создавали язык программирования. Вопрос, которым они интересовались - это вопрос о формализации понятия  вычислимой функции и создания универсального математического аппарата для определения  и работы с вычислимыми функциями. В то время эта область математики активно развивалась в трудах уже упомянутых Черча и Клини, а также Тьюринга (Alan Turing), Поста (Emil Post) и других. Во многих работах предлагался  следующий подход к формализации понятия функции: в качестве основы берется некоторый "минимальный" набор базовых функций и предлагаются способы построения из них более  сложных функций с помощью  тех или иных комбинаторов (функций высшего порядка). Таков, например, подход, использованный Геделем при создании им теории рекурсивных функций. Напротив, в созданном им лямбда-исчислении Черч сумел построить такую систему, при которой базовых функций нет вовсе, а вместо способов построения сложных функций из простых (комбинаторов) используются правила преобразований, с помощью которых можно получать из одних функций другие, эквивалентные им. Такой процесс преобразования формул напоминает процесс вычисления функции, происходящий при исполнении программы, написанной на функциональном языке программирования. Рассмотрим теорию Черча более подробно.

Основным понятием в лямбда-исчислении является понятие выражения или формулы. Его можно определить рекурсивно. Прежде всего, зафиксируем набор идентификаторов, которые в дальнейшем будем называть переменными. Мы будем использовать в качестве имен латинские буквы x, y, f и др. В формулах переменные обычно обозначают аргументы функций, задаваемых лямбда-выражениями, однако сама по себе переменная является простейшим видом выражения. Два других вида выражений - это определение безымянной функции (лямбда-выражение) и применение функции.

Лямбда-выражение имеет  вид (λx.e), где x - имя переменной, а e - выражение. Семантически такое выражение обозначает функцию с аргументом x и телом e. Применение функции записывается в виде (e1 e2), где e1 и e2 - выражения (e1 - функция, а e2 - ее аргумент). Приведем несколько примеров.

λx.x - простейшая функция, выдающая свой аргумент; скобки опущены, поскольку это не вызывает неоднозначности. 
λf.λx.f x - функция с двумя аргументами, применяющая свой первый аргумент ко второму. Строго говоря, надо было бы расставить скобки, чтобы выражение приняло вид λf.(λx.(f x)), однако, принято соглашение, по которому "операция" применения функции к аргументу имеет более высокий приоритет, чем "операция" образования лямбда-выражения, при этом функции применяются в порядке слева направо, то есть выражение f x y понимается как применение функции f к аргументу x, и применение полученного результата к аргументу y. 
(λx.x x)(λx.x x) - применение функции, заданной лямбда-выражением (λx.x x), к аргументу, представляющему собой такое же лямбда-выражение. Внутри тела, задающего лямбда-выражение, аргумент x применяется к себе.

Мы будем рассматривать  не классическое лямбда-исчисление, в  котором кроме функций и их применений к другим функциям ничего нет, а некоторое его расширение. В нашем расширенном лямбда-исчислении помимо безымянных функций, заданных лямбда-выражениями, будут использоваться константы, смысл которых задан вне лямбда-исчисления. Это будут привычные нам по языкам программирования константы, обозначающие целые числа, символы и логические значения, константа, обозначающая пустой список NIL (этим идентификатором мы будем обозначать объект, который ранее в языке Haskell, всегда обозначался нами парой квадратных скобок []), а также константы, задающие обозначения примитивных функций. Примитивные функции нашей системы следует рассмотреть особо.

Многие примитивные функции  уже хорошо нам знакомы по языку Haskell и многим другим языкам программирования. Это обычные арифметические операции сложения, умножения и другие, операции сравнения величин "больше", "меньше", "равны" и другие, операции над логическими значениями "и", "или" и другие. Мы будем пользоваться ими без какого-либо объяснения. Единственное отличие от стандартного использования этих и других операций от их использования в других языках программирования будет заключаться в том, что мы всегда будем использовать только префиксную запись операций, то есть вместо привычного 3+5 будем записывать выражение + 3 5. Конечно, все функции в нашем расширенном лямбда-исчислении будут карринговыми, то есть выражение + 3 также имеет смысл и представляет собой применение функции + к константе 3, в результате которого получается функция увеличения целого аргумента на 3.

Следует заметить также и  то, что если в классическом лямбда-исчислении применение любой функции к любому аргументу всегда осмысленно, поскольку  любой "объект" - как аргумент, так и результат - всегда представляет собой функцию одного аргумента, то в нашем расширенном лямбда-исчислении примитивные функции можно применять  только к "правильным" аргументам. Так, бессмысленным будет выражение + TRUE 0, поскольку невозможно выполнить сложение логического значения TRUE с числом 0. Также бессмысленным будет выражение / 3 0, поскольку результат деления числа 3 на число 0 не определен. Мы не будем рассматривать бессмысленные выражения.

В лямбда-исчислении определены эквивалентные преобразования выражений. С их помощью можно переходить от одних выражений к другим, эквивалентным  им. В функциональном программировании аналогом этому процессу служит процесс  вычисления выражения, поэтому мы иногда будем говорить об эквивалентном  преобразовании выражений в лямбда-исчислении как о вычислении выражений. Как  правило, осмысленными будут являться те преобразования, которые позволяют  упростить выражение, однако, все  преобразования на самом деле обратимы. В следующем разделе мы введем правила преобразований для выражений, которые позволят нам рассматривать  лямбда-исчисление как своеобразный язык программирования, позволяющий  по заданной программе (выражению) вычислить  результат работы этой программы (эквивалентное  ему "простейшее" выражение).

3.2. Система вывода  результатов

Прежде, чем рассматривать  преобразования выражений, введем важное понятие свободной и связанной переменной. Неформально говоря, вхождение переменной в некоторое выражение будет связанным, если оно находится внутри некоторого лямбда-выражения, в заголовке которого эта переменная упомянута в качестве аргумента. Другими словами, если имеется выражение, в которое в качестве подвыражения входит λx.e, то все вхождения переменной x в выражении e будут связанными. Если переменная не является связанной в некотором выражении, то она в нем будет свободной. Можно определить понятия свободных и связанных переменных и более формально. Для этого рассмотрим понятие "множества свободных переменных" некоторого выражения. Те переменные, которые не будут входить в это множество, будут в этом выражении связанными.

Итак, если выражение E представляет собой переменную x, то множество свободных переменных этого выражения F(E) содержит только эту переменную: F(E) = { x }. Если выражение представляет собой одну из стандартных констант нашего расширенного лямбда-исчисления, то оно не содержит ни свободных, ни связанных вхождений переменных, F(c) = {}. Если выражение является применением функции к аргументу и имеет вид E = e1 e2, то множество свободных переменных этого выражения является объединением множеств свободных переменных выражений e1и e2: F(E) = F(e1)  È F(e2). Наконец, если выражение имеет вид лямбда-выражения E = λx.e, то его множество свободных переменных получится, если из множества свободных переменных выражения e убрать переменную x: F(E) = F(e) \ { x }.

Следует отметить, что одна и та же переменная может быть связанной  в некотором выражении и одновременно свободной в некотором его  подвыражении. Так, например, в выраженииλf.f x переменная x - свободная, а переменная f - связанная. Однако если рассматривать только тело этого лямбда-выражения f x, то в нем обе переменных f и x свободные. Вообще говоря, выражения, содержащие свободные переменные, хотя и являются формально допустимыми, но, как правило, бессмысленны. Например, выражение λf.f x представляет собой функцию, которая применяет свой аргумент к переменной "x". Поскольку переменная x - свободная, то ее смысл в этом выражении не определен. Если же связать эту переменную, то мы получим уже вполне осмысленное выражение λx.λf.f x, представляющее собой функцию, которая применяет свой второй аргумент к первому. Обычно мы рассматриваем выражения, содержащие свободные переменные, только в качестве составных частей других выражений, в которых рассматриваемые переменные уже являются связанными.

Мы рассмотрим четыре способа  преобразования выражений в лямбда-исчислении. Первое из рассматриваемых преобразований называется переименованием переменных или α-преобразованием. Смысл этого преобразования состоит в том, что суть функции не меняется, если заменить имя ее формального аргумента. Формально α-преобразование заключается в замене в выражении λx.e имени переменной x на любое другое имя с одновременной заменой всех свободных вхождений этой переменной в выражение e. Преобразование возможно, если только новая переменная уже не входит свободно в выражение e, а также если при этом свободное вхождение переменной не окажется связанным. Так, например, в выражении λx.λf.f x y можно заменить переменную x, скажем, на переменную z. В результате получится выражение λz.λf.f z y. Разумеется, новое выражение эквивалентно исходному и имеет тот же смысл. Однако, в том же выражении переменную x нельзя заменить на y, поскольку переменная y входит в тело лямбда-выражения свободно, так что получившееся после замены выражение λy.λf.f y y уже будет иметь другой смысл - в нем оба вхождения переменной y оказываются связанными. Нельзя также произвести и замену x на f, поскольку это приведет к тому, что в теле лямбда-выражения свободное вхождение переменной x превратится в связанное вхождение переменной f, и получившееся выражение λf.λf.f f y также будет иметь уже другой смысл.

Переименование не приводит к изменению длины или структуры  выражения, оно применяется не как  средство для "вычисления" выражения, но только для "технических" целей. Два следующих преобразования - это "вычислительные" преобразования, которые, вообще говоря, приводят к  упрощению выражения, сведению его  к кратчайшей форме. Поэтому эти  преобразования называют еще редукциями от слова reduce - сокращать, редуцировать. В программировании эти две редукции соответствуют применению "встроенных" или "определенных программистом" функций к фактическому аргументу или аргументам.

Преобразование, называемое δ-редукцией, соответствует применению "встроенной" функции к константным аргументам. Правило δ-редукции имеет следующий вид. Пусть имеется выражение e e1 e2... ek, где e - константа, представляющее имя "встроенной" функции с k аргументами, а e1, e2,... ek - значения, могущие служить аргументами этой функции. Тогда такое выражение можно заменить на эквивалентное ему выражение, представленное значением, получающимся как результат применения функции к заданным значениям аргумента. Так, например, если константа+ представляет функцию арифметического сложения целых, а константа OR - функцию логического "или", то в результате δ-редукции выражение + 1 4 может быть преобразовано к выражению 5, а выражение OR TRUE FALSE - к выражению TRUE. Теоретически δ-редукция обратима, то есть можно действовать и наоборот, представляя константы в виде применения встроенных функций к аргументам-константам. Однако на практике желание представить константу 5 в виде + 2 3 никогда не возникает.

Преобразование, называемое β-редукцией, соответствует применению функции, представленной лямбда-выражением, к аргументу. Если исходное выражение имело вид (λx.e) a, то в результате применения β-редукции оно будет преобразовано в e{x|a} - выражение e, в котором все свободные вхождения переменной x заменены на выражение a. Например, выражение((λx.+ x x) 3) в результате применения β-редукции будет преобразовано в (+ 3 3), которое, в свою очередь, может быть преобразовано в (6) с помощью применения δ-редукции.

Если в некоторое выражение  входит в качестве подвыражения такое  выражение, к которому можно применить  одну из редукций, то такое подвыражение называется редуцируемым или сокращенно редексом (от redex - reducible expression). Таким образом, процесс преобразования выражения сводится, в основном, к применению β- и δ-редукций к редексам, содержащимся в исходном выражении.

Заметим, что при применении β-редукции замене подлежат именно свободные переменные тела лямбда-выражения. Рассмотрим, например, следующее выражение:((λx.+ x ((λx.* x x) 2)) 4). В этом выражении имеются два подвыражения-редекса, к которым можно применить β-редукцию. Первый из этих редексов - это само выражение целиком, второй - подчеркнутое подвыражение. Если применить β-редукцию к первому из этих редексов - внешнему, - то получится выражение (+ 4 ((λx.* x x) 2)). Здесь при применении редукции свободное вхождение переменной x было заменено константой 4, а связанное вхождение этой переменной во внутреннем редексе осталось неизменным. Мы можем, однако, применить β-редукцию к внутреннему редексу, тогда исходное выражение будет преобразовано в выражение ((λx.+ x (* 2 2)) 4).

Последнее преобразование, называемое η-преобразованием, выражает тот факт, что две функции, которые при применении к одному и тому же аргументу дают один и тот же результат, эквивалентны. Формально η-преобразование может быть записано следующим образом: λx.E x эквивалентно E. Действительно, первое из этих выражений - λx.E x - представляет собой функцию, которая при задании ей в качестве аргумента некоторого значения выдает результат, эквивалентный результату применения функции E к этому аргументу. Возможность применения η-преобразования означает, что полученная функция эквивалентна функции E.

Основное назначение лямбда-исчисления состоит в том, чтобы показать, что любая вычислимая функция  может быть представлена в виде лямбда-выражения. При этом редукции и другие преобразования служат необходимым аппаратом для доказательства того, что построенная функция действительно дает нужный результат при применении ее к тем или иным аргументам. Например, легко видеть, что функция, представленная лямбда-выражением (λx.* x x) представляет собой функцию возведения в квадрат. Чтобы показать, что это действительно так, можно попробовать применить эту функцию к некоторым аргументам и посмотреть, действительно ли получается нужный результат (разумеется, это не строгое доказательство, а, скорее, процесс отладки, призванный убедить автора функции в том, что его функция "работает правильно"). Проверим, например, что функция действительно выдаст результат 36, если применить ее к аргументу 6. Для этого составим выражение ((λx.* x x) 6) и проведем его редукции. Сначала в результате применения β-редукции получится выражение (* 6 6), к которому можно, в свою очередь, применить δ-редукцию и окончательно получить в результате значение 36.

Вообще, редукции можно применять  до тех пор, пока в выражении имеется  хотя бы один редекс. Если ни одного редекса  в выражении нет, то говорят, что  выражение находится в нормальной форме. Наш процесс "отладки" сводится к преобразованию исходного выражения  к его нормальной форме.

Как мы уже видели, в одном  и том же выражении может содержаться  несколько редексов, а значит, процесс  преобразования выражения к нормальной форме - это не однозначный процесс. Например, мы видели, что исходное выражение ((λx.+ x ((λx.* x x) 2)) 4) может быть преобразовано двумя разными способами либо к (+ 4 ((λx.* x x) 2)), либо к((λx.+ x (* 2 2)) 4). В любом случае получившееся выражение еще не находится в нормальной форме, и может быть преобразовано далее. В первом случае процесс дальнейшего преобразования выражения происходит однозначно: сначала применяется β-редукция к единственному имеющемуся в выражении редексу, а потом два раза применяется δ-редукция. В результате последовательно получим выражения (+ 4 (* 2 2)), затем (+ 4 4) и, наконец, 8. Во втором случае опять имеем два редекса в выражении - δ-редекс (* 2 2) и все выражение, представляющее собой β-редекс. Последовательно преобразуя это выражение применением δ- и β-редукций, получим сначала ((λx.+ x 4) 4), потом (+ 4 4) и, наконец 8. Как и следовало ожидать, несмотря на разные способы преобразования выражения результат - нормальная форма - получился одним и тем же.

Справедлив и более  общий факт: если у некоторого выражения  существует нормальная форма, то она  единственна, то есть какими бы способами  ни выполнять преобразования, результат  всегда будет одним и тем же, если только вообще он будет достигнут. На самом деле нормальная форма существует не всегда, так же как не любая  программа обязана завершиться  выдачей результата. Например, уже  рассматривавшееся нами ранее выражение (λx.x x)(λx.x x) не имеет нормальной формы. Действительно, само это выражение не является нормальной формой, поскольку к нему можно применить β-редукцию. Однако, при подстановке аргумента (λx.x x) вместо переменной x в тело лямбда-выражения x x, мы получим опять то же самое выражение(λx.x x)(λx.x x). Выражение, подобное только что рассмотренному, является простейшей формой "зацикливающейся" программы.

Когда мы изучали программирование на языке Haskell, нам встречались функции, которые могли выдавать значение при одном способе вычисления, и "зацикливаться" при другом способе вычисления. В качестве таких примеров можно было рассмотреть любую из функций обработки "бесконечных" списков, которые были весьма полезны и выдавали осмысленный результат при ленивом способе передачи аргументов в функцию, однако, при энергичном способе вычисления эти функции никогда не заканчивали работу. Подобные примеры выражений можно привести и для лямбда-исчисления. Например, выражение (λx.λy.y)((λx.x x)(λx.x x)) можно привести к нормальной форме, если выполнить β-редукцию, считая все выражение редексом. Действительно, выражение представляет собой применение функции (λx.λy.y) к некоторому аргументу. Однако, аргумент x не используется в теле функции - λy.y, так что независимо от того, что представляет собой этот аргумент, результатом такой β-редукции будет выражение λy.y. С другой стороны, в исходном выражении есть и еще один редекс - "зацикливающееся" выражение(λx.x x)(λx.x x). Если применять β-редукцию к нему, то вычисления никогда не закончатся.

Можно найти и еще одну аналогию. Программы на языке Haskell могли "зациклиться" при энергичном способе вычислений и выдавать осмысленный результат при ленивых вычислениях. Однако, невозможно привести пример, при котором некоторая программа нормально заканчивает работу при энергичном способе вычислений и не может закончить работу при ленивых вычислениях. В этом смысле ленивые вычисления  - это более "аккуратный" способ исполнения программы, при котором программа всегда выдает некоторый результат, если только она может выдать результат хотя бы при одном способе вычислений. Аналогично этому, в лямбда-исчислении существует такой порядок применения редукций, который гарантирует получение нормальной формы, если только нормальная форма вообще существует для заданного выражения. Рассмотрим различные порядки применения редукций.

Пусть в некотором выражении  имеется несколько редексов. Заметим прежде всего, что любые два редекса могут быть расположены только таким образом, что они либо совсем не пересекаются, либо один из них содержится внутри другого. Так, например, в выражении (λx.λy.y)((λx.x x)(λx.x x)) имеются два редекса, при этом один из них - это полностью все выражение, а другой, содержащийся в нем, представляет собой аргумент вызова. Назовем редекс самым внешним, если он не содержится ни в каком другом из редексов в рассматриваемом выражении. Так, в рассматриваемом выражении редекс, представляющий собой все выражение, является самым внешним. Напротив, назовем редекс самым внутренним, если внутри него не содержится редексов. Второй из рассматриваемых в нашем выражении редексов - аргумент вызова - является самым внутренним. Конечно, может оказаться, что в выражении есть несколько самых внутренних и несколько самых внешних редексов, причем одни и те же редексы могут быть как самыми внешними, так и самыми внутренними. Разумеется, если редекс содержится внутри другого и при этом внутри себя также содержит редексы, то он не будет ни самым внешним, ни самым внутренним.

Рассмотрим следующий  канонический порядок редукций: пусть  преобразования происходят таким образом, что редукция всегда применяется  к самому левому из самых внутреннихредексов. При этом может оказаться, что в некоторый момент выражение окажется в нормальной форме, и тогда "вычисления" будут закончены. Может, конечно,  оказаться и так, что этот процесс никогда не будет закончен. В выражении (λx.λy.y)((λx.x x)(λx.x x)) самым внутренним является "зацикливающийся" редекс (λx.x x)(λx.x x), поэтому наш "канонический" порядок вычислений не сможет привести выражение к нормальной форме. Этот описанный порядок редукций называется аппликативным, сокращенно - АПР (аппликативный порядок редукций). Аппликативный порядок редукций можно представлять себе как порядок, при котором в каждом вызове функции прежде всего "вычисляется" значение аргумента вызова, а потом уже происходит подстановка этого значения в тело вызываемой функции. Таким образом, этот порядок редукций соответствует энергичному способу вычисления значения функций в функциональном программировании.

Можно рассмотреть и еще  один порядок применения редукций. Можно всегда применять редукцию к самому левому из самых внешних редексов. Этот порядок редукций называетсянормальным или сокращенно НПР (нормальный порядок редукций). Таким образом, если выражение представляет собой применение функции к аргументам, то подстановка аргумента в тело функции происходит до того, как преобразования будут производиться над самими аргументами. Такая схема преобразования выражения похожа на процесс ленивых вычислений в функциональных языках программирования, но если обращение к аргументу в теле функции происходит несколько раз, то при схеме ленивых вычислений в функциональных языках программирования вычисление аргумента все-таки осуществляется лишь однажды - при первом обращении к аргументу; в дальнейшем происходит обращение к уже вычисленному значению. В нашей же схеме применения редукций к выражениям в лямбда-исчислении процесс преобразования выражения, которое служит аргументом применения функции, будет происходить столько раз, сколько раз аргумент появляется в определении этой функции.

Рассмотрим, например, следующее  выражение, представляющее собой применение функции возведения в квадрат  к результату сложения двух чисел: (λx.* x x)(+ 3 4). Все выражение представляет собой самый внешний редекс, а выражение аргумента - самый внутренний редекс. Поэтому при аппликативном порядке редукций выражение будет приведено к нормальной форме с помощью следующих трех шагов преобразования. Сначала, после применения δ-редукции к выражению аргумента получим (λx.* x x) 7, потом β-редукция преобразует это выражение к (* 7 7) и, наконец, последнее применение δ-редукции приведет выражение к нормальной форме 49. При нормальном порядке редукций первой будет применена β-редукция ко всему выражению, в результате чего получится выражение (* (+ 3 4) (+ 3 4)), представляющее собой применение функции умножения к двум одинаковым аргументам, представляющим собой сдублированное выражение, которое в исходном выражении было представлено лишь в одном экземпляре. Теперь для получения окончательного результата потребуются еще три шага δ-редукции, после которых будут последовательно получены выражения (* 7 (+ 3 4)), затем (* 7 7) и, наконец, 49.

Приведенный пример показывает, что при применении НПР для  приведения выражения к нормальной форме может потребоваться больше шагов, чем при применении АПР, однако, НПР более "надежен", так как он позволяет получить нормальную форму выражения всегда, если только такая форма вообще существует. Так, например, уже рассмотренное нами ранее выражение(λx.λy.y)((λx.x x)(λx.x x)) может быть приведено к нормальной форме за один шаг при применении НПР, однако, АПР не позволит найти эту нормальную форму ни за какое конечное число шагов

До сих пор мы преобразовывали  выражения, используя только β- и  δ-редукции. В применении α- и η-преобразований просто не было необходимости. Рассмотрим, однако, следующее выражение: λy.(λy.+ 2 y)(+ 1 y). В этом выражении имеется функция, тело которой представляет собой применение некоторой простой функции аргументу (+ 1 y). К сожалению, формальные аргументы обеих функций представлены переменной с одним и тем же именем - y. Это может привести к ошибке, если подстановку производить неправильно. Пусть, например, описанное выражение применяется к константе 1. При применении НПР в выражение (λy.+ 2 y)(+ 1 y) надо подставить единицу вместо свободного вхождения переменной y. В результате получится выражение (λy.+ 2 y)(+ 1 1), которое в результате следующих шагов будет преобразовано последовательно в (+ 2 (+ 1 1)), затем в (+ 2 2) и, наконец, в 4. Если, однако, ошибочно выполнить подстановку вместо всех вхождений переменной y в тело функции, то мы получим выражение (λy.+ 2 1)(+ 1 1), которое в результате дальнейших преобразований примет вид сначала (+ 2 1) и после следующего шага - 3. Это, очевидно, неправильно, но для того, чтобы такой ошибки избежать, надо при каждой подстановке определять, какие вхождения переменной являются свободными, а какие связанными. Если выражения достаточно сложные, то это не так-то просто.

Можно, однако, с самого начала постараться избежать подобных ошибок, выполнив α-преобразование перед применением редукций. Так, если сначала преобразовать исходное выражение к виду λz.(λy.+ 2 y)(+ 1 z), то при применении его к константе 1 ошибку сделать будет уже гораздо труднее. Правда, ошибиться можно и при выполнении начального α-преобразования.

В вышеописанном примере  α-преобразование использовалось только для того, чтобы облегчить применение редукций; если преобразование происходит автоматически, и программа, выполняющая преобразование, достаточно "интеллектуальна", чтобы отличать свободные вхождения переменных от связанных, то переименование можно было и не производить. Однако, бывают случаи, когда без переименования переменных не обойтись. Рассмотрим, например, следующее выражение: λy.(λx.λy.+ x y) y. Здесь также имеются два лямбда-выражения, имеющих одну и ту же переменную - y. Соответственно, во внешнем лямбда-выражении одно вхождение переменной y является свободным, а другое - связанным. В этом выражении имеется единственный редекс, представляющий собой тело функции, определенной внешним лямбда-выражением. Попытка применить β-редукцию без предварительного проведения α-преобразования приведет к ошибке: мы получим выражение λy.(λy.+ y y), в котором свободное вхождение переменной y попало в позицию, где переменная y связана.

Очевидно, что полученное выражение не эквивалентно исходному. Чтобы убедиться в этом, можно попробовать применить исходную и результирующую функцию к одним и тем же аргументам, например, к аргументам 1 и 2. Для исходного выражения, применяя β-редукции в нормальном порядке, последовательно получим следующие выражения: ((λy.(λx.λy.+ x y) y) 1 2), затем (((λx.λy.+ x y) 1) 2), ((λy.+ 1 y) 2), (+ 1 2), и, наконец, 3. Для выражения, полученного в результате неправильного применения редукции, получим: ((λy.(λy.+ y y)) 1 2), ((λy.+ y y) 2), (+ 2 2) и, наконец, 4. Итак, видим, что иногда применение β-редукции без предварительного переименования переменных может привести к ошибке.

Можно высказать и более  общее утверждение: β-редукция может привести к ошибке тогда, когда выражение, имеющее в своем составе свободную переменную, подставляется в качестве аргумента в выражение, имеющее в своем составе связанную переменную с тем же именем. Заметим, что необходимость в такой подстановке возникает лишь в определенном случае, а именно, тогда, когда редукции производятся внутри лямбда-выражения, то есть преобразованию подвергается тело определяемой функции. Если имеется некоторое лямбда-выражение, содержащее внутри себя редексы, то при применении АПР редукции в теле лямбда-выражения всегда будут производиться до того, как это лямбда-выражение будет применено к аргументу. Однако, при применении НПР необходимость в выполнении редукций внутри лямбда-выражения может возникнуть только тогда, когда это лямбда-выражение не применяется уже ни к каким аргументам, в противном случае, сначала будет произведена подстановка аргумента, а затем уже будет производиться редукция полученного выражения. Это означает, что мы можем избежать необходимости переименования переменных в выражении, если будем применять НПР, оставляя редексы внутри лямбда-выражений без преобразования. Следуя этому правилу, мы в результате последовательного применения β- и δ-редукций не получим нормальной формы выражения, однако, получим довольно близкий ее эквивалент - так называемую слабую заголовочную нормальную форму (сокращенно - СЗНФ).