Навигация
Главная
Поиск
Форум
FAQ's
Ссылки
Карта сайта
Чат программистов

Статьи
-Delphi
-C/C++
-Turbo Pascal
-Assembler
-Java/JS
-PHP
-Perl
-DHTML
-Prolog
-GPSS
-Сайтостроительство
-CMS: PHP Fusion
-Инвестирование

Файлы
-Для программистов
-Компонеты для Delphi
-Исходники на Delphi
-Исходники на C/C++
-Книги по Delphi
-Книги по С/С++
-Книги по JAVA/JS
-Книги по Basic/VB/.NET
-Книги по PHP/MySQL
-Книги по Assembler
-PHP Fusion MOD'ы
-by Kest
Professional Download System
Реклама
Услуги

Автоматическое добавление статей на сайты на Wordpress, Joomla, DLE
Заказать продвижение сайта
Программа для рисования блок-схем
Инженерный калькулятор онлайн
Таблица сложения онлайн
Популярные статьи
OpenGL и Delphi... 65535
Форум на вашем ... 65535
HACK F.A.Q 65535
Бип из системно... 65535
Гостевая книга ... 65535
Invision Power ... 65535
Пример работы с... 65535
Содержание сайт... 65535
Организация зап... 65535
Вызов хранимых ... 65535
Создание отчето... 65535
Программируемая... 65535
Эмулятор микроп... 65535
Подключение Mic... 65535
Создание потоко... 65535
Приложение «Про... 65535
Оператор выбора... 65535
Модуль Forms 65409
ТЕХНОЛОГИИ ДОСТ... 62301
Имитационное мо... 57989
Реклама
Сейчас на сайте
Гостей: 5
На сайте нет зарегистрированных пользователей

Пользователей: 13,087
новичок: sergeevo
Новости
Реклама
Выполняем курсовые и лабораторные по разным языкам программирования
Подробнее - курсовые и лабораторные на заказ
Delphi, Turbo Pascal, Assembler, C, C++, C#, Visual Basic, Java, GPSS, Prolog, 3D MAX, Компас 3D
Заказать программу для Windows Mobile, Symbian

Расчет обратной матрицы на Delphi + Пояснительная записка
Моделирование процесса обеспечивающего надежность функционирования АСУ Т...
Поиск пути в графе заданном списками инцедентности на Turbo Pascal

Реклама



Подписывайся на YouTube канал о программировании, что бы не пропустить новые видео!

ПОДПИСЫВАЙСЯ на канал о программировании
Код де Брейна
Задача 20.1 Для выражения:
let x = plus in x (4,(x where x = 3)); ;



построить λ-выражение и выражение кода де Брейна и вычислить
последнее с помощью SECD-машины.
Решение.
DB--1. Известно, что в ходе выполнения λ -конверсии возника-
ют коллизии переменных. Например, “прямое” выполнение β-
редукции для (λxy.x)y могло бы дать λy.y:
(λxy.x)y = λy.y,



что совершенно недопустимо, поскольку:


Заметим, далее, что в замкнутом терме существенной важ-
ной информацией о переменной служит глубина ее связыва-
ния, то есть количество символов λ , стоящих между пере-
менной и связыванием λ (не считая последний оператор). То-
гда переменная оказывается замененной на число, которое,
однако, нельзя смешивать с обычным натуральным числом.
Для отличия числа, заменяющие переменные, от обычных на-
туральных чисел первые будем называть числами де Брейна.
Теперь, например, для
P = λy.(λxy.x)y



кодирование по де Брейну приобретает вид:


Скажем, правило (β), примененное к этому выражению, дает
λλ.1 , и нет необходимости в преобразовании λxy.x в λxv.x,
которое ликвидирует коллизию. Основной вопрос - это опи-
сание смысла выражений. Это зависит от ассоциаций значе-
ний и идентификаторов, то есть от среды. Таким образом,
означивание представляет собой функцию k M k, ассоцииру-
ющую значение со средой. Представим обычные семантиче-
ские равенства, где приложение функции к аргументу пред-
ставляется просто записью непосредственно вслед за симво-
лом функции символа аргумента:

k x k env = env(x),
k c k env = c,
k (MN) k env = k M k env(k N k env),
k λx.M k env d = k M k env[x ← d],



где:
env(x) - значение x в среде env;
c - константа, обозначающее значение,
также называемое c, что
соответствует обычной практике;
env[x ← d] - среда env, где x замещен на значение d.
Вообще, формализм де Брейна может быть рассмотрен по
аналогии с комбинаторной логикой с соответствующей ада-
птацией правил. Для осуществления перехода от обычных λ
-выражений к кодировке переменных числами де Брейна рас-
смотрим ряд правил и соглашений. Пусть среда env имеет
вид (. . .((), wn). . . , w0), где значение wi ассоциировано с чи-
слом i де Брейна. Такое предположения учитывает довольно
сильные ограничения. Среды, в которых происходит вычисле-
ние выражений, считаются связанными структурами, а не
массивами. Такой выбор тесно связан с выполнением требо-
вания эффективности. Прежде всего данный выбор ведет к
простому машинному описанию:


Интерес представляют не только значения сами по себе, а
значения с точки зрения обеспечиваемых ими вычислений. При
комбинаторном подходе подчеркивается, что значением, на-
пример, MN служит комбинация значений M и N.
Вводится три комбинатора:
S с арностью 2,
Λ c арностью 1, 0 c арностью 1
и бесконечно много комбинаторов n! в том смысле, что:
k n k = n!,
k c k env = c,
k MN k = S(k M k,k N k),
k λ.M k = Λ(k M k).



Отсюда легко устанавливается процедура перехода от се-
мантических равенств к чисто синтаксическим:

0!(x, y) = y,
(n+ 1)!(x, y) = n!x,
(0
x)y = x,
S(x, y)z = xz(yz),
Λ(x)yz = x(y, z)



Такие правила близки кSK-правилам: первые три указывают
на “забывающее” аргумент свойство (наподобие комбинато-
ра ); четвертое -- некаррированная форма правила S; пятое
-- в точности каррирование, то есть преобразование функции
от двух аргументов в функцию от первого аргумента, задаю-
щую функцию от второго аргумента.
Введем также комбинатор пары < ·,· >, где
k (M, N) k=,



и снабдим его выделителями (проекциями) F st и Snd. Вве-
дем также оператор композиции “◦” и новую команду ε. Рас-
смотрим S (·,·) и n! как сокращения для “ε◦ < ·,· >” и
“Snd ◦ F stn” соответственно, где F stn+1 = F st ◦ F stn.
Сведем теперь все комбинаторные равенства воедино:
(ass) (x ◦ y)z = x(yz),
(fst) F st(x, y) = x,
(snd) Snd(x, y) = y,
(dpair) < x, y > z = (xz, yz),
(ac) ε(Λ(x)y, z) = x(y, z),
(quote) (0
x)y = x,



где (dpair) устанавливает связь спаривания и образования со-
вокупности, а (acc)- композиции и аппликации. Можно заме-
тить, что S(x, y)z = ε(xz, yz). Тем самым придается од-
нородность рассмотрению операторов F st, Snd и ε . Кроме
того, справедливо равенство:

0
M = Λ(M ◦Snd),



откуда следует, что
(0x)yz = xz.



Пользуясь синтаксическими и семантическими равенствами,
получаем для M = (λx.x(4,(λx.x)3))+ :

M0 =k M k=k (λ.0(4,(λ.0)3))+ k
= S(k λ.0(4,(λ.0)3) k,k + k)
= S(Λ(k 0(4,(λ.0)3) k),k + k)
= S(Λ(S(0!,k (4,(λ.0)3) k)),k + k)
= S(Λ(S(0!, <0 4,S(Λ(0!),
0 3) >)),Λ(+◦Snd)).



DB--2. Теперь произведем вычисления по методу Лендина дляSECD-
машины, то есть следует означивать путем приложения 0 к
среде. В данном случае среда пуста, поскольку терм замкнут.
При означивании 0 применим стратегию самого левого и при
том самого внутреннего выражения. Для краткости обозна-
чим:
A = S(0!, <0 4, B >), B = S(Λ(0!),3).



Приведем полную последовательность редукций:
(Λ(A),Λ(+◦Snd))()
→ ε(Λ(A)(),Λ(+◦Snd)())
→ A env
(здесь: для сокращения env = ((),Λ(+◦Snd)()))
→ ε(0!env, <0 4, B > env)
→ ε(Λ(+◦Snd)(),(0
4 env, B env))
→ ε(Λ(+◦Snd)(),(4, B env))
→ ε(Λ(+◦Snd)(),(4, ε(Λ(0!)env,0 3 env)))
→ ε(Λ(+◦Snd)(),(4, ε(Λ(0!)env,3)))
→ ε(Λ(+◦Snd)(),(4,0!(env,3)))
→ ε(Λ(+◦Snd)(),(4,3))
→ (+◦Snd)((),(4,3))
→ +(Snd((),(4,3)))
→ +(4,3)
⇒ 7.



Видно,что результат совпадает с результатом, полученным
в ходе непосредственных вычислений выражения.
Контрольные вопросы.
1. Назовите альтернативные способы устранения коллизии пере-
менных в λ -выражениях.
2. Обоснуйте необходимость введения оператора композиции.
3. Покажите связь и различие между понятиями “пара” и “сово-
купность”.
Указание. Воспользуйтесь теоретико-множественными определени-
ями для этих понятий, положив f : D → E, g : D → F.
совокупность : h =< f, g >: D → E ×F;
пара : [f, g] = (f, g) : (D → E)×(D → F).
Упражнение. Постройте выражения де Брейна для приводимых да-
лее λ-выражений.
1. λy.yx.



Ответ:
k λy.yx k= Λ(S(0!,1!)).



2. (λx.(λz.zx)y)((λt.t)z).



Указание. Обозначим исходное выражение черезQи перейдем
к выражению R = λzxy.Q. Тогда, рассмотрев дерево предста-
вления R, можем записать его в виде:
R0 = (λ.(λ.01)1)((λ.0)2),



и простой заменой “λ” на “Λ”, “◦” на "S", “n” на “n!” получить
код де Брейна для Q.


Ответ.
QDB(z,x,y) = S(Λ(S(Λ(S(0!,1!))1!)),S(Λ(0!),2!))



(порядок имен переменных в индексе Q соответствует поряд-
ку их связывания в промежуточном выражении R и позволяет
восстановить исходное определение с соответствующими сво-
бодными переменными).
Опубликовал Kest June 20 2014 15:15:11 · 0 Комментариев · 1685 Прочтений · Для печати

• Не нашли ответ на свой вопрос? Тогда задайте вопрос в комментариях или на форуме! •


Комментарии
Нет комментариев.
Добавить комментарий
Имя:



smiley smiley smiley smiley smiley smiley smiley smiley smiley
Запретить смайлики в комментариях

Введите проверочный код:* =
Рейтинги
Рейтинг доступен только для пользователей.

Пожалуйста, залогиньтесь или зарегистрируйтесь для голосования.

Нет данных для оценки.
Гость
Имя

Пароль



Вы не зарегистрированны?
Нажмите здесь для регистрации.

Забыли пароль?
Запросите новый здесь.
Поделиться ссылкой
Фолловь меня в Твиттере! • Смотрите канал о путешествияхКак приготовить мидии в тайланде?
Загрузки
Новые загрузки
iChat v.7.0 Final...
iComm v.6.1 - выв...
Visual Studio 200...
CodeGear RAD Stud...
Шаблон для новост...

Случайные загрузки
ZipTV
Delphi Russian Kn...
Rotolabel
PHP в примерах
DateEdit
ЯЗЫК ПРОГРАММИРОВ...
Pro-Download Sys...
ActiveX в Delphi
JanComp
С/C++ Программиро...
Панель случайной ...
OnlineIP
Род Стивенс. Delp...
Разработка Web-пр...
Платформа програм...
Нестандартные при...
Allsubmitter 4.7 ...
CaptionButton
C++ Builder в за...
CwstatusBar

Топ загрузок
Приложение Клие... 100471
Delphi 7 Enterp... 87432
Converter AMR<-... 20080
GPSS World Stud... 13063
Borland C++Buil... 11922
Borland Delphi ... 8631
Turbo Pascal fo... 7041
Visual Studio 2... 5000
Калькулятор [Ис... 4853
FreeSMS v1.3.1 3543
Случайные статьи
Нетиповые операции...
Система управления...
5.2.2. Ввод литер
Создание восстанов...
Искажения образа т...
Возникновение взаи...
Окно Add Table пос...
Резюме: куда включ...
Создание документа
Необоснованный азарт
Решение задачи мет...
Персональные услуг...
ОЧЕРЕДИ
Оказывается, деньг...
Идентификация типа...
клиентских машинах...
Кардшаринг нтв
Структура жеста
ЦС предприятия нео...
telling (X)
r\Network\System P...
Отчет по доходам н...
Счет в Сингапуре
IPSecПри работе пр...
Сейчас в Интернете...
Статистика



Друзья сайта
Программы, игры


Полезно
В какую объединенную сеть входит классовая сеть? Суммирование маршрутов Занимают ли таблицы память маршрутизатора?