Преобразование функции, которая вычисляет неподвижную точку

Ответ 1

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

Может быть полезно отметить, что для вашей реализации поиска неподвижной точки (используя 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

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

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

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 обнаруживает определенный вид фиксированной точки, а именно наименее доступную фиксированную точку poset, указанную функцией.

Ответ 2

Только для записи возможно определить функцию 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 }
[]