So let us start.

First thing before I forget, there are the exercises I mentioned last time and have published

the first exercise sheet.

It's on the web page.

Hopefully everyone has found it.

And you're supposed to work in triples, so group together.

What else?

Is there any questions about it?

I don't know if you just maybe have taken a look at it, if it looks clear, doable.

So there's the AHAskel exercise, which is the very last one, which indicates that eventually

we are going to prepare some ground for Haskell programming.

And since the deadline is the next week already, so this should happen in between.

And I hope that we can do it on next, so basically tomorrow.

So if you come with your laptops, this will be welcome, because we are going to do some

examples.

All right.

So and back to the lecture.

So first, some errata to the previous lecture.

I made a mistake by claiming that the rules for ifs are different for call by value and

call by name.

That was actually not true.

Sorry for that.

I've checked this.

Apparently there is some sort of laziness in the if construction, which is present both

in call by name and call by value.

And in call by name and call by value, we still have this effect that we evaluate the

condition to true.

I mean, if we evaluate the condition to true, then we do not care about the other program.

So we just evaluate p.

So this is more or less a minor thing, but there is a more serious thing where else we

have to have mistaken this time.

And well, first I recall the notion of a value as.

So it's one of the following options.

First option, it's this unique element of the union, of the terminal type.

I don't remember how I called it.

So it's this type which contains one element only.

So then there are numbers and there are booleans.

So this is a place where we get recursive because we'll say that values, a pair of values

where values are recursively defined.

And that I've probably forgotten this time.

So a lambda abstraction is also a value, which for the reason we discussed before that it's

so reusable and for technical reason it's very convenient in defining semantics.

And then, so this evaluation relation is defined in such a way that p is a arbitrary program

and c is a value in the sense of the above definition.

And I gave the rules for products which were something like this.

So if t reduces to c1, c2, then pr1 of t reduces to c1.

And under the same assumptions, assumption, pr2 reduces to c2.

So this is in call by value, call by value.

So I showed this rules last time they were correct.

But the situation was called by name is considerably more different because in call by name were