Просмтор этого файла доступен только зарегистрированным пользователям. Но у нас супер быстрая регистрация: достаточно только электронной почты!

Текст из файла (страница 2)

Определение 4.Терм содержательно эквивалентен терму (обозначается ), если .

Определение 5.Терм содержательно не сравним с термом (обозначается ), если

.

Заметим, что операции конструирования термов являются монотонными относительно отношений содержательного включения и содержательной эквивалентности:

и

.

1. Трансформационная семантика.

Трансформационная семантика FALGOLа задается множеством правил редукции и конверсии, сохраняющих содержательную эквивалентность термов. Пусть , обозначают либо вызовы значений переменных, либо процедуры, , , – термы.

Правила редукции-конверсии:

1. ;

2. ;

3.  ;

4. ;

5.  ;

6. , где ;

7.   ;

8. , где ;

9. ;

1. ;

2. , где , если  ;

3. ;

4. , где , если  ;

5.    ;

6.    ;

7. ; где - «неопределенное» инициальное значение, выполнение терма как программы на FALGOL-машине никогда не завершается;

8. Сборка «мусора». Пусть   . Тогда



 ,

где – результат подстановки вместо в .

Правила вывода.

П1.  .

П2.  для всех .

1. Язык со статическим связыванием.

Язык Falgol со статическим связыванием переменных фактически представляет собой подмножество термов языка FALGOL, из числа элементов которого исключаются символы связывания переменных, а в качестве новых, вводимых по определению, элементов в языке Falgol используются введенные выше по определению конструкции:

• – «распроцедуривание»;

• – «блок» с блочной переменной и «телом» ;

• – «функция» с параметром и «телом» ;

• – «рекурсивная процедура» с переменной рекурсии и «телом» ;

• – «неопределенное» инициальное значение .

Множество свободно используемых переменных терма определяется теперь непосредственно так:

  ;      ;    ;

    ;         .

Аналогично определяется и множество свободных изменяемых переменных терма :

  ;      ;    ;   ;

  ;     ;      .

Все правила сохраняются в той же формулировке, за исключением правила 6:

1. .

Вводятся новые правила:

1. Для всех атомарных констант из расширенного набора ( – арность константы ) полагаем, что   и для всех нульарных констант и (то есть все нульарные константы попарно не эквивалентны). Для атомарных констант из расширенного набора могут вводиться произвольные правила следующего вида c различными левыми частями:

,

где и , и для всех , а – произвольный замкнутый терм ( );

1. для всех и ;

2. для всех и .

Согласно аксиомам и некоторым выводимым конверсиям, семантически базовой конструкцией следовало бы считать блок с некоторым множеством операторных переменных:

, где , , а при будем считать, что . В этом случае получим:

.

Введем обобщенный оператор присваивания как частичное отображение множества переменных в множество объектных термов, т.е. в объединение множества вызовов значений переменных и множества термов-процедур. Для изображения обобщенных операторов присваивания будем использовать следующую нотацию: , где .

1. Чисто функциональный язык.

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

1. пустая строка есть -терм,

2. если – -терм, то , (для всех ) – -термы,

3. если и – -термы, а , то и – -термы,

4. других -термов, не определенных п.п. 1-3, нет.

Практически более удобным является другое определение множества -термов:

1. пустая строка есть -терм,

2. и (для всех ) – -термы,

3. если – -терм, а , то и – -термы,

4. если и – -термы, то – -терм,

1. других -термов, не определенных п.п. 1-4, нет.

Для -исчисления определены правила -редукции, -редукции и -конверсии (здесь и далее , ):

1. ,

2. ,

3. .

Отношение редукции на множестве -термов определяется как рефлексивное и транзитивное замыкание отношений , и , распространяемое на произвольные контексты -термов:

1. ,

2. ,

3. ,

4. ,

5. ,

6. ,

а отношение конверсии как рефлексивное, транзитивное и симметричное замыкание отношений , и , распространяемое на произвольные контексты -термов, дополненное правилом экстенсиональности (8):

1. ,

2. ,

3. ,

4. ,

5. ,

6. ,

7. ,

8. .

Покажем, например, что имеет место редукция:  . Действительно,  и .

Отсюда следует доказываемое утверждение. Аналогично можно показать, что имеет место и редукция  .

Вторым примером является доказательство конверсии .

Действительно, , и далее искомый результат следует по правилу экстенсиональности.

Третьим примером является доказательство редукции  , известной как правило замены операторной переменной:

Доказательство:

 .

Система правил для строгого -исчисления редукций без использования правила экстенсиональности может выглядеть так:

1. ,

2. ,

3. ,

4.  ,

5. .

Термы -исчисления строятся по тем же синтаксическим правилам, что и -термы, за исключением константы , которая в -исчислении вводится по определению: . Трансляцию -термов в -исчисление определим так:

,

,

,

а обратную трансляцию -термов в -исчисление так:

,

,

.

-Исчисление использует единственное правило редукции:

.

Отношения редукции и конверсии на множестве -термов определяются так же, как и на множестве -термов, за исключением правила экстенсиональности, которое выглядит так::

1. .

При трансляции -термов в -исчисление правила редукции и становятся в нем выводимыми:

,

.

Определим теперь правила трансляции -термов в язык -исчисления следующим образом ( -терм будем называть -образом -терма ):

,

,

.

Очевидно, что . Тогда получим:

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

Если исключить присваивания, блоки и, без потери выразительности, рекурсивные процедуры, то даже без расширенного набора констант (правила 19,20) получим чисто функциональный язык (в [ ] он был назван исчислением функциональных абстракций – ИФА), по своим возможностям очень близкий к -исчислению. Система правил редукции и конверсии для ИФА будет выглядеть так (с рекурсивными процедурами):

1.   [ ] ;

2. ;

3. ;

4. ;

5.   ;

6. ;

7.  

или так (без рекурсивных процедур):

1.   [ ] ;

3. ;

5.   ;

6. .

Определим правила конвертирования -термов в ИФА:

• ;

• ;

• .

Для правила -редукции получим диаграмму

15

Характеристики

Список файлов лекций