Навигация
Главная
Поиск
Форум
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
Подключение Mic... 65535
Приложение «Про... 65535
Оператор выбора... 65535
Организация зап... 64682
Создание потоко... 62664
Модуль Forms 61267
Создание отчето... 61239
ТЕХНОЛОГИИ ДОСТ... 57704
Пример работы с... 55212
Имитационное мо... 53097
Реклама
Сейчас на сайте
Гостей: 10
На сайте нет зарегистрированных пользователей

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

Расчет размера дохода на одного человека в Turbo Pascal
Моделирование процесса обработки заданий на вычислительном центре на GP...
Обучающая и тестирующая программа по здаче экзамена ПДД на 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 Комментариев · 1392 Прочтений · Для печати

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


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



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

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

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

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

Пароль



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

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

Случайные загрузки
Правила программи...
Text effect
Delphi Russian Kn...
Illusion
3D Тетрис [Исходн...
ATComponents
PHP 5 для "чайников"
BIOS
PolyFlow
THttpScan v4.1
CS:Source - монит...
Синтаксический ан...
SearchAndReplace
Создание Web-сайт...
Ранги для форума
C# Учебный курс
База предприятий ...
Последнее загруж...
JBlabel3D
Пример клиента ФТ...

Топ загрузок
Приложение Клие... 100386
Delphi 7 Enterp... 83602
Converter AMR<-... 20051
GPSS World Stud... 11328
Borland C++Buil... 11247
Borland Delphi ... 8186
Turbo Pascal fo... 6988
Visual Studio 2... 4970
Калькулятор [Ис... 4421
FreeSMS v1.3.1 3516
Случайные статьи
Понятие свойства. ...
Точность подачи ко...
Ассоциативные массивы
Блок дАМА
Полиморфизм
Карта JOB
Вычисление значени...
Вид граничного режима
передаваемых по ГВС
Глава 9. Обратн...
Жесткие диски
События Dynamic HTML
Ввод программ
Аналоговый сигнал ...
Содержание
Корзины для элементов
Стандартные числов...
Оптимальная сортир...
Разное
Понятие "документ"...
Об этой книге XXXII
Метод экспертного ...
Обновление связанн...
Ускоренное умножение
ОБЯЗАТЕЛЬНЫЕ ИДЕНТ...
Статистика



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


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