Reading material

Pages 77-78.

Additional material

Arrays in Standard ML 

  local
    fun helper(a, 0) = []
      | helper(a, n) = append(helper(a, n-1), [Array.sub(a, n-1)])
  in
    fun toList(a) = helper(a, Array.length(a))
  end;
defines a function of type 
  'a array -> 'a list
which returns the contents of the array as a list. For example, 
  toList(Array.array(5, 1));
returns 
  [1,1,1,1,1] : int list

Question

The function Array.fromList is of type 'a list -> 'a array and, given a list, returns an array containing the elements of the list. For all lists xs, toList(Array.fromList(xs)) = xs. If you were to prove this by structural induction, what would be the base case and the inductive step?