mult (x, y + 1) = add (x, mult (x, y)).
Formally, the second step is an application of primitive recursion, in which h is
identified with the add function, and g 2 (x, y) is the projector function p 1 (x, y).
Example 13.3
Substraction is not quite so obvious. First, we must define it, taking into account
that negative numbers are not permitted in our system. A kind of subtraction is
defined from usual subtraction by
x y = x – y if x ≥ y,
x y = 0 if x < y.
The operator is sometimes called the monus; it defines subtraction so that its
range is I.
Now we define the predecessor function
pred (0) = 0,
pred (y +1) = y,
and from it, the subtracting function
subtr (x, 0) = x,
subtr (x, y +1) = pred (subtr (x, y)).
To prove that 5 – 3 = 2, we reduce the proposition by applying the definitions a
number of times:
Formally, the second step is an application of primitive recursion, in which h is
identified with the add function, and g 2 (x, y) is the projector function p 1 (x, y).
Example 13.3
Substraction is not quite so obvious. First, we must define it, taking into account
that negative numbers are not permitted in our system. A kind of subtraction is
defined from usual subtraction by
x y = x – y if x ≥ y,
x y = 0 if x < y.
The operator is sometimes called the monus; it defines subtraction so that its
range is I.
Now we define the predecessor function
pred (0) = 0,
pred (y +1) = y,
and from it, the subtracting function
subtr (x, 0) = x,
subtr (x, y +1) = pred (subtr (x, y)).
To prove that 5 – 3 = 2, we reduce the proposition by applying the definitions a
number of times: