[MUSIC] Welcome again. In this lecture I will explain to you a useful extension of the data types. Namely structured data types or functional data types. So, assume we would like to specify the status of, well, an arbitrary object. Let's take a tap. So a tap can be closed or open or broken. And the way we can specify this using the struct key word. And what we write down here is just an abbreviation. Writing that's the status has three constrictors, namely open, closed, and broken. And what does this actually mean? Well, there's complete translation to the key words that we already know. So if I write down sort statuses is strict open closed or broken, I actually mean to write down that I have a sort status. That I have three constrictors. That I have a number of auxiliary functions, such as equality and inequality, and if. And there is a standard definition for all these functions. So if we would take as an example equality, then it has this self-evident definition that s is equal to s is true. And that when we have two of the elements, then if you apply this equality function to these elements, and these elements are different then the result is false. So open equals closed is equal to false. And open equal to broken is equal to false. And the same holds for closed. And we can declare something similar, or automatically something similar is declared for broken. Okay, so if we declare such a data type with the struct construct. Then because we know how it is translated to standard data perhaps we can ask and answer elementary questions. Such as how many elements does this domain of this data type's status have? So this was the definition. And what you can see is this domain has at most three elements because we have three constructors. And all the elements in the data pack must be denotable by a constructor, so we can have, at most, three. We can also see that all the terms denotable by constructors are different. And if they must all be different, then we have exactly 3. And how can we see that these terms are different? Well, that's by this mapping to booleans. So let's assume that, or let's look at closed and opens, and assume that closed is actually equal to open. What we will show is that this leads to true is equal to false as follows. And from that we can conclude that there is no model where closed is equal to open. So, in all models closed must be not equal to open. How do we derive this, well we have already seen this once. True, by the equations is equal to closed is closed. By this assumption we know that closed is equal to open. So the first closed can be replaced by open, and then we get open is equal to closed. And for that we have an equation saying that that is equal to false. So we see that true is equal to false, and this is our contradiction. And so we know, and that applies to all data types defined with structs, that all the elements denotable by constructors must be different. [COUGH] There are a few useful functions for the useful extensions to the Struct data type and one is so called recognizer function. That allows to recognize a particular constrictor. So It's written with a question mark. It's totally optional. And it has an arbitrary name here we have chosen. It's open simply to recognize the constructor is open. So if you get some element of sort status, you can ask if it is open. Whether that element is actually open. And in the same way we can define it is closed and it is broken. And also this has a standard translation to the standard way we define data types. So what happens is that typically three maps are declared. So, these are auxiliary functions. And that we typically have equations of the shape is_open applied to open is true. I think that it's quite self evident is_open(closed) is false, and the same holds with the application of is_open applied to broken. And with six more equations we can actually define all recognizer functions on all the constructors. And this is done implicitly when you declare the, when you write down the declaration at the top. Okay? Let's make data types that we can declare a little bit more complex. So instead of using constants, we can also use functions at the right hand side. And use that for instance to declare tuples, or pairs of elements. So let's assume that we want to declare a data type with pairs of integers. And that can typically be done using this declaration. What does this mean? Well, it means that we declare sort tuple, that we declare constructor with as arguments to integers, yielding a tuple. That we have all these standard functions available automatically And let's just look at the standard definition declared for equality. So if we want to know whether two pairs are equal, then that is reduced to the question on whether the arguments are equal. So in general, functions If you have different constrictors in such a struct, then the elements are different. If you have similar constrictors, then the arguments must be equal. We can add also a recognizer function to sort tuple or to the pair. And we can add projection functions, that allows us to get the elements of the arguments of the function pair. So that's done like this with a left and a right. And typically if you declare a left and a right, you declare a function. An auxiliary map left and right. And we have this auxiliary is_pair. And the typical equations for this auxiliary functions are that the left applied to a pair use the first element so n. The right yields the second element. So this is typically the simple and only equation for this projection function, and for the recognizer function we have this equation. And when the is_pair applies to a pair it's always true. And because there's only one constrictor in this data type, there is no equation where is_pair applies to something that yields false. So, yet, for another example. One of the typical applications of system validation is to analyze communication protocols. Where messages are exchanged between different entities. And for that we need a data type message, and a message could typically consist of an address to which the
message is sent and an address from which the message is sent and some form of content. And often, there are also acknowledgements playing a role. So an acknowledgment could typically have the shape. Where you have a to address and a from address. How do you specify this? Well let's assume that we have the sort reference available, and that it won't say anything about it's structure. And not really interested in the data type content, except that I assume that it is available, but I want to specify sort and message. And that's the structure with two elements, one corresponding to a message with content. So there is a message with three arguments, a to_address, from_address. And a content with projection functions, to, from, and c. And a recognizer function is message. And we have this acknowledgement message. That's the other constructor function in this data type. And it has two arguments. Namely, the to address and the from address. And we added this recognizer function is acknowledgement. And this is the whole, this is the complete specification of a sort message to be used in such communication protocols. If you reduce to functional languages, then you may know that it's very common to write down recursive data types. And that's also possible with the struct data, the struct key word. So let's assume that we want to specify the sort tree. Trees are very common data structures in computer science. This can be done as follows, by saying that a leaf is a tree. So in here I put a natural number in the leaf, and I have a recognizer function val. The projection function val that gets the number of a leaf, and to recognize a function is a leaf. And we have a node with two sub-trees. One with projection function left, one with projection function right, and the recognizer is a tree. And this whole declaration declares the tree data structure. So what is a tree? A tree is typically a tree consisting of only a leaf, or it's typically this tree with two leafs and one node, or we can make The Tree even more complex. And what you can immediately see and understand is that with this extremely simple declaration you can make trees of arbitrary size. Let's do exercise. Let's look at this definition or attempt to define a list and the question is, is this actually a proper way to define a list? And this is not about the fact that I used a string empty list instead of a square, square brackets for the empty list or I used cones instead of. A triangle is just about structure of this data type declaration. And the question is does it specify this list? Second exercise. Here we have some arbitrary sort T with two constructors, single constructor that used a single element. And you can also make larger objects, namely using the constructor more applies to an element of sorts t. And now the question is can you determine, based on this definition alone, how many elements this data type has? Okay? So, what did we do? We introduce this a key word struct, for a structured type or a functional type. And this is really very convenient, and very often used in specification. I showed you that you can add recognizers and projection functions at will. And I also showed you that there's a standard translation of these structured types or functional types to the standard mechanisms to define data types. So there's nothing really new here. You can also define it using the key words sort, cons, map, var, and eqn. In the next lecture, I will also explain that you can also use quantifiers in your expressions. Thank you for watching. [MUSIC]