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)))]))

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

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:

3.3 Improving Claims

(define-language Lon

(l (n ...))

(n number))

; a simple demonstration of a syntax rule

(define-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 ...))    (mcons      n_h      (+* 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 3—one 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)

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

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