Лекция на тему FALGOL - теоретическая модель языков программирования высокого уровня (Лекция на тему FALGOL – теоретическая модель языков программирования высокого уровня), страница 2
Описание файла
Документ из архива "Лекция на тему FALGOL – теоретическая модель языков программирования высокого уровня", который расположен в категории "". Всё это находится в предмете "параллельные системы и параллельные вычисления" из 9 семестр (1 семестр магистратуры), которые можно найти в файловом архиве НИУ «МЭИ» . Не смотря на прямую связь этого архива с НИУ «МЭИ» , его также можно найти и в других разделах. Архив можно найти в разделе "лекции и семинары", в предмете "параллельные системы и параллельные вычисления" в общих файлах.
Онлайн просмотр документа "Лекция на тему FALGOL - теоретическая модель языков программирования высокого уровня"
Текст 2 страницы из документа "Лекция на тему FALGOL - теоретическая модель языков программирования высокого уровня"
Определение 4.Терм содержательно эквивалентен терму (обозначается ), если .
Определение 5.Терм содержательно не сравним с термом (обозначается ), если
Заметим, что операции конструирования термов являются монотонными относительно отношений содержательного включения и содержательной эквивалентности:
-
Трансформационная семантика.
Трансформационная семантика FALGOLа задается множеством правил редукции и конверсии, сохраняющих содержательную эквивалентность термов. Пусть , обозначают либо вызовы значений переменных, либо процедуры, , , – термы.
Правила редукции-конверсии:
-
; где - «неопределенное» инициальное значение, выполнение терма как программы на FALGOL-машине никогда не завершается;
где – результат подстановки вместо в .
Правила вывода.
-
Язык со статическим связыванием.
Язык Falgol со статическим связыванием переменных фактически представляет собой подмножество термов языка FALGOL, из числа элементов которого исключаются символы связывания переменных, а в качестве новых, вводимых по определению, элементов в языке Falgol используются введенные выше по определению конструкции:
Множество свободно используемых переменных терма определяется теперь непосредственно так:
Аналогично определяется и множество свободных изменяемых переменных терма :
; ; ; ;
Все правила сохраняются в той же формулировке, за исключением правила 6:
Вводятся новые правила:
-
Для всех атомарных констант из расширенного набора ( – арность константы ) полагаем, что и для всех нульарных констант и (то есть все нульарные константы попарно не эквивалентны). Для атомарных констант из расширенного набора могут вводиться произвольные правила следующего вида c различными левыми частями:
где и , и для всех , а – произвольный замкнутый терм ( );
Согласно аксиомам и некоторым выводимым конверсиям, семантически базовой конструкцией следовало бы считать блок с некоторым множеством операторных переменных:
, где , , а при будем считать, что . В этом случае получим:
Введем обобщенный оператор присваивания как частичное отображение множества переменных в множество объектных термов, т.е. в объединение множества вызовов значений переменных и множества термов-процедур. Для изображения обобщенных операторов присваивания будем использовать следующую нотацию: , где .
-
Чисто функциональный язык.
Язык -исчисления (множество -термов) есть подмножество термов языка , построенных без использования символов присваивания, конструкций блоков и рекурсивных процедур. Другими словами,
Практически более удобным является другое определение множества -термов:
Для -исчисления определены правила -редукции, -редукции и -конверсии (здесь и далее , ):
Отношение редукции на множестве -термов определяется как рефлексивное и транзитивное замыкание отношений , и , распространяемое на произвольные контексты -термов:
а отношение конверсии как рефлексивное, транзитивное и симметричное замыкание отношений , и , распространяемое на произвольные контексты -термов, дополненное правилом экстенсиональности (8):
Покажем, например, что имеет место редукция: . Действительно, и .
Отсюда следует доказываемое утверждение. Аналогично можно показать, что имеет место и редукция .
Вторым примером является доказательство конверсии .
Действительно, , и далее искомый результат следует по правилу экстенсиональности.
Третьим примером является доказательство редукции , известной как правило замены операторной переменной:
Доказательство:
Система правил для строгого -исчисления редукций без использования правила экстенсиональности может выглядеть так:
Термы -исчисления строятся по тем же синтаксическим правилам, что и -термы, за исключением константы , которая в -исчислении вводится по определению: . Трансляцию -термов в -исчисление определим так:
а обратную трансляцию -термов в -исчисление так:
-Исчисление использует единственное правило редукции:
Отношения редукции и конверсии на множестве -термов определяются так же, как и на множестве -термов, за исключением правила экстенсиональности, которое выглядит так::
При трансляции -термов в -исчисление правила редукции и становятся в нем выводимыми:
Определим теперь правила трансляции -термов в язык -исчисления следующим образом ( -терм будем называть -образом -терма ):
Очевидно, что . Тогда получим:
Следовательно, имеет место диаграмма . -Правило (правило замены операторной переменной) одинаково имеют место и в -исчислении, и в -исчислении (в нем оно выводимо). Очевидно и то, что если -терм находится в -нормальной форме, то -терм также находится в -нормальной форме. Таким образом, подмножество -образов -термов с правилами и -редукции и -конверсии образуют систему, изоморфную -исчислению, со всеми вытекающими отсюда следствиями.
Если исключить присваивания, блоки и, без потери выразительности, рекурсивные процедуры, то даже без расширенного набора констант (правила 19,20) получим чисто функциональный язык (в [ ] он был назван исчислением функциональных абстракций – ИФА), по своим возможностям очень близкий к -исчислению. Система правил редукции и конверсии для ИФА будет выглядеть так (с рекурсивными процедурами):
или так (без рекурсивных процедур):
Определим правила конвертирования -термов в ИФА:
Для правила -редукции получим диаграмму
15