On Tue, Feb 24, 2009 at 9:53 AM, Peter Hilal <pe...@hilalcapital.com> wrote:
> Could someone provide a solution to do the following problem from Bird: > > The function "log" can be specified by the condition that log (2^m) = m for > all m. Construct a program for log and prove that it meets the > specification. Well, here is the least solution on Nat: log n = head [ m | m <- [0..], 2^m == n ] This meets the specification, and is _|_ everywhere else :-) The proof is trivial. Luke
_______________________________________________ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
