SOE ex.9.9


{-
    when first time I see this exercise, it remind me the:
    x = x + 1
      = (x + 1) + 1
      = ((x + 1) + 1) + 1
        ...

    Here, we have:
    fix f = f (fix f)
          = f (f (fix f))
          = f (f (f (fix f)))
          = ...
    f must be a function.
    f (...) => assume argument is a type "a".
    f (f (...)) => return of f(...) will match the argument type.
    => so, f must be type (a -> a).
       and fix f = output of f(.....)
    => so,
           fix f :: (a -> a) -> a
-}

fix :: (a -> a) -> a
fix f = f (fix f)

remainder :: Integer -> Integer -> Integer
remainder a b = if a < b then a else remainder (a-b) b

{-
    Rewrite remainder using fix.
    We have to find a function type (a -> a).

    fix (\_ -> 1) = 1
    
    fix f = a0 = f(a1) = f(f(a2)) = f(f(f(a3))) = f(f...f(an)...)
    ==> f(a2) = a1, f(a3) = a2, ..., f(an) = an_1


  Tricky question...
  I frist come out with this one:

  remainder' a b = fix (\a -> if a < b then a else a-b)

  which is not good.

  Maybe need to find something f :: ((a->b) -> (a->b)) ?

  After some research, this is related to Fixed point combinator (Y combinator).
 
  so, I come out with my solution as:
-}

remainder' :: Integer -> Integer -> Integer
remainder' a b = fix (\f n -> if n < b then n else f (n-b)) a

{-------------------------------------------------------------------------
  Some references:

  http://en.wikipedia.org/wiki/Y_combinator

  http://www.google.com/search?hl=en&client=firefox-a&rls=org.mozilla%3Aen-US%3Aofficial&hs=c40&q=%22fix+f+%3D+f+%28fix+f%29%22&btnG=Search

  http://www.cs.wright.edu/~tkprasad/courses/cs776/FixedPoint.ppt

  http://www.cacs.louisiana.edu/~mgr/404/burks/foldoc/92/42.htm

  http://sequence.complete.org/node/149

  http://www.dcs.ed.ac.uk/home/stg/NOTES/node2.html

  http://www.cl.cam.ac.uk/research/hvg/Isabelle/dist/library/HOLCF/Fix.html
-------------------------------------------------------------------------}

Leave a Reply