John Harrison - Введение в функциональное программирование (1108517), страница 33
Текст из файла (страница 33)
" , [ h ; t ] ) )| | a ( Punct " ] " )>> (K ( Fn ( " [ ] " , [ ] ) ) ) ) i n p u tand r u l e i n p u t= ( term ++ ( a ( Punct " . " )>> (K [ ] )| | a ( Constant ":−" ) ++ term ++many ( a ( Punct " , " ) ++ term >> snd ) ++a ( Punct " .
" )>> ( fun ( ( (_, h ) , t ) ,_) −> h : : t ) ) ) i n p u t ; ;l e t parse_term = f s t o ( term ++ f i n i s h e d >> f s t ) o l e x ; ;l e t p a r s e _ r u l e s = f s t o ( many r u l e ++ f i n i s h e d >> f s t ) o l e x ; ;1479.4. Пролог и доказательство теорем9.4.4Глава 9.
ПримерыУнификацияПролог использует набор правил для разрешения текущей цели. Дляэтого он подбирает правила для цели. Правило, состоящее из одного терма,разрешает цель немедленно, если оно совпадает с целью. В случае правила видаterm :- term1 , . . . , termn . , если цель совпадает с term, то требуется разрешить,как подцель, по порядку каждый termi . Цель является разрешимой, когда этовыполнимо.Однако, цели и правила не обязаны совпадать в точности до терма. В составцели и сопоставляемого правила могут входить переменные, и при сравнениицели с правилом переменные могут присваивать (правильно было бы говоритьсвязывать) соответствующие значения.
Такое сравнение со связыванием называетсяунификацией. Оно означает, что мы можем пренебречь проверкой отдельныхвариантов исходной цели, т.е. ограничиться P (Y ) вместо P (f (X)). Например:• Для унификации f (g(X), Y ) и f (g(a), X) связываются X = a и Y = a. Послеэтого термы будут: f (g(a), a).• Для унификации f (a, X, Y ) и f (X, a, Z) связываются X = a и Y = Z, послечего оба терма примут вид f (a, a, Z).• Недопустимо унифицировать f (X) и X ().В общем случае, унификация неоднозначна. Например, во втором примере можновыбрать связывание Y = f (b) и Z = f (b). Однако, всегда предпочтительнее наиболееобщая унификация, из которой остальные выводятся дальнейшей конкретизацией(сравните с наиболее общими типами в ML).
Для того чтобы найти её, требуетсярекурсивно (и синхронно) обходить вглубь оба терма, и при нахождении переменнойв одном терме, связывать её с соответствующим подтермом другого терма. При этомтакже требуется следить, чтобы уже связанные переменные не унифицировалисьповторно с отличными термами и чтобы не возникало ситуаций, как в последнемпримере, когда переменная, связываемая с термом входит в него же. Простаяреализация этой идеи такова:148Глава 9. Примеры9.4. Пролог и доказательство теоремl e t rec u n i f y tm1 tm2 i n s t s =match tm1 withVar ( x ) −>( t r y l e t tm1 ’ = a s s o c x i n s t s inu n i f y tm1 ’ tm2 i n s t swith Not_found −>augment ( x , tm2 ) i n s t s )| Fn ( f1 , a r g s 1 ) −>match tm2 withVar ( y ) −>( t r y l e t tm2 ’ = a s s o c y i n s t s inu n i f y tm1 tm2 ’ i n s t swith Not_found −>augment ( y , tm1 ) i n s t s )| Fn ( f2 , a r g s 2 ) −>i f f1 = f2then i t l i s t 2 u n i f y a r g s 1 a r g s 2 i n s t se l s e r a i s e ( e r r o r " f u n c t i o n s ␣do␣ not ␣match" ) ; ;Аккумулятор переменных insts должен пополнятся с «проверкой наличия».http://en.wikipedia.org/wiki/Occurs_check А именно, мы должны запретитьсвязывания переменной X с нетривиальным термом, включающем X, как в третьемпримере выше.
Большинство реализаций Пролога игнорируют подобную проверкуили по (заявленным) причинам эффективности, или для поддержки циклическихструктур данных, более сложных чем простые термы первого порядка.1499.4. Пролог и доказательство теоремГлава 9. Примерыl e t rec o c c u r s _ i n x =fun ( Var y ) −> x = y| ( Fn (_, a r g s ) ) −> e x i s t s ( o c c u r s _ i n x ) a r g s ; ;l e t rec s u b s t i n s t s = fun( Var y ) −> ( t r y a s s o c y i n s t s with Not_found −> tm)| ( Fn ( f , a r g s ) ) −> Fn ( f , map ( s u b s t i n s t s ) a r g s ) ; ;l e t raw_augment =l e t augment1 t h e t a ( x , s ) =l e t s ’ = s u b s t t h e t a s ini f o c c u r s _ i n x s & not ( s = Var ( x ) )then r a i s e ( e r r o r " Occurs ␣ check " )e l s e ( x , s ’ ) infun p i n s t s −> p : : ( map ( augment1 [ p ] ) i n s t s ) ; ;l e t augment ( v , t ) i n s t s =l e t t ’ = s u b s t i n s t s t in match t ’ withVar (w) −> i f w <= v theni f w = v then i n s t se l s e raw_augment ( v , t ’ ) i n s t se l s e raw_augment (w, Var ( v ) ) i n s t s| _ −> i f o c c u r s _ i n v t ’then r a i s e ( e r r o r " Occurs ␣ check " )e l s e raw_augment ( v , t ’ ) i n s t s ; ;9.4.5Перебор с возвратамиПролог выполняет поиск в глубину, но он может использовать возврат: допустимправило успешно унифицирует цель, но последующие цели не могут быть разрешеныпри текущих связываниях.
Тогда выполняется возврат, связывание переменныхосвобождается, и с текущей целью сверяется другое правило.150Глава 9. Примеры9.4. Пролог и доказательство теоремl e t rec f i r s t f =fun [ ] −> r a i s e ( e r r o r "No␣ r u l e s ␣ a p p l i c a b l e " )| ( h : : t ) −> t r y f h with e r r o r _ −> f i r s t f t ; ;l e t rec expand n r u l e s i n s t s g o a l s =f i r s t ( fun r u l e −>i f g o a l s = [ ] then i n s t s e l s el e t conc , asms =rename_rule ( s t r i n g _ o f _ i n t n ) r u l e inl e t i n s t s ’ = u n i f y conc ( hd g o a l s ) i n s t s inlet local , g l o b a l = p a r t i t i o n( fun ( v ,_) −> o c c u r s _ i n v conc o re x i s t s ( o c c u r s _ i n v ) asms ) i n s t s ’ inl e t g o a l s ’ = (map ( s u b s t l o c a l ) asms ) @( t l g o a l s ) inexpand ( n + 1 ) r u l e s g l o b a l g o a l s ’ ) r u l e s ; ;Для генерации новых переменных используется функция rename :let rec rename s =fun (Var v) -> Var("~"^v^s)| (Fn(f,args)) -> Fn(f,map (rename s) args);;let rename_rule s (conc,asms) =(rename s conc,map (rename s) asms);;Наконец, соберём всё вместе, в одну функцию prolog, которая пытаетсяразрешить цель, используя заданные правила:type outcome = No | Yes of (string * term) list;;let prolog rules goal =try let insts = expand 0 rules [] [goal] inYes(filter (fun (v,_) -> occurs_in v goal)insts)with error _ -> No;;Результат функции - сообщение о том, что цель или не может быть разрешена,или разрешается с заданными связываниями.
В последнем случае мы возврашаемтолько один ответ (один набор связанных переменных), но можно изменить код так,чтобы выводились все возможные решения.9.4.6ПримерыДавайте испытаем написанный интерпретатор на примерах из какой-нибудькниги по Прологу. Например:1519.4. Пролог и доказательство теоремГлава 9. Примеры#let rules = parse_rules"male(albert).male(edward).female(alice).female(victoria).parents(edward,victoria,albert).parents(alice,victoria,albert).sister_of(X,Y) :female(X),parents(X,M,F),parents(Y,M,F).";;rules : (term * term list) list =[‘male(albert)‘, []; ‘male(edward)‘, [];‘female(alice)‘, []; ‘female(victoria)‘, [];‘parents(edward,victoria,albert)‘, [];‘parents(alice,victoria,albert)‘, [];‘sister_of(X,Y)‘,[‘female(X)‘; ‘parents(X,M,F)‘; ‘parents(Y,M,F)‘]]#prolog rules ("sister_of(alice,edward)");;- : outcome = Yes []#prolog rules (parse_term "sister_of(alice,X)");;- : outcome = Yes ["X", ‘edward‘]#prolog rules (parse_term "sister_of(X,Y)");;- : outcome = Yes ["Y", ‘edward‘; "X", ‘alice‘]Поскольку Пролог является скорее реляционным чем функциональным языком,можно использовать запросы в более гибкой форме, например спрашивать при какихаргументах можно получать заданный результат:#let r = parse_rules"append([],L,L).append([H|T],L,[H|A]) :- append(T,L,A).";;r : (term * term list) list =[‘append([],L,L)‘, [];‘append(H .
T,L,H . A)‘, [‘append(T,L,A)‘]]#prolog r (parse_term "append([1,2],[3],[1,2,3])");;- : outcome = Yes []#prolog r (parse_term "append([1,2],[3,4],X)");;- : outcome = Yes ["X", ‘1 . (2 . (3 . (4 . [])))‘]#prolog r (parse_term "append([3,4],X,X)");;- : outcome = No#prolog r (parse_term "append([1,2],X,Y)");;- : outcome = Yes ["Y", ‘1 . (2 . X)‘]В таких случаях Пролог представляется в значительной степениинтеллектуальным.
Но за этой наружностью стоит простой поиск, а значит«интеллектуальность» хрупка. Например, следующий код зацикливается:#prolog r (parse_term "append(X,[3,4],X)");;9.4.7Доказательство теоремПролог действует как простой доказыватель теорем, используя базу логическихфактов (правил) для доказательства цели. Однако он весьма ограничен в152Глава 9. Примеры9.4. Пролог и доказательство теоремдоказательных возможностях, частично из-за неполноты стратегии поиска в глубину,частично потому что он может выполнять логические выводы только определённоговида. Вообще, можно реализовать более мощную пролого-подобную систему: Stickel(1988).
Далее мы покажем, как в сущности на тех же идеях (унификация и возврат)строится более функциональный доказыватель теорем.Унификация является эффективным способом ограничения переменных снавешенным квантором общности. Например, имея правила ∀X. p(X) ⇒ q(X) иp(f (a)), можно унифицировать оба выражения, включающие p и тем самым связатьX с f (a). Напротив, самые ранние системы доказательства теорем пытались строитьвсевозможные термы из доступных констант и функций («Эрбрановского базиса»).Обычно поиск вглубь может привести к бесконечному зацикливанию, такчто мы должны незначительно изменить стратегию поиска. Будем использоватьпоиск вглубь с итеративным погружением.
Это значит, что поиск вглубьимеет фиксировнный предел, по достижению которого выполняется возврат. Еслидоказательство не найдено при заданной глубине, её значение увеличивается иделается ещё один поиск. Таким образом, сначала ищутся доказательства глубины 1,в случае провала - глубины 2, 3 и так далее. В качестве предельной глубины могутиспользоваться различные параметры, например, высота или размер дерева поиска;мы будем использовать число унифицируемых переменных.Манипулирование формуламиДля обозначения формул будем использовать термы первого порядка.
Добавимтакже новые константы для логических операторов, некоторые из которых инфиксные.Оператор~(p)p&qp|qp --> qp <-> qforall(X,p)exists(X,p)Значениене ppиqp или qp влечёт q (импликация)p только и если только q (эквивалентность)для всех X, p (квантор общности)существует X такой что p (квантор существования)Альтернативный подход заключается в добавлении отдельного типа для формул,но тогда потребуется добавить код и для синтаксического разбора, и печати.
![](https://s.studizba.com/z.php?f=/templates/si/i/noavatar.png&w=100&h=100&t=1"){kind=avatar}
