Конспект установочных лекций по комплексному курсу Информатика, Теория информации



Рекурсивные объявления функций в системах подстановки термов


Пусть снова дано рекурсивное объявление функции 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

 ...

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




Содержание  Назад  Вперед