Ответ 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, указанную функцией.