Yes, so this is the idea I guess.

I mean for after this, I don't know, seven lectures that I've given, I'm seriously hoping

that I would have some rest.

So I propose that we do so organize these practicals in such a way that you present

your solutions and we discuss them.

Hi Thomas.

Maybe do something additional to that and there are some programming exercises so you

can also, when we come to them, you can also maybe connect your laptop to the beamer and

show your solutions.

I'm sure that you're proud for your programs and you will certainly like to show that to

the others and comment the features that you used and how you designed them.

You see, that's really awesome and a lot more observation that we have.

It's theSS

good

d

the

food

good

So everyone handle out the solutions or not?

Yes, that would be nice.

There are these other sheets from the other group maybe.

You can bind them too.

So, I will check them offline.

I propose that some of you maybe choose the solution of the first exercise at the board and comment the solution about that.

I can give your work back so that you use it for the presentation.

There was a small issue because I didn't have proof of the lemma which was given.

So, you used the lemma but you didn't prove it. So, present your solution as if the lemma was there and someone else may prove the lemma.

I give you the microphone.

Since you are recording this anyway.

So, you are supposed to show an equivalence between big step and small step semantics.

So, if you are going to show big steps then this is equivalent to p reduces to q and big steps semantics.

For brevity I will just omit this notation here because it is clear what we are talking about anyway.

So, I will show this in two directions. First of all from left to right.

It is very simple because well it can be shown using this lemma.

So, if p reduces to q and q reduces to a value let's call it c then we already have p evaluates to c2.

So, I did not prove this lemma. Some of you can do that hopefully.

But well we can show all of the rest with that.

So, as I said I will prove this via induction and this of course means that I need some sort of start.

And the start is simply that if p is already q then that means obviously that p reduces to q in small step semantics.

But also that p reduces to... wait.

So, p is equal to q and q itself is of course...

No, that is not what I am trying to say.

What I am actually trying to say is that if p has to be formed lambda x dot sum p prime.

So, if p is already a value then we have that p converges to this value in small step semantics.

Of course because it is already a value but also the same in big step semantics.

So, this is the start of our induction.

So, we are going to write over the steps of...

So, we are going to write over the steps to look at reduction chains with some number of...

So, this arrow which we used in the second... so it says that we reduce to something so there is actually a rule for that but it is just equal.

Yes, that would be correct.