Примеры редукций

Определение 4: Конечная последовательность или свертываний называется «редукцией». Один шаг или свертывания обозначается стрелкой без индекса, просто «».

Замечание 5: Использование констант и правил излишне, так как константы можно реализовать только атомарными термами в виде переменных (т. е., «чистое исчисление» —

исчисление без констант и правил).

Примеры редукций (используемые редексы подчеркнуты):

1.

2.

(31) Нормальные формы выражений

Определение: Если для выражения нельзя применить никакого правила редукции, т. е. выражение не содержит редексов и находится в «нормальной форме».

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

While—(существует хотя бы один редекс) – do – (преобразовывать один из редексов) – end – (выражение теперь в нормальной форме).

Замечание 2: свертывания не всегда могут давать желаемый результат – может происходить зацикливание.

ПРИМЕР:

а)

б)

ПОРЯДОК РЕДУКЦИЙ (стратегия выбора редексов)

1.  АППЛИКАТИВНЫЙ порядок редукции (АПР): вначале преобразовывается самый левый из самых внутренних редексов, не содержащих других редексов:

такой порядок редукции в данном примере привел к зацикливанию.

2.  НОРМАЛЬНЫЙ порядок редукции (НПР): вначале преобразовывается самый левый из самых внешних редексов, которые не содержатся в других редексах:

такой порядок редукции в данном примере привел за один шаг к окончанию вычислений.

ЗАМЕЧАНИЕ: Функция в случае НПР отбрасывает свой аргумент .

ВЫВОДЫ:

1.  НПР в таких случаях эффективно откладывает вычисление любых редексов внутри выражения аргумента до тех пор, пока это возможно: «не делай ничего, пока это не потребуется». Это пример «ленивых вычислений» — стратегия НПР, которая встречается в некоторых функциональных языках, например, в алгоритмическом языке Clean.

2.  Стратегия АПР соответствует “энергичным вычислениям» -«делай все, что можешь». Эта стратегия применяется в языке ЛИСП, которая может приводить иногда к зацикливанию.

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

Теорема «стандартизации»: Если выражение имеет нормальную форму (НФ), то НПР гарантирует достижение этой НФ (с точностью до замены связанных переменных).

(32)Рекурсивные функции

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

а) — сложение всех целых чисел:

– если , то , иначе складываем (+) число с суммой для числа, меньшего на 1, чем , т. е. (1–) обозначает уменьшение на 1. Это была форма записи рекурсивной функции на языке Гильберта-Клини, а в форме абстракции: Осталось связать переменную со значением функции , чтобы сделать функцию анонимной. Это можно сделать с помощью специальной функции «комбинатор»:

.

Например, функция «» имеет бесконечное число «неподвижных» точек. Таким образом, в исчислении функция записывается так:

Проверим, например, должно быть равно 1.:

Определим «комбинатор» как