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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

Свойства:

Int(p,a) = p(a)

p(a) = Obρ(a)

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

Pa(b) = p(a,b)

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

 

1) Intp(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) = Intp(x) = Obρ(x) #

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

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

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

ЛИТЕРАТУРА

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