0:00

Welcome again.

In this lecture, we will specify the natural numbers in the style of Peano.

So, how can we define the natural numbers?

Well, we will use the Peano

style for that.

That will not be particularly efficient but

it is very straight forward.

So we declare simply sort Not and this is the model.

0:44

So we have the element

zero in this model one.

And this is two, and so it goes on.

What we know is that number of elements can a most countably infinite

because we can only make.

Incountabley infinite number of terms using construct to zero into successor.

One of the problems is that the elements can be equal, so we have no guarantee

up until now that elements two and three are different, are equal.

>> And it can even be worse it could be that zero in

a particular model is even equal to one and two or

that even all elements in this model map to only one model elements.

And we will see later how we can deal with this by adding a mapping to the Booleans.

But first, let's be concerned with the question

of how to define a standard function for instance addition.

So we declare this function add as having two arguments of time Nat to time Nat.

And we simply define it on all possible patterns in

its arguments based on the cons zero, zero,

zero and begin to see this is a nice definition.

Because zero plus zero ought to be zero.

We need two variables.

If we add the zero to the successor of n so

the left-hand side represents n + 1.

And this can be written as n + 1 or the successor of n.

Similarly, the successor of n added to zero is the successor of n.

And this one is a slightly more complex, if we have the successor of n

to the successor of m, then we have at the left hand side, n+m+2, and this is equal

2:42

to the successor of that of n and the successor of m that also represents n+m+2.

And what you can see is the function add is applied to smaller objects

at the right, and that means that it is a good equation or a good rewrite rule.

Can we simplify these equations?

Well if can look at the first two equations we can see that the second

argument is always the result.

So we can simplify the first two,

by simply writing the add of zero of n is equal to n.

And can we simplify the second two also.

Well, it's not that straightforward, but

we can actually replace it by this single equation.

And that means that specification of addition, boils down to this,

namely this two equations characterize addition.

You can ask shouldn't we add the symmetric variance

showing add n,zero = n, like this to it?

And probably the add to the successor n and

m, about the add of n and the successor m like this.

And the answer to that is that it is not necessary

if you want to calculate the add on closed terms, where you don't have variables.

But if you have variables, the last two equations can be very useful.

And are therefore often added to certain specification.

Let's go back to this question of

guaranteeing that all the natural numbers are not equal.

So what we have to do is to use the only

fact that we know about elements that have to be not equal that we have available,

maybe that true is not equal to false, and for that we have to add some function.

From natural numbers to Booleans, and in this particular case we take

an arbitrary function at least smaller than and that can be defined as follows.

So, n is always smaller than zero, so n's smaller than zero.

Sorry, n is never smaller than zero.

So n smaller than zero is equal to false.

Zero is always smaller than n plus one.

5:05

So zero smaller successor n is true is defining rule.

And if we apply smaller than on the successor of n nth to the successor of n.

Then this is always equal to n smaller than m, and you can see that the right

hand side is a less complex expression than the left hand side, so

this is a good rewrite rule again.

5:28

So if we have edit this, how can we show that numbers are different?

So, let's take the three defining equations and put them here on top and

ask ourselves can we show that zero is not equal to successor of zero?

Or, in order to prove that we assume that

zero is equal to successor of zero and we will show that true is equal to false.

6:13

Using the assumption, we replace this first zero by the successor of zero.

So we get succ(zero) < succ(zero).

We can simplify this using the third equation.

And we obtain zero < zero.

And using the first equation, we get false.

So we have shown that true is equal to false,

if we assume that zero = succ(zero).

So, there cannot be a model where true is equal to false and hence,

there cannot be a model where zero is equal to the successor of zero.

So, what we know is that for all models that there are,

zero must be not equal to the successor of zero.

Well we can apply this for all expressions that you can write down with zero and

the successor of zero.

If these two expressions are not equal,

we can show that they are also not representing the same elements.

So this shows that all elements in the model must be different.

So typically what we get is that if we specify the natural numbers and we add

7:41

So given if we have these constrictors, we actually have an induction principle on

natural numbers and that's exactly the induction principle that we know.

So, suppose we would like to proof a property on all natural numbers.

And what we have to do is prove this property on zero.

And we have to prove this property for the successor of n for any number, n.

Assuming that you already know that the property holds for n.

And if this has been known,

we can conclude that a property has been proven for all natural numbers.

So how can we visualize this?

Let's have the natural numbers here.

So, put zero here, successful zero at this spot, two, three.

8:35

And all the other numbers.

Now, with the first line we have proven a property for zero.

So the property fi holds for zero.

Now if we look at the second line we see that because the property holds for

zero it's also valid for the successor of zero.

And because we have now have proven it for successor of zero,

we now also know that it holds for the successor of zero.

And this goes on and you can see that it holds for all numbers.

9:52

Okay, let's do an exercise.

If we want to specify multiplication and

we get these two equations for that,

is this a correct specification of multiplication

in the sense that we know multiplication.

And now let's do the same for subtraction.

So if we give the following rules for subtraction,

all natural numbers, is this well defined, okay?

We gave specification of natural numbers in the style of Peano.

As I said, not particularly efficient, but quite insightful.

We showed how we can guarantee that all

the elements in the model of the natural numbers

are different by giving a mapping to the Booleans.

And we indicated how the constructors gave rights to the induction principle on

the natural numbers and we will see that such induction principles also exist for

all other data types that we can define with constructors.

In the next lecture I will show you how we can actually specify

efficient numbers.

Thank you for watching.