Главная » Просмотр файлов » Лямбда-исчисление

Лямбда-исчисление (547599), страница 2

Файл №547599 Лямбда-исчисление (Файлы для подготовки к экзамену) 2 страницаЛямбда-исчисление (547599) страница 22015-08-23СтудИзба
Просмтор этого файла доступен только зарегистрированным пользователям. Но у нас супер быстрая регистрация: достаточно только электронной почты!

Текст из файла (страница 2)

Определение 4. Отношение редукции на некотором множестве термов называется конфлюэнтным, если имеет место утверждение:

.

Теорема 2 (Черча-Россера).

Отношение -редукции на множестве -термов является конфлюэнтным.

Доказательство можно найти в монографиях, посвященных более глубокому изложению теории -исчисления, например в [2].

Следствие 1 (теоремы 2).

Если -терм имеет нормальную форму, то она – единственная (с точностью до -конверсии).

Доказательство очевидно.

Если к определению отношения -редукции термов добавить дополнительно условие симметричности, то минимальное отношение, удовлетворяющее перечисленным ниже требованиям, называется отношением -конверсии термов и обозначается инфиксом :

  1. .

  2. .

  3. .

  4. .

  5. , где - произвольный -контекст.

Следствие 2 (теоремы 2).

Если (терм конвертируется с термом ), то существует такой терм , что и .

Доказательство очевидно.

Соглашение об обозначениях.

Для облегчения дальнейшего изложения примем некоторые соглашения о сокращенном представлении -термов:

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

  2. Вместо символов переменных могут использоваться любые строчные латинские буквы, причем разным буквам будут соответствовать переменные с разными номерами.

  3. Прописные латинские буквы в позициях переменных рассматриваются как метапеременные; в качестве их значений могут быть переменные с любыми конкретными номерами.

Например, запись представляет собой сокращенную запись терма .

Теорема 3 (Карри).

Для любого -терма и любой переменной существует -терм , такой, что .

Иными словами, всякое уравнение имеет решение в -исчислении (с точностью до отношения конверсии термов).

Доказательство.

Пусть ( называют парадоксальным комбинатором Карри). Тогда терм , существование которого утверждает теорема 3, может быть получен так: . Действительно,

  1. Моделирование в -исчислении конструктивных объектов и вычислимых функций.

Пусть - подмножество замкнутых, т.е. не содержащих свободных вхождений переменных, -термов ( -термов); - подмножество -термов в нормальной форме ( -термов), а - их пересечение (множество -термов).

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

, где - арность -го конструктора для сорта . Для всех через обозначим взаимно-однозначные отображения в множество -термов. Если , то будем далее обозначать как « » и называть -образом объекта . Если для построения объектов различных сортов используются различные наборы конструкторов, то в обозначении -образа объекта нет необходимости указывать его сорт , и он обозначается просто как « ». Определим образы объектов по общему правилу. Пусть . Тогда « » « »« »…« » .

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

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

Пример 1. Сорт - логические значения, конструкторы , :

« » ,

« » .

Заметим, что образы логических значений играют роль функций выбора значения одного из двух аргументов, « » - первого, а « » - второго, что позволяет использовать это при моделировании условных определений .

Действительно, « » , а

« » .

Пример 2. Сорт - натуральные числа, конструкторы , :

« » ,

« » « » .

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

« »

« » « » « » « » .

« » « » . В этом примере используется упомянутый выше прием условного определения.

« » « » « » . Описание образа функции умножения натуральных чисел.

« » « » « » « » . Описание образа функции возведения в степень для натуральных чисел.

« » « » « »

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

Пример 3. Сорт - последовательности натуральных чисел любой конечной длины, конструкторы , , где :

« » ,

« » « »« » .

« » « » . Описание образа функции сцепления двух последовательностей в одну.

« » « » .

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

« » « » « » . Описание образа функции, изменяющей порядок следования элементов последовательности на обратный.

« » « »

« » « » . слияния двух упорядоченных по неубыванию последовательностей натуральных чисел в одну общую неубывающую последовательность.

« » « » . Описание функции, выделяющей подсписок элементов с нечетными номерами в списке – аргументе.

« » « » . Описание функции, выделяющей подсписок элементов с четными номерами в списке – аргументе.

« » « » « » « »

« » « » . Описание функции сортировки по неубыванию последовательности натуральных чисел методом слияния.

Пример 4. Сорт - -термы, конструкторы , и :

« » « » ,

« » « »« » ,

« » « »« » ,

« » « » « » « » « »

« » . Описание предиката, устанавливающего, находится -терм в нормальной форме или нет. - вспомогательный предикат:

« » « » « » « » « »

« » .

« » « » « » « » « » « » « » « » . Описание предиката , где

« » « » « » « » « » . Описание предиката неравенства двух натуральных чисел.

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

« » « » « » .

« » « »

« »

« »

« »

« »

« »

« »

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

« » « » « » « » . Описание частичной функции, вычисляющей нормальную форму заданного -терма.

« »

« »

« »

« »

« »

« »

« » . Описание функции, вычисляющей шаг редукции для самого левого редекса заданного -терма, не находящегося в нормальной форме.

« » , т. е. « »« »« » « ».

« » - образ функции, вычисляющей образ заданного терма, т.е. « »« » «« »».

  1. Алгоритмически неразрешимые проблемы.

Теорема 4(о существовании специальной фиксированной точки).

Для всякого -терма существует -терм , такой, что « » .

Доказательство.

Пусть « » , где « » « » . Действительно,

« » « » « » « »« » « »« »

« »« »«« »» « « » » « » .

Определение 5. Пусть и - подмножества множества . называется рекурсивно отделимым от , если существует рекурсивное подмножество множества , такое, что и .

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

Определение 6. Подмножество множества называется нетривиальным, если и .

Определение 7. Подмножество -термов замкнуто относительно отношения -конверсии, если .

Теорема 5 (о рекурсивной неотделимости).

Два произвольных нетривиальных подмножества -термов, замкнутых относительно отношения -конверсии, не являются рекурсивно отделимыми.

Доказательство.

Пусть и - два подмножества -термов, удовлетворяющие условиям теоремы. Так как они не пересекаются (в этом случае результат очевиден) и не пусты, то выберем в них по одному элементу: и . Предположим от противного, что существует рекурсивное подмножество , такое, что и . Рекурсивность означает, что существует всюду определенный на множестве -термов вычислимый предикат , такой, что Вычислимость этого предиката означает, что существует его -образ « », такой, что « »« » « », если , и « »« » « », если .

Построим терм « » , для которого будет иметь место утверждение: если , то « » , если , то « » . Согласно теореме 4 построим для -терма такой -терм , что « » . Возникает вопрос: или ? Начнем с первого предположения. Так как и , то . С другой стороны, « » , и, в силу замкнутости относительно отношения -конверсии, . Получилось противоречие. Рассмотрим второе предположение. Так как , а , то . С другой стороны, « » , и, в силу замкнутости относительно отношения -конверсии, . Вновь получилось противоречие. Следовательно, исходное предположение о рекурсивной отделимости и ложно.

Характеристики

Тип файла
Документ
Размер
1,05 Mb
Высшее учебное заведение

Список файлов ответов (шпаргалок)

Свежие статьи
Популярно сейчас
Зачем заказывать выполнение своего задания, если оно уже было выполнено много много раз? Его можно просто купить или даже скачать бесплатно на СтудИзбе. Найдите нужный учебный материал у нас!
Ответы на популярные вопросы
Да! Наши авторы собирают и выкладывают те работы, которые сдаются в Вашем учебном заведении ежегодно и уже проверены преподавателями.
Да! У нас любой человек может выложить любую учебную работу и зарабатывать на её продажах! Но каждый учебный материал публикуется только после тщательной проверки администрацией.
Вернём деньги! А если быть более точными, то автору даётся немного времени на исправление, а если не исправит или выйдет время, то вернём деньги в полном объёме!
Да! На равне с готовыми студенческими работами у нас продаются услуги. Цены на услуги видны сразу, то есть Вам нужно только указать параметры и сразу можно оплачивать.
Отзывы студентов
Ставлю 10/10
Все нравится, очень удобный сайт, помогает в учебе. Кроме этого, можно заработать самому, выставляя готовые учебные материалы на продажу здесь. Рейтинги и отзывы на преподавателей очень помогают сориентироваться в начале нового семестра. Спасибо за такую функцию. Ставлю максимальную оценку.
Лучшая платформа для успешной сдачи сессии
Познакомился со СтудИзбой благодаря своему другу, очень нравится интерфейс, количество доступных файлов, цена, в общем, все прекрасно. Даже сам продаю какие-то свои работы.
Студизба ван лав ❤
Очень офигенный сайт для студентов. Много полезных учебных материалов. Пользуюсь студизбой с октября 2021 года. Серьёзных нареканий нет. Хотелось бы, что бы ввели подписочную модель и сделали материалы дешевле 300 рублей в рамках подписки бесплатными.
Отличный сайт
Лично меня всё устраивает - и покупка, и продажа; и цены, и возможность предпросмотра куска файла, и обилие бесплатных файлов (в подборках по авторам, читай, ВУЗам и факультетам). Есть определённые баги, но всё решаемо, да и администраторы реагируют в течение суток.
Маленький отзыв о большом помощнике!
Студизба спасает в те моменты, когда сроки горят, а работ накопилось достаточно. Довольно удобный сайт с простой навигацией и огромным количеством материалов.
Студ. Изба как крупнейший сборник работ для студентов
Тут дофига бывает всего полезного. Печально, что бывают предметы по которым даже одного бесплатного решения нет, но это скорее вопрос к студентам. В остальном всё здорово.
Спасательный островок
Если уже не успеваешь разобраться или застрял на каком-то задание поможет тебе быстро и недорого решить твою проблему.
Всё и так отлично
Всё очень удобно. Особенно круто, что есть система бонусов и можно выводить остатки денег. Очень много качественных бесплатных файлов.
Отзыв о системе "Студизба"
Отличная платформа для распространения работ, востребованных студентами. Хорошо налаженная и качественная работа сайта, огромная база заданий и аудитория.
Отличный помощник
Отличный сайт с кучей полезных файлов, позволяющий найти много методичек / учебников / отзывов о вузах и преподователях.
Отлично помогает студентам в любой момент для решения трудных и незамедлительных задач
Хотелось бы больше конкретной информации о преподавателях. А так в принципе хороший сайт, всегда им пользуюсь и ни разу не было желания прекратить. Хороший сайт для помощи студентам, удобный и приятный интерфейс. Из недостатков можно выделить только отсутствия небольшого количества файлов.
Спасибо за шикарный сайт
Великолепный сайт на котором студент за не большие деньги может найти помощь с дз, проектами курсовыми, лабораторными, а также узнать отзывы на преподавателей и бесплатно скачать пособия.
Популярные преподаватели
Добавляйте материалы
и зарабатывайте!
Продажи идут автоматически
6384
Авторов
на СтудИзбе
308
Средний доход
с одного платного файла
Обучение Подробнее