Pattern Matching

There is an alternative way to define functions on the integers using pattern matching. For example, the function f in Section 5.1 on page  could have been defined as follows:

f:num->num;
f(0) <= 0;
f(n+1) <= (n+1)+f(n);

We now have two rules for f. One for when n=0 and the other for when n>0. To evaluate f(1) we use the second rule. f(1) matches the left hand side of the second rule with n=0 so to evaluate f(1) we evaluate the right hand side of the second rule with n=0. This gives (0+1)+f(0) which is 1+0 which gives 1.

Similarly, to evaluate f(2) we use the second rule. f(2) matches the left hand side of the second rule with n=1 so to evaluate f(2) we evaluate the right hand side of the second rule with n=1. This gives (1+1)+f(1) which is 2+1 which gives 3. etc.