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

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

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

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

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

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

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

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

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

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

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

5. других -термов, не определенных п.п. 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. .

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

,

,

,

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

,

,

.

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

.

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

8. .

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

,

.

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

,

,

.

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

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

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

1. [];

2. ;

3. ;

4. ;

5. ;

6. ;

7. 

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

1. [];

2. 

3. ;

4. 

5. ;

6. .

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

• ;

• ;

• .

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

16