The following is written in Literate Haskell style.
Let us first write a recursive Haskell function that tells if a natural number is even:
> isEven n = if (==) n 0 then True else (if isEven (pred n) then False else True)
From Lambda calculus, we know the Y combinator, which returns the fixed point function for any function f:
> y f = f (y f)
The definition above satisfies the fixed point definition of f(x) = x.
Now let us define the isEven function again now using Y:
> isEven' = y (\f n -> if (==) n 0 then True else (if f (pred n) then False else True))
Above, Y binds its function argument on f, which results in a recursive call:
y (\f n -> if (==) n 0 then True else (if f (pred n) then False else True)) = (\f n -> if (==) n 0 then True else (if f (pred n) then False else True)) (y (\f n -> if (==) n 0 then True else (if f (pred n) then False else True)))
Partial application results in:
(\n -> if (==) n 0 then True else (if (y (\f n -> if (==) n 0 then True else (if f (pred n) then False else True))) (pred n) then False else True))
Now let's ensure that the halting conditon for the recursion works. Let's pass it a zero:
(\n -> if (==) n 0 then True else (if (y (\f n -> if (==) n 0 then True else (if f (pred n) then False else True))) (pred n) then False else True)) 0 = if (==) 0 0 then True else (if (y (\f n -> if (==) n 0 then True else (if f (pred 0) then False else True))) (pred n) then False else True)
The first condition evaluates to True and thus the whole expression evaluates to True.
If we pass an argument larger than zero, call it $, we get:
if (y (\f n -> if (==) n 0 then True else (if f (pred n) then False else True))) (pred $) then False else True)
The first condition above is the recursive function itself, which returns True for zero. So we pass it the predecessor of n. If the predecessor of n is even, n itself must be odd. Otherwise n is even.
Now we can test that it works for some small values:
map (\n -> (n, isEven' n)) [0..5]
[(0,True),(1,False),(2,True),(3,False),(4,True),(5,False)]
Dolby is now a Browserling customer!
1 day ago
No comments:
Post a Comment