So, only three people voted for the slot for the exam.

I remind you, I think you guys voted, right?

If you didn't, so please do it.

And those who listen us offline, please vote.

Okay, so this is the last lecture.

I don't know how much I managed to tell you.

The point here that started from the previous time already is to show yet another collection

of examples where you can get bonus.

So we started with the denotational semantics and we have seen that denotational semantics

as something that provides examples of monads and that's the place where they rise naturally.

And another realm is algebraic data types.

So these are the monads which you typically use in Haskell because you first declare

an algebraic data type and then it turns out to be a monad.

And so what you start last time are monads.

So I can just say algebra.

So these are monads that arise from algebra in the sense, in the mathematical sense.

And these are traditionally the mathematical side of using monads and dealing with them.

And these are more like computer science but presently we can understand computationally

relevant monads in terms in algebraic terms.

I will try to show that.

And as you see this, this areas overlap because you can transfer from that side to that side

and there is something in common and there is something where there is some difference

but these are like three views and it's nice to have some understanding of monads in terms

of any of these approaches.

So I have already defined the concept of algebraic monads last time and postulated the theorem

that if you start with an algebraic theory and you consider terms, module law, equivalence

relation algebraic identified by the theories, then these terms or variables x from some

set x can be identified with the object t of x.

And that t which is derived from there can be shown to be a monad.

So I have to finish that construction because I claimed that that was a correct definition

but we need to verify this.

And I also mentioned that so correctness of the definition of t e.

I'm not sure if I introduce this notation.

Yes.

So that's the monad which arises from e.

And what we have to show is that our definition of the Clive's history, it doesn't depend

on the presentity of the equivalence class.

So we have to show.

So if we take some other t, then what sigma star of t is equal to sigma star of t prime.

Indeed.

So by definition, this thing is equal to

this thing is equal to this.

Here

and also.

So of course this t and t prime, they can have different sets of three variables.

But we can without loss of generality assume that these variables which you mentioned here,

they include both variables from t and t prime because I mean if some of the variables do

not occur in t, then the substitution just would not change the term.

So we always can extend the set of three variables that we involve.

And therefore.