Help with another Bird problem (3.3.4)
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. Note that this problem doesn't specify a domain, unlike problem 3.3.3, which specified Nat as the domain. Thanks.
On Tue, Feb 24, 2009 at 9:53 AM, Peter Hilal
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
participants (2)
-
Luke Palmer -
Peter Hilal