John Harrison - Введение в функциональное программирование (1108517), страница 32
Текст из файла (страница 32)
е. точность вычислений была бы неменьшей, чем количество выводимых цифр.l e t view x d =l e t n = 4 ∗ d inl e t out = x ( n ) // ( I n t 2 ∗∗/ I n t n ) inapprox_num_fix d out ; ;Начнём с простых примеров, которые работают, как ожидается:#let x = real_of_int 3;;x : int -> num = <fun>#let xi = real_inv x;;xi : int -> num = <fun>#let wun = real_mul x xi;;wun : int -> num = <fun>#view x 20;;it : string = "3.00000000000000000000"#view xi 20;;it : string = ".33333333333333333333"#view wun 20;;it : string = "1.00000000000000000000"Однако, дальнейшее тестирование обнаруживает в нашей реализации серьёзнуютрудноуловимую проблему, которая проявляется с ростом сложности задач.
Этапроблема — многократное вычисление одних и тех же значений. Помимо очевидногослучая — явного наличия общих подвыражений, многократное вычисление одних итех же выражений с различной точностью требуется в алгоритмах умножения и, вособенности, вычисления обратного числа. Количество обращений к одному и томуже подвыражению зависит от глубины его вложенности в исходное выражение иможет расти экспоненциально:1419.3. Точная арифметика вещественных чиселГлава 9. Примеры#let x1 = real_of_int 1 inlet x2 = real_mul x1 x1 inlet x3 = real_mul x2 x2 inlet x4 = real_mul x3 x3 inlet x5 = real_mul x4 x4 inlet x6 = real_mul x5 x5 inlet x7 = real_mul x6 x6 inview x7 10;;- : string = "+1.0000000000"Вычисление этого примера может занять несколько секунд.Для решения проблемы воспользуемся идеей кэширования или функций спамятью (Michie 1968).
Каждой функции поставим в соответствие ячейку памяти,(???ref. cell) в которой будем хранить её значение, вычисленное с наибольшей наданный момент точностью. При очередном обращении к функции с той же самойтребуемой точностью это значение может быть возвращено немедленно, без какихлибо повторных вычислений. Кроме того, менее точная аппроксимация (например,порядка n) всегда может быть получена из более точной (n + k, где k ≥ 1). Если намизвестно, что |fx (n + k) − 2n+k x| < 1, из этого следует:fx (n + k)1+|− 2n x|22k11=+ k |fx (n + k) − 2n+k x|2 211<+ k2 2≤ 1.|fx (n + k) ndiv 2k − 2n x| ≤Таким образом, использование fx (n + k) ndiv 2k в качестве аппроксимации порядка nобосновано.Для реализации функций с памятью воспользуемся обобщённой функцией memo,которую требуется добавить во все определённые ранее операции над вещественнымичислами:142Глава 9. Примеры9.3.
Точная арифметика вещественных чиселl e t r e a l _ o f _ i n t k = memo ( fun n −> ( I n t 2 ∗∗/ I n t n ) ∗/ I n t k ) ; ;l e t r e a l _ n e g f = memo ( fun n −> minus_num ( f n ) ) ; ;l e t r e a l _ a b s f = memo ( fun n −> abs_num ( f n ) ) ; ;l e t real_add f g = memo ( fun n −>( f ( n + 2 ) +/ g ( n + 2 ) ) ndiv ( I n t 4 ) ) ; ;l e t r e a l _ s u b f g = real_add f ( r e a l _ n e g g ) ; ;l e t r e a l _ i n t m u l m x = memo ( fun n −>l e t p = l o g 2 ( abs_num m) inl e t p1 = p + 1 in(m ∗/ x ( n + p1 ) ) ndiv ( I n t 2 ∗∗/ I n t p1 ) ) ; ;l e t r e a l _ i n t d i v m x = memo ( fun n −>x ( n ) ndiv ( I n t m) ) ; ;l e t real_mul x y = memo ( fun n −>l e t n2 = n + 2 inl e t r = n2 / 2 inl e t s = n2 − r inl e t xr = x ( r )and ys = y ( s ) inl e t p = l o g 2 xrand q = l o g 2 ys ini f p = 0 & q = 0 then I n t 0 e l s elet k = q + r + 1and l = p + s + 1and m = p + q + 4 in( x ( k ) ∗/ y ( l ) ) ndiv ( I n t 2 ∗∗/ I n t m) ) ; ;l e t r e a l _ i n v x = memo ( fun n −>l e t x0 = x ( 0 ) inlet k =i f x0 >/ I n t 1 thenl e t r = l o g 2 x0 − 1 inl e t k0 = n + 1 − 2 ∗ r ini f k0 < 0 then 0 e l s e k0elsel e t p = msd x inn + 2 ∗ p + 1 in( I n t 2 ∗∗/ I n t ( n + k ) ) ndiv ( x ( k ) ) ) ; ;l e t r e a l _ d i v x y = real_mul x ( r e a l _ i n v y ) ; ;где1439.4.
Пролог и доказательство теоремГлава 9. Примерыl e t memo f =l e t mem = r e f ( −1 , I n t 0 ) infun n −> l e t (m, r e s ) = !mem ini f n <= m theni f m = n then r e se l s e r e s ndiv ( I n t 2 ∗∗/ I n t (m − n ) )elsel e t r e s = f n inmem := ( n , r e s ) ; r e s ; ;Проведенная оптимизация делает вычисление упомянутого выше произведенияпрактически мгновенным.
Рассмотрим еще несколько примеров:#let pi1 = real_div (real_of_int 22) (real_of_int 7);;pi1 : int -> num = <fun>#view pi1 10;;it : string = "+3.1428571429"#let pi2 = real_div (real_of_int 355) (real_of_int 113);;pi2 : int -> num = <fun>#view pi2 10;;it : string = "+3.1415929204"#let pidiff = real_sub pi1 pi2;;pidiff : int -> num = <fun>#view pidiff 20;;it : string = "+0.00126422250316055626"#let ipidiff = real_inv pidiff;;ipidiff : int -> num = <fun>#view ipidiff 20;;it : string = "+791.00000000000000000000"В заключение отметим, что все расчеты, приведенные в данном разделе,можно, безусловно, проделать и в рациональной арифметике.
Но на деле можетоказаться, что наш подход более эффективен в некоторых ситуациях, так как онизбавляет от свойственного вычислениям в рациональных числах лавинообразногороста числителей и знаменателей, который абсолютно избыточен, когда намнужно лишь приближенное значение результата. Однако, предложенный методраскрывает в полной мере свои достоинства лишь тогда, когда нам потребуетсяввести трансцендентные функции наподобие exp, sin и т. д. Этот вопрос здесьрассматриваться не будет ввиду ограничений на объем курса, но может оказатьсяинтересным в качестве упражнения. Одним из подходов является применениечастичных сумм соответствующих рядов Тейлора.
Отметим, что конечные суммымогут быть вычислены напрямую вместо итеративного применения функциисложения — это существенно улучшает их точность.9.4Пролог и доказательство теоремЯзык Пролог популярен в области исследований по Искусственному Интеллекту,и используется в различных практических приложениях, таких как экспертныесистемы и интеллектуальные базы данных. В этой главе рассматривается какразличные механизмы Пролога, а именно: поиск вглубь с унификацией и возвратом,144Глава 9. Примеры9.4. Пролог и доказательство теореммогут быть реализованы в ML.
Мы не претендуем на полную реализацию Пролога,но результатов этого раздела достаточно, чтобы получить точное представление обосновных достоинствах языка и запустить несколько примеров.9.4.1Термы прологаДанные и код в Прологе представляются с помощью единой системы термовпервого порядка. Мы уже определяли тип термов для математических выражений,их печати, и соответствующих синтаксических анализаторов. Сейчас мы будемиспользовать нечто похожее, но с некоторыми модификациями. Во-первых, немногоупростим код, будем рассматривать константы как нуль-арные функции, т.е.
какфункции, принимающие пустой список аргументов. Соответственно определим:type term = Var of s t r i n g| Fn of s t r i n g ∗ ( term l i s t ) ; ;Там, где раньше использовался Const s, теперь будет Fn(s,[]). Обратитевнимание, функции различной арности (разным числом аргументов)рассматриваются как различные, даже если у них одинаковое имя.
Следовательнонет опасности, что константы будут спутаны с настоящими функциями.9.4.2Лексический анализВ целях следования соглашениям языка, которые включают чувствительностьк регистру, мы обновим функции лексического анализа. Не будем требоватьточного совпадения во всём, но учтём самое главное: символьно-цифровыеидентификаторы, начинающиеся с буквы в верхнем регистре или знакаподчёркивания, рассматриваются как переменные, а другие символьно-цифровыеидентификаторы и числа – как константы. Например, X и Answer – переменные, тогдакак x и john – константы.
Символьные идентификаторы, также как константы неразличаются, в отличии от символов пунктуации: левой и правой скобок, запятойи точки с запятой - их различать будем. Непунктуационные символы собираютсявместе до строки наибольшей возможной длины.type token = V a r i a b l e of s t r i n g| Constant of s t r i n g| Punct of s t r i n g ; ;Лексический анализатор, следовательно, выглядит так:1459.4. Пролог и доказательство теоремГлава 9. Примерыlet lex =l e t s e v e r a l p = many ( some p ) inl e t c o l l e c t ( h , t ) = h^( i t l i s t ( p r e f i x ^) t " " ) inl e t upper_alpha s = "A" <= s & s <= "Z" o r s = "_"and lower_alpha s = "a" <= s & s <= " z " o r "0 " <= s & s <= " 9"and punct s = s = " ( " o r s = " ) " o r s = " [ " o r s = " ] "or s = " , " or s = " .
"and s p a c e s = s = "␣" o r s = " \n" o r s = "\ t " inl e t alp h a n u m e r i c s = upper_alpha s o r lower_alpha s inl e t s y m b o l i c s = not s p a c e s & not a l p h a n u m e r i c s & not punct s inlet rawvariable =some upper_alpha ++ s e v e r a l a l p h a n u m e r i c >> ( V a r i a b l e o c o l l e c t )and r a w c o n s t a n t =( some lower_alpha ++ s e v e r a l a l p h a n u m e r i c | |some s y m b o l i c ++ s e v e r a l s y m b o l i c ) >> ( Constant o c o l l e c t )and rawpunct = some punct >> Punct inl e t token =( r a w v a r i a b l e | | r a w c o n s t a n t | | rawpunct ) ++s e v e r a l s p a c e >> f s t inl e t t o k e n s = ( s e v e r a l s p a c e ++ many token ) >> snd inl e t a l l t o k e n s = ( t o k e n s ++ f i n i s h e d ) >> f s t inf s t o a l l t o k e n s o explode ; ;Например:#lex "add(X,Y,Z) :- X is Y+Z.";;- : token list =[Constant "add"; Punct "("; Variable "X"; Punct ",";Variable "Y"; Punct ","; Variable "Z"; Punct ")";Constant ":-"; Variable "X"; Constant "is"; Variable "Y";Constant "+"; Variable "Z"; Punct "."]9.4.3Синтаксический анализОсновной синтаксический анализатор остаётся в значительной степени такимже, каким был ранее, система печати не меняется.
Единственная модификация –прологовские списки записываются в более удобной нотации. В Прологе «.» и «nil»соответствуют «::» и «[]» в ML. Мы также допускаем прологовскую запись «[H|T]»вместо «cons(H,T)», используемую для сравнения по образцу. После основныхфункций:let variable =fun ( V a r i a b l e s : : r e s t ) −> s , r e s t| _ −> r a i s e Noparse ; ;let constant =fun ( Constant s : : r e s t ) −> s , r e s t| _ −> r a i s e Noparse ; ;146Глава 9.
Примеры9.4. Пролог и доказательство теорему нас есть синтаксический анализатор для термов, а также правил Пролога, имеющихследующий вид:term.term:-term1 , . . . , termn .Собственно анализаторы:l e t rec atom i n p u t= ( c o n s t a n t ++ a ( Punct " ( " ) ++ t e r m l i s t ++ a ( Punct " ) " )>> ( fun ( ( ( name ,_) , a r g s ) ,_) −> Fn ( name , a r g s ) )| | constant>> ( fun s −> Fn ( s , [ ] ) )| | variable>> ( fun s −> Var s )| | a ( Punct " ( " ) ++ term ++ a ( Punct " ) " )>> ( snd o f s t )| | a ( Punct " [ " ) ++ l i s t>> snd ) i n p u tand term i n p u t = p r e c e d e n c e ( ! i n f i x e s ) atom i n p u tand t e r m l i s t i n p u t= ( term ++ a ( Punct " , " ) ++ t e r m l i s t>> ( fun ( ( h ,_) , t ) −> h : : t )| | term>> ( fun h −> [ h ] ) ) i n p u tand l i s t i n p u t= ( term ++ ( a ( Constant " | " ) ++ term ++ a ( Punct " ] " )>> ( snd o f s t )| | a ( Punct " , " ) ++ l i s t>> snd| | a ( Punct " ] " )>> (K ( Fn ( " [ ] " , [ ] ) ) ) )>> ( fun ( h , t ) −> Fn ( " .
![](https://s.studizba.com/z.php?f=/templates/si/i/noavatar.png&w=100&h=100&t=1"){kind=avatar}
