Лямбда-исчисление (547599), страница 2
Текст из файла (страница 2)
Определение 4. Отношение редукции на некотором множестве термов называется конфлюэнтным, если имеет место утверждение:
Теорема 2 (Черча-Россера).
Отношение -редукции на множестве
-термов является конфлюэнтным.
Доказательство можно найти в монографиях, посвященных более глубокому изложению теории -исчисления, например в [2].
Следствие 1 (теоремы 2).
Если -терм
имеет нормальную форму, то она – единственная (с точностью до
-конверсии).
Доказательство очевидно.
Если к определению отношения -редукции термов добавить дополнительно условие симметричности, то минимальное отношение, удовлетворяющее перечисленным ниже требованиям, называется отношением
-конверсии термов и обозначается инфиксом
:
Следствие 2 (теоремы 2).
Если (терм
конвертируется с термом
), то существует такой терм
, что
и
.
Доказательство очевидно.
Соглашение об обозначениях.
Для облегчения дальнейшего изложения примем некоторые соглашения о сокращенном представлении -термов:
-
Внешние скобки в представлении
-термов, полученных аппликацией, внутри текстов могут быть опущены (в основном, этим соглашением мы будем пользоваться при формулировке одного из вариантов комбинаторного исчисления в разделе 5).
-
Вместо символов переменных
могут использоваться любые строчные латинские буквы, причем разным буквам будут соответствовать переменные с разными номерами.
-
Прописные латинские буквы в позициях переменных рассматриваются как метапеременные; в качестве их значений могут быть переменные с любыми конкретными номерами.
Например, запись представляет собой сокращенную запись терма
.
Теорема 3 (Карри).
Для любого -терма
и любой переменной
существует
-терм
, такой, что
.
Иными словами, всякое уравнение имеет решение в
-исчислении (с точностью до отношения конверсии термов).
Доказательство.
Пусть (
называют парадоксальным комбинатором Карри). Тогда терм
, существование которого утверждает теорема 3, может быть получен так:
. Действительно,
Пусть - подмножество замкнутых, т.е. не содержащих свободных вхождений переменных,
-термов (
-термов);
- подмножество
-термов в нормальной форме (
-термов), а
- их пересечение (множество
-термов).
Пусть - многосортный эрбрановский универсум, где
- множество сортов объектов универсума. Предположим, что для построения объектов сорта
используется
различных конструкторов:
, где
- арность
-го конструктора для сорта
. Для всех
через
обозначим взаимно-однозначные отображения
в множество
-термов. Если
, то
будем далее обозначать как «
»
и называть
-образом объекта
. Если для построения объектов различных сортов используются различные наборы конструкторов, то в обозначении
-образа объекта
нет необходимости указывать его сорт
, и он обозначается просто как «
». Определим образы объектов по общему правилу. Пусть
. Тогда «
»
«
»«
»…«
»
.
-образом функции
, вообще говоря, частичной, назовем такой
-терм «
», что для всех наборов значений аргументов из области определения функции
(
,
,…,
или имеет место
«
»«
»«
»…«
»
«
», или
«
»«
»«
»…«
»
не имеет нормальной формы, если значение
не определено. Возможность решения уравнений в
-исчислении с помощью комбинатора Карри позволяет пользоваться рекурсивной формулировкой образов моделируемых функций. Конструкция же образа «
» любого объекта
такова, что терм вида
«
»
фактически осуществляет разбор случаев конструкции объекта
, так как
«
»
«
»«
»…«
»
, если
. Следовательно, терм
должен определять необходимое значение для этого случая как функцию от образов тех объектов, из которых построен объект
с помощью
-го из конструкторов для объектов сорта
.
Для освоения техники описанного моделирования в -исчислении различных конструктивных объектов и функций на этих объектах, в том числе и предикатов, познакомимся с некоторыми примерами. Будем, как и ранее, использовать имена, начинающиеся со строчных букв для обозначения сортов объектов, а имена, начинающиеся с прописных букв, для обозначения конструкторов. В случае, когда конструируемые объекты имеют общепризнанное представление, будем на его основе определять вводимые конструкторы. Арность конструкторов при необходимости указывается в скобках в качестве верхнего индекса.
Пример 1. Сорт - логические значения, конструкторы
,
:
Заметим, что образы логических значений играют роль функций выбора значения одного из двух аргументов, « » - первого, а «
» - второго, что позволяет использовать это при моделировании условных определений
.
Пример 2. Сорт - натуральные числа, конструкторы
,
:
« »
«
»
. В этом рекурсивном описании образа функции сложения натуральных чисел предполагается, что вместо переменной
будет подставлен образ числа, на единицу меньшего числа, образ которого подставляется вместо переменной
. Явное решение этого уравнения может быть получено так:
« »
«
»
. В этом примере используется упомянутый выше прием условного определения.
« »
«
»
«
»
. Описание образа функции умножения натуральных чисел.
« »
«
»
«
»
«
»
. Описание образа функции возведения в степень для натуральных чисел.
«
»
. Описание образа функции вычисления номера упорядоченной пары натуральных чисел диагональным способом нумерации.
Пример 3. Сорт - последовательности натуральных чисел любой конечной длины, конструкторы
,
, где
:
« »
«
»
. Описание образа функции сцепления двух последовательностей в одну.
Описание образа функции включения числа в качестве последнего элемента в заданный список.
« »
«
»
«
»
. Описание образа функции, изменяющей порядок следования элементов последовательности на обратный.
«
»
«
»
. слияния двух упорядоченных по неубыванию последовательностей натуральных чисел в одну общую неубывающую последовательность.
« »
«
»
. Описание функции, выделяющей подсписок элементов с нечетными номерами в списке – аргументе.
« »
«
»
. Описание функции, выделяющей подсписок элементов с четными номерами в списке – аргументе.
«
»
«
»
. Описание функции сортировки по неубыванию последовательности натуральных чисел методом слияния.
Пример 4. Сорт -
-термы, конструкторы
,
и
:
«
»
. Описание предиката, устанавливающего, находится
-терм в нормальной форме или нет.
- вспомогательный предикат:
« »
«
»
«
»
«
»
«
»
«
»
«
»
«
»
. Описание предиката
, где
« »
«
»
«
»
«
»
«
»
. Описание предиката неравенства двух натуральных чисел.
« »
«
»«
»
. Описание функции, вычисляющей наименьший номер переменной, не имеющей свободных вхождений в заданный терм, с помощью вспомогательной функции «
»:
. Описание функции, вычисляющей результат подстановки одного терма вместо свободных вхождений переменной с заданным номером в другой терм.
« »
«
»
«
»
«
»
. Описание частичной функции, вычисляющей нормальную форму заданного
-терма.
«
»
. Описание функции, вычисляющей шаг редукции для самого левого редекса заданного
-терма, не находящегося в нормальной форме.
« » - образ функции, вычисляющей образ заданного терма, т.е.
«
»«
»
««
»».
-
Алгоритмически неразрешимые проблемы.
Теорема 4(о существовании специальной фиксированной точки).
Для всякого -терма
существует
-терм
, такой, что
«
»
.
Доказательство.
Пусть «
»
, где
«
»
«
»
. Действительно,
Определение 5. Пусть и
- подмножества множества
.
называется рекурсивно отделимым от
, если существует рекурсивное подмножество
множества
, такое, что
и
.
Напомним, что подмножество множества
называется рекурсивным, если существует всюду определенный на
вычислимый предикат
, такой, что
.
Определение 6. Подмножество множества
называется нетривиальным, если
и
.
Определение 7. Подмножество
-термов замкнуто относительно отношения
-конверсии, если
.
Теорема 5 (о рекурсивной неотделимости).
Два произвольных нетривиальных подмножества -термов, замкнутых относительно отношения
-конверсии, не являются рекурсивно отделимыми.
Доказательство.
Пусть и
- два подмножества
-термов, удовлетворяющие условиям теоремы. Так как они не пересекаются (в этом случае результат очевиден) и не пусты, то выберем в них по одному элементу:
и
. Предположим от противного, что существует рекурсивное подмножество
, такое, что
и
. Рекурсивность
означает, что существует всюду определенный на множестве
-термов вычислимый предикат
, такой, что
Вычислимость этого предиката означает, что существует его
-образ «
», такой, что
«
»«
»
«
», если
, и
«
»«
»
«
», если
.
Построим терм «
»
, для которого будет иметь место утверждение: если
, то
«
»
, если
, то
«
»
. Согласно теореме 4 построим для
-терма
такой
-терм
, что
«
»
. Возникает вопрос:
или
? Начнем с первого предположения. Так как
и
, то
. С другой стороны,
«
»
, и, в силу замкнутости
относительно отношения
-конверсии,
. Получилось противоречие. Рассмотрим второе предположение. Так как
, а
, то
. С другой стороны,
«
»
, и, в силу замкнутости
относительно отношения
-конверсии,
. Вновь получилось противоречие. Следовательно, исходное предположение о рекурсивной отделимости
и
ложно.