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

Question

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

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

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

Answer 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

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

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

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

Answer 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 }
[]