Конспект установочных лекций по комплексному курсу Информатика, Теория информации
Рекурсивные объявления функций в системах подстановки термов
Пусть снова дано рекурсивное объявление функции let
f == (m х) n: Е.
Для выражения, которое использует f, применяется следующее правило замены термов: f(El)-^((mx)n:E)(El), т. е. для вычисления идентификатор f заменяется на правую часть рекурсивно описанной функции. Тем самых! рекурсивное объявление функции соответствует дальнейшему правилу подстановки термов, которое присоединяется к наличным правилам.
Пример (редукция для рекурсивно описанных функций). Для рекурсивного определения fct fac = (nat x) nat:
if x=0 then 1
else x * fac(x - 1) fi
возникает вычисление (пусть 2 стоит вместо succ(succ(zero))):
fас(2)
((nat x) nat: if... fi) (2)
if 2 = 0 then 1 else 2 * fac(2 - 1) fi
То, что с помощью этих правил замены действительно вычисляется значение, которое специфицируется и функциональной семантике (толкование неподвижной точки), может быть показано на основании свойств индуктивного толкования.
