На этом шаге мы рассмотрим взаимосвязь языков программирования LISP и PROLOG.
Функциональные определения легко переводятся в реляционные обозначения, если использовать [см.1, с.147]:
- эквивалентность
где F - предикатный символ, соответствующий функциональному символу f, и
f(x) <--> F(x y), (E1)
- свойства отношения равенства
Здесь P(t) представляет любое выражение, содержащее терм t. Символ "<-->" (читается "тогда и только тогда") выражает эквивалентность. Для-всех и Существует - это соответственно квантор всеобщности и квантор существования.
P(f(x)) <--> Для-всех y [ P(y) если f(x)=y ] (E2) P(f(x)) <--> Существует y [ P(y) и f(x)=y ] (E3)
Приведем ряд примеров перевода программ, написанных на языке LISP в программы на языке Prolog.
Пример 1. Перед Вами - программа на языке LISP, осуществляющая копирование списка целых чисел LST:
(DEFUN COPY (LAMBDA (LST)
(COND ( (NULL LST) NIL )
( T (CONS (CAR LST) (COPY (CDR LST))) ))))
Используем "более эквациональные" обозначения:
COPY (NIL) = NIL COPY (LST) = (CONS CAR (LST) COPY (CDR (LST)))
А теперь применим "TURBO-прологовские" обозначения:
COPY (NIL) = NIL COPY ([X|Y]) = [X | COPY (Y)]
Применяя (E1-E3) к определениям COPY, последовательно получаем:
COPY (NIL) = NIL <--> copy ([],[]). COPY ([X|Y]) = [X | COPY (Y)] <--> copy ([X|Y],[X|COPY (Y)] <--> copy ([X|Y],[X|Z]), если Z = COPY (Y) <--> copy ([X|Y],[X|Z]), если copy (Y,Z) <--> copy ([X|Y],[X|Z]) :- copy (Y,Z).
Каждый шаг перевода состоит в применении эквивалентности для замены подвыражения на эквивалентное подвыражение.
И наконец, меняем имена:
copy_list ([],[]).
copy_list ([Head|Tail],[Head|Tail1]) :-
copy_list (Tail,Tail1).
Пример 2. Перед Вами - программа на языке LISP, вычисляющая количество элементов в целочисленном списке LST:
(DEFUN LENGTH (LAMBDA (LST)
(COND ( (NULL LST) 0 )
( T (+ 1 (LENGTH (CDR LST))) ))))
Используем "более эквациональные" обозначения:
LENGTH (NIL) = 0 LENGTH (LST) = 1 + LENGTH (CDR LST)
А теперь применим "TURBO-прологовские" обозначения:
LENGTH (NIL) = 0 LENGTH ([X|Y]) = 1 + LENGTH (Y)
Применяя (E1-E3) к определениям COPY, последовательно получаем:
LENGTH (NIL) = 0 <--> length ([],0). LENGTH ([X|Y]) = 1 + LENGTH (Y) <--> length ([X|Y],1+LENGTH (Y)) <--> length ([X|Y],Z), если (U=LENGTH (Y))&(Z=1+U) <--> length ([X|Y],Z), если (length (Y,U))&(Z=1+U) <--> length ([X|Y],Z):- length (Y,U), Z = 1 + U.
Каждый шаг перевода состоит в применении эквивалентности для замены подвыражения на эквивалентное подвыражение.
И наконец, меняем имена:
sum_list ([],0). sum_list ([H|T],Sum) :- sum_list (T,Sum1), Sum = 1 + Sum1.
Пример 3. Перед Вами - программа на языке LISP, определяющая N-й элемент целочисленного списка:
(DEFUN NTH (LAMBDA (N LST)
(COND ( (> N (LENGTH LST)) 100 )
( (OR (< N 0) (ZEROP N)) -100 )
( (EQ N 1) (CAR LST) )
( T (NTH (- N 1) (CDR LST)) ))))
Используем "более эквациональные" обозначения:
NTH (N,LST) = 100, если N > LENGTH (LST) NTH (N,LST) = -100, если N <=0 NTH (1,LST) = CAR (LST) NTH (N,LST) = NTH (N-1,CDR(LST))
А теперь применим "TURBO-прологовские" обозначения:
NTH (N,LST) = 100, если N > LENGTH (LST) NTH (N,LST) = -100, если N <=0 NTH (1,[X|Y]) = X NTH (N,[X|Y]) = NTH (N-1,Y)
Применяя (E1-E3) к определениям COPY, последовательно получаем:
NTH (N,LST) = 100, если N > LENGTH (LST) <--> nth (N,LST,100), если (Z=LENGTH (LST)) & (N>Z) <--> nth (N,LST,100), если (length (LST,Z)) & (N>Z) <--> nth (N,LST,100) :- length (LST,Z), N>Z. NTH (N,LST) = -100, если N <=0 <--> nth (N,LST,-100), если N <=0 <--> nth (N,LST,-100) :- N <=0. NTH (1,[X|Y]) = X <--> nth (1,[X|Y],X). NTH (N,[X|Y]) = NTH (N-1,Y) <--> nth (N,[X|Y],Z), если NTH (N-1,Y))=Z <--> nth (N,[X|Y],Z), если (U=N-1) & (nth (N-1,Y,Z)) <--> nth (N,[X|Y],Z) :- U=N-1, nth (U,Y,Z).
Каждый шаг перевода состоит в применении эквивалентности для замены подвыражения на эквивалентное подвыражение.
И наконец, меняем имена:
find_n (N,LST,100):- sum_list (LST,V),N>V.
find_n (N,LST,-100):- N<=0.
find_n (1,[Head|_],Head).
find_n (Middle,[_|Tail],Z) :-
Middle1 = Middle - 1,
find_n (Middle1,Tail,Z).
Пример 4. Перед Вами - программа на языке LISP, удаляющая элемент X из целочисленного списка LST:
(DEFUN DELETE (LAMBDA (X LST)
(COND ( (NULL LST) NIL )
( (EQ (CAR LST) X) (DELETE X (CDR LST)) )
( T (CONS (CAR LST) (DELETE X (CDR LST))) ))))
Используем "более эквациональные" обозначения:
DELETE (NIL) = NIL DELETE (CAR(LST),LST) = DELETE (X,CDR(LST)) DELETE (X,LST) = CONS (CAR(LST),DELETE (X,CDR(LST)))
А теперь применим "TURBO-прологовские" обозначения:
DELETE (NIL) = NIL DELETE (X,[X|Y]) = DELETE (X,Y) DELETE (X,[Z|T]) = Z | DELETE (X,T)
Применяя (E1-E3) к определениям COPY, последовательно получаем:
DELETE (NIL) = NIL <--> delete ([],[]). DELETE (X,[X|Y]) = DELETE (X,Y) <--> delete (X,[X|Y],Z), если DELETE (X,Y)=Z <--> delete (X,[X|Y],Z), если delete (X,Y,Z) <--> delete (X,[X|Y],Z) :- delete (X,Y,Z). DELETE (X,[Z|T]) = Z | DELETE (X,T) <--> delete (X,[Z|T],[Z|V]), если DELETE (X,T) = V <--> delete (X,[Z|T],[Z|V]), если delete (X,T,V) <--> delete (X,[Z|T],[Z|V]) :- delete (X,T,V).
Каждый шаг перевода состоит в применении эквивалентности для замены подвыражения на эквивалентное подвыражение.
И наконец, меняем имена:
delete (_,[],[]).
delete (X,[X|Tail],List) :-
delete (X,Tail,List).
delete (X,[Z|Tail],[Z|V]):-
delete (X,Tail,V).
Программа на языке Prolog (TURBO Prolog , версия 2.0).
domains number = integer list = integer * predicates read_list (list) write_list (list) copy_list (list,list) sum_list (list,number) find_n (number,list,number) append (list,list,list) reverse (list,list) trance (list,list,list) delete (number,list,list) listmax (list,number) greater (number,number,number) goal write ("Вводите элементы списка... "), read_list (Lst), nl, write ("Результат ввода... "), write_list (Lst), nl, /* ------------------------------------------- */ write ("Копия списка... "), copy_list (Lst,Lst1), write_list (Lst1), nl, /* -------------------------------------- */ write ("Количество элементов в списке... "), sum_list (Lst,X1), write (X1), nl, /* ---------------------------------------------- */ write ("Отыщем в списке элемент с данным номеpом."), write ("Вводите номеp: "), readint (N), find_n (N,Lst1,T), write (T), nl, /* ---------------------------------------- */ write ("Склеим два списка... "), append (Lst,Lst1,Lst2), write_list (Lst2), nl, /* ---------------------------------------- */ write ("Обpатим заданный список."), write ("Вводите элементы списка... "), read_list (Lst3), nl, reverse (Lst3,Lst4), write_list (Lst4), nl, /* --------------------------------------- */ write ("Удалим из списка заданный элемент."), write ("Вводите элемент... "), readint (U), delete (U,Lst4,Lst5), write_list (Lst5), nl, write ("Найдем в числовом списке наибольший элемент. "), listmax (Lst5,A), write (A), nl. clauses /* ------------------------------------ */ /* Ввод списка целых чисел с клавиатуpы */ /* ------------------------------------ */ read_list ([H|T]):- readint (H), !, read_list (T). read_list ([]). /* ----------------------------------------- */ /* Вывод списка целых чисел на экpан дисплея */ /* ----------------------------------------- */ write_list ([]). write_list ([Head|Tail]) :- write (Head), write (" "), write_list (Tail). /* ------------------------------ */ /* Копиpование списка целых чисел */ /* ------------------------------ */ copy_list ([],[]). copy_list ([Head|Tail],[Head|Tail1]) :- copy_list (Tail,Tail1). /* (DEFUN COPY (LAMBDA (LST) */ /* (COND ( (NULL LST) NIL ) */ /* ( T (CONS (CAR LST) (COPY (CDR LST))) ) */ /* ) */ /* )) */ /* ---------------------------------- */ /* Опpеделение количества элементов в */ /* списке целых чисел */ /* ---------------------------------- */ sum_list ([],0). sum_list ([_|T],Sum) :- sum_list (T,Sum1), Sum = 1 + Sum1. /* (DEFUN LENGTH (LAMBDA (LST) */ /* (COND ( (NULL LST) 0 ) */ /* ( T (+ 1 (LENGTH (CDR LST))) )))) */ /* -------------------------------------- */ /* Hахождение элемента списка с номеpом N */ /* -------------------------------------- */ find_n (N,LST,100):- sum_list (LST,V),N>V. find_n (N,_,-100):- N<=0. find_n (1,[Head|_],Head). find_n (Middle,[_|Tail],Z) :- Middle1 = Middle - 1, find_n (Middle1,Tail,Z). /* (DEFUN NTH (LAMBDA (N LST) */ /* (COND ( (> N (LENGTH LST)) 100 ) */ /* ( (OR (< N 0) (ZEROP N)) -100 ) */ /* ( (EQ N 1) (CAR LST) ) */ /* ( T (NTH (- N 1) */ /* (CDR LST)) )))) */ /* ------------------------- */ /* "Склеивание" двух списков */ /* ------------------------- */ append ([],L,L). append ([N|L1],L2,[N|L3]) :- append (L1,L2,L3). /* ------------------------------------- */ /* Удаление из списка заданного элемента */ /* ------------------------------------- */ delete (_,[],[]). delete (X,[X|Tail],List) :- delete (X,Tail,List). delete (X,[Z|Tail],[Z|V]):- delete (X,Tail,V). /* (DEFUN DELETE (LAMBDA (X LST) */ /* (COND ( (NULL LST) NIL ) */ /* ( (EQ (CAR LST) X) */ /* (DELETE X (CDR LST)) ) */ /* ( T (CONS (CAR LST) */ /* (DELETE X (CDR LST))) )))) */ /* --------------------------- */ /* "Инверсия" элементов списка */ /* --------------------------- */ reverse (L,Z) :- trance (L,[],Z). trance ([],Result,Result). trance ([X|Y],Result,Z) :- trance (Y,[X|Result],Z). /* -------------------------------------------- */ /* Поиск наибольшего элемента в числовом списке */ /* -------------------------------------------- */ listmax ([X|[]],X). listmax ([X|Y],Z) :- listmax (Y,V), greater (X,V,Z). greater (X,Y,X) :- X>Y. greater (X,Y,Y) :- X<=Y. /* Конец пpогpаммы */
Замечания.
- Несмотря на то, что функциональные обозначения более привычны пользователю, чем реляционные, вычисления посредством
переписывающих правил менее универсальны, чем обратные рассуждения.
Например, в то время как функциональная программа может использоваться только для определения длины списка, реляционная программа обратима, и к ней можно обращаться с запросами, как к базе данных.
- Этот метод перевода дает простое доказательство того, что
хорновские дизъюнкты могут быть использованы для представления всех вычислимых функций (впервые это было доказано
Р.Хиллом (ссылку см. в [1, с.147]).
Набросок доказательства: С помощью проиллюстрированного выше метода перевода любую систему уравнений Эрбрана-Гёделя (представляющую вычислимую функцию) можно перевести в эквивалентное множество хорновских дизъюнктов. Более того, эффект использования уравнения как переписывающего правила для замены термов, которые совмещаются с левыми частями уравнений, на правые части этих уравнений можно промоделировать, используя соответствующие дизъюнкты в обратном направлении - для сведения проблем к подпроблемам. Такое моделирование ставит в соответствие любому вычислению посредством уравнений структурно схожее с ним вычисление на хорновских дизъюнктах, приводящее к тому же результату. Это показывает, что логические программы на хорновских дизъюнктах вычисляют все функции, которые вычислимы посредством уравнений Эрбрана-Геделя, что и требовалось доказать.
(1) Формальная логика. - Л.: Изд-во ЛГУ, 1977. - 358 с.
На следующем шаге мы рассмотри элементы вычислительной теории чисел.
