0:17

So, we have seen that we can declare functions in this way,

Â we have a function f of type DXE yielding something of type F.

Â And what's now nice is that we can also use

Â these function types as types itself, so

Â we can say that we have a valid type of form DXE to F.

Â And this opens up quite a lot of possibilities to give nice and

Â concise aspect specifications, and have rather remarkable data types.

Â For instance, we can write down the following.

Â Namely, the type of list from naturally numbers to natural numbers,

Â and now the list contains actual functions.

Â 1:24

There's another interesting feature, and

Â that's called type aliases, and

Â that's means that I can write down sort E is N,

Â and from this point on sort or

Â type E actually behaves like sort naturally number.

Â It's in some sense exactly like natural numbers, but

Â E is now an abbreviation that we can use.

Â So, we can also write down that we have a sort F, that's actually a function type.

Â 2:00

And then we can declare a constant f of type F,

Â and f itself is now a function.

Â And we can declare variables in the same way depending on such an abbreviated type,

Â and such a map f can be defined using equations in the ordinary way.

Â So, let's define a variable y,

Â then we can simply write down the equation f(y) is equal to 0.

Â So, the constant f of function type

Â 2:39

If you have functions, then we can actually change it's value by function

Â updates, and function updates are written as the function f which followed

Â by records, followed by two expressions with an arrow to the left.

Â And in this concrete case it means that the function when it is applied

Â to the value 1 will, from this point on yield 7,

Â so the function at position 1 is updated with 7.

Â So, if you have this function, we can apply it for instance to 1, so f of

Â 1 is equal to 0, that follows immediately from the equations at the lower left.

Â 3:19

And if we have this function update applies to F, and

Â we apply it to 1 then actually the updated value is a result of the function,

Â so in this case we will get 7.

Â So, some people once asked me, can we actually define arrays or

Â more aggressively, why don't you have arrays in and the answer for

Â that is that they can easily be specified using functions, and

Â functions are actually a nicer data type.

Â So, let's ask ourselves how can we specify an array of type integer?

Â Well, I do done very confidently like this.

Â So, this array is just a mapping from natural numbers to integers,

Â 4:12

and then we can try to define functions get and set.

Â So, get takes an index in Array, and

Â an Array an yields the integer at the particular position.

Â If you can do a set, getting an index, a new value for that index,

Â and an Array, and this will yield an updated Array.

Â 4:35

How you specify that?

Â Well, let's declare the necessary variables,

Â for the get we have this equation.

Â The get of getting the value at position n of the Array

Â a is exactly the same as applying a to the index n.

Â A was a function, and it yields the value at position n.

Â And setting value a at index n of the Array is the following,

Â namely, we simply apply the function update to

Â the Array a setting the position n to the value i.

Â 5:23

If you have function types, then you can ask also,

Â how can we denote functions explicitly?

Â In particular, if we would like to have a function f, so

Â that f acts as f square, how do we denote that?

Â And for this purpose, the lambda notation or lambda Calculus has been invented,

Â 5:43

so this function that we want to have can be denoted as follows.

Â We write down lambda x of a certain types, this means this is a function

Â with one argument of type integer dot,

Â and then the expression that's the result of the function in this case x square.

Â So, this is the function that each x squared and delivers x square.

Â We can have functions of more arguments.

Â So, a function of two arguments x and y of type integer

Â yielding the sum of the two arguments, so x plus y is written down like this.

Â And now that we can make functions and have function types, we can even do

Â weirder things, and write down functions that actually have arguments as functions.

Â So, we can write down lambda f, where f is a function from integer to integer,

Â so the first argument of this function is, itself, a function.

Â And then a concrete value x, and

Â deliver the value of x to which we apply the function f twice.

Â 6:51

This is what I wanted to say about functions, so

Â let's turn our attention to sets.

Â So, we have sets as the mathematical notion of a set.

Â So, sets are typical collections of elements

Â where each element can occur only once in the set.

Â And because it's convenient an often faster for

Â analysis to have finite sets, we also have a sort of finite sets,

Â where only finite collection of elements can be put into a set.

Â So, how can we denote set?

Â Well, a set can typically be noted like this, with curly brackets,

Â and then the elements of the set being listed.

Â So in this case we have the set with element d1, d2, d3.

Â You can even denote the empty set, but using this, we cannot yet

Â denote infinite sets.

Â We can use the element of constrict,

Â where we test whether a particular element d is in this particular set S.

Â Or if you would write this textually in specification we would use the keyword in,

Â so we would write s in S to denote that s is an element of S.

Â 8:12

Using set comprehension, we can actually make sets with infinite size, so

Â Set comprehension is written as follows, a curly bracket, then a variable of

Â a certain type indicating the elements that we can put into the set, then a bar

Â and a condition, which expresses which elements for d are in the set.

Â So, if the condition applied to d yields true it's in the set, and

Â otherwise it's not in the set.

Â So, typically if it would take the set comprehension of n of

Â type not with the condition true, we get a set of all natural numbers.

Â And then we would take n of type not with condition false,

Â we would get the empty set.

Â We have the standard operator on sets, namely union, intersection,

Â and set difference, and in specifications we denote

Â them as the better plus, and multiplication symbol.

Â We have set complement,

Â so for a given set give the set with all elements not in the set.

Â But if you have a finite set for instance,

Â the set with elements one and two over positive numbers then

Â the compliment of the set would be the set with all numbers, three, four, etc.

Â And that means that the compliment of a finite set does not yield to finite set,

Â and therefore it's not defined on a finite set.

Â If you would like to use set complement in

Â specification then you need the exclamation mark.

Â 10:25

Bags are exactly the same as sets,

Â except that in a bag it is recorded how often an element occurs in the bag.

Â Like finite sets, we have finite bags which only allow

Â a finite amount of elements, and this is the way we describe a finite bag.

Â So, this is the bag where element d1 occurs three times,

Â element d2 occurs six times, and element d3 occurs 20 times.

Â The empty bag is written down like this,

Â two curly brackets With a colon in between.

Â 11:16

Bag comprehension is almost like set comprehension, but

Â instead of having a condition saying where an element is or is not in the set,

Â we here allow an expression that indicates how often an element occurs in the set.

Â So, typically if you would have natural numbers you could write

Â down the set D column natural number

Â with as the number d itself, and that will yield the set where element 0 would occur.

Â 0 times element 1 would occur one times, 2 would occur two times etc.

Â 12:13

Let's do an exercise.

Â If we have this expression from the lambda Calculus,

Â then it denotes a number, but what is the number it denotes?

Â And if I have this expression as a set comprehension,

Â what is exactly the set that this expression indicates?

Â So, we define functions and function types,

Â we define function updates, and define lambda terms,

Â but which we can explicitly denote functions.

Â 12:52

I indicated that you can use sort aliases,

Â we saw a finite sets and ordinary mathematical sets.

Â And we saw the data type of bags and finite bags.

Â In the next lecture, I will define structure to data types, or

Â those data types used in functional languages.

Â And these are extremely convenient when it'll comes to specifications.

Â Thank you for watching.

Â [MUSIC]

Â