24 Feb
                
                    2009
                
            
            
                24 Feb
                
                '09
                
            
            
            
        
    
                11:53 a.m.
            
        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.