John Harrison - Введение в функциональное программирование (1108517), страница 34
Текст из файла (страница 34)
Изсоображений простоты ограничимся первым решением.Предварительная обработка формулОчевидно, программа упростится, если основная часть доказывателя не будетработать с импликациями и эквивалентностями. Следовательно, сначала определимфункцию, заменяющую их комбинацией других операторов.1539.4. Пролог и доказательство теоремГлава 9.
Примерыl e t rec p r o c tm =match tm withFn ( "~" , [ t ] ) −> Fn ( "~" , [ p r o c t ] )| Fn ( "&" , [ t 1 ; t 2 ] ) −> Fn ( "&" , [ p r o c t 1 ; p r o c t 2 ] )| Fn ( " | " , [ t 1 ; t 2 ] ) −> Fn ( " | " , [ p r o c t 1 ; p r o c t 2 ] )| Fn ( "−−>" , [ t 1 ; t 2 ] ) −>p r o c ( Fn ( " | " , [ Fn ( "~" , [ t 1 ] ) ; t 2 ] ) )| Fn ( "<−>" , [ t 1 ; t 2 ] ) −>p r o c ( Fn ( "&" , [ Fn ( "−−>" , [ t 1 ; t 2 ] ) ;Fn ( "−−>" , [ t 2 ; t 1 ] ) ] ) )| Fn ( " f o r a l l " , [ x ; t ] ) −> Fn ( " f o r a l l " , [ x ; p r o c t ] )| Fn ( " e x i s t s " , [ x ; t ] ) −> Fn ( " e x i s t s " , [ x ; p r o c t ] )| t −> t ; ;Определим две взаимно рекурсивные функции, которые по формуле и еёотрицанию строят «негативно нормальную форму» - формулу из элементарныхтермов и их отрицаний, связанных с помощью операторов «И», «ИЛИ» и кванторов.l e t rec nnf_p tm =match tm withFn ( "~" , [ t ] ) −> nnf_n t| Fn ( "&" , [ t 1 ; t 2 ] ) −> Fn ( "&" , [ nnf_p t 1 ; nnf_p t 2 ] )| Fn ( " | " , [ t 1 ; t 2 ] ) −> Fn ( " | " , [ nnf_p t 1 ; nnf_p t 2 ] )| Fn ( " f o r a l l " , [ x ; t ] ) −> Fn ( " f o r a l l " , [ x ; nnf_p t ] )| Fn ( " e x i s t s " , [ x ; t ] ) −> Fn ( " e x i s t s " , [ x ; nnf_p t ] )| t −> tand nnf_n tm =match tm withFn ( "~" , [ t ] )| Fn ( "&" , [ t 1 ;| Fn ( " | " , [ t 1 ;| Fn ( " f o r a l l "| Fn ( " e x i s t s "| t −> Fn ( "~"−> nnf_p tt 2 ] ) −> Fn ( " | " , [ nnf_n t 1 ; nnf_n t 2 ] )t 2 ] ) −> Fn ( "&" , [ nnf_n t 1 ; nnf_n t 2 ] ), [ x ; t ] ) −> Fn ( " e x i s t s " , [ x ; nnf_n t ] ), [ x ; t ] ) −> Fn ( " f o r a l l " , [ x ; nnf_n t ] ),[ t ] ) ; ;Идея такова: отрицание доказываемой формулы конвертируется в негативнонормальную формулу, с которой главный доказыватель попытается получитьпротиворечие.
Этого противоречия будет достаточно для доказательства исходнойформулы.Главный доказывательНа каждом этапе доказыватель имеет текущую формулу, список формул, которыеещё предстоит рассмотреть и список литералов. Он пытается получить противоречие.Используется следующая стратегия:• Если текущая формула – p & q, то p и q рассматриваются по отдельности, т.е pделается текущей формулой, а q добавляется к формулам «на рассмотрение».154Глава 9. Примеры9.4. Пролог и доказательство теорем• Если текущая формула имеет вид p | q, то делается попытка получитьпротиворечие сначала с p, а затем с q.• Если текущая формула- forall(X, p), для замещения X вводитсяновая переменная, правильное значение может быть получено позже, приунификации.• Если текущая формулаконстанта.- exists(X,p), для замещения X вводится новая• В противном случае, формула должна быть литералом, так что делаетсяпопытка унифицировать его противоречивым литералом.• Если унификация не удалась, литерал добавляется в список литералов, адоказыватель переходит к обработке следующей формулы.Нам необходима стратегия возврата, похожая на прологовскую: толькоесли текущие связывания позволяют разрешить все оставшиеся цели, мыдопускаем их.
Можно было бы снова использовать списки, но давайте попробуемпродолжения(continuations). Продолжение - это функция, передающаяся другойфункции, которая может вызываться из последней «для выполнения остаточныхвычислений». В нашем случае она принимает список с переменными и пытаетсяразрешить оставшиеся цели при заданных связываниях. Следовательно вместопопыток явно разрешить оставшиеся цели, мы просто вызываем функциюпродолжение.l e t rec prove fm unexp p l n l n c o n t i =i f n < 0 then r a i s e ( e r r o r "No␣ p r o o f " ) e l s ematch fm withFn ( "&" , [ p ; q ] ) −>prove p ( q : : unexp ) p l n l n c o n t i| Fn ( " | " , [ p ; q ] ) −>prove p unexp p l n l n( prove q unexp p l n l n c o n t ) i| Fn ( " f o r a l l " , [ Var x ; p ] ) −>l e t v = mkvar ( ) inprove ( s u b s t [ x , Var v ] p ) ( unexp@ [ fm ] ) p l n l ( n − 1 ) c o n t i| Fn ( " e x i s t s " , [ Var x ; p ] ) −>l e t v = mkvar ( ) inprove ( s u b s t [ x , Fn ( v , [ ] ) ] p ) unexp p l n l ( n − 1 ) c o n t i| Fn ( "~" , [ t ] ) −>( t r y f i r s t ( fun t ’ −> l e t i ’ = u n i f y t t ’ i incont i ’ ) plwith e r r o r _ −>prove ( hd unexp ) ( t l unexp ) p l ( t : : n l ) n c o n t i )| t −>( t r y f i r s t ( fun t ’ −> l e t i ’ = u n i f y t t ’ i incont i ’ ) nlwith e r r o r _ −>prove ( hd unexp ) ( t l unexp ) ( t : : p l ) n l n c o n t i ) ; ;1559.4.
Пролог и доказательство теоремГлава 9. ПримерыИ, наконец, доказыватель:let prover =l e t rec p r o v e _ i t e r n t =t r y l e t i n s t s = prove t [ ] [ ] [ ] n I [ ] inlet globinsts = f i l t e r( fun ( v ,_) −> o c c u r s _ i n v t ) i n s t s inn, globinstswith e r r o r _ −> p r o v e _ i t e r ( n + 1 ) t infun t −> p r o v e _ i t e r 0 ( nnf_n ( p r o c ( parse_term t ) ) ) ; ;Так реализуется стратегия итеративного погружения.
Доказыватель пытаетсянайти доказательство с наименее общими связываниями переменных; если этоудаётся, он возвращает их число и сами значения переменных.ПримерыВот несколько простых примеров, взятых из Pelletier (1986).#let P1 = prover "p --> q <-> ~(q) --> ~(p)";;P1 : int * (string * term) list = 0, []#let P13 = prover "p | q & r <-> (p | q) & (p | r)";;P13 : int * (string * term) list = 0, []#let P16 = prover "(p --> q) | (q --> p)";;P16 : int * (string * term) list = 0, []#let P18 = prover "exists(Y,forall(X,p(Y)-->p(X)))";;P18 : int * (string * term) list = 2, []#let P19 = prover "exists(X,forall(Y,forall(Z,(p(Y)-->q(Z))-->p(X)-->q(X))))";;P19 : int * (string * term) list = 6, []Пример побольше:#let P55 = prover"lives(agatha) & lives(butler) & lives(charles) &(killed(agatha,agatha) | killed(butler,agatha) |killed(charles,agatha)) &(forall(X,forall(Y,killed(X,Y) --> hates(X,Y) & ~(richer(X,Y))))) &(forall(X,hates(agatha,X)--> ~(hates(charles,X)))) &(hates(agatha,agatha) & hates(agatha,charles)) &(forall(X,lives(X) & ~(richer(X,agatha))--> hates(butler,X))) &(forall(X,hates(agatha,X) --> hates(butler,X))) &(forall(X,~(hates(X,agatha)) | ~(hates(X,butler))| ~(hates(X,charles))))--> killed(agatha,agatha)";;P55 : int * (string * term) list = 6, []Фактически доказыватель может работать детективом:156Глава 9.
Примеры9.4. Пролог и доказательство теорем#let P55’ = prover"lives(agatha) & lives(butler) & lives(charles) &(killed(agatha,agatha) | killed(butler,agatha) |killed(charles,agatha)) &(forall(X,forall(Y,killed(X,Y) --> hates(X,Y) & ~(richer(X,Y))))) &(forall(X,hates(agatha,X)--> ~(hates(charles,X)))) &(hates(agatha,agatha) & hates(agatha,charles)) &(forall(X,lives(X) & ~(richer(X,agatha))--> hates(butler,X))) &(forall(X,hates(agatha,X) --> hates(butler,X))) &(forall(X,~(hates(X,agatha)) | ~(hates(X,butler))| ~(hates(X,charles))))--> killed(X,agatha)";;P55’ : int * (string * term) list = 6, ["X", ‘agatha‘]Дальнейшее чтениеСимвольное дифференцирование- классическое приложение дляфункциональных языков.
Другие символьные операции также используются –Davenport, Siret, and Tournier (1988) содержит обзор того, что могут делать системыкомпьютерной алгебры и как они работают. В Paulson (1983) обсуждается стратегияупрощения, использованная нами в более общих условиях.Синтаксический анализ с помощью функций высшего порядка - другойпопулярный пример. Похоже он давно уже вошёл в в фольклор функциональногопрограммирования; первоначально он был рассмотрен в Burge (1975).
Наши примерыосновываются на Paulson (1991) и Reade (1989).Первое определение «вычислимого вещественного числа» было дано в Turing(1936). Его подход основывался на десятичных расширениях, но позже потребовалисьизменения –(Turing 1937), по причинам, рассматриваемым далее в упражнениях.Подход к вещественной арифметике, осуществлённый нами, основывается на работеBoehm, Cartwright, O’Donnel, and Riggle (1986).
Недавняя более эффективнаяреализация на CAML Light была описана в Ménissier-Morain (1994). Эта статья (нафранцузском) содержит подробное доказательство корректности всех алгоритмовдля элементарных трансцендентных функций. Альтернативное решение использует«дробно-линейные преобразования», см. Potts (1996).Наш подход к прологовскому поиску и возврату, основанный на использованиисписков и продолжений, достаточно стандартен. За подробностями о реализацииПролога обращайтесь, например, к Boizumault (1993), с подробностями о текущемиспользовании языка стоит ознакомиться по Clocksin and Mellish (1987).
Детальноеобсуждение продолжений, во многих их проявлениях, даётся в Reynolds (1993).Алгоритм унификации, расммотренный в курсе прост и достаточно функционален,но не блещет эффективностью. За информацией о более быстрых императивныхалгоритмах обращайтесь к Martelli and Montanari (1982). Наш доказыватель теоремосновывается на leanTAP (Beckert and Posegga 1995). О другом важном методедоказывания теорем, для удобства основывающемся на прологовском стиле поиска,можно прочитать в (Stickel 1988).1579.4.
Пролог и доказательство теоремГлава 9. ПримерыУпражнения1. Модифицируйте систему печати так, чтобы она учитывала ассоциативностьоператоров и не печатала избыточных скобок.2. Правила дифференцирования для 1/g(x) и f (x)/g(x) не корректны, когдаg(x) = 0. В действительности большинство коммерческих систем компьютернойалгебры игнорирует это факт.
Напишите новую версию differentiate, котораявозвращает не только производную, но также и список условий, которыедолжны удовлетворяться, чтобы производная считалась корректной.3. Запрограммируйте простую процедуру интегрирования. Достаточнореализовать основные правила интегрирования, хотя это не позволит взятьлюбой интеграл. 64. Прочитайте документацию на библиотеку format, и попробуйте реализоватьформатированную печать многострочного вывода.5. Что случится, если функции синтаксического анализатора - term, atom ипрочие будут η-редуцированы удалением слова input? Что случится, еслиprecedence будет последовательно η-редуцироваться с помощью удаленияinput?6. На сколько хорошо анализатор с приоритетами, сгенерированный функциейprecedence, обрабатывает различные операторы с одинаковым приоритетом?Как можно улучшить его работу? Можете ли вы усовершенствовать его так,чтобы запись допускала смешение лево- и правоассоциативных операторов?7.
Перепишите анализатор так, чтобы при ошибках разбора он возвращалинформативные сообщения.Представьте вещественное число с помощью функции, генерирующей первые8. (*) ???TODO спросить у мамы )9. Реализуйте мультиразрядную цклочисленную арифметику. Постройтеалгоритм произведения, выполняющийся за O(nlog2 3 ) (??? времени памяти????),где n – общее число цифр в аргументах.10. (*) Extend the real arithmetic routines для функций типа exp и sin.11. Наша предподготовка и приведение к негативной нормальной форме могутвыполняться за время экспоненциальное от длины ввода, если ввод содержитмножество вхождений операторов эквивалентности.
![](https://s.studizba.com/z.php?f=/templates/si/i/noavatar.png&w=100&h=100&t=1"){kind=avatar}
