В.Ш. Кауфман - Языки программирования - концепции и принципы (1990) (1160787), страница 50
Текст из файла (страница 50)
Подводя итог, можно сказать, что идея подстановки работает в Рефале три
раза:
1. Интерпретация i определяет подстановку значений переменных вместо их
обозначений.
2. Тем самым она определяет соответствие обобщенной и конкретной
марковских подстановок (т.е. "подстановку" конкретной подстановки вместо
обобщенной).
3. Правая часть этой конкретной подстановки заменяет ведущий терм.
При этом подбор согласующей интерпретации есть, по существу, анализ
ведущего терма, а порождение конкретной правой части подстановки при
найденной интерпретации - синтез заменяющего выражения (в правой части
всегда должно быть правильное выражение - это еще одно требование Рефала). В
этом смысле левая часть предложения служит образцом структуры ведущего терма
(терм и предложение согласуются, если структура терма соответствует
образцу), а правая - образцом для синтезируемого заменяющего выражения.
Упражнение. Покажите, что если ведущий терм согласуется с некоторым
предложением, то соответствующее согласование единственно.
Подсказка. Оно либо левое, либо правое.
13.3.3. Исполнитель (МТ-машина)
Теперь легко объяснить, как действует исполнитель, имея в поле зрения
обрабатываемое выражение, а в поле определений - программу (т.е. кортеж
предложений). Он выполняет следующий цикл:
1. Выделяет ведущий терм. Если такового нет, останавливается. Выражение
в поле зрения считается результатом.
2. Ищет первое по порядку предложение, которое согласуется с ведущим
термом. Соответствующее согласование всегда единственно. Значит, единственна
и изображаемая при соответствующей интерпретации переменных марковская
подстановка. Она и применяется к ведущему терму. И цикл начинается сначала с
обновленным полем зрения.
Если нет согласующихся с ведущим термом предложений, то исполнитель
останавливается с диагностикой "согласование невозможно".
13.3.4. Программирование в модели МТ
Задачу перевода в ПОЛИЗ (с учетом старшинства операций) решает
следующая программа.
{e1+e2}R -> {e1}{e2}+
{e1*e2}R -> {e1}{e2}*
{(e)} -> {e}
{e} -> e
Упражнение 1. Доказать, что это правильная программа.
[Обратите внимание: действиями исполнителя полностью управляет
структура обрабатываемых данных.] .
Упражнение 2. Можно ли эту программу написать короче? Например, так:
{e1 s:(+I*) e2}R -> {e1}{e2}S
{(e)} -> {e}
{e} -> e
Упражнение 3. Можно ли здесь отказаться от правого согласования?
Упражнение 4. Напишите программу аналитического дифференцирования
многочленов по переменной "x".
13.3.5. Основное семантическое соотношение в модели МТ
Рассмотрим функцию sem, реализуемую МТ-программой p. Ее тип, очевидно
sem:P x E -> E
где Р - программы, Е - выражения.
[Уже тип функции sem указывает на принципиалъное отличие от модели Н -
программа не меняется. В модели Н программа - часть (изменяемого)
состояния.]
Пусть ft - функция, выделяющая в выражении ведущий функциональный терм,
l и r - функции, выделяющие соответственно левую и правую части выражения,
оставшиеся после удаления ведущего терма. Конкатенацию (соединение) строк
литер будем обозначать точкой ".". Удобно считать, что если ведущего терма
в выражении е нет, то ft = <>, r(e) = e, где <> обозначает пустое слово. Все
эти три функции типа E -> W, где W - тип "слов" (произвольных
последовательностей литер), так как результаты могут и не быть выражениями.
Пусть далее step - функция типа
Р х Т' -> E ,
где Т' = Т U {<>}. Она реализуется одним шагом работы МТ-машины -
отображает пару
(программа, ведущий терм или пусто)
в выражение, получающееся из этого терма применением соответствующей МТ-
подстановки. Функция step, естественно, частичная - она не определена, если
согласование с p невозможно; step(p,<>) = <> по определению.
Учтем, что p не меняется и вся зависимость sem от p скрыта в функции
step. Поэтому позволим себе для краткости явно не указывать p среди
аргументов функций sem и step. Тогда можно выписать следующее соотношение
для sem:
sem(e) = sem(l(e).step(ft(e)).r(e))
Если обозначить l(e), r(e) и ft(e) соответственно через l, r и f, то
получим более выразительное соотношение:
(a) sem(l.ft.r) = sem(l.step(ft).r)
Покажем, что на самом деле справедливо следующее основное соотношение
(b) sem(l.ft.r) = sem(l.sem(ft).r)
Действительно, если step(ft) не содержит функциональных термов, то
sem(ft) = step(ft)
и (b) cледует из (a).
Если же step (ft) содержит функциональные термы, то так как l таких
термов не содержит, все функциональные термы из step(ft) будут заменены
раньше, чем изменится l или r. Но последовательные замены термов в step(ft)
- это и есть вычисление sem(ft).
Если такое вычисление завершается и между l и r не остается
функциональных термов, то вычисление sem от исходного выражения будет
нормально продолжено с выражения l.sem(ft).r.
Если же sem(ft) вычислить не удается из-за отсутствия согласования, то
на этом же месте окажется невозможным согласование и для исходного
выражения. Тем самым равенство доказано.
В соотношении (b) зафиксированы следующие свойства МТ-семантики:
1. Результат применения программы к ведущему терму не зависит от его
контекста, а значит, и от истории применения программы к исходному
выражению;
2. "Область изменения" в выражении e до полного вычисления его ведущего
терма ограничена этим термом;
3. Если l и r не содержат функциональных скобок, они никогда не могут
быть изменени.
Аналогичными рассуждениями можно обобщить соотношение (a). Обозначим
через ft1,...,ftn последовательные терминальные функциональные термы в e
(т.е. не содержащие других функциональных термов), а через r0,...,rn -
слова , не содержащие функциональных термов и такие, что
e = r0.ft1.,...,.ftn.rn
Тогда справедливо следующее соотношение:
(c) sem(r0.ft1.,...,.ftn) = sem(r0.sem(ft1).,...,.sem(ftn).rn)
Упражнение. Докажите справедливость этого соотношения.
Не забудьте, что участок r0.sem(ft1).,...,.sem(ftn).rn может содержать
функциональные термы.
Отметим также очевидное соотношение
sem(sem(e)) = sem(e).
Таким образом, обработка в модели МТ обладает четкой иерархической
структурой. Другими словами, выполнение программы p над выражением e можно
представлять себе как "вычисление" этого выражения, начиная с любого из
"терминальных функциональных поддеревьев" соответствующего дерева.
13.3.6. Пример вычисления в модели МТ
Сопоставим вычисление по школьным правилам выражения (10+2)*(3+5) с
обработкой в модели МТ выражения {10+2} {3+5}* по программе перевода в
ПОЛИЗ. Изобразим последовательно получаемые деревья, соответствующие
обрабатываемым выражениям (слева - для школьной арифметики, справа - для
модели МТ).
Шаг 1 (исходные деревья)
* . . *
/ \ / \
/ \ / \
10+2 3+5 {10+2} {3+5}
Деревья явно похожи (вершины изображают операции, дуги - отсылки к тем
операндам, которые еще следует вычислить).
Шаг 2 (применение одной из операций, для которых готовы операнды)
12 * . . . + . *
I / I \
I / I \
3+5 {10} {2} {3+5}
Видно, что дерево справа "отстает" от дерева слева. Сказывается
различие результатов функций step и sem. Последим за правым деревом до
завершения вычисления функции sem({10+2}).
Шаг 2.1
10 . + . *
/ \
{2} {3+5}
Шаг 2.2
10 2 + . *
\
{3+5}
Вот теперь деревья снова похожи!
Слово "вычисление" означает здесь процесс, вполне аналогичный
вычислению значения обычного школьного алгебраического выражения после
подстановки вместо переменных их значений. Однако, аналогия касается не типа
допустимых значений (в школьной алгебре - числа, а здесь - сбалансированные
по скобкам тексты), а способа планирования обработки (способа
программирования).
И в школьной алгебре, и в модели МТ план обработки в определенном
смысле содержится в обрабатываемом (вычисляемом) выражении. Роль исполнителя
состоит в том, чтобы выполнять указанные операции над допустимыми
операндами, подставляя результат операций в обрабатываемое выражение на
место вычисленного терма.
[Существенные отличия состоят в том, что, во-первых, школьные операции
считаются заранее известными, предопределенными, а смысл единственной МТ-
операции step задается полем определений; во-вторых, результат школьных
операций - всегда "окончательный" (новых операций в нем не содержится - это
число), а результат операции step - в общем случае "промежуточный" - им
может оказаться выражение с новыми функциональными термами. Заметим, что
второе отличие исчезает, если от функции step перейти к функции sem - ее
результат всегда "окончательный", ведь (sem(sem(e)) = sem(e)).]
Шаг 3
12*8 10 2 + . . + *
/ \
{3} {5}
Шаг 3.1
10 2 + 3 . + *
\
{5}
Шаг 3.2
10 2 + 3 5 + *
Шаг 4
96 10 2 + 3 5 + *
(нет функциональных термов)
Итак, мы убедились, что МТ-вычисления очень похожи на вычисления
обычных арифметических формул.
Несколько замечаний. Вычисления по формулам очень поучительны для
программистов. Из этого древнейшего способа планирования вычислений можно
извлечь много полезных идей.
Во-первых, это четкая структура вычислений - она, как мы видели,
древовидная.
Во-вторых, операнды рядом с операциями (их не нужно доставать из общей
памяти).
В-третьих, результат не зависит от допустимого изменения порядка
действий (с сохранением иерархии в соответствии с деревом выражения). Отсюда
- путь к параллельному вычислению, если позволяют вычислительные ресурсы
(когда есть несколько процессоров).
В-четвертых, принцип синхронизации таких вычислений прост - всякая
операция должна ждать завершения вычислений своих операндов (ничто другое на
ее выполнение не влияет). На этом принципе основаны так называемые
конвейерные вычисления и вычисления "управляемые потоком данных" (data
flow).
В-пятых, результаты операций никуда не нужно посылать - они нужны там,
где получены.
Наконец, отметим еще одну идею, в последние годы привлекающую внимание
исследователей, стремящихся сделать программирование надежным,
доказательным, систематическим. Речь идет о том, что над школьными формулами
можно выполнять систематические преобразования (упрощать, приводить подобные
члены, явно выражать неизвестные в соотношениях и т.п.). Есть надежда
определить практичную алгебру преобразований и над хорошо организованными
программами. Это позволит систематически выводить программы, проверять их
свойства, оптимизировать и т.п.
Обратите внимание: значение функции sem не зависит от порядка
вычисления терминальных функциональных термов. А в нашем исходном
определении модели МТ требовалось, чтобы всегда выбирался самый левый из
всех таких термов. При отсутствии взаимного влияния непересекающихся термов
это требование несущественно. В реальном Рефале указанное влияние возможно.
13.3.8. Аппликативное программирование
Модель МТ относится к широкому классу аппликативных моделей вычислений.
Это название (от слова apply - применять) связано с тем, что в некотором
смысле единственной операцией в таких моделях оказывается операция
применения функции к ее аргументу, причем единственной формой влияния одного
применения на другое служит связь по результатам (суперпозиция функций). В
частности, функции не имеют побочного эффекта.
[Напомним, что побочным эффектом функции называется ее влияние на
глобальные объекты, не являющиеся аргументами; в модели МТ переменные
локальны в предложениях, а отсутствие побочного эффекта на поле зрения мы
уже обсуждали.]
Аппликативные модели привлекательны тем, что сохраняют многие полезные
свойства вычислений по формулам. Самое важное из них - простая и ясная
структура программы, четко отражающая требования к порядку вычислений и
связям компонент.
Вместе с тем по своей алгоритмической мощности аппликативные модели не
уступают другим моделям вычислений.
Задача. Доказать, что модель МТ алгоритмически полна, т.е. для всякого
нормального алгоритма А найдется эквивалентная ему МТ-программа (допускается
заменять алфавит, в котором работает А).
Однако пока наша модель МТ бедна в том отношении, что ко всем термам
применяется одна и та же функции step. Это плохо и потому, что программу
трудно понимать (особенно, если она длинная) и потому, что она будет
медленно работать, если каждый раз просматривать все предложения поля
определений.
К счастью, модель МТ легко приспособить к более гибкому стилю
аппликативного программирования.
13.3.9. Структуризация поля определений: МТ-функции