Математическая логика и теория алгоритмов

упростить. Такая часть выражения называется р е д е к с о м , а операция упрощения называется редукцией. Процесс редукции завершается, когда выражение, преобразо­ ванное редукцией, не содержит больше редекса. Выражение, не со­ держащее редекса, называется нормальнойформой. Например, при оценке выражения (+(/62)(х25)) сначала выби­ раются редексы и упрощаются соответственно до 3 и 10. Полученное выражение (+3 10) также является редуцируемым, поэтому имеем (+3 10)~>13. Результат (оценка выражения) 13 невозможно упростить, поэтому он считается нормальной формой. Применение функции. Применение функции / к аргументу х обозначается как ( f x ) . Функция от нескольких аргументов представля­ ется, например, следующим образом { f { x , y , z ) ) . Однако функцию от не­ скольких аргументов можно интерпретировать как результат синтеза функций от одного аргумента. Например (+3 4) можно интерпрети­ ровать как (+3)4, т.е. как прибавление тройки к аргументу 4. Л а м б д а - а б с т р а щ и я - это одно выражение, определяющее функцию. Например, выражение (Ал.+л:!) определяет функцию прибавления единицы к переменной х . Запись Ах. показывает, что это выражение является ламбда-абстракцией, ф о р м а л ь н ы м пара етром которой является х. Выражение, которое следует за точкой (в данном случае это +л:1), является телом ламбда- абстракции. Рассмотрим следующее ламбда-выражение; (Хл:.+лу)3. Здесь X считается связанной переменной, 3— значением для х. Для оценки этого выражения необходимо, чтобы переменная у уже имела какое-либо значение. Обычно значение свободной пере­ менной определяется во внешнем выражении, содержащем это выра­ жение. 261