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

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

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

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

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