Example 8.2.1.Using informal induction we can define the 'sum' (+)function using only initial functions as for all x,y__Nat sum(x,0) = x, sum(x,y+1) = succ(sum(x,y)).Formally, this is a definition via primitive recursion,
namely, sum = pr(_1, succ ° _2).
1
3
Once the sum function is defined we can use it toform other definitions. Informally the 'product' (*)function can be expressed as prod(x,0) = 0, prod(x,y+1) = sum(prod(x,y), x).Formally this is again defined via primitive recursion,prod = pr(zero, sum ° <_2, _3>).
3
3
Previous slide | Next slide | Back to first slide | View graphic version |