[Haskell-cafe] Help with another Bird problem (3.3.4)

Luke Palmer lrpalmer at gmail.com
Tue Feb 24 17:39:13 EST 2009

On Tue, Feb 24, 2009 at 9:53 AM, Peter Hilal <peter at 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

-------------- next part --------------
An HTML attachment was scrubbed...
URL: http://www.haskell.org/pipermail/haskell-cafe/attachments/20090224/8f04ff4e/attachment.htm

More information about the Haskell-Cafe mailing list