So let us go on.

In the lecture yesterday I presented the denotational semantics of PCF called by name semantics.

And I argued before that operational semantics and denotational semantics are two sides of

the same coin and this can be justified formally.

Now we relate them, we can say is sound, a denotational semantic is sound.

If whenever we have this then the denotation of P is equal to the denotation of C. So if

we evaluate to a value via the rules or the operational semantics then the denotations

of the original program and the obtained value must be the same.

And then the other property is adequacy, it works in an opposite direction in a certain

sense.

So whenever P is equal to C then if the type of

P is either star or bull or not.

So that's a converse, if the denotations are the same then using the operational semantics

we can converge to this value but this is not precisely the converse of this because

this is true for any type of P and this is true only for the base types like bullions

and natural and the star type.

The thing is of course if we convert to a lambda abstraction then this wouldn't hold

because there are more than one normal form of a function even if the function have the

same denotations.

So we've got different terms for divergence but from the denotational point of view all

of them are diversions.

So all of them are equal.

But if we restrict this return types of this things to be the data types then it's true.

And this property together they somehow justify that if you have these two styles of semantics

and this property is hold for them it indicates that this semantics are fit together.

So there are more properties about the agreement of the operational semantics and the denotational

semantics stronger than this one.

This is like the most basic one so if you have them then it's alright.

But you might have stronger properties.

We don't consider them but they are more difficult to achieve and it's nicer than if you can

achieve them.

But these are like minimum and it's sufficient in most of the cases.

So and now I can at least state as a fact that presented

all by name

this sound and adequate with respect to this.

So that's tricky to prove and you're not going to do it.

But for your information this is true.

And now then we have this picture for call by name.

As I promised we consider the corresponding situation was called by value and was called

by value the semantics is not as straightforward as for call by name.

And it could be more difficult but it can be simplified and presented in quite concise

way due to this magic let construct.

That's part of the motivation for me to present the semantics to you because I want to show

the use of the construct and that's going to be quite important in the future.

So first of all we need to assign a semantics to the types as we did in call by value and

call by name.

So I first I introduce an auxiliary function.

Let's write it as an underscore.

Because again so in call by value the things are a bit more complicated because you need

to talk about values all the time.