Induction

In this problem we consider a procedure for computing all pairs of the elements in a list. For a list (e_n...e₁) we define the pairs to be a list containing all pairs (e_i, e_j), for i > j and 1 <= i,j <= n. We choose to represent each pair as a Scheme <pair>. For example, here are some lists with corresponding lists of pairs:

(a) ->  ()
(a b) -> ((a b))
(a b c) -> ((a b) (a c) (b c))

The following procedure is purported to compute the unordered pairs for a given list, lst:

(define (all-pairs lst)
  (cond
    ((empty? (tail lst)) empty)
    ((empty? (tail (tail lst))) (list lst))
    (else (append (pair-with-list (head lst) (tail lst))
                  (all-pairs (tail lst))))))

All-pairs makes use of the helper procedure

(define (pair-with-list elt lst)
  (if (empty? lst)
    empty
    (cons (list elt (head lst))
          (pair-with-list elt (tail lst)))))

Prove by induction that (all-pairs lst) produces a list containing all the pairs for any lst of length n>1, using the above definition of pairs. You may assume that

(pair-with-list x (en ... e1))

returns the list ((x e_n) ... (x e₁)), for any length n. You may further assume that (append l1 l2) correctly forms the concatenation of the lists l1 and l2, for any length lists.

Solution

Return to CS 212 Prelim 1 - Spring 1997