On this page:
3.1 Conjectures
3.2 Inductive Proofs
3.3 Improving Claims

3 Recursive Functions and Inductive Proofs

On many occasions, programming language researchers formulate claims about programming languages as relations between functions. Since the collection of terms in a language is usually defined in an inductive (self-referential) manner, they design recursive functions to process terms. To prove claims about functions (and relations), they then use structural induction. If you don’t, find reading material to supplement the lectures. This last introductory lecture summarizes what you are expected to know about structural induction and strengthening claims from your undergraduate curriculum.

3.1 Conjectures

Say you have a language and you have defined some functions on the language:

(define-language Shapes
  (s (square x y r)
     (overlay s s))
  ((x y r) number)
  ; for the results
  (t (rectangle x y x y))
; determine the area of a shape
(define-metafunction Shapes
  ; we leave off the optional contract because there is no specification for the domain
  [(area (rectangle x_min x_max y_min y_max))
   ,(* (- (term x_max) (term x_min)) (- (term y_max) (term y_min)))]
  [(area (square x y r))
   ,(* (term r) (term r))]
  [(area (overlay s_top s_bot))
   ,(+ (term (area s_top)) (term (area s_bot)))])
; compute the bounding rectangle of a shape
(define-metafunction Shapes
  bb : s -> t
  [(bb (square x y r))
   (rectangle x ,(+ (term x) (term r)) ,(- (term y) (term r)) y)]
  [(bb (overlay s_top s_bot))
   (bb-aux (bb s_top) (bb s_bot))])
; auxiliary function:
(define-metafunction Shapes
  bb-aux : t t -> t
  [(bb-aux (rectangle x_min1 x_max1 y_min1 y_max1)
              (rectangle x_min2 x_max2 y_min2 y_max2))
   (rectangle ,(min (term x_min1) (term x_min2))
              ,(max (term x_max1) (term x_max2))
              ,(min (term y_min1) (term y_min2))
              ,(max (term y_max1) (term y_max2)))]))

You can experiment with these functions:
> (term (bb (overlay (square 1.1 2.7 3) (square -7.2 -2.0 3))))

'(rectangle -7.2 4.1 -5.0 2.7)

> (term (area (bb (overlay (square 1.1 2.7 3) (square -7.2 -2.0 3)))))


> (term (area (square 1.1 2.7 3)))


> (term (area (square -7.2 -2.0 3)))


From experiments such as these and/or inspiration, you may come up with conjectures such as

the area of the bounding area of some shape s is always larger than the area of the s

in English or, with Redex,

(> (area (bb s)) (area s))

It turns out that Redex comes with a random testing tool that can help you check such conjectures:
> (redex-check Shapes s (> (term (area (bb s))) (term (area s))))

redex-check: counterexample found after 1 attempt:

(square 2 0 1)

The redex-check facility generates examples of s with respect to language Shapes and checks whether the conjecture—formulated as a Boolean expression— (> (term (area (bb s))) (term (area s))) produces true. If so, great. If not, it has found a counter-example, and in this case it has. A square’s bounding box is itself, and the area of the two are equal. So we revise our conjecture to use >= and not just >:
> (redex-check Shapes s (>= (term (area (bb s))) (term (area s))))

redex-check: counterexample found after 7 attempts:

(overlay (square 2 0 1) (square 2 1 2))

But again, redex-check finds a counter-example. This time, the counter-example consists of a combination of two squares that overlap. While the area of the bounding box is just the area of the surrounding rectangle, the area function computes the area of an overlay construction as the sum of the two.

Draw the situation on a grid to figure out why the conjecture fails.

To fix the conjecture, we need to change the area function. Specifically, we need to subtract the overlap between the two shapes:
(area (overlay s_top s_bot)) =
(- (+ (area s_top) (area s_bot)) (area (intersection s_top s_bot)))
meaning we also need to define the intersection function.

In short, before you try to prove conjectures it is often helpful to have them checked so that minor typos or real misunderstandings are eliminated before you invest effort in a full-fledged proof.

3.2 Inductive Proofs

It is time to study the structure of proofs for claims about inductive functions and sets. Here is a mathematical statement of the claim:

Claim: for all Shapes s, area(bb(s)) >= area(s)

The claim is about the elements of an infinitely large set. When such a set is defined by induction, we can usually (but not always) use mathematical induction, specifically, a modification called structural induction. The key to structural induction is that you may assume that the claim holds for all pieces of a compound structure. This is similar to plain mathematical induction where you assume that the claim holds for n and then prove it for n+1. Also, such proofs are usually organized in analogy to the definition. That is, the proof proceeds by case analysis that includes as many cases as the inductive definition and the same kind of shapes.

Here is an outline of the proof of the above claim according to these two principles.

Proof Organization By induction on the structure of the definition of Shapes and by case analysis on the construction of s:

  1. s = square(x,y,r) In this so-called base case, you must prove that area(bb(square(x,y,r))) >= area(square(x,y,r)), without any further assumptions.

  2. s = overlay(stop,sbot) Here you may assume that
    1. area(bb(stop)) >= area(stop)

    2. area(bb(sbot)) >= area(sbot)

    These two statements are called induction hypotheses. From these induction hypotheses, you must prove that area(bb(overlay(stop,sbot))) >= area(overlay(stop,sbot)) and you may use the definitions of the functions.

The outer (numeric) enumeration sets up the case analysis for s; the inner (alphabetical) enumeration is the essence of the induction proof strategy. End of organization

Proof Let us fill in the gaps:
  1. If s is a square, its bounding box is the same square, meaning the areas of the two shapes are the same. You can perform an algebraic computation using the function definitions for bb and area.

  2. From the two induction hypotheses, you get

    area(bb(stop)) + area(bb(sbot))

    >= area(stop) + area(sbot)

    >= area(stop) + area(sbot) - area(intersection(stop,sbot))

    = area(overlay(stop,sbot))

    because area(intersection(stop,sbot)) >= 0. (An area is positive!)

    Using the definitions of area and bb, you also get


    >= area(bb(stop)) + area(bb(sbot))

    with some reasonably straightforward simple claims about max and min.

    If you now compose these two calculations, you get the desired conclusion.

3.3 Improving Claims

(define-language Lon
  (l (n ...))
  (n number))
; a simple demonstration of a syntax rule
  (t x)
  ; ==>> (rewrite to)
  (term x))
; act like cons for Redex
(define-metafunction Lon
  mcons : n l -> l
  [(mcons n l) ,(cons (term n) (term l))])
; act like + for Redex
(define-metafunction Lon
  m+ : n n -> n
  [(m+ n_1 n_2) ,(+ (t n_1) (t n_2))])

(define-metafunction Lon
  abs.v1 : l -> l
  [(abs.v1 ()) ()]
  [(abs.v1 (n_h n_r ...))
     (+* n_h
         (abs.v1 (n_r ...))))])
(define-metafunction Lon
  +* : n l -> l
  [(+* n l)
   ,(map (λ (x) (+ x (t n)))
         (t l))])

(define-metafunction Lon
  abs.v2 : l -> l
  [(abs.v2 l) (aux l 0)])
(define-metafunction Lon
  aux : l n -> l
  [(aux () n) ()]
  [(aux (n_h n_r ...) n)
   (mcons (m+ n n_h)
     (aux (n_r ...)
          (m+ n n_h)))])

Figure 3: Two ways of computing absolute distances

On occasion, structural induction is not quite enough. To illustrate this point, let us study the claim that the two versions of the abs function in figure 3one plain structural, one in accumulator-style—are equal. That is, given the same list of relative distances they produce the same list of absolute distances.

Claim: for all Lists of numbers l, abs.v1(l) = abs.v2(l)

Since abs.v2(l0) = aux(l0,0), we really mean

Claim: for all Lists of numbers l, abs.v1(l) = aux(l,0)

What you may not see from the definition of Lon is that lists have an inductive definition. Here it is:
; A Lon (list of numbers) is one of:
;  empty or ()
;  (cons Number #, Lon)
It has the two obvious clauses, and it is inductive in the expected case (the cons case) and position (cons consumes a number and a list). Hence we can adapt the proof organization from above:

Proof Organization By induction on the structure of the definition of Lists and by case analysis on the construction of l:

  1. l = () In this so-called base case, you must prove that abs.v1( () ) = aux( () ,0), without any further assumptions.

  2. s = (nfirst nrest ...) Here you may assume that

    abs.v1( (nrest ...) ) = aux((nrest ...), 0)

    which is the induction hypothesis for an inductive definition with a single self-reference.

    From the inductive hypothesis, you must prove that abs.v1( (nfirst nrest ...) ) = aux((nfirst nrest ...), 0) and you may use the definitions of the functions.

Again, the enumeration sets up the case analysis for l; the nested math display enumeration is the essence of the induction proof strategy. End of organization

You can probably see that the first item follows from a trivial calculation. The problem is the second item, the inductive step. Let us start by simplifying the left side of the goal:

abs.v1( (nfirst nrest ...) )

= cons(nfirst,+*(nfirst, abs.v1(nrest ...)))

= cons(nfirst,+*(nfirst, aux( (nrest ...), 0)))

The last step of the calculation follows from the induction hypothesis. But as you can easily see from any example, this last line is not equational equal to aux( (nfirst nrest ...), 0) because it unfolds like this:

aux( (nfirst nrest ...), 0 ) = cons (nfirst, aux( (nrest ...) nfirst))

What this means that we need to improve our claim so that the induction goes through:

for all lists l and for any number n, +*(n,abs.v1(l)) = aux(l,n)

The first case, l = () works out easily again.

The second case, l = (nfirst nrest ...) relies on the induction hypothesis:

+*(n,abs.v1( (nfirst nrest ...) ))

= +*(n,cons(nfirst,+*(nfirst,abs.v1( (nrest ...) )))) by def. of abs.v1

= cons(n+nfirst,+*(n,+*(nfirst,abs.v1( (nrest ...) )))) by ’laws’ of +*

= cons(n+nfirst,+*(n+nfirst,abs.v1( (nrest ...) ))) by ’laws’ of +*

= cons(n+nfirst,aux( (nrest ... ),n+nfirst)) by IH

= aux( (nfirst nrest ... ),n) by def. if aux

Naturally, what we called ’laws’ of +* are claims about this auxiliary function, and these claims deserve a proof. They are good practice proof and follow from straightforward structural induction.

P.S. Yes, an alternative way to proceed would have been to prove

+*(n,aux(l)) = aux(l,n)