1. Уважаемые друзья!

    С 8 февраля 2018 года наш форум переходит в режим Элитарного Клуба.
    Теперь незарегистрированным посетителям запрещено подглядывать и подслушивать наши тайные переговоры, а чтобы зарегистрироваться, нужно... впрочем, если вы действительно достойны стать членом Клуба, то вы наверняка разберётесь, как это сделать.

    Возрадуйтесь, обладатели зарегистрированных аккаунтов! Обещаем вам чистки, репрессии и все остальные бонусы тоталитарного сообщества.

    Всегда ваша,
    Администрация Корума

ДМ. Формализм де Брейна

Тема в разделе "Вопросы высшей математики", создана пользователем BA3a, 28 июн 2013.

Модераторы: onyx
  1. BA3a

    BA3a for love and rock-n-roll VIP

    Теоретический минимум

    Напомним для начала постулаты [​IMG] и [​IMG] [​IMG]-конверсии:
    [​IMG] [​IMG]
    [​IMG] [​IMG]

    Семантические равенства, приложение функции к аргументу представляется записью вслед за символом функции символа аргумента:
    [​IMG]
    где [​IMG] — значение [​IMG] в среде [​IMG];
    [​IMG] — константа (считаем среду самоозначивающей);
    [​IMG] — среда [​IMG], где [​IMG] замещён на значение [​IMG], т.е. выполнена подстановка [​IMG] вместо [​IMG] в [​IMG].

    Необходимость кода де Брейна

    Предположим, у нас есть [​IMG]-выражение вида
    [​IMG].
    Редуцируем его по правилу [​IMG]:
    [​IMG].
    В том же самом выражении теперь переименуем по правилу [​IMG] переменные:
    [​IMG].
    После этого, если мы применим правило [​IMG], получится следующее выражение:
    [​IMG].
    Как видно, в первом случае произошло неправомерное связывание переменной [​IMG], что привело к искажению значения [​IMG]-выражения. Согласитесь, тождественная функция и константная функция совпадают, только когда переменная из среды вычисления совпадает с константой в выражении.
    Напрашивается очевидное решение: перед применением выражения к среде переименовывать все связанные переменные в нём по правилу [​IMG] на незанятые названия. Но в реальных вычислениях код может быть очень объёмным, и задача может становиться очень непростой. Николас Говерт де Брёйн, занимаясь разработкой Automath (языка, реализующего парадигму изоморфизма Карри — Ховарда, утверждающую о взаимно-однозначном соответствии между формальным доказательством и компьютерной программой) столкнулся с этой проблемой. Он разработал очень простой и наглядный способ избавления от имён переменных, названный формализмом де Брейна или кодами де Брейна.

    Формализм де Брейна

    В замкнутом терме существенно важной информацией о переменной является глубина её связывания, то есть количество символов [​IMG], стоящих между переменной и связыванием [​IMG]. Можно заменить её на число, которое, для отличия от обычных чисел, называется числом де Брейна. Покажем на примере [​IMG]. Для ясности восстановим опущенные символы [​IMG]:
    [​IMG].
    Начнём со скобки: от единственной переменной [​IMG] до её связывания надо пройти через [​IMG]. Заменяем её на [​IMG]:
    [​IMG].
    Перейдём теперь к оставшейся снаружи переменной [​IMG]. Как видно, она сразу связывается, то есть её следует заменить на [​IMG]:
    [​IMG].
    Теперь все переменные из исходного выражения заменены на числа, обозначающие их глубину связывания и имена переменных при [​IMG] больше не нужны. В итоге выражение принимает вид
    [​IMG].
    Нетрудно убедиться, что в случае необходимости исходное выражение восстанавливается с точностью до переименования переменных. Учитывая постулат [​IMG], этой точности вполне достаточно.

    Связь формализма де Брейна с вычислениями в среде

    Пусть среда [​IMG] имеет вид
    [​IMG]
    где значение [​IMG] ассоциировано с [​IMG] числом де Брейна. Таким образом среда представляет из себя связанную структуру из пустой среды и [​IMG] переменных. Такой выбор ведёт к такому индуктивному написанию семантических равенств:
    [​IMG]
    Вводим три комбинатора:
    [​IMG] с арностью 2,
    [​IMG] с арностью 1,
    [​IMG] с арностью 1
    и бесконечно много комбинаторов [​IMG] в том смысле, что:
    [​IMG].
    Отсюда легко устанавливается процедура перехода от семантических равенств к чисто синтаксическим:
    [​IMG]
    Такие правила близки к [​IMG]-правилам: первые три указывают на «забывающее» аргумент свойство (наподобие комбинатора [​IMG]); четвёртое — некаррированная форма правила [​IMG]; пятое — в точности каррирование. Введём также комбинатор пары [​IMG] где
    [​IMG]
    и снабдим его проекциями [​IMG] и [​IMG]. Введём также оператор композиции [​IMG] и команду [​IMG]. Рассмотрим [​IMG] и [​IMG] как сокращения для [​IMG] и [​IMG] соответсвенно. Сведём все эти комбинаторные равенство воедино:
    [​IMG]
    Используя этот аппарат, можно проводить вычисления в декартовой среде с использованием нотации де Брейна.

    Более основательные источники
    • Вольфенгаген В.Э. Комбинаторная логика в программировании. Вычисления с объектами в примерах и задачах. -- М.:МИФИ, 1994; 2-е изд. – М.: АО “ Центр ЮрИнфоР ”, 2003. – 336 с.
    • Вольфенгаген В.Э. Методы и средства вычислений с объектами. Аппликативные вычислительные системы. -- М.:АО ``Центр ЮрИнфоР’’, 2004. - xvi+789 с.
    • Видеолекция В.Э. Вольфенгагена.
  2. Silver MC's

    Silver MC's ┬┴┬┴┤(・_├┬┴┬┴

    BA3a, все очень здорово оформлено) единственное, что хотелось бы - примеры, много примеров :huh:
  3. BA3a

    BA3a for love and rock-n-roll VIP

    Silver MC's, можно устроить. Правда, по де Брейну примеры уж больно однотипные получатся, боюсь. «Вот выражение, вот пересчитали лямбды, вот заменили на числа. Оп — обратно восстановили, заметьте, по смыслу не поменялось». Я ещё напишу про модели, может, даже сегодня. Думаю, полезно будет перенсти часть курса сюда. Правда, мне КАМ не нравится. Некрасивая абстракция, на мой взгляд.
Модераторы: onyx

Поделиться этой страницей