Computation with recursion operators

Five plus two : an annotated example.

Recall the definition of plus:

plus = [i:nat][j:nat] nat_rec i ([k:nat] suc) j

Also recall the rules for evaluating nat_rec:

nat_rec m f zero    =>  m 
nat_rec m f (suc i) => f i (nat_rec m f i)

Let us calculate plus five two. The names for numbers are abbreviations, so that two = suc (suc zero).

plus five two 
 = ([i:nat][j:nat] nat_rec i ([k:nat] suc) j) five two

First, we beta-reduce, substituting five for i:

 = ([j:nat] nat_rec five ([k:nat] suc) j) two

Then we beta-reduce again, substituting two for j (and eliminating the outermost set of parentheses):

 =  nat_rec five ([k:nat] suc) two

Now let us expand the definition of two (not a computation step, just for clarity). We will not need to expand the definition of five.

 =  nat_rec five ([k:nat] suc) (suc (suc zero))

Now we look at the rules for nat_rec. The last argument is not zero, so the second rule applies. The three arguments are

m = five
f = ([k:nat] suc)
(suc i) = (suc (suc zero))

Hence i = (suc zero). Applying the rule, we have

 = ([k:nat] suc) (suc zero) (nat_rec five ([k:nat] suc) (suc zero))

We reduce the application ([k:nat] suc) (suc zero) by substituting suc zero for k in suc. Since k does not appear in suc, we are left with suc, giving the whole term as:

 = suc (nat_rec five ([k:nat] suc) (suc zero))

Again we look at the rules for nat_rec. The last argument to nat_rec is still not zero, so the second rule applies again. The three arguments this time are

m = five
f = ([k:nat] suc)
(suc i) = (suc zero)

Hence i = zero. Applying the rule, we have

 = suc (([k:nat] suc) zero (nat_rec five ([k:nat] suc) zero))

Again, reducing ([k:nat] suc) zero leaves only suc:

 = suc (suc (nat_rec five ([k:nat] suc) zero))

Looking at the rules for nat_rec, we see that the first rule applies - the arguments to nat_rec are:

m = five
f = ([k:nat] suc)
zero

Thus we apply the first rule, replacing nat_rec five ([k:nat] suc) zero) with five:

 = suc (suc five)

So, plus five two is suc (suc five), or 7. Here are the steps again:

plus five two 
 = ([i:nat][j:nat] nat_rec i ([k:nat] suc) j) five two
 = ([j:nat] nat_rec five ([k:nat] suc) j) two
 =  nat_rec five ([k:nat] suc) two
 =  nat_rec five ([k:nat] suc) (suc (suc zero))
 = ([k:nat] suc) (suc zero) (nat_rec five ([k:nat] suc) (suc zero))
 = suc (nat_rec five ([k:nat] suc) (suc zero))
 = suc (([k:nat] suc) zero (nat_rec five ([k:nat] suc) zero))
 = suc (suc (nat_rec five ([k:nat] suc) zero))
 = suc (suc five)

Judith Underwood
Fri Oct 25 14:58:22 BST 1996