Свойства исчисления предикатов

Теорема Геделя о полноте исчисления предикатов

Имеют место следующие метатеоремы.

Теорема 14.1 Всякая теорема классического исчисления предикатов первого порядка есть тавтология.

Теорема 14.2 Всякая тавтология является теоремой классического исчисления предикатов первого порядка.

Вторая из этих теорем доказана К. Геделем (1930) и является утверждением о полноте классического исчисления предикатов первого порядка.

Непротиворечивость

Теория К непротиворечива. Доказательство следует из теоремы 14.1 и аналогично доказательству о теории L.

Проблема разрешения в логике предикатов

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

Исчисление предикатов первого порядка

Исчисление предикатов, в котором кванторы могут связывать только предметные переменные, но не могут связывать предикаты или функторы, называется исчислением первого порядка. Исчисления, в которых кванторы могут связывать не только предметные переменные, но и предикаты, функторы или иные множества объектов называются исчислениями высших порядков

Основные конструкции языка Пролог (объекты и термы, факты, правила, запросы).

Объекты и термы Пролога

Объектами Пролога являются

• имена (начинаются со строчной буквы), строки символов (заключаются в апострофы) и числа - константные объекты или константы; например, автомобиль, дом, иван, 'a+b', 'X', 123;
• переменные - могут принимать значения других объектов, и мы их будем писать прописными латинскими буквами: например, X, A, W;
• списки - их элементами являются любые объекты; списки мы заключаем в квадратные скобки, разделяя элементы запятыми; например, [] - пустой список (он является константой, мы его будем обозначать также nil и любой список завершать этим элементом, чтобы показать конец списка), [a, b, c, nil] - список, состоящий из трех констант a, b и c; [X, [b, Y, 'X', nil], nil] - список, состоящий из двух элементов, первый из которых - переменная X, а второй - список из трех элементов: имени b, переменной Y и строки 'X'.

Завершающий список элемент nil можно при записи опускать, подразумевая его в необходимых случаях. Для конкатенации (соединения) списков и элементов в один список используется точка как бинарная операция соединения левой части (головы списка) и правой части (хвоста списка). В случае операции конкатенации квадратные скобки на нулевом уровне можно опускать. Например, a.X.Y.a при X=b, Y=c есть список [a, b, c, a], также при X=[b], Y=[c] есть тот же список, а при X=[b, [d, e]] и Y=[[c]] есть список [a, b, [d, e], [c], a].

Термами являются объекты Пролога и составные термы. Составной терм образуется из имени функции и списка аргументов (термов Пролога) в круглых скобках. Синтаксически составной терм имеет вид

где f - имя n-арного функтора, а t_i (i 1,n)- аргументы.

Примерами составных термов являются: холодный (вода), отец (иван, петр), list(d, list(b, nil)) и bintree(bintree(nil, 7, nil), L, 12).

В первом примере составным термом является высказывание с именем булевой функции 1 аргумента-константы, которое имеет логическое значение истина или ложь.

Во втором примере отношение "иван является отцом петра" задается как булева функция с 2 аргументами-константами.

В третьем примере бинарная функция с именем list и двумя аргументами имеет в качестве первого аргумента константный объект d , а в качестве второго аргумента - составной терм с именем той же функции и возвращает, по-видимому, список.

В четвертом примере функция с именем bintree и тремя аргументами возвращает в виде списков бинарное дерево с корнем 7, правым сыном 12 и левым сыном, который определяется переменной L .

Термы, в которые не входят переменные, называют основными, а термы, содержащие переменные, - неосновными. Так, три первых примера выше являются основными термами, а четвертый пример - неосновным термом.

В логическом программировании основной структурой является предикатная функция, описываемая составным термом, которая имеет истинностное значение (истина или ложь), возможно зависящее от значений аргументов. Такой предикат называется атомарным, или атомом.

Факты

Факты - это простейшие утверждения относительно объектов программы, которые считаются истинными, т. е. имеют смысл аксиом программы. Каждый факт оформляется в виде атомарного предиката и стрелки влево, которая находится справа от него. Так, в следующем примере

задается, что объекты иван и петр являются мужчинами, что иван является отцом петра и что дважды два - четыре.

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

означает, что любой объект программы "любит яблоко". Универсальные факты сокращают запись программы. on_load_lecture();

Правила

Хотя универсальные факты могут сократить запись, но все же использование только этого приема не всегда позволяет создать обозримую базу знаний либо в принципе не позволяет ее создать.

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

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

Правило Пролога есть продукция, посылкой которой является конъюнкция атомарных предикатов, а заключением - 1 атомарный предикат. Правило имеет следующий синтаксис:

где A, B_i (i 1,m) - атомарные предикаты и запятая в правой части правила означает конъюнкцию. Читать правило нужно так: "Если B₁ и B₂ и т.д. и B_m, то A." Нетрудно видеть, что факт Пролога есть правило с пустой правой частью (m=0). Левая часть правила называется его заголовком, а правая часть - телом правила. Совокупность правил с одним и тем же предикатом в заголовке называется процедурой.

Решение вышеописанного примера состоит в определении отношения предок следующим образом: предком лица является либо мать, либо отец, либо мать предка, либо отец предка. Таким образом все решение сводится к следующей процедуре из 4 правил:

Заметим, что отношение предок определено этими правилами рекурсивно. Теперь для определения родства между двумя лицами достаточно также задать рекурсивно отношение родственники следующей процедурой из 3 правил:

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

Совокупность фактов и правил образует программу Пролога (или базу знаний).

Запросы

Запросы - это цели выполнения программы Пролога. Запрос является атомарным предикатом или конъюнкцией атомарных предикатов и имеет синтаксис:

где B_i (i 1,m) - атомарный предикат, а запятая, разделяющая атомы, означает операцию конъюнкции. Обозначение переменных запроса несущественно, и при переобозначении каждой переменной запрос не изменяется.

Если запрос не имеет переменных, то ответом на запрос является значение "Да" в случае, когда истинность конъюнкции предикатов запроса следует из истинности конъюнкции фактов и правил программы, и значение "Нет" в противном случае.

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

Рассмотрим пример программы, которая образована из следующей совокупности фактов

Пусть имеется запрос

Этот запрос не имеет переменных. Но правила процедуры предок позволяют установить, что предками федора являются анна, петр, иван и елена, а предками марии являются яков и елена. Поскольку федор и мария имеют общего предка елену, то правила процедуры родственники позволяют установить истинность запроса. Поэтому ответ на него Да.

Для запроса

не удается установить его верность, так как ни вера не является предком марии, ни мария не является предком веры и нет у них общего предка. Поэтому ответ на запрос Нет.

Пусть теперь имеется запрос

Этот запрос требует установить всех лиц, которые являются предками федора. Ответы на запрос образуют список анна, петр, иван, елена значений переменной X, каждое из которых логически выводится из фактов и правил.

Рассмотрим другой запрос

Этот запрос требует установить всех лиц, для которых елена является предком (потомки елены). Ответы на запрос образуют список иван, яков, петр, мария, анна, федор.

Наконец, для запроса

нет ни одного значения переменной X, при котором мы могли бы вывести это отношение. Поэтому ответом на запрос является Нет, т. е. вера не имеет потомков.
Рекурсивные функции. Лямбда – исчисление Черча.

Рекурсивные функции

(от позднелатинского recursio — возвращение), название, закрепившееся за одним из наиболее распространённых вариантов уточнения общего понятия арифметического алгоритма, т.е. такого алгоритма, допустимые исходные данные которого представляют собой системы натуральных чисел, а возможные результаты применения являются натуральными числами. Р. ф. были введены в 30-х гг. 20 в. С. К. Клини, в свою очередь основывавшимся на исследованиях К. Гёделя, Ж. Эрбрана и др. математиков.
Каждая Р. ф. задаётся конечной системой равенств точно охарактеризованного типа в том смысле, что её значения вычисляются с помощью этой системы равенств по точно формулируемым правилам, причём таким образом, что в итоге для вычисления значений заданной Р. ф. получается алгоритм определённого типа.

Арифметические функции, для вычисления значений которых имеются какие-либо алгоритмы, принято называть вычислимыми. Вычислимые функции играют в математике важную роль. Вместе с тем, если понятию алгоритма здесь не будет придан точный смысл, то и само понятие вычислимой функции окажется несколько расплывчатым. Р. ф. уже в силу самого характера своего определения оказываются вычислимыми. В известном смысле верно и обратное: имеются серьёзные основания считать, что математическое по своему характеру понятие рекурсивности является точным эквивалентом несколько расплывчатого понятия вычислимости. Предложение считать понятие вычислимости совпадающим по объёму с понятием рекурсивности известно в теории Р. ф. под названием тезиса Чёрча по имени американского математика А. Чёрча, впервые (в 30-х гг. 20 в.) сформулировавшего и обосновавшего это предложение. Принятие тезиса Чёрча позволяет придать понятию вычислимой арифметической функции точный математический смысл и подвергнуть это понятие изучению при помощи точных методов.
Р. ф. являются частичными функциями, т. е. функциями, не обязательно всюду определёнными. Чтобы подчеркнуть это обстоятельство, часто в качестве синонима используют термин «частично рекурсивные функции». Р. ф., определённые при любых значениях аргументов, называют общерекурсивными функциями.
Определению Р. ф. может быть придана следующая форма. Фиксируется небольшое число чрезвычайно простых исходных функций, вычислимых в упомянутом выше интуитивном смысле (функция, тождественно равная нулю, функция прибавления единицы и функции, выделяющие из системы натуральных чисел член с данным номером); фиксируется небольшое число операций над функциями, переводящих вычислимые функции снова в вычислимые (операторы подстановки, примитивной рекурсии и минимизации). Тогда Р. ф. определяются как такие функции, которые можно получить из исходных в результате конечного числа применений упомянутых выше операций.
Оператор подстановки сопоставляет функции f от n переменных и функциям g1, . . ., gn от m переменных функцию h от m переменных такую, что для любых натуральных чисел x1, .., xm

f (g1(x1, .., xm), ..., gm(x1, .., xm))@h(x1, .., xm)

(здесь означает, что оба выражения, связываемые@и ниже условное равенство им, осмыслены одновременно и в случае осмысленности имеют одно и то же значение).
Оператор примитивной рекурсии сопоставляет функциям f от n переменных и g от n + 2 переменных функцию h от n + 1 переменных такую, что для любых натуральных чисел x1, .. .., xn, y

f(x1, .., xn),@h(x1, .., xn ,0)

g(x1, .., xn, y, h(x1, .., xn, y )).@h(x1, .., xn, y + 1)

Оператор минимизации сопоставляет функции f от n переменных функцию h от n переменных такую, что для любых натуральных чисел x1, .., xn
f(x1, .., xn-1, y)@h(x1, .., xn)

где у таково, что f(x1, .., xn-1, y-1) определены и отличны от xn, а f(x1, .., xn, y) определена и равна xn, если же у с указанными свойствами не существует, то значение h(x1, .., xn) считается не определённым.

Важную роль в теории Р. ф. играют т. н. примитивно рекурсивные функции — Р. ф., получающиеся из исходных функций в результате конечного числа применений одних лишь операторов подстановки и примитивной рекурсии. Они образуют собственную часть класса общерекурсивных функций. В силу известной теоремы Клини о нормальной форме Р. ф. могут быть указаны такие конкретные примитивно рекурсивные функции U от одной переменной и от n переменных и дляjTn от n + 2 переменных, что для любой Р. ф. (x1, ...,jлюбых натуральных чисел x1, . . ., xn имеет место равенство , x1, ...,j U(y), где у есть наименьшее из чисел z таких, что Tn(@xn) —j представляет собой т. н. геделев номер функции jxn,z) = 0 (здесь число, которое эффективно строится по системе равенств, задающей ). Из этой теоремы, в частности, вытекает, что для Р. ф. от пjфункцию переменных может быть построена универсальная Р. ф. от n+1 переменных, от n переменных и для любыхjт. е. такая Р. ф. Фn, что для любой Р. ф. натуральных чисел x1, . . ., xn имеет место условное равенство

Фn( , x1, . . ., xn).@( x1, . . ., xn) j

Это — один из центральных результатов общей теории Р. ф.
Теория Р. ф., являясь частью алгоритмов теории, представляет собой разветвленную математическую дисциплину с собственной проблематикой и с приложениями в др. разделах математики. Понятие «Р. ф.» может быть положено в основу конструктивного определения исходных математических понятий. Широкое применение теория Р. ф. нашла в математической логике. В частности, понятие примитивно рекурсивной функции лежит в основе первоначального доказательства знаменитой теоремы Гёделя о неполноте формальной арифметики, а понятие «Р. ф.» в его полном объёме было использовано С. К. Клини для интерпретации интуиционистской арифметики (исследование это составило целую эпоху в области семантики). Аппарат теории Р. ф. используется также в теории вычислительных машин и программирования.

Исследования показали, что все известные уточнения общего понятия алгоритма, в том числе Р. ф., взаимно моделируют друг друга и, следовательно, ведут к одному и тому же понятию вычислимой функции. Это обстоятельство служит серьёзным доводом в пользу тезиса Чёрча.

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

По сравнению с языками функционального программирования, подобным Haskell, в лямбда-исчислении не хватает чисто практических средств, позволяющих удобно записывать функции. Прежде всего бросается в глаза отсутствие средств описания рекурсивных функций. Действительно, рекурсивные обращения всегда происходят с использованием имени функции, однако лямбда-исчисление - это язык для описания безымянных функций! Конечно, иногда мы можем обойтись и без использования рекурсии, если имеется достаточно богатый набор встроенных функций. Так, например, имея функцию высшего порядка foldr в качестве одной из встроенных функций, мы можем написать функцию вычисления факториала натурального числа и без использования рекурсии. Аналогично, функция свертки дерева foldTree позволила нам написать без использования рекурсии функцию разглаживания дерева flatten. На самом деле можно показать, что имея достаточно богатый набор мощных функций высшего порядка, можно всегда обойтись без использования рекурсивных вызовов (такой стиль программирования называется программированием с помощью комбинАторов или комбинАторным программированием). Однако, чистое лямбда-исчисление не предполагает использования встроенных функций вообще! Возникает вопрос: достаточно ли средств лямбда-исчисления для того, чтобы выразить в нем всевозможные вычислимые функции, если в нем невозможно обычным образом задавать рекурсивные функции, а встроенных функций, позволяющих обойти эту проблему, нет вообще?
В этом разделе мы постепенно построим чистое лямбда-исчисление, последовательно выразив в виде лямбда-выражений все имевшиеся у нас ранее константы и встроенные функции, и задав с помощью тех же лямбда-выражений все управляющие конструкции языков функционального программирования, включая рекурсию, условное вычисление и др. Начнем мы именно с выражения прямой и косвенной рекурсии в чистом лямбда-исчислении.
Пусть у нас имеется функция, в определении которой есть прямое рекурсивное обращение к себе, например, такое, как определение функции вычисления факториала в языке Haskell.
fact n = if n == 0 then 1 else n * fact(n-1)

Прежде всего, зададим эту функцию с помощью конструкций лямбда-исчисления, считая, что у нас имеются встроенные функции для вычитания (функция '-'), умножения (функция '*') и сравнения с нулем (функция 'eq0'), кроме того, считаем, что у нас также есть функция 'if' для условного вычисления и константы '0' и '1'. Тогда определение функции будет выглядеть следующим образом.
fact = λn.if (eq0 n) 1 (* n (fact (- n 1)))

Здесь мы пока по-прежнему использовали задание имени для функции fact для того, чтобы выразить рекурсию. Построим теперь новую функцию, в которой вызываемая функция fact будет аргументом:

sFact = λfact.λn.if (eq0 n) 1 (* n (fact (- n 1)))

Конечно, эта новая функция не будет тем факториалом, который мы пытаемся построить хотя бы потому, что ее аргументом является не целое число, а некоторая функция, однако она некоторым вполне определенным образом связана с той функцией вычисления факториала, которую мы пытаемся построить. Зададимся задачей найти такую функцию f, что она является неподвижной точкой определенной нами функции sFact, то есть такую f, что выполнено равенство f = sFact f. Очевидно, что если такую неподвижную точку удастся найти, то найденная функция f как раз и будет тем самым факториалом, который мы ищем, поскольку будет выполнено равенство

f = sFact f = λn.if (eq0 n) 1 (* n (f (- n 1)))

Итак, задача нахождения функции, эквивалентной заданной рекурсивной функции, свелась к задаче построения неподвижной точки для некоторой другой функции. Кажется, что эту задачу - задачу нахождения неподвижной точки - в общем виде решить не удастся. A priori вообще не ясно, всегда ли такая неподвижная точка существует. Однако оказывается, что удается построить функцию, которая для заданного аргумента вычисляет его неподвижную точку. Если обозначить через Y такую функцию нахождения неподвижной точки, то для любой функции f должно быть справедливо равенство Y f = f(Y f). Другими словами, результатом применения функции Y к функции f должно быть такое значение x, что x = f(x). Одну из таких функций предложил Хаскелл Карри, которая в его честь называется Y-комбинатором Карри. Вот запись этой функции в нотации лямбда-исчисления:
Y = λh.(λx.h (x x))(λx.h (x x))

Проверим, действительно ли для этой функции выполнено равенство Y f = f(Y f). Для этого запишем выражение Y f и попробуем привести его к СЗНФ. После того, как вместо Y будет подставлено соответствующее лямбда-выражение, мы сможем выполнить один шаг β-редукции, и получим выражение (λx.f (x x))(λx.f (x x)). Это выражение еще не находится в СЗНФ, так что мы можем выполнить еще один шаг и с помощью β-редукции привести его к виду f ((λx.f (x x))(λx.f (x x))). Это выражение также не находится в СЗНФ, более того, теперь видно, что привести это выражение к СЗНФ вообще никогда не удастся, так как каждый следующий шаг редукции приводит только к увеличению длины выражения. Однако, из проведенных шагов хорошо видно, что выражение Y f действительно эквивалентно выражению f(Y f), поскольку второе получается из первого за один шаг редукции.

Итак, мы получили, что выражение для рекурсивной функции можно получить, если построить некоторое вспомогательное выражение, а затем применить к нему Y-комбинатор Карри. Получившееся при этом выражение не может быть приведено к СЗНФ, однако оно все же будет работать как соответствующая рекурсивная функция. Давайте убедимся в этом, построив описанным способом функцию для вычисления факториала заданного числа, а затем применим ее к конкретному числу, скажем, числу 2, и проверим, как получается результат вычисления - число 2, равное fact(2). Для этого попробуем привести к СЗНФ выражение (Y sFact) 2, где Y обозначает Y-комбинатор Карри, а sFact - функцию, приведенную выше, полученную из рекурсивного определения факториала. Последовательные шаги по преобразованию выражения к СЗНФ показаны ниже.

Y sFact 2

sFact (Y sFact) 2

(λfact.λn.if (eq0 n) 1 (* n (fact (- n 1)))) (Y sFact) 2

(λn.if (eq0 n) 1 (* n ((Y sFact) (- n 1)))) 2

if (eq0 2) 1 (* 2 ((Y sFact) (- 2 1)))

(* 2 (Y sFact 1))

Остановимся пока здесь. Мы видим, что последовательное выполнение β- и δ-редукций привело нас от выражения Y sFact 2 к выражению (* 2 (Y sFact 1)). Это уже показывает, что преобразование выражения происходит именно так, как ведет себя рекурсивное вычисление факториала. Однако, давайте продолжим преобразования.

Y sFact 2

sFact (Y sFact) 2

(λfact.λn.if (eq0 n) 1 (* n (fact (- n 1)))) (Y sFact) 2

(λn.if (eq0 n) 1 (* n ((Y sFact) (- n 1)))) 2

if (eq0 2) 1 (* 2 ((Y sFact) (- 2 1)))

(* 2 (Y sFact 1))

(* 2 (sFact (Y sFact) 1)

(* 2 (λfact.λn.if (eq0 n) 1 (* n (fact (- n 1)))) (Y sFact) 1)

(* 2 (λn.if (eq0 n) 1 (* n ((Y sFact) (- n 1)))) 1)

(* 2 (if (eq0 1) 1 (* 1 ((Y sFact) (- 1 1)))))

(* 2 (* 1 (Y sFact 0)))

(* 2 (* 1 (sFact (Y sFact) 0)))

(* 2 (* 1 ((λfact.λn.if (eq0 n) 1 (* n (fact (- n 1)))) (Y sFact) 0)))

(* 2 (* 1 ((λn.if (eq0 n) 1 (* n ((Y sFact) (- n 1)))) 0)))

(* 2 (* 1 (if (eq0 0) 1 (* 0 ((Y sFact) (- 0 1))))))

(* 2 (* 1 1))

2
Преобразования закончились вполне предсказуемым результатом, так что можно заключить, что применение Y-комбинатора Карри действительно приводит к нужному результату. Существенно, что мы использовали при вычислениях нормальный порядок редукций, так как при аппликативном порядке редукций вычисления просто никогда не были бы закончены. Существуют и другие формы Y-комбинаторов, в частности, такие, которые применимы и при АПР, однако, все известные другие выражения для Y-комбинаторов выглядят сложнее, чем Y-комбинатор Карри.

Если несколько функций определяются таким образом, что в теле каждой из них имеются вызовы других функций из этого набора, то говорят, что мы имеем дело со взаимно-рекурсивными функциями. На самом деле этот случай можно свести к прямой рекурсии и, тем самым, выразить в лямбда-исчислении не только прямую, но и взаимную рекурсию. Для того, чтобы свести взаимную рекурсию к прямой, нам потребуются некоторые дополнительные встроенные функции. Во-первых, введем серию функций кортежирования, которые составляют кортеж из своих аргументов. Будем считать, что если k - некоторое натуральное число, то функция TUPLE-k имеет k аргументов и выдает в качестве результата кортеж из k элементов. Еще одна функция нужна для того, чтобы, наоборот, выделять элемент с заданным номером из кортежа. Назовем эту функцию ELEM. Функция ELEM имеет два аргумента: n - номер элемента кортежа - натуральное число, не превосходящее длины кортежа T, который является вторым аргументом этой функции. Результатом работы функции служит n-ый элемент кортежа T. Если число n - не натуральное или превосходит число элементов кортежа, заданного вторым аргументом, то результат работы функции не определен.
Теперь пусть имеются определения взаимно-рекурсивных функций
f1 = F1(f1, f2,... fn)

f2 = F2(f1, f2,... fn)

...
fn = Fn(f1, f2,... fn)

где все Fi - выражения, в которых встречаются рекурсивные обращения к определяемым функциям f1, f2,... fn. Прежде всего образуем новое выражение, представляющее собой кортеж, в котором собраны все определения функций:
T = TUPLE-n F1(f1, f2,... fn) F2(f1, f2,... fn)... Fn(f1, f2,... fn)

каждая из определяемых функций f1, f2,... fn может быть теперь выражена с помощью выделения соответствующего элемента этого кортежа:
fi = ELEM i T

поэтому если мы теперь подставим в определение кортежа T вместо всех вхождений fi их выражения в виде элемента кортежа, то мы получим рекурсивное определение для кортежа T с прямой рекурсией:

T = TUPLE-n F1((ELEM 1 T),... (ELEM n T))... Fn((ELEM 1 T),... (ELEM n T))

Кортеж T теперь может быть представлен как и раньше с помощью Y-комбинатора
Y (λT.TUPLE-n F1((ELEM 1 T),... (ELEM n T))... Fn((ELEM 1 T),... (ELEM n T)))

а каждая из отдельно взятых функций может быть получена в виде элемента этого кортежа.
Теперь попробуем представить в виде лямбда-выражений все стандартные константы и функции, использованные нами ранее. Для этого нам надо будет выбрать представление и разработать технику выполнения операций над целыми числами, логическими значениями и списками. Основным критерием для выбора того или иного представления будет функциональность этого представления, то есть нам надо, чтобы все представляемые нами константы и стандартные функции "вели себя правильно", в соответствии с нашими представлениями о результатах выполнения операций. Проще всего определить логические константы и операции над ними, поскольку таких констант всего две - истина и ложь, а операции над ними подчиняются очень простым законам. С этого и начнем.
Основное назначение логических значений состоит в том, чтобы организовать выбор в ходе вычислений, поэтому начать следует с того, как можно реализовать функцию выбора IF. Эта функция имеет три аргумента, при этом первым аргументом как раз и является логическое значение. Если логическое значение надо представлять некоторой функцией, то проще всего сделать так, чтобы само это логическое значение и отвечало за выбор альтернативы при выполнении функции IF. То есть реализуем функцию так, чтобы она просто применяла свой первый аргумент к остальным двум, а уже этот аргумент отбрасывал бы один из аргументов и оставлял второй. Тогда реализация констант TRUE и FALSE, а также функция IF получают следующее представление.
IF = λp.λt.λe.p t e

TRUE = λx.λy.x

FALSE = λx.λy.y

Проверим, что каковы бы ни были выражения A и B, выражение IF TRUE A B эквивалентно выражению A, а выражение IF FALSE A B - эквивалентно B. Действительно, при подстановке наших лямбда-выражений после преобразований в НПР последовательно получаем:

IF TRUE A B

(λp.λt.λe.p t e) (λx.λy.x) A B

(λt.λe.(λx.λy.x) t e) A B

(λe.(λx.λy.x) A e) B

(λx.λy.x) A B

(λy.A) B

A
Разумеется, совершенно аналогично выражение IF FALSE A B будет преобразовано в B.
Над логическими значениями TRUE и FALSE можно выполнять обычные операции логического сложения, умножения, отрицания и пр. Разумеется, их надо определить так, чтобы при их применении получались правильные результаты. Это нетрудно сделать; вот как могут выглядеть, например, операции AND, OR и NOT:

AND = λx.λy.x y FALSE

OR = λx.λy.x TRUE y

NOT = λx.x FALSE TRUE

Здесь в определении новых операций использованы уже определенные ранее константы TRUE и FALSE. Сами операции определены совершенно естественным образом "по МакКарти". Аналогично можно определить и другие операции над логическими значениями, и, по существу, этим и исчерпываются все необходимые средства для работы с логическими значениями. Теперь приступим к определению арифметических значений и функций в терминах чистого лямбда-исчисления.
Мы ограничимся только арифметикой натуральных чисел, все остальные числа - рациональные, вещественные, комплексные и др. можно получить, комбинируя натуральные числа и определяя соответствующие операции над такими числами. Натуральные же числа представляют собой абстракцию подсчета тех или иных объектов. Для построения модели счета нужно выбрать, что мы будем считать. Вообще говоря, считать можно что угодно, при этом можно получить весьма различные модели арифметики, мы, однако, следуя Тьюрингу, будем подсчитывать, сколько раз некоторая функция применяется к своему аргументу. Это приводит нас к следующему определению натурального числа N. Число N представляется функцией с двумя аргументами, которая выполняет N-кратное применение своего первого аргумента ко второму. Более точно, сначала запишем определение для функции ZERO, представляющей число нуль, а затем покажем, как определяется число N+1, если число N уже определено. Тем самым будет возможно построить определение любого натурального числа N.
ZERO = λf.λx.x -- функция f ноль раз применяется к аргументу x, так что аргумент возвращается неизменным

(N+1) = λf.λx.f (N f x)

Заметим, кстати, что константа ZERO определена в точности так же, как константа FALSE, однако далеко идущих выводов из этого сходства делать все же не следует. Из приведенного определения целых чисел немедленно следует определение функции следования, которая добавляет единицу к своему аргументу:

SUCC = λn.λf.λx.f (n f x)

Теперь нетрудно также определить операции сложения и умножения целых чисел. Так, например, можно сказать, что для того, чтобы сложить два числа m и n, надо m раз увеличить число n на единицу. Аналогично, чтобы умножить m на n, надо m раз применить функцию увеличения на n к нулю. Отсюда следуют определения:

PLUS = λm.λn.m SUCC n

MULT = λm.λn.m (PLUS n) ZERO

К сожалению, определить операции вычитания в представленной нами арифметике совсем не так просто. Прежде всего определим функцию PRED, которая выдает предыдущее натуральное число для всех чисел, больших нуля, а для аргумента, равного нулю, выдает также ноль. Одно из возможных определений такой функций выглядит следующим образом:

PRED = λn.λf.λx.n (λg.λh.h (g f)) (λu.x) (λu.u)

Проверьте, что применение этой функции к значению ZERO действительно выдает в качестве результата ZERO, а применение этой функции к, скажем, значению 2 (представленному функцией λf.λx.f (f x)) может быть преобразовано к значению 1 (функции λf.λx.f x). Такое упражнение позволит вам понять, как происходит уменьшение количества применений функции f к аргументу. Теперь уже нетрудно определить и функцию вычитания на множестве натуральных чисел, которая для заданных аргументов m и n выдает n и выдает ноль при m³значение (m-n) при m < n.

MINUS = λm.λn.n PRED m

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

EQ0 = λn.n (λx.FALSE) TRUE

Очевидно, что если применить функцию к значению ZERO, то функция (λx.FALSE) не будет применена ни разу к своему аргументу, поэтому результатом применения функции будет значение TRUE. Если же значение аргумента отлично от нуля, то функция (λx.FALSE) после первого же применения выдаст значение FALSE, и в дальнейшем, сколько бы раз ее ни применять, выдаваемым значением так и будет оставаться FALSE. Теперь можно определить функции сравнения двух чисел с помощью операций GE ("больше или равно") и LE ("меньше или равно"), используя только что определенную операцию сравнения с нулем и операцию вычитания натуральных чисел MINUS.

GE = λm.λn.EQ0 (MINUS m n)

LE = λm.λn.EQ0 (MINUS n m)

Остальные операции сравнения легко выражаются через эти операции сравнения и уже определенные ранее логические операции:

GT = λm.λn.NOT (LE m n)

LT = λm.λn.NOT (GE m n)

EQ = λm.λn.AND (GE m n) (LE m n)

NEQ = λm.λn.NOT (EQ m n)

Теперь, когда уже определена арифметика и логика, давайте, вооруженные опытом описания различных стандартных функций построим функции для формирования составных значений, подобных кортежам или спискам. Представляемые нами составные значения будут больше всего напоминать списки, как они определены в языке LISP, то есть списки элементов самого разного типа (элементом такого списка может быть любое значение, в том числе другой список, число, логическое значение или, вообще говоря, любая функция). Для создания таких списков необходимо определить одно базовое значение - пустой список - и функции, позволяющие из двух заданных значений создавать их пару (функция CONS), а также выделять первый и второй элемент пары (функции HEAD и TAIL). Для того, чтобы можно было исследовать списки в программах, требуется определить также по крайней мере одну логическую функцию NULL, которая выдает значение TRUE или FALSE в зависимости от того, является ли ее аргумент пустым списком или нет.

Функция CONS может соединять в пару два своих аргумента, просто создавая функцию, которая будет применять свой аргумент к обеим частям пары как к двум своим аргументам. Другими словами, если H и T - два произвольных значения, то их пару можно представить функцией (λs.s H T). Таким образом, функция CONS получает следующее определение:
CONS = λh.λt.λs.s h t

Для того, чтобы из составного значения (λs.s H T) выделить первый элемент H, надо применить эту функцию к такому значению s, которое выдаст первый из двух своих аргументов. Таким значением является уже определенная нами ранее константа TRUE. Ясно, что результатом применения (λs.s H T) TRUE будет значение H. Таким образом, функция HEAD получает следующее определение:

HEAD = λl.l TRUE

Не нашли, что искали? Воспользуйтесь поиском по сайту: