На этом шаге мы введем это понятие.
Иногда мы будем записывать индуктивные определения функций и предикатов на упрощённом языке программирования, который будем называть языком структурированных программ. Каждая структурированная программа предназначена для вычисления значения некоторой функции y = F(x1,..., xn) для заданных значений аргументов x1,...,xn.
Структурированные программы состоят из последовательности определений функций, каждое из которых имеет следующий вид:
F(x1,...,xn) ⇔ <Предикат_1>
THEN <Терм_1>
ELSE IF <Предикат_2>
THEN <Терм_2>
...
ELSE IF <Предикат_m>
THEN <Терм_m>
ELSE OTHERWISE <Терм_ (m+1)>
Для каждой структурированной программы необходимо ещё указать тип функции, т.е. ее область определения и множество значений.
Опишем содержательную операционную семантику структурированной программы.
- Определение.
-
Сначала вычисляется значение предиката <Предиката_1>. Если предикат истинен, то значением функции F является значение терма
<Терм_1>. Если значение предиката ложно, то переходим к рассмотрению предиката <Предикат_2>. Процесс идет таким образом до тех пор,
пока не будет обнаружен первый из предикатов, который истинен.
Если ни один из предикатов не окажется истинным, то значением функции является значение терма <Терм_ (m+1)>.
Введём рекурсию в язык структурированных программ следующим образом: функция F, определяемая в структурированной программе, может входить как часть в любое из выражений (термов) или предикатов в программе. Такое появление F является фактически рекурсивным обращением к этой же функции.
Выполнение программы заключается в её применении к некоторым конкретным данным из области определения.
Пример. Рассмотрим структурированную программу, предназначенную для вычисления значений функции Аккермана с типом A: N×N→N:
A(x1,x2) ⇔ IF x1=0
THEN x2+1
ELSE IF x2=0
THEN A(x1-1,1)
ELSE OTHERWISE A(x1-1, A(x1, x2-1)).
Вычислим значение функции A(1,2), пользуясь описанной содержательной операционной семантикой:
A(1,2) ⇔ A(0, A(1,1)) ⇔ A(0, A(0, A(1,0))) ⇔ A(0, A(0, A(0,1))) ⇔
⇔ A(0, A(0,2)) ⇔ A(0,3) ⇔ 4.
Приведём также индуктивное определение на языке LISP:
(DEFUN Akkerman (LAMBDA (m n)
(COND ( (EQ m 0) (+ n 1) )
( (EQ n 0) (Akkerman (- m 1) 1) )
( T (Akkerman (- m 1) (Akkerman m (- n 1))) ))
))
На следующем шаге мы рассмотрим синтез программ на языке функционального программирования из индуктивных определений.
