[MUSIC] Nice to see you again. In this lecture, I will explain you the basic mechanism behind the specification of data types. So how can we specify a data type? Well, it's very simple. We simply declare the data type D as sort D. And what I mean by that is that we declare that we have this set of elements that represent D. So the only constraint is that D is a low empty domain and so it has at least one element. And we call this set of elements the model of the data type. So, how many elements does D have? It can have one element, or it can have two elements, or it can have an infinite number of elements, something like this. Or it can even be there are so many elements that you cannot even count them. This is called an uncountably infinite number of elements. So let's apply this to the booleans. We declared booleans as sort B. Sometimes, people like, I like this open B on my slides, but you can also provide the booleans in B O O L, and then you declare sort Bool. Booleans consist of two elements, namely true and false, and these are the constructors of the booleans. And that means that every element of the booleans can either be written down with a true or a false. More general, if we have a domain that the constructors, and every element of that domain can be written down as the application of a constructor to some smaller elements in that domain. So, how does the domain of the boolean look like? Well that is a set, with two elements. One represents true, one stand for false. But is not possible, is this. Namely that we have this domain with three elements. Because we only have the two constructors, and that means that we can have at most two elements in our domain. However it's possible to do this, namely to have a domain with only one element that both represents true and false. And it means a true and false become equal. This is so undesired that we actually forbid this explicitly in the semantics of the language. So we have a special semantic rule. And that says that elements representing true and false must be different. And this is the only rule where these elements, where it is explicitly stated that elements must be different. If you later on want to explicitly say that some other elements or some other data pack are different then this can only be done by relating them to the inequality of true and false. Okay, we can also have the desire to have more functions Booleans, for example, the functions not, and, and or and we can specify them using the keyword map, and that means that they do not give any constraint on a number of elements. They are not constructors, they are just arbitrary functions with the types indicated. But if we do not say anything explicitly about these functions, they have no specific meaning yet. The only thing that they are are total functions. And we need equations to specify them explicitly. And what is useful to know is that these equations are used internally, using term rewriting to be evaluated. So if you at some point have to analyze a big specification then it's useful to sometimes add external rewrite fulls to make an analysis possible. Okay how do we specify these functions. So let's first concentrate on the not. The not has this definition. So the not of the true is false. And the not of the false is true. And this is in accordance with our own intuition about the not. And what we see here is that it is very useful to specify a function on the constructors. So you take the constructors true and false and specify it separately for true and false. And sometimes, not in this case, you can make specification a little bit more concise or smaller. But if you want to be sure that you deal with all cases, define your functions on the constructors. You may ask yourself, wouldn't we like to add extra equations? For instance, the equation not(not(b))=b. And this can have its use. For instance to reduce complex expressions. It's not necessary for the completeness of the definition. So not as defined for all the elements by the two equation that we have already given. But if you would like to add them this is done as follows. So we have to declare the variable that we've used in the equation. And then we simple add it to our list of equations. In the same way we can define the N. So in accordance with what I just said, we tried to define N on all explicit constructors. So the and of the true and true is true, and the and of, well, set of arguments where one is false, is always equal to false. And if they are both false, it's also false, so this is the standard definition of an and. If you look at the and, that we see here, that we can write this down a little bit more concisely. Namely, the second element of the and true and b is equal. The second element of and true b is equal to b. And in the same way, we can specify or we can write this a little bit more concisely because now you see that second argument does not matter, and we have the and of false and b as equal to false. So if you write down this a little bit concisely then we get the following specification. Mainly theand of true MP is P, and the and of false and b Is equal to false. Now you may ask, why not also define the and of b and true is equal to b? And the and of b and false is equal to false? Well again, these rules that we have given here are complete for expressions without variables but if you have expressions without bit variables it can be convenient to add them. So let's just add them. So these are the two equations that we have to add. Okay. Well in this way we can define all the other operators also so I do not spent too much time on that but that's not the question namely. If we have specification can be proved certain properties with this. For instance, can we prove that the and of b and b is equal to b? And this can be done with what we call case distinction or induction booleans. And what we use is that the variable b represent boolean that we have only two booleans, so if we can prove this for true and false then we have proven for all boolean b. So, we have to prove and(b,b) for b is true and b is false. So, the and true true is true and b immediately derives that from one of the equations that we defined on the previous slide and the end of false false is also equal to false which also follows immediately from these equations. And now we can say that we have proven this for all booleans b. And, the principle that we have used is called induction on Bool. And some people find this a little bit of an overkill to call this induction on Bool, so we can also call this case distinction on Bool. Okay let's just summarize the operations that are available on Booleans. So we have the not that we specified. And we prefer to use in the tekst and on slides this hook symbol, this logical symbol. In the tools, you can use negation as an exclamation mark where the exclamation mark is negation. We have the and operator, we prefer to use the logical and symbol, and in the tools, we use the double and. Typically, we use these operators as infix symbols and not as prefix symbol, in accordance what is used in logical texts, or even in programming languages. The or is the or symbol, or two bars. The implies is just the implies arrow or the is larger than sign. We have an if on all the data types which is the if then else so it has a condition, a Boolean as first argument, and then two elements of another type. And it delivers depending on the value of the Boolean one of these elements. For all data types, also for the booleans, we have equality, written as this curly SRS2S symbols and you have the non-equality, and that is what we have available on the booleans Okay, let's do an exercise. If I defined or, and we have not yet defined the word explicitly, as false, is that then okay? Second exercise, suppose I have the definition of the booleans, and I would like to add the following equation, namely the not of true is equal to true. And we already know that the not of true is equal to false. Is it allowed to add it? So what did we do? We showed the basic mechanism to define new data packs and we showed also how Booleans are defined using that mechanism. We gave these five keywords. There are no more keywords to define data types. And we sort to declare a sort. Cons to define constructors. Map to define functions and the combinations of a var and eqn to define the actual leer functions Fortunately, you don't have to define all your data types yourself in this way. Most of the standard data types you will need are defined in this formalism in Appendix B of the book, but you can use them without explicitly declaring them. In the next lecture, we will apply what we have learnt to the special case of natural numbers. >> [MUSIC]
