2 Постановка задачи: о связном предъявлении теории информатики и практики программирования в теме исполнения для теоретического мышления. 13 (стр. 8 из 25)
Монотонность очевидна. Если M1ÍM2, то D(M1)ÍD(M2).
Проверим непрерывность: M0=^, Mi+1=D(Mi), тогда MiÊMi+1.
UD(Mi)=UMi+1=D(UMi).
Формальные языки могут трактоваться как решения уравнений для множеств. Рассмотрим язык, определяемый БНФ (см. п. 3.4).
<x>::=1|2<x>
Зафиксируем решетку множеств по включению. Язык можем воспринимать как решение уравнения
Доказательство монотонности и непрерывности оператора t аналогично случаю для оператора D.
Решением уравнения является регулярное множество 2*×1.
Подведем итог использованию неподвижной точки. В рассмотренных примерах практическая роль уравнений незначительна, так как примеры достаточно простые. Это похоже на использование техники пределов для поиска предельного значения простой непрерывной функции. Но, уже приятно то, что с единых позиций рассматриваются рекурсивные функции, типы, формальные языки.
Конечно же, настоящая роль теории неподвижной точки скажется в исследовании классов задач. Например, если регулярные языки будут определяться взаимной рекурсией, то известно, что их решение (наименьшую неподвижную функцию) можно искать аналогом метода Гаусса. Доказательство этого факта легче получить, если обобщить теорию неподвижной точки на декартово произведение. Тогда, выяснив совпадение индуктивной схемы и теоретико-множественной, от преобразований надо требовать свойства равносильности, то есть исследовать на теоретико-множественном уровне.
3.2 Редукционные реализации (математический аспект).
Кажется весьма выгодной в отношении обучения тесная связь, существующая между теорией неподвижной точки, проблемой свободных переменных и комбинаторной редукцией. Это позволяет в обучении естественно переходить к математическому аспекту прагматика, а от него - к классу профессионала.
Поэтому в этом пункте мы собираемся рассмотреть различные методы, используемые для реализации функциональных языков. При этом будет использоваться лямбда-нотация для функциональных выражений, которая является достаточно мощной, чтобы выразить все черты функционального языка, и в то же время достаточно простой, чтобы легко описать различные методы реализации без рассмотрения специфики языков. Кроме того, лямбда-нотация происходит из области математической логики, называемой лямбда-исчислением, на котором основаны многие теоретические результаты в области функциональных языков. Основные понятия бестипового лямбда-исчисления приводятся в приложении.
Все функциональные языки основаны на применении функций. В лямбда-исчислении применение функций выражается b-редукцией. Неформально роль b-редукции состоит в том, чтобы заменить каждое вхождение формального параметра функции соответствующим параметром. В основе любой реализации лежит порядок выполнения последовательных редукций и условий, при которых последовательность редукций завершается. Существует два пути выполнения b-редукций: мы можем либо оставить ссылку на формальный параметр баз изменений, но запомнить обозначаемую ею величину, либо выполнить подстановку, которая заменяет ссылку на параметр его фактическим значением. Эти два подхода ведут к реализациям, основанным соответственно на контексте и копировании.
Примером первого подхода является реализация, основанная на SECD-машине (см. Приложения). Кроме того, что фактические параметры запоминаются в отдельном контексте, эта реализация рассматривает лямбда-выражения “текстуально”, то есть как строки символов. Альтернативой этому является использование двумерного графового представления выражений. Общая модель, использующая такое представление, называется редукцией графов. Эта модель основана на копировании, поскольку применение функций к аргументу ведет к копированию графа тела функции с выполнением соответствующей подстановки аргумента.
3.2.1 Несколько слов о редукции графов.
Редукция графов возникла как мощная модель реализации “ленивых” функциональных языков, особенно на параллельных компьютерах. Суперкомбинаторы и вполне задержанные вычисления являются двумя из важнейших методов, пригодных для эффективной реализации редукции графов.
Дадим краткое описание редукции графов. Рассмотрим функциональную программу (lx. AND x x) (NOT TRUE). Представим эту программу деревом ее грамматического разбора
где знак @ стоит на месте функциональной аппликации. Отметим, что карринг отражен в поддереве для (AND x x).
Это дерево содержит два так называемых редуцируемых выражения (или редекса), которые состоят из применения (аппликации) функции к своему аргументу (аргументам): применение NOT к TRUE и применение lx-абстракции к (NOT TRUE). Чтобы применить lx-абстракцию к ее аргументу (NOT TRUE) мы заменяем верхний узел @ некоторой конкретизацией тела lx-абстракции, в которой вместо каждого вхождения x подставляется указатель на аргумент:
Заметим, что дерево превратилось в граф. Теперь мы можем применить NOT к его аргументу TRUE, получив
Наконец, выполнив операцию AND, получим FALSE.
Каждый из выполненных шагов вычисления называется редукцией. Этот простой пример показывает, что
1) Исполнение функциональной программы заключается в вычислении некоторого выражения.
2) Функциональная программа допускает естественное представление в виде дерева (или, в более общем случае, графа).
3) Вычисление сводится к последовательности простых шагов, называемых редукциями, которые заключается в применении функции к некоторым аргументам (отсюда термин редукция графов). Каждая редукция является локальным преобразованием графа.
4) Лямда-абстракция применяется к своему аргументу путем создания нового наполнения (конкретизации) своего тела, в котором вместо каждого свободного вхождения формального параметра подставляется указатель на этот параметр.
5) Вычисление завершается, когда больше нет редуцируемых выражений. При этом говорят, что выражение имеет нормальную форму.
6) Порядок редуцирования редексов не влияет на ответ. Теорема Черча-Россера гарантирует, что стратегия проведения - редукций - безразлична. Теорема Черча-Россера для b-редукции: Если P|>bМ и P|>bN, то существует такой терм T, что M|>bT, N|>bT.
7) Редукции можно без опасений применять одновременно, так как они не мешают друг другу. Например, первые две редукции в нашем примере можно выполнить одновременно.
Простейший способ реализации редукции графов заключается в том, чтобы выполнить обход тела лямбда-абстракции и построить его новую копию, подставляя указатель на аргумент вместо каждого свободного вхождения формального параметра. Тело абстракции рассматривается как шаблон и не изменяется в результате этой операции. Однако, этот способ неэффективен по причине большого количества проверок в каждом узле шаблона. Этот способ моделирует редукцию графов и является интерпретирующим.
Более эффективным способом является компиляция, сопоставляющая каждому лямбда-телу фиксированную последовательность команд, которую компилятор может построить заранее. Скомпилированный код будет выполняться гораздо быстрее, чем алгоритм обхода дерева (по тем же причинам, по которым скомпилированный код выполняется быстрее интерпретированного кода в обычных языках).
Но, к сожалению, не все лямбда-абстракции поддаются такой компиляции. Возникает проблема свободных переменных.
3.2.2 Проблема свободных переменных.
Рассмотрим лямбда-абстракцию lx. (ly. - x y). При применении ее к некоторому аргументу, например 3, мы наполняем ее тело, создавая тем самым новую лямбда-абстракцию (lx. - y 3). Каждое применение lx-абстракции к новым аргументам создает новые и различные ly-абстракции, тем самым лишая нас надежды скомпилировать единственный фиксированный код для каждой лямбда-абстракции.
Проблема заключается в свободном вхождении x в тело ly-абстракции. Каждый раз мы вынуждены строить новое наполнение ly-абстракции.
Имеются ли какие-либо решения этой проблемы? К счастью, ответом является “да”. Есть два подхода, которые можно выбрать. Один из путей решения данной проблемы - обеспечить прямой доступ к значениям свободных переменных, то есть такой механизм, который поддерживает явный контекст. Этот подход приводит нас к SECD-машине, основанной на среде, содержащей значения всех свободных переменных.
Другой подход заключается в том, чтобы преобразовать явные свободные переменные при компиляции. Один из способов добиться этого заключается в трансляции l-выражений в комбинаторную логику и в определении машины редукции графов для комбинаторных графов (комбинаторы, как и l-выражения, могут быть представлены в виде графов). Второй метод состоит в трактовке всех свободных переменных как аргументов дополнительных l-абстракций; этот метод называется l-поднятием (lifting) [9] [25].
Существуют также более сложные методы, например, использование суперкомбинаторов [9].
3.2.3 Комбинаторная редукция
Рассмотрим формализацию вычислительных предписаний, которые представляются КОМБИНАТОРАМИ. В аппликативном программировании их роль значительна и в прагматическом плане (т.к. они могут послужить реализацией аппликативного интерпретатора), и в теоретическом плане (т.к. они являются теми функциями, которые порождают функции).