Лямбда-исчисление (547599), страница 2
Текст из файла (страница 2)
Определение 4. Отношение редукции на некотором множестве 
термов называется конфлюэнтным, если имеет место утверждение:
.
Теорема 2 (Черча-Россера).
Отношение 
-редукции на множестве 
-термов является конфлюэнтным.
Доказательство можно найти в монографиях, посвященных более глубокому изложению теории -исчисления, например в [2].
Следствие 1 (теоремы 2).
Если -терм 
имеет нормальную форму, то она – единственная (с точностью до 
-конверсии).
Доказательство очевидно.
Если к определению отношения -редукции термов добавить дополнительно условие симметричности, то минимальное отношение, удовлетворяющее перечисленным ниже требованиям, называется отношением -конверсии термов и обозначается инфиксом 
:
-
![]()
. -
![]()
. -
![]()
. -
![]()
. -
![]()
, где ![]()
- произвольный ![]()
-контекст.
Следствие 2 (теоремы 2).
Если 
(терм 
конвертируется с термом 
), то существует такой терм 
, что 
и 
.
Доказательство очевидно.
Соглашение об обозначениях.
Для облегчения дальнейшего изложения примем некоторые соглашения о сокращенном представлении -термов:
-
![]()
-
![]()
-
Внешние скобки в представлении
![]()
-термов, полученных аппликацией, внутри текстов могут быть опущены (в основном, этим соглашением мы будем пользоваться при формулировке одного из вариантов комбинаторного исчисления в разделе 5). -
Вместо символов переменных
![]()
могут использоваться любые строчные латинские буквы, причем разным буквам будут соответствовать переменные с разными номерами. -
Прописные латинские буквы в позициях переменных рассматриваются как метапеременные; в качестве их значений могут быть переменные с любыми конкретными номерами.
Например, запись 
представляет собой сокращенную запись терма 
.
Теорема 3 (Карри).
Для любого -терма и любой переменной 
существует -терм 
, такой, что 
.
Иными словами, всякое уравнение 
имеет решение в -исчислении (с точностью до отношения конверсии термов).
Доказательство.
Пусть 
(
называют парадоксальным комбинатором Карри). Тогда терм , существование которого утверждает теорема 3, может быть получен так: 
. Действительно,
-
Моделирование в
![]()
-исчислении конструктивных объектов и вычислимых функций.
Пусть 
- подмножество замкнутых, т.е. не содержащих свободных вхождений переменных, -термов (
-термов); 
- подмножество -термов в нормальной форме (
-термов), а 
- их пересечение (множество 
-термов).
Пусть 
- многосортный эрбрановский универсум, где 
- множество сортов объектов универсума. Предположим, что для построения объектов сорта 
используется 
различных конструкторов:
, где 
- арность 
-го конструктора для сорта . Для всех 
через 
обозначим взаимно-однозначные отображения 
в множество -термов. Если 
, то 
будем далее обозначать как «
» 
и называть -образом объекта . Если для построения объектов различных сортов используются различные наборы конструкторов, то в обозначении -образа объекта нет необходимости указывать его сорт , и он обозначается просто как « ». Определим образы объектов по общему правилу. Пусть 
. Тогда « » 
«
»«
»…«
» 
.
-образом функции 
, вообще говоря, частичной, назовем такой -терм «
», что для всех наборов значений аргументов из области определения функции (
, 
,…, 
или имеет место 
« »« »« »…«
» 
«
», или « »« »« »…« » не имеет нормальной формы, если значение не определено. Возможность решения уравнений в -исчислении с помощью комбинатора Карри позволяет пользоваться рекурсивной формулировкой образов моделируемых функций. Конструкция же образа « » любого объекта 
такова, что терм вида « » 
фактически осуществляет разбор случаев конструкции объекта , так как « » 
« »« »…« » , если . Следовательно, терм 
должен определять необходимое значение для этого случая как функцию от образов тех объектов, из которых построен объект с помощью -го из конструкторов для объектов сорта .
Для освоения техники описанного моделирования в -исчислении различных конструктивных объектов и функций на этих объектах, в том числе и предикатов, познакомимся с некоторыми примерами. Будем, как и ранее, использовать имена, начинающиеся со строчных букв для обозначения сортов объектов, а имена, начинающиеся с прописных букв, для обозначения конструкторов. В случае, когда конструируемые объекты имеют общепризнанное представление, будем на его основе определять вводимые конструкторы. Арность конструкторов при необходимости указывается в скобках в качестве верхнего индекса.
Пример 1. Сорт 
- логические значения, конструкторы 
, 
:
«
» 
,
«
» 
.
Заметим, что образы логических значений играют роль функций выбора значения одного из двух аргументов, « » - первого, а « » - второго, что позволяет использовать это при моделировании условных определений 
.
Действительно, « » 
, а
« » 
.
Пример 2. Сорт 
- натуральные числа, конструкторы 
, 
:
«
» 
,
«
» 
«
» .
«
» 
« » 
. В этом рекурсивном описании образа функции сложения натуральных чисел предполагается, что вместо переменной 
будет подставлен образ числа, на единицу меньшего числа, образ которого подставляется вместо переменной 
. Явное решение этого уравнения может быть получено так:
« » 
«
» 
« » 
« » 
« » 
.
«
» 
« » 
. В этом примере используется упомянутый выше прием условного определения.
«
» 
« » « » 
. Описание образа функции умножения натуральных чисел.
«
» 
«
» « » « » . Описание образа функции возведения в степень для натуральных чисел.
«
» 
« » « » 
« » 
. Описание образа функции вычисления номера упорядоченной пары натуральных чисел диагональным способом нумерации.
Пример 3. Сорт 
- последовательности натуральных чисел любой конечной длины, конструкторы 
, 
, где 
:
«
» ,
«
» 
«
»«
» .
«
» 
« » 
. Описание образа функции сцепления двух последовательностей в одну.
«
» 
« » 
.
Описание образа функции включения числа в качестве последнего элемента в заданный список.
«
» 
« » 
« » 
. Описание образа функции, изменяющей порядок следования элементов последовательности на обратный.
«
» 
« » 
« » 
« » 
. слияния двух упорядоченных по неубыванию последовательностей натуральных чисел в одну общую неубывающую последовательность.
«
» 
« » 
. Описание функции, выделяющей подсписок элементов с нечетными номерами в списке – аргументе.
«
» 
« » 
. Описание функции, выделяющей подсписок элементов с четными номерами в списке – аргументе.
«
» 
« » « » « » 
« » « » 
. Описание функции сортировки по неубыванию последовательности натуральных чисел методом слияния.
Пример 4. Сорт 
- -термы, конструкторы 
, 
и 
:
«
» 
«
» ,
«
» 
«
»«
» ,
«
» 
« »« » ,
«
» 
« » 
« » 
«
» 
« »
« » 
. Описание предиката, устанавливающего, находится -терм в нормальной форме или нет. - вспомогательный предикат:
« » « » « » « » « »
« » .
«
» 
«
» 
« » 
« » 
« » 
« » 
« » 
« » 
. Описание предиката 
, где
« » 
« » 
« » 
« » « » 
. Описание предиката неравенства двух натуральных чисел.
«
» 
«
»« » 
. Описание функции, вычисляющей наименьший номер переменной, не имеющей свободных вхождений в заданный терм, с помощью вспомогательной функции « »:
« » 
« » 
« » 
.
«
» 
« » 
« » 
« » 
« » 
« » 
« » 
« » 
. Описание функции, вычисляющей результат подстановки одного терма вместо свободных вхождений переменной с заданным номером в другой терм.
«
» 
« » 
« » «
» 
. Описание частичной функции, вычисляющей нормальную форму заданного -терма.
« » 
« » 
« »
« »
« » 
« » 
« » 
. Описание функции, вычисляющей шаг редукции для самого левого редекса заданного -терма, не находящегося в нормальной форме.
«
» 
, т. е. « »« »« » « ».
«
» - образ функции, вычисляющей образ заданного терма, т.е. « »« » «« »».
-
Алгоритмически неразрешимые проблемы.
Теорема 4(о существовании специальной фиксированной точки).
Для всякого -терма существует -терм 
, такой, что 
« » 
.
Доказательство.
Пусть 
« » , где 
« » 
« » 
. Действительно,
« » « » « » 
« »« » « »« » 
« »« »«« »» 
«
« » » 
« » .
Определение 5. Пусть 
и 
- подмножества множества 
. называется рекурсивно отделимым от , если существует рекурсивное подмножество 
множества , такое, что 
и 
.
Напомним, что подмножество множества называется рекурсивным, если существует всюду определенный на вычислимый предикат 
, такой, что 
.
Определение 6. Подмножество 
множества называется нетривиальным, если 
и 
.
Определение 7. Подмножество 
-термов замкнуто относительно отношения -конверсии, если 
.
Теорема 5 (о рекурсивной неотделимости).
Два произвольных нетривиальных подмножества -термов, замкнутых относительно отношения -конверсии, не являются рекурсивно отделимыми.
Доказательство.
Пусть и - два подмножества -термов, удовлетворяющие условиям теоремы. Так как они не пересекаются (в этом случае результат очевиден) и не пусты, то выберем в них по одному элементу: 
и 
. Предположим от противного, что существует рекурсивное подмножество , такое, что и . Рекурсивность означает, что существует всюду определенный на множестве -термов вычислимый предикат 
, такой, что 
Вычислимость этого предиката означает, что существует его -образ « », такой, что « »« » « », если 
, и « »« » « », если 
.
Построим терм 
« » 
, для которого будет иметь место утверждение: если 
, то 
«
» 
, если 
, то « » 
. Согласно теореме 4 построим для -терма 
такой -терм 
, что « » 
. Возникает вопрос: 
или 
? Начнем с первого предположения. Так как и , то 
. С другой стороны, 
« » 
, и, в силу замкнутости относительно отношения -конверсии, 
. Получилось противоречие. Рассмотрим второе предположение. Так как , а , то 
. С другой стороны, « » 
, и, в силу замкнутости относительно отношения -конверсии, 
. Вновь получилось противоречие. Следовательно, исходное предположение о рекурсивной отделимости и ложно.
![](https://s.studizba.com/z.php?f=/templates/si/i/noavatar.png&w=100&h=100&t=1"){kind=avatar}
