Навигация
Главная
Поиск
Форум
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
Подключение Mic... 65535
Создание потоко... 65535
Приложение «Про... 65535
Оператор выбора... 65535
Создание отчето... 63898
Модуль Forms 63632
ТЕХНОЛОГИИ ДОСТ... 60477
Пример работы с... 59845
Имитационное мо... 55944
Реклама
Сейчас на сайте
Гостей: 4
На сайте нет зарегистрированных пользователей

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

моделирование процесса поступления заявок в ЭВМ на GPSS + Пояснительная ...
Моделирование работы перекрёстка по регулированию движения на GPSS + Поя...
Компьютерный магазин на 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 Комментариев · 1572 Прочтений · Для печати

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


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



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

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

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

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

Пароль



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

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

Случайные загрузки
GPSS World Studen...
Х. М. Дейтел, П. ...
SynEdit
Text effect
API (Применение A...
Цветной Grid
Swat [Исходник на...
Delphi World 6.0
Atb
Программирование ...
32 урока по Delphi
База данных: Книж...
Error mod
BIOS
Программирование ...
Работа с картотеками
FatScrollbar
DCMintry
Панель "ссылки"
ZipTV

Топ загрузок
Приложение Клие... 100449
Delphi 7 Enterp... 85813
Converter AMR<-... 20067
GPSS World Stud... 12518
Borland C++Buil... 11575
Borland Delphi ... 8504
Turbo Pascal fo... 7023
Visual Studio 2... 4989
Калькулятор [Ис... 4739
FreeSMS v1.3.1 3536
Случайные статьи
Ограничение проток...
Приведение к супер...
Команда UPDATE
Визуальные фильтры
Определить самую д...
blueyonder
Модуль Image
Блок DSU
Демонстрация неско...
Влияние ЭВМ на сис...
Ограничения модемов
Операция V0P_MAP
Структуры XForms
отдельного диска в...
Числовые SQL-функц...
Схема простого тес...
Банкетные стулья К...
действие, которое ...
Инициализация конс...
Виды роботов Яндекса
Указатель this
Lol boosting
Передать содержимо...
Главное меню
Формы и методы рез...
Статистика



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


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