La transformation d'une fonction qui calcule un point fixe

Question

I ai une fonction qui calcule un point fixe en termes de iterate:

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
                             )

Notez que nous pouvons faire abstraction de cela:

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

Cette fonction peut être écrit en termes de solution? Il semble qu'il devrait y avoir une transformation de ce régime à quelque chose avec fix, mais je ne vois pas.

Answer 1

Il y a un peu qui se passe ici, de la mécanique de l'évaluation paresseuse, à la définition d'un point fixe à la méthode de trouver un point fixe. Bref, je crois que vous pouvez interchanger à tort point fixe d'application de fonction dans le calcul lambda avec vos besoins.

Il peut être utile de noter que l'implémentation de trouver le point fixe (en utilisant de iterate) nécessite une valeur de départ de la séquence d'application de la fonction. Cela contraste à la fonction fix, qui ne nécessite pas une telle valeur de départ (en heads-up, les types donnent à cette distance déjà: findFixedPoint est de type (a -> a) -> a -> a, alors que fix est de type (a -> a) -> a). Ceci est en soi parce que les deux fonctions font des choses subtilement différentes.

La fouille Let dans ce un peu plus profond. Tout d'abord, je dois dire que vous devrez peut-être donner un peu plus d'informations (votre implémentation de pairwise, par exemple), mais avec un premier essai naïf, et mon (peut-être biaisées) la mise en œuvre de ce que je crois que vous voulez de pairwise , votre fonction findFixedPoint est équivalent dans résultat à fix, pour un certaine classe de fonctions uniquement

Jetons un coup d'oeil à un code:

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

contraste ce à la définition de fix:

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

et vous remarquerez que nous constatons un genre très différent de point fixe ( dire que nous abusons évaluation paresseuse pour générer un point fixe pour l'application de la fonction dans la section sens mathématique, où l'on ne l'évaluation arrêt ssi * la fonction résultante, appliquée à lui-même, à evalue la même fonction).

Pour illustration, nous allons définir quelques fonctions:

lambdaA = const 3
lambdaB = (*)3          

et nous allons voir la différence entre fix et 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                            

maintenant, si nous ne pouvons pas spécifier la valeur de départ, ce qui est fix utilisé? Il se trouve qu'en ajoutant fix au calcul lambda, nous gagnons la possibilité de spécifier l'évaluation des fonctions récursives. Considérez fact' = \rec n -> if n == 0 then 1 else n * rec (n-1), on peut calculer le point fixe de fact' comme:

*Main> (fix fact') 5
120      

où l'évaluation (fix fact') applique de façon répétée fact' elle-même jusqu'à ce que nous arrivons à la même fonction , que nous appelons alors la valeur 5. Nous pouvons le voir dans:

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

Alors qu'est-ce que tout cela signifie? en fonction de la fonction que vous avez affaire, vous ne serez pas nécessairement en mesure d'utiliser fix pour calculer le type de point fixe que vous voulez. Ceci est, à ma connaissance, en fonction de la fonction (s) en question. Toutes les fonctions ont le genre de point fixe calculé par fix!

* Je l'ai évité de parler de la théorie de domaine, comme je crois qu'il ne confondez pas un sujet déjà subtile. Si vous êtes curieux, fix trouve un certains type de point fixe, à savoir le point le moins du poset fixe disponible la fonction est spécifiée sur.

Answer 2

Pour la petite histoire, il est possible pour définir la fonction findFixedPoint à l'aide fix. Comme Raeez l'a souligné, les fonctions récursives peuvent être définies en termes de fix. La fonction qui vous intéresse peut être défini récursivement comme:

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

Cela signifie que nous pouvons définir comme fix ffp où ffp est:

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)

Pour un exemple concret, supposons que f est défini comme

f = drop 1

Il est facile de voir que pour chaque liste finie l nous avons findFixedPoint f l == []. Voici comment fix ffp fonctionnerait lorsque le « argument de valeur » est []:

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

D'autre part, si l ' "argument de valeur" est [42], nous aurions:

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