[MUSIC] Welcome again. In the previous lecture you saw how we could specify numbers with Peano Arithmetic. But now I will explain how numbers are really modeled. And I'm sure I'll. We saw the specification of Peano arithmetic as a quite straightforward specification of natural numbers, but it's really inefficient if it comes to system validation tasks. So, what we need to do is to define a far more efficient data type for numbers. And we want to start with positive numbers. So these are the numbers from one up til infinity. And for this, we use the symbol N+ in general. Or we write sometimes also Pos. But on the slides, I prefer to use N Plus for positive numbers. And the positive numbers have two constrictors. The first constrictor is at c1, and because these numbers are used mainly internally in the tools, and we are not really see them when we do specification. We can use this somewhat awkward function name. @c1 represents 1. And we also have this function, @cDub. With two arguments, a boolean, and a positive number. And this is what it represents. Namely @cDub of a boolean B, and a positive number P, represents 2p plus 1, if the boolean is true, and 2p if the boolean is false. So, @c1 represents 1, @cDub with false represents 2. Basically two times one. @cDub with a true and @c1 represents 3. Two times one plus one. And in this way, we can make bigger and bigger numbers. And something, well this was already the same with Peano arithmatic, but we do not have an upper bound on the numbers. Any number can be made using this data type. And, as I said already, this is a somewhat awkward representation, but, as it is used internally, and we can simply write down ordinary numbers in specifications. The fact that these numbers look so ugly is not really a problem. Okay. Let's specify some functions on positive numbers and let's just take one, namely equality, as an example. So, equality gets two numbers and delivers a boolean. Expressing on whether these numbers are the same or not. We need some variables. And then if we have two equal numbers, then if you apply equality to them then this should yield true. And if you have the number one and a number which basically represents two times something and at sometime a something is one or larger. So, we compare one with something that's larger than one. Then equality on these should actually yield false. This is simply the symmetric case, and that should also yield false. And if we have two members, cDub(b,p), and cDub(c,q). Then these are equal when they are both odd or even. And that can be seen by the Booleans, b and c. So b should be equal to c. And we also need that p and q must be equal. You can specify many more operations. But I will just give a list of the operations that are available. So we have the function, max. Minimum. Successor that adds one to a natural number. A positive number. Addition adds to a positive numbers. Multiplication. And, we have the if, equality, non-equality and also, the inequalities on numbers available. These last four functions are available for all data types. Okay, well now that we have the positive numbers, it's relatively easy to make natural numbers. Because natural number simply consist out of positive numbers and zero. We denote natural numbers with this common mathematical symbol N. And sometimes you write not for natural numbers. We have this weird-looking constructor @c0, representing 0. And we have this embedding of positive numbers into natural numbers. If I have a positive number, say one, and I apply @cNat to it. It becomes the natural number one, but still represents one. Well, let's then define equality on natural number, just as an example. So, if we have two similar expressions. So, and they apply equality to it. So N is equal to N, then that should yield true days are equal. If we have two numbers, namely zero and some positive numbers embedded in the natural numbers, then they can never be equal. So zero is equal to a positive number yields false, and in a symmetric case it's also false. And if we have two positive numbers that we compare to each other as natural numbers. Then we can do this by simply comparing the positive numbers. The operations on natural numbers are exactly the same as operations on positive numbers. And, in addition, we also have modulo, the div operator, and exponentiation. Okay. Well in the same style, we can define integers. And I will not give all the details. But this is done quite similarly by an embedding of the natural numbers for the numbers zero and larger. For the integers zero and larger. And by an embedding of the positive numbers that I embedded into minus one, until minus infinity. We use this standard symbol Z for integers, or we sometimes write Int. And we have a few extra operators that we can define on integers, and which were not available on positive or natural numbers. So minus is defined on integers. We have absolute value which makes sense here. We have the predecessor, which we did not have before, and that's all. Well and then we can look at reals, I already know that it is common symbol r, r with the string real. And well how the yields are represented is something that takes a little bit too much time but for us it is probably only interesting how we can use them. So the division operator is the most important operator that we have on Reals. We have a floor that rounds a real down to the nearest integer. We have ceil which rounds up to the nearest integer. And we have the common round operator that provides the rounded value. And there is something very particular about reals, namely they are completely precise. So in the same way as the natural numbers did not have the largest value, and are in some sense really representing the mathematical natural numbers and integers. And the positive numbers have the same property. The reals also represent the real reals, in as far as we can express them with operators that we have available. But concretely this means that if you start with the number one, and you divide it by two you will get a half. If you again divide it by two you will get one fourth. If you again divide it and you continue dividing, you will get smaller and smaller numbers. But you will never, ever get zero. Okay. Now that we have four of these types of numbers you can ask, how can we convert different numbers to each other? And in one way this is done automatically. So if I have a positive number, this is automatically also a natural number. Is automatically an integer, and is automatically a real number. So this is basically saying the same. And, this concretely means that one is a positive number, but if needed, it converts itself to a natural number. And to an integer, or even to a real automatically. What's the purpose of this? The purpose is the following, mainly suppose I have this division operator that works on two reals and delivers a real. And I write down 1/2. Then what happens is that if we do not have this automatic conversion, then the 1 Is a positive number. And it should be automatically, it should be explicitly converted to a real number. And we should have to write a conversion operator in there, and the same applies to the two. So this is then not the common number that we are used to write. So by having these automatic type conversions. We can write 1 divided by 2 as we are used to, without being concerned about the types. So this also applies to for instance a minus operator. So if you have the minus, and the type of minus is integer, and it delivers an integer. If ever I write down 0 minus 17, then 0 has the type, not. And is automatically converted to an integer. 17 has the type pos, and it's also converted to an integer. And then minus can apply to this term, and the whole expression has the type integer. So upgrading of types is automatic, but downgrading of types must be done explicitly. And there are cases where you really would like to do this. Consider for instance, this situation where we have a variable of type not. We have this expression, N minus one. And because mine is defined on integers, N minus one actually yields an integer. But it's often the case that we know that N is larger than zero, and N minus one is still a natural number. So in that case we can actually say that the N minus one. Should be interpreted as a natural number, but we have to add this type conversion to it. So we say that N minus 1 is explicitly converted to a nat by the function Int2Nat. And for every pair of types, it should function type to type is available. Another example is Int2Pos to translate an integer to a positive number. Or Real2Int. Or Pos2Real. And this last one is also done automatically so you probably will never use that. But it's still available. And you may ask, if I write down the Int2Pos(0), 0 is not a positive number, so what does this represent? And by what I explained to you up til now, we can actually understand what this means. So all functions are total functions. That means that Int2Pos Is some positive number. And we also know that the positive numbers are defined by the constrictors. So the positive numbers really are the numbers one, two, three, up till infinity, and nothing else. So that means that Int2Pos, must be one of the numbers 1 up til infinity. Which we do not know which one, and if we do not specify which one it is, and we have not specified that. We have all kinds of models of our data types, and there's one model, the Int2Pos 0 is equal to 1. And there's 1 model, the Int2Pos 0 is equal to 2, etc. And this means, in practice, that, if the rewriters encounters the term Int2Pos:0, it cannot deal with it. Because it only rewrites something if it is valid in all models. And that means that it simply leaves an expression Int2Pos:0 untouched. And that can be used as follows if you have specifications all of a sudden there are terms of the form Int2Post(0) that occur. Then you know that mostly like something is wrong or not desired. And you can start to figure out what the problem really is. There's another caveat, which confused people. Suppose we have a function from natural number to natural numbers. We have a variable of type positive number. Now we can apply the function f to N. And write the following rewrite rule. So the f(n)=n+1. What this actually says is that this is the f(Pos2Nat(n))=n+1. And people might write this down, and may expect that f, if it is applied to zero, will actually rewrite to one. But that's not the case at all. Because 0 must match Pos2Nat(n) before it can be rewritten, and this is not the case. And so this rewrite rule will not apply. If we apply f to 0, nothing will happen, and this term will simply be untouched by the rewriting system. Okay, this is what I would like to tell about these numbers. So let's go to do some exercises. If we have the following expression, namely the cDub of true apply to the cDub of false apply to c1, which number does this represent? A second exercise, here we have two expressions and the suggested type for the expressions. Which of the terms have been correctly typed, if any? Okay. So what did we do? We specified the data types for the positive, the natural numbers, the integers, and the real numbers. Fortunately, these are only internal types. In specifications we can use common notations, but so now and then, especially if our specifications become complex, we may see the internal structures of these data types. And we also showed that we have automatic type conversions between these terms. Most of them that we want to see are automatic, but sometimes we have to apply a type conversion explicitly to make our specifications well timed. Next time we will deal with specification of lists. Thank you for watching. [MUSIC]
