Преобразование функции, которая вычисляет фиксированную точку - PullRequest
10 голосов
/ 10 июня 2011

У меня есть функция, которая вычисляет фиксированную точку в терминах итерации:

equivalenceClosure :: (Ord a) => Relation a -> Relation a
equivalenceClosure = fst . List.head                -- "guaranteed" to exist 
                   . List.dropWhile (uncurry (/=))  -- removes pairs that are not equal
                   . U.List.pairwise (,)            -- applies (,) to adjacent list elements
                   . iterate ( reflexivity
                             . symmetry
                             . transitivity
                             )

Обратите внимание, что мы можем абстрагироваться от этого до:

findFixedPoint :: (a -> a) -> a -> a
findFixedPoint f = fst . List.head
                 . List.dropWhile (uncurry (/=))  -- dropWhile we have not reached the fixed point
                 . U.List.pairwise (,)            -- applies (,) to adjacent list elements
                 . iterate
                 $ f

Может ли эта функция быть записана всроки исправления?Кажется, что из этой схемы должно быть что-то с исправлением, но я этого не вижу.

Ответы [ 2 ]

11 голосов
/ 10 июня 2011

Здесь происходит довольно многое, от механики ленивых вычислений до определения фиксированной точки, до метода нахождения фиксированной точки. Короче говоря, я полагаю, что вы, возможно, неправильно меняете применение приложения с фиксированной точкой функции в лямбда-исчислении на ваши потребности.

Может быть полезно отметить, что ваша реализация поиска фиксированной точки (с использованием iterate) требует начального значения для последовательности применения функции. Сравните это с функцией fix, которая не требует такого начального значения (как правило, типы уже выдают это: findFixedPoint имеет тип (a -> a) -> a -> a, тогда как fix имеет тип (a -> a) -> a). По сути, это связано с тем, что две функции делают разные вещи.

Давайте углубимся в это немного глубже. Во-первых, я должен сказать, что вам, возможно, потребуется дать немного больше информации (например, о вашей реализации попарно), но с наивной первой попыткой и моей (возможно, ошибочной) реализацией того, что, как я полагаю, вы хотите получить из попарно Ваша findFixedPoint функция эквивалентна в результате до fix, для только определенного класса функций

Давайте посмотрим на код:

{-# LANGUAGE RankNTypes #-}                                                      

import Control.Monad.Fix                                                                              
import qualified Data.List as List                                                                   

findFixedPoint :: forall a. Eq a => (a -> a) -> a -> a                                                
findFixedPoint f = fst . List.head                                                                    
                 . List.dropWhile (uncurry (/=))  -- dropWhile we have not reached the fixed point    
                 . pairwise (,)                   -- applies (,) to adjacent list elements            
                 . iterate f                                                                          

pairwise :: (a -> a -> b) -> [a] -> [b]                                                             
pairwise f []           = []                                                                        
pairwise f (x:[])       = []                                                                        
pairwise f (x:(xs:xss)) = f x xs:pairwise f xss

противопоставьте это определению fix:

fix :: (a -> a) -> a
fix f = let x = f x in x

и вы заметите, что мы находим совсем другой вид с фиксированной точкой (то есть мы злоупотребляем ленивым вычислением, чтобы сгенерировать фиксированную точку для применения функции в математическом смысле , где мы только останавливаем оценку , если * результирующая функция, примененная к самой себе, вычисляет ту же функцию).

Для иллюстрации давайте определим несколько функций:

lambdaA = const 3
lambdaB = (*)3          

и посмотрим разницу между fix и findFixedPoint:

*Main> fix lambdaA               -- evaluates to const 3 (const 3) = const 3
                                 -- fixed point after one iteration           
3                                  
*Main> findFixedPoint lambdaA 0  -- evaluates to [const 3 0, const 3 (const 3 0), ... thunks]
                                 -- followed by grabbing the head.
3                                  
*Main> fix lambdaB               -- does not stop evaluating      
^CInterrupted.                   
*Main> findFixedPoint lambdaB 0  -- evaluates to [0, 0, ...thunks]
                                 -- followed by grabbing the head
0                            

Теперь, если мы не можем указать начальное значение, для чего используется fix? Оказывается, добавив fix к лямбда-исчислению, мы получаем возможность задавать оценку рекурсивных функций. Рассмотрим fact' = \rec n -> if n == 0 then 1 else n * rec (n-1), мы можем вычислить фиксированную точку fact' как:

*Main> (fix fact') 5
120      

, где при оценке (fix fact') неоднократно применяет сам fact' до тех пор, пока мы не достигнем той же функции , которую мы затем вызываем значением 5. Мы можем видеть это в:

  fix fact'
= fact' (fix fact')
= (\rec n -> if n == 0 then 1 else n * rec (n-1)) (fix fact')
= \n -> if n == 0 then 1 else n * fix fact' (n-1)
= \n -> if n == 0 then 1 else n * fact' (fix fact') (n-1)
= \n -> if n == 0 then 1
        else n * (\rec n' -> if n' == 0 then 1 else n' * rec (n'-1)) (fix fact') (n-1)
= \n -> if n == 0 then 1
        else n * (if n-1 == 0 then 1 else (n-1) * fix fact' (n-2))
= \n -> if n == 0 then 1
        else n * (if n-1 == 0 then 1
                  else (n-1) * (if n-2 == 0 then 1
                                else (n-2) * fix fact' (n-3)))
= ...

Так что же все это значит? в зависимости от функции, с которой вы работаете, вы не обязательно сможете использовать fix для вычисления желаемой фиксированной точки. Насколько мне известно, это зависит от рассматриваемой функции (ей). Не все функции имеют вид фиксированной точки, вычисляемый как fix!

* Я избегал говорить о теории предметной области, так как считаю, что это только запутает и без того тонкую тему. Если вам интересно, fix находит определенный вид фиксированной точки, а именно наименьшую доступную фиксированную точку набора, над которой указана функция.

2 голосов
/ 05 марта 2013

Только для записи, можно определить функцию findFixedPoint, используя fix. Как указал Раиз, рекурсивные функции могут быть определены в терминах fix. Интересующая вас функция может быть рекурсивно определена как:

findFixedPoint :: Eq a => (a -> a) -> a -> a
findFixedPoint f x = 
   case (f x) == x of
       True  -> x
       False -> findFixedPoint f (f x)

Это означает, что мы можем определить его как fix ffp, где ffp:

ffp :: Eq a => ((a -> a) -> a -> a) -> (a -> a) -> a -> a
ffp g f x = 
   case (f x) == x of
       True  -> x
       False -> g f (f x)

Для конкретного примера предположим, что f определяется как

f = drop 1

Легко видеть, что для каждого конечного списка l у нас есть findFixedPoint f l == []. Вот как fix ffp будет работать, когда «аргумент значения» равен []:

(fix ffp) f []
    = { definition of fix }
ffp (fix ffp) f []
    = { f [] = [] and definition of ffp }
[]

С другой стороны, если «аргумент значения» равен [42], мы бы получили:

fix ffp f [42]
    = { definition of fix }
ffp (fix ffp) f [42]
    = { f [42] =/= [42] and definition of ffp }
(fix ffp) f (f [42])
    = { f [42] = [] }
(fix ffp) f []
    = { see above }
[]
...