Logo Questions Linux Laravel Mysql Ubuntu Git Menu
 

Transforming a function that computes a fixed point

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.

like image 317
nomen Avatar asked Jun 09 '11 22:06

nomen


People also ask

How do you find the fixed points of a function?

The point p is a fixed point of the function g(x) if g(p) = p. The point p is a root of the function f(x) if f(x) = 0. f(x) has a root at p iff g(x) = x - f(x) has a fixed point at p. g(x) has a fixed point at p iff f(x) = x - g(x) has a root at p.

What are fixed points in a transformation?

fixed-point theorem, any of various theorems in mathematics dealing with a transformation of the points of a set into points of the same set where it can be proved that at least one point remains fixed.

What is fixed point in functional analysis?

In mathematics, a fixed-point theorem is a result saying that a function F will have at least one fixed point (a point x for which F(x) = x), under some conditions on F that can be stated in general terms. Some authors claim that results of this kind are amongst the most generally useful in mathematics.

How do you find the fixed point of a differential equation?

Fixed Points for Differential EquationsA point X is fixed if it does not change. A point X is fixed if its derivative is zero: dX dt = 0.


2 Answers

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.

like image 88
Raeez Avatar answered Sep 25 '22 00:09

Raeez


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 }
[]
like image 37
Joao F. Ferreira Avatar answered Sep 26 '22 00:09

Joao F. Ferreira