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