Transformar una función que calcula un punto fijo

Question

Tengo una función que calcula un punto fijo en términos de iterado:

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
                             )

Observe que podemos abstraer de esto a:

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

¿Se puede escribir esta función en términos de solución? Parece que debería haber una transformación de este esquema a algo con la solución, pero no lo veo.

Answer 1

Aquí está sucediendo un poco, desde la mecánica de la evaluación perezosa, hasta la definición de un punto fijo hasta el método de encontrar un punto fijo. En resumen, creo que puede estar intercambiando incorrectamente el Aplicación del punto de la función fijo en el cálculo Lambda con tus necesidades.

Puede ser útil tener en cuenta que su implementación de encontrar el punto fijo (utilizando iterate) requiere un valor inicial para la secuencia de la aplicación de función. Contrasta esto con el fix función, que no requiere tal valor inicial (como un avance, los tipos ya lo regalan: findFixedPoint es de tipo (a -> a) -> a -> a, mientras fix tiene tipo (a -> a) -> a). Esto es inherentemente porque las dos funciones hacen cosas sutilmente diferentes.

Vamos a profundizar en esto un poco más profundo. Primero, debo decir que es posible que deba dar un poco más de información (su implementación de pares, por ejemplo), pero con un ingenuo que se introduzca, y mi implementación (posiblemente defectuosa) de lo que creo que desea fuera de pares , su findFixedPoint la función es equivalente en resultado a fix, para cierta clase de funciones solamente

Echemos un vistazo a algún código:

{-# 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

contrasta esto con la definición de fix:

fix :: (a -> a) -> a
fix f = let x = f x in x

y notarás que estamos encontrando un tipo muy diferente de punto fijo (es decir, abusamos de la evaluación perezosa para generar un punto fijo para la aplicación de función en el sentido matemático, donde solo dejamos de evaluación IFF* La función resultante, aplicada a sí misma, se evalúa a la misma función).

Para la ilustración, definamos algunas funciones:

lambdaA = const 3
lambdaB = (*)3          

y veamos la diferencia entre fix y 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                            

Ahora, si no podemos especificar el valor inicial, ¿qué es fix ¿usado para? Resulta que agregando fix Para el cálculo de Lambda, obtenemos la capacidad de especificar la evaluación de funciones recursivas. Considerar fact' = \rec n -> if n == 0 then 1 else n * rec (n-1), podemos calcular el punto fijo de fact' como:

*Main> (fix fact') 5
120      

Donde evaluar (fix fact') se aplica repetidamente fact' en sí hasta que llegamos al mismo función, que luego llamamos con el valor 5. Podemos ver esto en:

  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)))
= ...

Entonces, ¿qué significa todo esto? Dependiendo de la función con la que está tratando, no necesariamente podrá usar fix Para calcular el tipo de punto fijo que desee. Esto es, que yo sepa, depende de las funciones en cuestión. No todas las funciones tienen el tipo de punto fijo calculado por fix!

*He evitado hablar sobre la teoría del dominio, ya que creo que solo confundiría un tema ya sutil. Si tienes curiosidad fix encuentra un cierto tipo de punto fijo, a saber, el punto fijo menos disponible del POSET se especifica la función.

Answer 2

Solo para que conste, es posible Para definir la función findFixedPoint usando fix. Como Raeez ha señalado, las funciones recursivas se pueden definir en términos de fix. La función que le interesa se puede definir recursivamente como:

findFixedPoint :: Eq a => (a -> a) -> a -> a
findFixedPoint f x = 
   case (f x) == x of
       True  -> x
       False -> findFixedPoint f (f x)

Esto significa que podemos definirlo como fix ffp dónde ffp es:

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)

Para un ejemplo concreto, supongamos que f Se define como

f = drop 1

Es fácil ver eso para cada lista finita l tenemos findFixedPoint f l == []. Aquí es cómo fix ffp funcionaría cuando el "argumento de valor" sea []:

(fix ffp) f []
    = { definition of fix }
ffp (fix ffp) f []
    = { f [] = [] and definition of ffp }
[]

Por otro lado, si el "argumento de valor" es [42], tendríamos:

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