The following content has been provided by the University of Erlangen-Nürnberg.

We just moved to what we are here to do.

So in the last lectures you've been seeing definitions of data types by co-induction or co-data types.

And you've seen how to write functions, building such kind of data types,

and how to prove certain properties about them using co-induction and by simulations.

In the last lecture last Monday you saw an example of a co-data type that involved sums.

So that was possibly infinite streams, lists of things that could either finish or run infinitely.

And I think you saw some function definitions using it,

but you didn't manage to see what the by simulation notion that corresponds to it.

So today we are going to do a similar example and try to pay more attention

at what's the by simulation notion and how to prove things in this case.

So we will be doing this by example. I mean we will build an example and elaborate it.

So I don't know if you play computer games. I used to. I don't do anymore, but these days there are many, many games

which use this thing called computer generated terrains where you play and there wasn't some guy,

some level designer drawing the levels, but they are generated on the fly by a program.

And this idea of having a dynamic terrain, this data type corresponding to dynamic terrain

is another example of a dynamic thing that can be modeled using co-data types.

So because this is not a course on game programming and we want to do something which is simple and can fit just half of a blackboard or something,

we will use a simplification. So we will think of a very, very silly type of terrain for some game

where we have some sort of first person game and at each screen we see some objects scattered around

of which we won't care very much what these objects are, trees, weapons, people, whatever, they just fit on the screen.

And then in each scenario we have two alternatives. Either the scenario has nowhere else to go

and we are stuck there, we've reached the end of the universe, or we have two alternatives.

We have two paths. That branch we can decide to move left and see what's there or move right and see what's there.

There we will find again one of these settings with objects and perhaps a fork, perhaps we are stuck.

It's a very, very simple setting. And already this idea of a terrain, very simple terrain, we can model it using a co-data type.

Let's write the definition. We are defining another type for a terrain.

And as I said, the terrain can list, we can see in each screen several objects, we don't care what those objects will be.

Weapons, people, whatever, so we will just make this type parametric on the possible objects we could have.

So here A, you think about some game element, whatever.

And then what are the observers of this co-data type?

Well, I will include one observer which I will call objects, which just gives us the list of objects we can see on the current screen.

So this will be a function from a terrain and let's say this gives us a list of A's. Maybe there's nothing, maybe we have a tree and a sword.

And as I said before, we have two possible cases. We are either stuck and there's nowhere to go forward, we are on a dead end, or we have a junction and we have two directions to choose.

So in the first case where we are stuck, we include for that observer that end that can only be applied to a terrain where we are stuck effectively.

So I use the label stuck for this kind of terrain we could have.

And there's no additional information there. If we are stuck, we can apply this observer, but we know what we will see.

This is just to give an observer that will allow us to say that we are in the stuck case.

If on the other hand, our terrain, the current place where we are now is a junction, then we have two options.

We can move left or we can move right. So we can add observers for those cases.

I will use junction to name this alternative where we can be, where we have a junction.

And the left observer sends us to another terrain, the result of picking the left, the road that goes to the left, and right gives us the result of going to the right.

I'll be pressing the wrong button for the rest of the afternoon.

So this defines our very simple, naive data type for a dynamic terrain on a very simple and rather boring game.

If we want to look at it as a co-algebra, this would correspond to a co-algebra.

So we have a function for a function that we can call T sub A of X, just to give it one name.

And what this is, well, what we have is a list of A's in every position.

So we have the star means list of A's and we also have, so we take a product, two alternatives.

Either we have, well, the unit when we are in this case, or we have two Xs. Sorry, this is alternative.

We can have the unit when we are in the stack case, or we have a product of two Xs. This means X times X.