0:00

Welcome again.

Â In this lecture, we will specify the natural numbers in the style of Peano.

Â So, how can we define the natural numbers?

Â Well, we will use the Peano

Â style for that.

Â That will not be particularly efficient but

Â it is very straight forward.

Â So we declare simply sort Not and this is the model.

Â 0:44

So we have the element

Â zero in this model one.

Â And this is two, and so it goes on.

Â What we know is that number of elements can a most countably infinite

Â because we can only make.

Â Incountabley infinite number of terms using construct to zero into successor.

Â One of the problems is that the elements can be equal, so we have no guarantee

Â up until now that elements two and three are different, are equal.

Â >> And it can even be worse it could be that zero in

Â a particular model is even equal to one and two or

Â that even all elements in this model map to only one model elements.

Â And we will see later how we can deal with this by adding a mapping to the Booleans.

Â But first, let's be concerned with the question

Â of how to define a standard function for instance addition.

Â So we declare this function add as having two arguments of time Nat to time Nat.

Â And we simply define it on all possible patterns in

Â its arguments based on the cons zero, zero,

Â zero and begin to see this is a nice definition.

Â Because zero plus zero ought to be zero.

Â We need two variables.

Â If we add the zero to the successor of n so

Â the left-hand side represents n + 1.

Â And this can be written as n + 1 or the successor of n.

Â Similarly, the successor of n added to zero is the successor of n.

Â And this one is a slightly more complex, if we have the successor of n

Â to the successor of m, then we have at the left hand side, n+m+2, and this is equal

Â 2:42

to the successor of that of n and the successor of m that also represents n+m+2.

Â And what you can see is the function add is applied to smaller objects

Â at the right, and that means that it is a good equation or a good rewrite rule.

Â Can we simplify these equations?

Â Well if can look at the first two equations we can see that the second

Â argument is always the result.

Â So we can simplify the first two,

Â by simply writing the add of zero of n is equal to n.

Â And can we simplify the second two also.

Â Well, it's not that straightforward, but

Â we can actually replace it by this single equation.

Â And that means that specification of addition, boils down to this,

Â namely this two equations characterize addition.

Â You can ask shouldn't we add the symmetric variance

Â showing add n,zero = n, like this to it?

Â And probably the add to the successor n and

Â m, about the add of n and the successor m like this.

Â And the answer to that is that it is not necessary

Â if you want to calculate the add on closed terms, where you don't have variables.

Â But if you have variables, the last two equations can be very useful.

Â And are therefore often added to certain specification.

Â Let's go back to this question of

Â guaranteeing that all the natural numbers are not equal.

Â So what we have to do is to use the only

Â fact that we know about elements that have to be not equal that we have available,

Â maybe that true is not equal to false, and for that we have to add some function.

Â From natural numbers to Booleans, and in this particular case we take

Â an arbitrary function at least smaller than and that can be defined as follows.

Â So, n is always smaller than zero, so n's smaller than zero.

Â Sorry, n is never smaller than zero.

Â So n smaller than zero is equal to false.

Â Zero is always smaller than n plus one.

Â 5:05

So zero smaller successor n is true is defining rule.

Â And if we apply smaller than on the successor of n nth to the successor of n.

Â Then this is always equal to n smaller than m, and you can see that the right

Â hand side is a less complex expression than the left hand side, so

Â this is a good rewrite rule again.

Â 5:28

So if we have edit this, how can we show that numbers are different?

Â So, let's take the three defining equations and put them here on top and

Â ask ourselves can we show that zero is not equal to successor of zero?

Â Or, in order to prove that we assume that

Â zero is equal to successor of zero and we will show that true is equal to false.

Â 6:13

Using the assumption, we replace this first zero by the successor of zero.

Â So we get succ(zero) < succ(zero).

Â We can simplify this using the third equation.

Â And we obtain zero < zero.

Â And using the first equation, we get false.

Â So we have shown that true is equal to false,

Â if we assume that zero = succ(zero).

Â So, there cannot be a model where true is equal to false and hence,

Â there cannot be a model where zero is equal to the successor of zero.

Â So, what we know is that for all models that there are,

Â zero must be not equal to the successor of zero.

Â Well we can apply this for all expressions that you can write down with zero and

Â the successor of zero.

Â If these two expressions are not equal,

Â we can show that they are also not representing the same elements.

Â So this shows that all elements in the model must be different.

Â So typically what we get is that if we specify the natural numbers and we add

Â 7:41

So given if we have these constrictors, we actually have an induction principle on

Â natural numbers and that's exactly the induction principle that we know.

Â So, suppose we would like to proof a property on all natural numbers.

Â And what we have to do is prove this property on zero.

Â And we have to prove this property for the successor of n for any number, n.

Â Assuming that you already know that the property holds for n.

Â And if this has been known,

Â we can conclude that a property has been proven for all natural numbers.

Â So how can we visualize this?

Â Let's have the natural numbers here.

Â So, put zero here, successful zero at this spot, two, three.

Â 8:35

And all the other numbers.

Â Now, with the first line we have proven a property for zero.

Â So the property fi holds for zero.

Â Now if we look at the second line we see that because the property holds for

Â zero it's also valid for the successor of zero.

Â And because we have now have proven it for successor of zero,

Â we now also know that it holds for the successor of zero.

Â And this goes on and you can see that it holds for all numbers.

Â 9:52

Okay, let's do an exercise.

Â If we want to specify multiplication and

Â we get these two equations for that,

Â is this a correct specification of multiplication

Â in the sense that we know multiplication.

Â And now let's do the same for subtraction.

Â So if we give the following rules for subtraction,

Â all natural numbers, is this well defined, okay?

Â We gave specification of natural numbers in the style of Peano.

Â As I said, not particularly efficient, but quite insightful.

Â We showed how we can guarantee that all

Â the elements in the model of the natural numbers

Â are different by giving a mapping to the Booleans.

Â And we indicated how the constructors gave rights to the induction principle on

Â the natural numbers and we will see that such induction principles also exist for

Â all other data types that we can define with constructors.

Â In the next lecture I will show you how we can actually specify

Â efficient numbers.

Â Thank you for watching.

Â