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]