Рекурсивные функции и лямбда исчисление а черча
В основе функционального программирования лежит идея, что в результате каждого действия возникает значение. Значения становятся аргументами следующих действий, и конечный результат всей задачи выдается пользователю. Программа строится из логически расчлененных определений функций, которые состоят из организующих вычисления управляющих структур и из вложенных, часто вызывающих самих себя (рекурсивных) вызовов функций.
Основными средствами функционального программирования как раз и являются композиция и рекурсия. Ни ячеек памяти, ни операторов присваивания, ни циклов, ни, тем более, блок-схем, ни передач управления.
В основе функционального программирования лежит строгий математический аппарат лямбда-исчисления Чёрча и теория рекурсивных функций.
Введенное в 1931 году математиком Алонзо Черчем, лямбда-исчисление оперирует всего тремя типами элементов:
• символами, представляющими переменные и константы;
• скобками для группировки символов;
• обозначениями функций с использованием греческой буквы лямбда.
Лямбда-исчисление используется для синтаксического описания свойств математических функций и обработки их в качестве правил.
Функциональная программа состоит из совокупности определений функций. Функции, в свою очередь, представляют собой вызовы других функций и предложении, управляющих последовательностью вызовов.
Вычисления начинаются с вызова некоторой функции, которая в свою очередь вызывает функции, входящие в состав ее определения и т. д. в соответствии с иерархией определений и структурой условных предложений. Функции могут прямо или опосредованно вызывать сами себя. Каждый вызов возвращает некоторое значение в вызвавшую его функцию, вычисление которой после этого продолжается. Процесс вычислений повторяется до тех пор, пока запустившая вычисления функция не вернет конечный результат пользователю. В функциональном программировании нет места присваиванию и передаче управления. Разветвление вычислений основано на механизме обработки аргументов условного предложения. При таком подходе к программированию рекурсия является единственным способом организации повторяющихся вычислений.
В функциональной программе не должно быть:
• функций с побочными эффектами.
Этот перечень следует из основного свойства функционального программирования – прозрачности по ссылкам.
Прозрачность по ссылкам – необходимое условие функциональной программы
Прозрачность по ссылкам (функциональность) является фундаментальным свойством математических функций и может быть сформулировано следующим образом: значение функции зависит только от нее самой и аргументов вызова. Это означает, что каждое выражение определяет единственную величину, которую нельзя изменить ни путем ее вычисления, ни предоставлением различным частям программы возможности совместно использовать это выражение.
Ссылки на некоторую величину эквивалентны самой величине, и возможность ссылаться на некоторое выражение из другой части программы не влияет на значение этого выражения.
Большинство императивных языков позволяют функции в процессе своего выполнения читать и изменять значения глобальных переменных. Такие функции называются функциями с побочными эффектами. Поэтому, если вызывать одну и ту же функцию несколько раз с одним и тем же аргументом, можно в результате получать различные результаты.
В функциональном программировании оператор присваивания отсутствует, объекты нельзя изменять и уничтожать, можно только создавать новые путем декомпозиции и синтеза существующих объектов. О ненужных объектах позаботится встроенный в язык сборщик мусора (удаление ненужных объектов программы вынесено на уровень системы). Благодаря этому в функциональных языках все функции свободны от побочных эффектов.
Из отсутствия побочных эффектов следует еще одно преимущество – параллелизм вычислений. На интуитивном уровне понятно, что если все функции для вычислений используют только свои параметры, можно вычислять независимые функции в произвольном порядке или, скажем, параллельно, на результат вычислений это не повлияет. Причем параллелизм этот может быть организован как на уровне компилятора языка, так и на уровне архитектуры. В лямбда-исчислении доказывается теорема, которая подтверждает это интуитивное соображение на уровне математической теории.
Функциональным языкам присущи энергичный и ленивый виды вычислений.
В большинстве императивных языков программирования при применении функции к аргументу сначала вычисляется аргумент, а затем уже передается функции. В этом случае говорят, что аргумент передается по значению, подразумевая при этом, что только его значение передается в тело функции. Такое правило вычислений или механизм вызова называется вызовом по значению. Его преимущество заключается в том, что реализация достаточно проста: сначала вычисляется аргумент, а затем вызывается функция. Недостатком является избыточное вычисление, когда в некоторых случаях значение аргумента не требуется вызываемой функции.
Противоположным вызову функции по значению является вызов по необходимости, при котором все аргументы передаются функции в невычисленном виде и вычисляются только тогда, когда в них возникает необходимость внутри тела функции. Преимущество вызова по необходимости состоит в отсутствии лишних вычислений, если значение аргумента не понадобится. Его недостаток более сложная, по сравнению с вызовом по значению, реализация системы программирования. В этом случае функциям передаются не значения тех или иных параметров, а выражения, которые при определенных условиях придется вычислять и применять уже в теле функции. Вызов по необходимости не характерен для императивных языков программирования и многих функциональных языков, а функциональные языки, поддерживающие вызов по необходимости, в большинстве своем снабжены конструкторами, обеспечивающими вычисление по схеме вызов по значению.
В теории функционального программирования принято говорить о двух крайних видах вычисления: энергичном и ленивом. Эти варианты выделяются, так как представляют крайние случаи, хотя существуют и другие варианты.
Ленивое вычисление – стратегия планирования, при которой вычисления не выполняются до тех пор, пока не возникнет необходимость в их результатах.
Энергичное вычисление – стратегия, при которой вычисления выполняются, как только появляется возможность их выполнить. Принцип энергичного вычисления можно сформулировать следующим тезисом: «на каждом шаге вычисляется все, что может быть вычислено». Не важно, пригодится ли в конечном случае полученный результат. Таким образом, всегда существует вероятность выполнения лишних вычислений.
Принцип ленивого вычисления: «не вычислять ничего, что не требуется в данный момент». Можно провести некоторую аналогию энергичного вычисления в функциональных языках с механизмом вызова по значению в императивных языках, а ленивое вычисление с механизмом вызова по необходимости. Однако между ними не существует тождественного равенства, и точное соотношение между этими терминами будет ясно, после изучения гл. 9.
Если функциональный язык не поддерживает отложенные вычисления, то он называется строгим (strict) языком программирования, в отличие от нестрогого (lazy) языка, с ленивой стратегией вычисления.
Математические основы функционального программирования: лямбда-исчисление А.Черча и теория рекурсивных функций: основные понятия и положения. Программирование в функциональных обозначениях. Строго функциональный язык. Соответствие между функциональными и императивными программами.
Введение в лямбда-исчисление
В 1941 году в своей статье “исчисление функций” американский математик Алонсо Черч предложил достаточно простой формализм для описания частично рекурсивных функций (Частично рекурсивная функция – функция, зависящая от своего результата при других входных параметрах и, возможно, определённая не для всех входных данных ), а также высказал знаменитый тезис Черча, одной из формулировок которого является следующая: любая функция, вычислимая интуитивно, эквивалентна некоторой частично рекурсивной функции . При этом следует понимать, что, несмотря на слово “интуитивно”, описание алгоритма должно быть однозначным и не должно требовать от исполняющего его домысливания этого алгоритма, под интуитивным вычислением понимается лишь представление о том, что алгоритм вычисления действительно существует. Существует также деление тезиса Черча на “слабую” и “ сильную” формулировки, последняя из которых утверждает априори эквивалентность всех определений вычислимости. Тезис Черча не был, да и не может быть доказан в виду нестрогой формулировки, однако с тех пор никому так и не удалось его опровергнуть.
Чистое лямбда-исчисление является формальной теорией, в которой существуют лишь три конструкции – переменные, определения и применения функций. В чистом лямбда-исчислении изучаются редукции, причём теория не содержит никаких дополнительных выражений, за исключением альфа и бета-редукций. Существует также лямбда-эта теория, где дополнительно рассматривается эта-редукция.
Лямбда-исчисление очень удобно для определения вычислимости. Например, Тьюринг показал, что вычислимость в терминах машины Тьюринга эквивалентна собственно возможности лямбда-описания системы. Клин доказал, что эта возможность описания также эквивалентна рекурсивности Гёделя-Гербрандта. Таким образом, если задача сформулирована с помощью лямбда-исчисления, то она имеет решение за конечное время ( Следует понимать разницу между чистым лямбда-исчислением и языками функционального программирования. Утверждение, что любая сформулированная на Lisp задача вычислима – неверно ).
Лямбда-исчисление оперирует следующими основными понятиями – лямбда-выражение, редукция и редекс. Лямбда-выражение – специального вида выражение, синтаксис которого с помощью формул Бэкуса-Наура можно записать так:
M ::= x | ( M 1 M 2 ) | ( x.M)
Где x – переменная, (M 1 M 2 ) – применение функции M 1 к аргументу M 2
( x.M) – абстракция (определение функции с параметром x и телом M ).
В качестве примера приведём лямбда-выражение ( x. x*x) 10. Данное выражение означает применение функции возведения в квадрат к числу 10. Такая формула называется термом. Результатом редукции этого терма, очевидно, явится число 100. В чистом лямбда-исчислении рассматриваются только переменные, абстракции и применения, оно не рассматривает никаких привязок к конкретным предметным областям. Поэтому приведённый пример ( x. x*x) 10 не может считаться чистым лямбда-термом, так как содержит в себе арифметические знаки. В прикладном лямбда-исчислении допустимы константы, которые могут быть не только числовыми, но также и именами объектов и функций. Когда говорят о лямбда-исчислении, обычно имеют в виду именно прикладное лямбда-исчисление.
Для лямбда-термов вводится понятие бета-эквивалентности. M = N. Для приведённого выше примера можно сказать, что ( x. x*x) 10= 10*10. В более общем виде это записывается так:
Упрощённо говоря, бета-эквивалентность означает, что левая и правая части выражения имеют одно и то же значение.
Одним из синтаксических соглашений лямбда-исчисления является то, что применение функции имеет более высокий приоритет, нежели абстракция, поэтому ( x . x y ) должно рассматриваться как ( x .( x y )) , т.е. определение функции x как применение x к переменной y. Также в лямбда-выражениях иногда раскрывают скобки, например, ( ( x y ) z ) можно представить как x y z , а ( x ( y z )) как x ( y z ) . При отсутствии функций применения группируются слева направо. Также выражения, содержащие несколько вложенных абстракций могут быть преобразованы к одной абстракции, например, выражение x. y . z . M , может быть записано как xyz.M
Вхождение переменной x сразу за символом в x.M называется связывающим вхождением или просто связыванием x . Все вхождения x в ( x.M) называются связанными в области этого связывания. Все не связанные вхождения переменных в терм являются свободными. Каждое вхождение переменной может быть либо связанным, либо свободным (не может быть и тем и другим). Надо иметь в виду, что переменная является свободной в терме, если хотя бы в одном из подтермов она является свободной, например, ( x. y ) ( y . y ) переменная y является свободной.
Применение функции может рассматриваться как подстановка значения, к которому она применяется, во все вхождения аргумента в тело функции. Например, ( x. x +5* x * x ) m может рассматриваться как m + m * m 2 . Подстановка терма. Подстановка терма N вместо переменной x в терме N записывается как
Если свободные переменные в N не имеют связанных вхождений в M , то терм
Если же существует такая переменная y , которая свободна в N и связана в M , то все связанные вхождения y в M заменяются на некоторую новую переменную z . Так продолжается до тех пор, пока не станет возможным применение предыдущего правила
По сравнению с языками функционального программирования, подобным Ilaskell, в лямбда-исчислении не хватает чисто практических средств, позволяющих удобно записывать функции. Прежде всего, бросается в глаза отсутствие средств описания рекурсивных функций. Действительно, рекурсивные обращения всегда происходят с использованием имени функции, однако лямбда-исчисление — это язык для описания безымянных функций! Конечно, иногда мы можем обойтись и без применения рекурсии, если имеется достаточно богатый набор встроенных функций. Например, имея функцию высшего порядка foldr в качестве одной из встроенных функций, мы можем написать функцию вычисления факториала натурального числа и без использования рекурсии. Аналогично функция свертки дерева tfoldr позволила нам в гл. 4 написать без использования рекурсии функцию линеаризации дерева linearize.
Имея достаточно богатый набор мощных функций высшего порядка, можно всегда обойтись без использования рекурсивных вызовов (такой стиль программирования был, например, использован Джоном Бэкусом при создании системы программирования FP). Однако чистое лямбдаисчисление не предполагает использования встроенных функций вообще! Возникает вопрос: достаточно ли средств лямбда-исчисления для того, чтобы выразить в нем всевозможные вычислимые функции, если в нем невозможно обычным образом задавать рекурсивные функции, а встроенных функций, позволяющих обойти эту проблему, нет вообще?
В этом и следующем параграфах мы постепенно построим чистое лямбда-исчисление, последовательно выразив в виде лямбда-выражений все имевшиеся у нас ранее константы и встроенные функции и задав с помощью тех же лямбда-выражений все управляющие конструкции языков функционального программирования, включая рекурсию, условное вычисление и др. Начнем мы именно с выражения прямой и косвенной рекурсии в чистом лямбда-исчислении.
Пусть у нас имеется функция, в определении которой есть прямое рекурсивное обращение к себе, например, такое, как определение функции вычисления факториала в языке Haskell: fact n = if n == 0 then 1 else n * fact(n-l)
Прежде всего, зададим эту функцию с помощью конструкций лямбда- исчисления, считая, что у нас имеются встроенные функции для вычитания (функция -), умножения (функция *) и сравнения с нулем (функция eqO). Кроме того, считаем, что у нас также есть функция IF для условного вычисления и константы 0 и 1. Тогда определение функции будет выглядеть следующим образом:
fact = An.IF (eqO п) 1 (* п (fact (- п 1)))
Здесь мы пока по-прежнему использовали задание имени для функции fact, чтобы выразить рекурсию. Построим теперь новую функцию, в которой вызываемая функция fact будет аргументом: sFact = Af.An.IF (eqO n) 1 (* n (f (- n 1) ) )
Конечно, эта новая функция не будет тем факториалом, который мы пытаемся построить, хотя бы потому, что ее аргументом является не целое число, а некоторая функция, однако она некоторым вполне определенным образом связана с той функцией вычисления факториала, которую мы пытаемся построить. Зададимся задачей найти такую функцию f, что она является неподвижной точкой определенной нами функции sFact, т.е. такую f, что выполнено равенство f = sFact f. Очевидно, что если такую неподвижную точку удастся найти, то найденная функция f как раз и будет тем самым факториалом, который мы ищем, поскольку будет выполнено равенство
f = sFact f = An.IF (eqO n) 1 (* n (f (- n 1)))
Итак, задача нахождения функции, эквивалентной заданной рекурсивной функции, свелась к задаче построения неподвижной точки для некоторой другой функции. Кажется, что эту задачу — задачу нахождения неподвижной точки — в общем виде решить не удастся. A priori вообще не ясно, всегда ли такая неподвижная точка существует. Однако оказывается, что удается построить функционал, который для заданного функционального аргумента вычисляет его неподвижную точку. Если обозначить через Y такой функционал нахождения неподвижной точки, то для любой функции f должно быть справедливо равенство Y f = f (Y f). Другими словами, результатом применения функции Y к функции f должно быть такое значение х, что х = f (х). Одну из таких функций предложил Хаскелл Карри, и теперь эта функция в его честь называется Y-комбинатором Карри. Вот запись этой функции в нотации лямбда-исчисления:
Y = Ah. (Ax.h (х х) ) (Ax.h (х х) )
Проверим, действительно ли для этой функции выполнено равенство
Y f = f (Y f). Для этого запишем выражение Y f и попробуем привести его к СЗНФ. После того как вместо Y будет подставлено соответствующее лямбда-выражение, мы сможем выполнить один шаг р-редукции, и в результате получим выражение (Хх. f (х х) ) (Хх. f (х х) ). Это выражение еще не находится в СЗНФ, так что мы можем выполнить еще один шаг и с помощью Р-редукции привести его к виду f ( (Хх. f (х х)) (Хх. f (х х))). Это выражение также не находится в СЗНФ, более того, теперь видно, что привести это выражение к СЗНФ вообще никогда не удастся, так как каждый следующий шаг редукции приводит только к увеличению длины выражения. Однако из проведенных шагов очевидно, что выражение Y f действительно эквивалентно выражению f (Y f), поскольку второе получается из первого за два шага редукций.
Итак, выражение для рекурсивной функции можно получить, если построить некоторое вспомогательное выражение, а затем применить к нему Y-комбинатор Карри. Получившееся при этом выражение не может быть приведено к СЗНФ, однако оно все же будет работать как соответствующая рекурсивная функция. Убедимся в этом, построив описанным способом функцию для вычисления факториала заданного числа, а затем применим ее к конкретному числу, скажем, 2, и проверим, как получается результат вычисления — число 2, равное (fact 2). Для этого попробуем привести к СЗНФ выражение (Y sFact) 2, где Y обозначает Y-комбинатор Карри, a sFact — функцию, приведенную выше, полученную из рекурсивного определения факториала. Последовательные шаги по преобразованию выражения к СЗНФ показаны ниже:
sFact (Y sFact) 2
- (Af.An.IF (eqO n) 1 (* n (f (- n 1)))) (Y sFact) 2
- (An.IF (eqO n) 1 (* n ( (Y sFact) (- n 1)))) 2
IF (eqO 2) 1 (* 2 ((Y sFact) (- 2 1)))
Остановимся па этом месте. Мы видим, что последовательное выполнение (3- и 6-редукций привело нас от выражения Y sFact 2 к выражению (* 2 (Y sFact 1)). Это уже показывает, что преобразование выражения происходит именно так, как ведет себя рекурсивное вычисление факториала. Продолжим преобразования:
- (* 2 (Y sFact 1))
- (* 2 (sFact (Y sFact) 1)
- (* 2 (Af.An.IF (eqO n) 1 (* n (f (- n 1)))) (Y sFact) 1)
- (* 2 (An.IF (eqO n) 1 (* n ((Y sFact) (- n 1)))) 1)
- (* 2 (IF (eqO 1) 1 (* 1 ((Y sFact) (- 1 1)))))
- (* 2 (* 1 (Y sFact 0)))
- (* 2 (* 1 (sFact (Y sFact) 0)))
- (* 2 (* 1 ((Xf.Xn.IF (eqO n) 1 (* n (f (- n 1)))) (Y sFact)
- 0) ) )
- (* 2 (* 1 ( (Xn. IF (eqO n) 1 (* n ( (Y sFact) (- n 1)))) 0)))
- (* 2 (* 1 (IF (eqO 0) 1 (* 0 ( (Y sFact) (- 0 1))))))
- (* 2 (* 1 1))
- 2
Преобразования закончились вполне предсказуемым результатом, так что можно заключить, что применение Y-комбинатора Карри действительно приводит к нужному результату. Мы избежали зацикливания при вычислении функции, полученной с помощью Y-комбинатора, так как на предпоследнем шаге функция IF просто отбросила ненужное далее подвыражение, содержащее эту функцию. Это вполне соответствует тому, как при «обычных» вычислениях мы попадаем в ветку, не содержащую рекурсивного обращения.
Существенно, что мы использовали при вычислениях нормальный порядок редукций, так как при аппликативном порядке редукций вычисления просто никогда не были бы закончены. Существуют и другие формы Y-комбинаторов, в частности такие, которые применимы и при АИР, однако все другие известные выражения для Y-комбинаторов выглядят сложнее, чем Y-комбинатор Карри.
Если несколько функций определяются таким образом, что в теле каждой из них имеются вызовы других функций из этого набора, то говорят, что мы имеем дело со взаимно-рекурсивными функциями. Этот случай можно свести к прямой рекурсии и, тем самым, выразить в лямбда-исчислении не только прямую, но и взаимную или косвенную рекурсию. Для того чтобы свести взаимную рекурсию к прямой, нам потребуются некоторые встроенные функции, упомянутые в параграфе 9.1. Во-первых, это набор функций кортежирования TUPLE-k, которые составляют кортеж из своих аргументов, и во-вторых, функция INDEX, позволяющая извлечь элемент кортежа по его номеру.
Теперь пусть имеются определения взаимно-рекурсивных функций f 1 = Fx (fг, f2, . . . fn) f2 = F2 [f1, f2. fn)
где все Fi — выражения, в которых встречаются рекурсивные обращения к определяемым функциям fir f2, . . . fn. Прежде всего, образуем новое выражение, представляющее собой кортеж, в котором собраны все определения функций:
Каждая из определяемых функций fir f2, . . . fn может теперь быть выражена с помощью выделения соответствующего элемента этого кортежа:
поэтому если мы теперь подставим в определение кортежа Т вместо всех вхождений fi их выражения в виде элемента кортежа, то получим рекурсивное определение для кортежа Т с прямой рекурсией:
Fn( (INDEX 1 T). (INDEX n T) )
Кортеж T теперь может быть представлен, как и раньше, с помощью Y-комбинатора
Y (AT.TUPLE-n Fx ( (INDEX 1 Т), . . . (INDEX n T) ) . . .
Fn((INDEX 1 T). (INDEX n T) ) )
а каждая из отдельно взятых функций может быть получена в виде элемента этого кортежа.
В этой главе мы узнаем о лямбда-исчислении. Лямбда-исчисление описывает понятие алгоритма. Ещё до появления компьютеров в 30-е годы двадцатого века математиков интересовал вопрос о возможности создания алгоритма, который мог бы на основе заданных аксиом дать ответ о том верно или нет некоторое логическое высказывание. Например у нас есть базовые утверждения и логические связки такие как “и”, “или”, “для любого из”, “существует один из”, с помощью которых мы можем строить из базовых высказываний составные. Некоторые из них окажутся ложными, а другие истинными. Нам интересно узнать какие. Но для решения этой задачи прежде всего необходимо было понять а что же такое алгоритм?
Ответ на этот вопрос дали Алонсо Чёрч (Alonso Church) и Алан Тьюринг (Alan Turing). Чёрч разработал лямбда-исчисление, а Тьюринг теорию машин Тьюринга. Оказалось, что задача автоматического определения истинности формул в общем случае не имеет решения.
В основе лямбда-исчисление лежит понятие функции. Мы можем составлять сложные функции из простейших, а также подставлять в функции аргументы, которые могут быть как константами так и другими функциями. Как только мы составили выражение мы можем передать его вычислителю. Он подставляет аргументы в функции и возвращает такое выражение, в котором невозможно далее проводить подстановки аргументов. Этот процесс проведения подстановок считается вычислением алгоритма.
В рамках теории машин Тьюринга алгоритм описывается по-другому. Машина Тьюринга имеет внутреннее состояние, Состояние содержит некоторое значение, которое изменяется по ходу работы машины. Машина живёт не сама по себе, она читает ленту символов. Лента символов – это большая цепочка букв. На каждую букву машина реагирует серией действий. Она может изменить значение состояния, обновить букву в ленте или перейти к следующему или предыдущему символу. Есть состояния, которые обозначают конец работы, они называются терминальными. Как только машина дойдёт до терминального состояния мы считаем, что вычисление алгоритма закончилось. После этого мы можем считать результат из состояний машины.
Функциональные языки программирования основаны на лямбда-исчислении. Поэтому мы будем говорить именно об этом описании алгоритма.
Лямбда исчисление без типов
Составление термов
Можно считать, что лямбда исчисление это такой маленький язык программирования. В нём есть множество символов, которые считаются переменными, они что-то обозначают и неделимы. В лямбда-исчислении программный код называется термом. Для написания программного кода у нас есть всего три правила:
Переменные $x$ , $y$ , $z$ … являются термами.
Если $M$ и $N$ – термы, то $(MN)$ – терм.
Если $x$ – переменная, а $M$ – терм, то $(\lambda x .M)$ – терм
В формальном описании добавляют ещё одно правило, оно говорит о том, что других термов нет. Первое правило, говорит о том, что у нас есть алфавит символов, который что-то обозначает, эти символы являются базовыми строительными блоками программы. Второе и третье правила говорят о том как из базовых элементов получаются составные. Второе правило – это правило применения функции к аргументу. В нём $M$ обозначает функцию, а $N$ обозначает аргумент. Все функции являются функциями одного аргумента, но они могут принимать и возвращать функции. Поэтому применение трёх аргументов к функции $Fun$ будет выглядеть так:
$$(((Fun\ Arg1)\ Arg2)\ Arg3)$$
Третье правило говорит о том как создавать функции. Специальный символ лямбда ( $\lambda$ ) в выражении $(\lambda x .M)$ говорит о том, что мы собираемся определить функцию с аргументом $x$ и телом функции $M$ . С такими функциями мы уже сталкивались. Это безымянные функции. Приведём несколько примеров функций. Начнём с самого простого, определим тождественную функцию:
Функция принимает аргумент $x$ и тут же возвращает его в теле. Теперь посмотрим на константную функцию:
$$(\lambda x .(\lambda y .x))$$
Константная функция является функцией двух аргументов, поэтому наш терм принимает переменную $x$ и возвращает другой терм функцию $(\lambda y .x)$ . Эта функция принимает $y$ , а возвращает x . В Haskell мы бы написали это так:
Точка сменилась на стрелку, а лямбда потеряла одну ножку. Теперь определим композицию. Композиция принимает две функции одного аргумента и направляет выход второй функции на вход первой:
$$(\lambda f .(\lambda g .(\lambda x .(f(gx)))))$$
Переменные $f$ и $g$ – это функции, которые участвуют в композиции, а $x$ это вход результирующей функции. Уже в таком простом выражении у нас пять скобок на конце. Давайте введём несколько соглашений, которые облегчат написание термов:
Понятие вычислимости — очень важная и красивая математическая идея. Примечателен также и ее малый возраст в сравнении с другими столь же фундаментальными математическим проблемами: она была впервые выдвинута только в 1930-х годах. Эта проблема имеет отношение ко всем областям математики (хотя, справедливости ради, отметим, что большинство математиков пока не часто обращаются к вопросам вычислимости). Сила этой идеи связана отчасти с существованием четко определенных и все же неразрешимых математических операций (как, например, проблема остановки машины Тьюринга и некоторые другие, которые мы рассмотрим в главе 4). Если бы не было таких невычислимых объектов, то теория алгоритмической разрешимости не представляла бы особого интереса для математики. В конце концов, математики любят головоломки.
Задача о разрешимости определенной математической операции может их заинтриговать, особенно потому, что общее решение этой головоломки само по себе алгоритмически не разрешимо.
Следует сделать еще одно замечание. Вычислимость — это по-настоящему «абсолютная» математическая идея. Это абстрактное понятие, которое никак не зависит от какой-либо конкретной реализации в терминах «машин Тьюринга» в том виде, как я их описал выше. Как я уже указывал, нет необходимости придавать какое-либо специальное значение «лентам», «внутренним состояниям» и т. п., характерным для гениального, но тем не менее частного подхода Тьюринга. Существуют также и другие способы выражения идеи вычислимости, причем исторически первым было «лямбда-исчисление», предложенное американским логиком Алонзо Черчем совместно со Стивеном Клини. Процедура, предложенная Черчем, значительно отличалась от метода Тьюринга и была гораздо более абстрактна. Фактически, форма, в которой Черч изложил свою теорию, делала связь между ними и чем бы то ни было «механическим» совсем не очевидной. Главная идея, лежащая в основе процедуры Черча, абстрактна по своей сути — это математическая операция, которую сам Черч назвал «абстрагированием».
Мне кажется, что стоит привести краткое описание схемы Черча не только потому, что она подчеркивает математическую природу идеи вычислимости, не зависящую от конкретного понятия вычислительной машины, но и потому, что она иллюстрирует мощь абстрактных идей в математике. Читатель, не достаточно свободный в математике и не увлеченный излагаемыми математическими идеями как таковыми, скорее всего предпочтет сейчас перейти к следующей главе — и не утратит при этом нить рассуждений. Тем не менее я полагаю, что таким читателям будет небесполезно следовать за мной еще какое-то время и оценить чудесную по своей стройности и продуманности схему Черча (см. Черч [1941]).
В рамках этой схемы рассматривается «универсальное множество» различных объектов, обозначаемых, скажем, символами
каждый из которых представляет собой математическую операцию, или функцию. (Штрихованные буквы позволяют создавать неограниченные наборы символов для обозначения таких функций.) «Аргументы» этих функций, т. е. объекты, на которые эти функции действуют, в свою очередь являются объектами той же природы, т. е. функциями. Более того, результат действия одной функции на другую (ее «значение») также представляет собой функцию. (Поистине, в системе Черча наблюдается замечательная экономия понятий.) Поэтому, когда мы пишем[56]
а = bс,
мы подразумеваем, что функция b, действуя на функцию c, дает в результате другую функцию а. В рамках этой схемы нетрудно сформулировать понятие функции двух или более переменных. Если мы хотим представить f как функцию двух переменных, скажем р и q, то мы можем просто написать
(что есть результат действия функции fp на функцию q ). Для функции трех переменных можно использовать выражение
Теперь мы можем перейти к описанию важнейшей операции абстрагирования. Для нее мы будем использовать греческую букву ? (лямбда). Непосредственно за ней будет следовать символ одной из функций Черча, скажем х, который мы будем рассматривать как «фиктивную переменную». Каждое появление х в квадратных скобках, следующих сразу за этим выражением, обозначает теперь просто место, куда подставляется все, что идет за всем этим выражением. Таким образом, когда мы пишем
?x. [fx],
мы подразумеваем функцию, которая при действии на, например, а имеет значение fа, т. е.
(?х. [fx ])a = fа.
Другими словами, ?х. [fх] — это просто функция f, т. е.
?х. [fх ] = f.
Сказанное выше требует определенного осмысления. Это одна из тех математических тонкостей, которые на первый взгляд кажутся настолько педантичными и тривиальными, что их смысл часто совершенно ускользает от понимания. Рассмотрим пример из знакомой всем школьной математики. Примем за f тригонометрическую функцию — синус угла. Тогда абстрактная функция «sin» будет определяться выражением
?х. [sin х ] = sin.
(Не придавайте большого значения тому, что в качестве «функции» х может фигурировать величина угла. Мы скоро увидим, каким образом числа можно иногда рассматривать как функции, а величина угла — это просто число.) До сих пор все на самом деле тривиально. Однако представим себе, что обозначение «sin» не было изобретено, но нам известно о существовании представления sin х в форме степенного ряда:
Тогда мы могли бы ввести определение
Можно было поступить еще проще и определить, например, операцию «одна шестая куба», для которой не существует стандартного «функционального» обозначения:
К обсуждаемым проблемам большее отношение имеют выражения, составленные просто из элементарных функциональных операций Черча, таких как
Это функция, которая, действуя на другую функцию, скажем g, дает дважды итерированную g, действующую на x
Мы могли бы сначала «абстрагироваться» от x и рассмотреть выражение
которое можно сократить до
Это и есть операция, применение которой к g дает функцию «вторая итерация g». По сути, это та самая функция, которую Черч обозначил номером 2 :
2 = ?fx.[f (fx)],
так что (2g) y = g (gy). Аналогичным образом он определил:
3 = ? fx. [f (f (fx))],
4 = ?fх. [f (f (f (fx)))], и т. д.,
1 = ?fх. [fх] и 0 = ? fx.
Видно, что 2 Черча больше похоже на «дважды», 3 — на «трижды» и т. д. Значит, действие 3 на функцию f, т. е. 3f равносильно операции «применить f три раза», поэтому 3f при действии на у превращается в
(3f)y = f (f (f (y))) -
Посмотрим, как в схеме Черча можно представить очень простую математическую операцию — прибавление 1 к некоторому числу. Определим операцию
S = ?abc. [b ((аb)с)].
Чтобы убедиться, что S действительно прибавляет 1 к числу в обозначениях Черча, проверим ее действие на 3 :
поскольку (3b)с = b (b (bc)). Очевидно, эта операция с таким же успехом может быть применена к любому другому натуральному числу Черча. (В действительности, операция
?аbс. [(аb)(bс)] приводит к тому же результату, что и S.)
А как насчет удвоения числа? Удвоение числа может быть получено с помощью операции
что легко видеть на примере ее действия на 3 :
Фактически, основные арифметические операции — сложение, умножение и возведение в степень могут быть определены, соответственно, следующим образом:
М = ?fgx. [f (gx)],
P = ?fg. [fg]
Читатель может самостоятельно убедиться (или же принять на веру), что
(Am) n = m + n,
(Mm) n = m x n,
(Pm) n = n m ,
где m и n — функции Черча для двух натуральных чисел, m + n — функция, выражающая их сумму, и т. д. Последняя из этих функций поражает больше всего. Посмотрим, например, что она дает в случае m = 2, n = 3:
Операции вычитания и деления определяются не так легко (на самом деле нам потребуется соглашение о том, что делать с (m — n ), когда m меньше n, и с (m/n ), когда m не делится на n ). Решающий шаг в развитии этого метода был сделан в начале 1930-х годов, когда Клини удалось найти выражение для операции вычитания в рамках схемы Черча! Затем были описаны и другие операции. Наконец, в 1937 году Черч и Тьюринг независимо друг от друга показали, что всякая вычислимая (или алгоритмическая) операция — теперь уже в смысле машин Тьюринга — может быть получена в терминах одного из выражений Черча (и наоборот).
Это воистину замечательный факт, который подчеркивает глубоко объективный и математичный характер понятия вычислимости. На первый взгляд, понятие вычислимости по Черчу не связано с вычислительными машинами. И тем не менее, оно имеет непосредственное отношение к практическим аспектам вычислений. В частности, мощный и гибкий язык программирования LISP включает в себя как существенный элемент основные структуры исчисления Черча.
Как я отмечал ранее, существуют и другие способы определения понятия вычислимости. Несколько позже, но независимо от Тьюринга, Пост предложил во многом сходную концепцию вычислительной машины. Тогда же благодаря работам Дж. Хербранда и Геделя появилось и более практичное определение вычислимости (рекурсивности). X. Б. Карри в 1929 году, и ранее, в 1924, М. Шенфинкель, предложили иной подход, который был отчасти использован Черчем при создании своего исчисления (см. Ганди [1988]). Современные подходы к проблеме вычислимости (такие как машина с неограниченным регистром, описанная Катлендом [1980]) в деталях значительно отличаются от разработанного Тьюрингом и более пригодны для практического использования. Однако понятие вычислимости во всех этих подходах остается неизменным.
Как и многие другие математические идеи, особенно наиболее фундаментальные и красивые, идея вычислимости кажется овеществленной и объективно существующей в платоновском смысле. Именно к этому мистическому вопросу о платоновской реальности математических понятий мы и обратимся в следующих двух главах.
Данный текст является ознакомительным фрагментом.
Продолжение на ЛитРес
4.3. Исчисление предикатов
4.3. Исчисление предикатов Построение исчисления предикатов осуществляется, с одной стороны, аналогично построению исчисления высказываний, а с другой - качественно отличается от него.Сходство и даже связь между обоими исчислениями заключается, во-первых, в том, что
3. “Рогатка” Черча и не-фрегевская аргументация
3. “Рогатка” Черча и не-фрегевская аргументация Проиллюстрируем особенности применения неклассической аргументации на примере аргумента Алонзо Черча — так называемой “рогатки” Черча. Это имя ввиду простоты приводимой Черчем аргументации было дано Дж.Барвайсом и
б) Исчисление вероятностей
б) Исчисление вероятностей Помимо теоретико-познавательного применения исчисления вероятностей, Венский кружок предпринял подробное исследование теоретических оснований этого исчисления. Это было обусловлено столкновением различных теорий в исчислении
§ 5. Исчисление классов
§ 5. Исчисление классов Развитие адекватной символьной записи наряду с открытием формальных свойств отношений позволили обобщить традиционную логику, равно как и получить мощное исчисление.Например, операции сложения, умножения и т. д. в математических науках могут
§ 6. Исчисление суждений
§ 6. Исчисление суждений Исчисление суждений изначально разрабатывалось как еще одна интерпретация символов, применяемых в теории классов. В определенной мере оба эти исчисления обладают тождественной формальной структурой, и каждое суждение в теории классов обладает
§ 2. Математика, или исчисление, вероятности
§ 2. Математика, или исчисление, вероятности Современное изучение вероятности началось, когда шевалье де-Мере, известный картежник XVII века, поинтересовался у своего друга, праведного Паскаля, как лучше делать ставки при игре в кости. С тех пор основное количество
ВЕРОЯТНОСТНОЕ ИСЧИСЛЕНИЕ СМЫСЛОВ
ВЕРОЯТНОСТНОЕ ИСЧИСЛЕНИЕ СМЫСЛОВ Я также уверен в том, что кризис Европы коренится в заблуждениях рационализма. Однако это не означает, что рациональность во зло как таковая или что она играет подчиненную роль по отношению к целостности человеческого
Бентам — гедонистское исчисление и правовая реформа
Бентам — гедонистское исчисление и правовая реформа Английский юрист Иеремия Бентам (Jeremy Bentham, 1748–1832) принадлежал к так называемым философским радикалам, которые выступали за серьезную правовую реформу британского общества. Соответственно, он подвергал критике
5. Исчисление лояльности
5. Исчисление лояльности Степень жесткости критериев предоставления гражданства должна определяться по двум координатным осям, группам признаков, коэффициентам: 1. коэффициент групповой лояльности, 2. коэффициент личной сознательности.КГЛ (коэффициент групповой
II. ИСЧИСЛЕНИЕ БЕСКОНЕЧНО–МАЛЫХ И ЕГО ОСНОВНЫЕ КАТЕГОРИИ
II. ИСЧИСЛЕНИЕ БЕСКОНЕЧНО–МАЛЫХ И ЕГО ОСНОВНЫЕ КАТЕГОРИИ 1. Бытие, небытие, становление. Приступая к логическому анализу всех основных категорий, оперирование с которыми создает науку математического анализа, мы должны помнить, что далеко не все, понятное математически,
1.6. Противоречит ли точка зрения C тезису Черча—Тьюринга?
1.6. Противоречит ли точка зрения C тезису Черча—Тьюринга? Вспомним, что точка зрения C предполагает, что обладающий сознанием мозг функционирует таким образом, что его активность не поддается никакому численному моделированию — ни нисходящего, ни восходящего, ни
Тезис Черча — Тьюринга
Тезис Черча — Тьюринга После ознакомления с принципами построения простых машин Тьюринга легко убедиться, что все основные математические операции, такие как сложение двух чисел, их перемножение или возведение одного из них в степень другого, могут на самом деле быть
11. Дифференциальное исчисление и просветление
11. Дифференциальное исчисление и просветление Уже в течение, по меньшей мере, двадцати пяти столетий математика составляет неотъемлемую часть интеллектуального воспитания и наследия человека. Однако за этот длительный период времени не было достигнуто общего
Читайте также: