# 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