Transforming a function that computes a fixed point

Question

I have a function which computes a fixed point in terms of 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
                             )

Notice that we can abstract from this to:

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

Can this function be written in terms of fix? It seems like there should be a transformation from this scheme to something with fix in it, but I don't see it.

Audriaaudrie

Answer 1

There's quite a bit going on here, from the mechanics of lazy evaluation, to the definition of a fixed point to the method of finding a fixed point. In short, I believe you may be incorrectly interchanging the fixed point of function application in the lambda calculus with your needs.

It may be helpful to note that your implementation of finding the fixed-point (utilizing iterate) requires a starting value for the sequence of function application. Contrast this to the fix function, which requires no such starting value (As a heads up, the types give this away already: findFixedPoint is of type (a -> a) -> a -> a, whereas fix has type (a -> a) -> a). This is inherently because the two functions do subtly different things.

Let's dig into this a little deeper. First, I should say that you may need to give a little bit more information (your implementation of pairwise, for example), but with a naive first-try, and my (possibly flawed) implementation of what I believe you want out of pairwise, your findFixedPoint function is equivalent in result to fix, for a certain class of functions only

Let's take a look at some 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

contrast this to the definition of fix:

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

and you'll notice that we're finding a very different kind of fixed-point (i.e. we abuse lazy evaluation to generate a fixed point for function application in the mathematical sense, where we only stop evaluation iff* the resulting function, applied to itself, evaluates to the same function).

For illustration, let's define a few functions:

lambdaA = const 3
lambdaB = (*)3          

and let's see the difference between fix and 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                            

now if we can't specify the starting value, what is fix used for? It turns out that by adding fix to the lambda calculus, we gain the ability to specify the evaluation of recursive functions. Consider fact' = \rec n -> if n == 0 then 1 else n * rec (n-1), we can compute the fixed point of fact' as:

*Main> (fix fact') 5
120      

where in evaluating (fix fact') repeatedly applies fact' itself until we reach the same function, which we then call with the value 5. We can see this in:

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

So what does all this mean? depending on the function you're dealing with, you won't necessarily be able to use fix to compute the kind of fixed point you want. This is, to my knowledge, dependent on the function(s) in question. Not all functions have the kind of fixed point computed by fix!

*I've avoided talking about domain theory, as I believe it would only confuse an already subtle topic. If you're curious, fix finds a certain kind of fixed point, namely the least available fixed point of the poset the function is specified over.

Wigwam

Just noticed that there's an excellent high-level overview of the use of fix here #4787921 that you may find useful. – Wigwam

So, in summary, the difference between the kind of fixed point operator I wanted and "fix" is the order of operations? – Audriaaudrie

Sorry, meant to edit my previous comment, but ran out of time: So, in summary, the difference between the kind of fixed point operator I wanted and "fix" is the order of operations? How can Haskell even compare functions by "equality", when such an operation is known to be undecidable? And how can we develop a fixed point operator that accepts an approximate solution, as in Brouwer's fixed point theorem for contraction mappings? – Audriaaudrie

Answer 2

Just for the record, it is possible to define the function findFixedPoint using fix. As Raeez has pointed out, recursive functions can be defined in terms of fix. The function that you are interested in can be recursively defined as:

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

This means that we can define it as fix ffp where ffp is:

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)

For a concrete example, let us assume that f is defined as

f = drop 1

It is easy to see that for every finite list l we have findFixedPoint f l == []. Here is how fix ffp would work when the "value argument" is []:

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

On the other hand, if the "value argument" is [42], we would have:

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

Phylloid