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. And in the domain we have two constrictors, namely zero and the successor. Zero stands for zero and successor represents N plus one 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 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. 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. 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. So we start with true. Using the second equation, we can prove it equal to zero smaller than the successor of zero. So in the second equation, we take n to be equal to zero. 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 this smaller than then with these equations, we get the natural numbers as we know it. Let's make one remark about induction. 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. 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. So, this is called induction on the natural numbers. And why is it valid? Well it's valid, because we have zero and successor as the constructors of sort Nat. And that means that any element of sort Nat can be written by zero or the application of a number of successors to zero. And that means that the scheme, this induction scheme, guarantees that you have dealt with all cases when proving a particular property. And you may conclude that it holds for all the natural numbers. 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.
