Процедура смешанных вычислений

Поиск универсальных методов – одна из главных парадигм современной науки. Но более эффективны специализированные методы. Между универсальными и специальными методами существует глубинная связь.

Поскольку ЭВМ - детерминированный автомат, то при фиксированной программе ρ для любого входного данного x выходное значение z будет некоторой функцией φ, полностью определяемой программой ρ φ(x) = z.

Сама программа ρ вместе с ее данными х выполняется посредством интерпретации Int (алгоритм Int встроен в конструкцию ЭВМ).

Int(ρ,x) = φ(x) =z.

Частная задача (более специализированная) возникает тогда, когда мы обладаем некоторой дополнительной априорной информацией относительно исходных данных. Рассматривая задачу от многих аргументов, мы можем сказать, что часть аргументов фиксирована.

Пусть φ = φ(х,y) и x = a - фиксировано;

Тогда φ(а,у) = π(у): Int(π,b) = φ(a,b).

Смешанные вычисления предполагают универсальную процедуру нахождения программы π как функции исходной общей программы; значений ее связанных входных переменных и указанных свободных переменных.

Определение:

Результат смешанных вычислений называется остаточной программой.

Если все входные переменные связаны, то остаточная программа выродится в выдачу результата; если все входные переменные оставить свободными, то остаточная программа совпадет с исходной.

Пример.

[λxy. +xy]

 Пусть x=1

[λy. +1y] – специальная программа, прибавляющая к числу 1

х = 1

у = 1

 

Специальная программа будет выдавать результат.

а¹⁶=(((а²) ²) ²)² - т.е. вместо 16 умножений будем иметь только 4 умножения.

Обычные и смешанные вычисления связаны друг с другом. Обычные вычисления –процедура Int, которая для любой программы ρ и заданных значений всех ее входных переменных вычисляет значение функции φ, реализуемой программой.

Определение:

Смешанные вычисления - универсальная процедура Mix, которая для любой программы, заданных значений ее связанных переменных и указанных свободных входных переменных вычисляет остаточную программу.

Int(p;a,b) = φ(a,b)

Mix(p,a,b) = out(с), где с = φ(a,b)

Mix(p,0,{x,y}) = p

Mix(p,a,y) = pa, где Int(pa,b) = φ(a,b).

Традиционно способ описания работы программы заключается в систематическом чтении программного текста и выделении последовательности базисных команд, которые выполняют фактическую обработку информации.

Эта последовательность базисных команд называется протоколом вычисления.

Протокол по своей записи сам является выполняемой программой и может применяться к некоторому разнообразию входных данных; при этом условные выражения должны заменяться на предикаты (которые должны принять истинное значение).

λх.if x=0 ERR 3/x _{↓предикат}

Протокол: (zerop x) ERR

                   Not (zerop x) 3/x

 

Определения:

Предикат - функция одного аргумента, принимающая значение истина или ложь.

Протокол, порождаемый какими-либо данными, противоречит любым данным, порождающим некоторый другой протокол.

Выполнение программы можно рассматривать как двухэтапный процесс декомпозиции.

1) Извлечение базисных команд, образующих протокол;

2) Выполнение базисных команд, образующих протокол (т.е. прямые вычисления).

Множество протоколов возникает из-за разных выборов альтернатив при проверке условий. Это множество протоколов называется детерминантом программы.

Выполнение программы - передача ее входных данных всем протоколам детерминанта. (Все протоколы противоречивы – функция невычислима, результат неизвестен; существует несколько непротиворечивых протоколов – функция многозначна; существует единственный непротиворечивый протокол – он выдает результат выполнения программы).

Протокол - линейная запись команд; при выполнении очередной команды она редуцируется (убирается).

Предположим, у нас определены некоторые входные переменные, часть протоколов отсечется из-за противоречивости; в оставшихся - часть команд редуцируется. Если получить программный текст, детерминант которого совпадает с оставшимся детерминантом, то, фактически, мы получим остаточную программу. Основное препятствие реализации метода - то, что не каждый детерминант соответствует какой-то программе, для этого он должен принадлежать классу автоматных множеств. Поэтому надо организовать процесс частичной редукции так, чтобы в любой момент находиться в пределах некоторого программного текста, который и будет считаться результатом специализации универсальной программы.

Определим частичные вычисления:

 1) выполним программу для не полностью заданных значений переменных;

 2) будем печатать те команды, которые нельзя выполнить из-за отсутствия информации (в том числе нередуцируемые альтернативы и присваивания, нераскрытые итерации). Последовательность невыполненных команд образует остаточную программу.

Детерминант остаточной программы - некоторое непротиворечивое расширение редукции детерминанта исходной программы.

Вычисления смешанные потому, что чередуются шаги обычных вычислений и формирования остаточных программ.

 

Трансформационные семантики

В операционных семантиках обычные и смешанные вычисления существенно отличаются (хотя и обладают сходной функцией). Это противоречие устраняет трансформационный подход.

Идея трансформационного подхода:

Рассматривается программа, и ищутся команды, которые могут быть выполнены в данный момент. Выполненные команды редуцируются, т.е. убираются из программы.

Из-за итераций не все команды могут быть удалены после первого выполнения. Поэтому в правила преобразования программного текста включаются также “раскрытия”, которые отщепляют от итерации один экземпляр (для редукции).

Команды итерации хранятся в виде особого объекта-замыкания, где они либо представлены явно, либо в виде ссылки на соответствующую подпрограмму - шаг итерации (соответственно рекурсия без памяти - среда хранится явно и - с памятью).

Трансформационная семантика не показывает, какая команда должна выполняться, лишь показывает список команд, которые могут быть выполнены.

Определение:

Неподвижная точка - это состояние программы, при котором не может быть выполнена ни одна команда.  

Если заданы все аргументы правильно составленной программы и выполнены все команды, то неподвижная точка есть результат (его выдача).

Если же заданы не все аргументы, то неподвижная точка - остаточная программа.

Определение:

Система преобразований любой текстовой информации, которая приводит к одной и той же неподвижной точке независимо от порядка применения допустимых преобразований называется системой Черча - Россера.

Трансформационные семантики опираются на ряд правил преобразования текста программ, которые могут быть легко расширены.

При построении трансляторов:

Проекция смешанного вычислителя на интерпретатор входного языка – это программа транслятора с этого языка на машинный. Таким образом, по теореме Успенского (следствие из проекций Футамуры), для того, чтобы на данный машинный язык можно было перевести любой другой язык программирования, необходимо и достаточно, чтобы в машинном языке были определены смешанные вычисления.

Tran(ρ,a) - транслятор с входного языка.

Ob_ρ(x) - объектная программа, перевод ρ в машинный язык.

Свойства:

Int(p,a) = p(a)

p(a) = Ob_ρ(a)

Tran(p,x) = Ob_ρ(x)

P_a(b) = p(a,b)

Mix(p,a,y) = P_a(y)

 

Проекции Футамуры

1) Int_p(x) = Ob_ρ(x)

2) Mix Int(p,x) = Tran(p,x)

# 1. Ob_ρ(a) = Int(p,a) = p(a)

2. Tran(p,x) = Mix(Int,p,x) = Int_p(x) = Ob_ρ(x) #

Смешанные вычисления хорошо соответствуют λ-исчислению, каррируется каждый аргумент, его подстановка ведет к преобразованию тела λ-абстракции, т.е. получению остаточной программы.

Контрольные вопросы

1. Дайте определения протокола вычислений и остаточной программы.
2. Для чего необходим механизм смешанных вычислений?
3. Укажите область применения трансформационных семантик.
4. Укажите связь между теоремой Черча – Россера и системами Черча – Россера.
5. Выпишите проекции Футамуры и докажите их.

ЛИТЕРАТУРА

1. Бердж В. Методы рекурсивного программирования.
2. Вольфенгаген В.Э. Категориальная абстрактная машина. М.:МИФИ, 1993
3. Вольфенгаген В.Э. Комбинаторная логика в программировании. Вычисления с объектами в примерах и задачах. М.:МИФИ, 1994
4. Вольфенгаген В.Э., Горюнова И.А., Косиков С.В. Методы и средства построения систем знания. М.:МИФИ, 1992 (ч. 1, ч. 2)
5. Ершов А.П. Смешанные вычмсления. «В мире науки» №6, М.:Мир, 1984.
6. Косиков С.В., Мясников А.В. Математические методы и средства в новой информационной технологии. М.:МИФИ, 1990
7. Методические указания к проведению практических занятий по курсу "Дискретная математика". Специальные главы дискретной математики. (Составители: Вольфенгаген В.Э., Чепурнова И.В., Гаврилов А.В.) М.:МИФИ, 1990)