Scoping revisited

The construction local .. in .. end which we saw earlier is used to make one or more declarations local to another declarations. At times we might wish to make some declarations local to an expression so Standard ML provides let .. in .. end for that purpose. As an example of its use consider a simple recursive routine which converts a non-negative integer into a string. For a little extra effort we also make the function able to perform conversions into bases such as binary, octal and hexadecimal. The function is called radix and, for example, an application of the form radix(15, "01") returns "1111", the representation of fifteen in binary.

(* This function only processes non-negative numbers *)
 
val rec radix = fn (n, base) =>
let
   val b = size base
   val digit = fn n => str (String.sub (base, n))
   val radix' = 
      fn (true, n) => digit n
       | (false, n) => radix (n div b, base) ^ digit (n mod b)
in
   radix' (n < b, n)
end;

This implementation uses a function called sub to subscript a string by numbering beginning at zero. The sub function is provided by the String component of the Standard ML library and is accessed by the long identifier String.sub.

Notice one other point about this function. It is only the function radix which must be marked as a recursive declaration--so that the call from radix' will make sense--the two functions nested inside the body of radix are not recursive.

Exercise

(Zeller's congruence) The implementation of the function zeller can be slightly simplified if zeller is a recursive function. Implement this simplification.

Exercise

Devise an integer function sum'' which agrees with sum everywhere that they are both defined but ensure that sum'' can calculate sums for numbers larger than the largest argument to sum which produces a defined result. Use only the features of the Standard ML language introduced so far. You may wish to check your solution on an implementation of the language which does not provide arbitrary precision integer arithmetic.

Exercise

Consider the following function, ...

val rec sq = fn 1 => 1
              | n => (2 * n - 1) + sq (n - 1);

Prove by induction that 1 + ... + (2n - 1) = n², for positive n.