Theory behind updating variable, state

[AdamBJ]

I'm a bit confused about the concept of state and the way the update function works. We can use the update function to update the contents of a variable like this:

Example aexp1 : aeval (update empty_state X 5) (APlus (ANum 3) (AMult (AId X) (ANum 2))) = 13.

We store 5 in X with the call to update empty_state X 5, so (APlus (ANum 3) (AMult (AId X) (ANum 2))) evaluates to 13.

But the textbook says "A state represents the current values of all the variables at some point in the execution of a program."

How can state represent the state of all the variables in a program and at the same time be used to update the value of a single variable in our program? Also, how does the update operation actually work? Here's the definition:

Definition update (st : state) (x : id) (n : nat) : state := fun x' ⇒ if eq_id_dec x x' then n else st x'.

The definition says " if the id x = the id x', then return n, otherwise return st x'. In plain English, what does this mean exactly? Does it say "if x = x' return the value stored in x, otherwise return"... what exactly? What is the meaning of st x'? Is it the current state of the program, ie the current values of all the variables in our program at the time update is called?

[jaewooklee93]

With the type state, you can think of it as a infinitely large memory indexed by all natural numbers. If you want to read a value from the memory, you should provide a type id, which is just a wrapper for nat. So, st x will return the value written in the position specified by x (Again, you can think that x is simply a natural number like 0,1,2,...). Either, you can think of that memory, or type state as a function from nat to nat as well.

You may be confused about the definition of update. Here you have to understand the notion of functional programming language first. There is no mutable persistent state recorded by the memory in the pure functional programming. However, we want to define such memory concept in the functional language Coq. So that objective looks contradictory at first glance.

The definition of update is a compromise. That function accepts an old memory st, position x to write and new value n, and then returns another memory, updated. We didn't change the value of old memory (and, in fact, we couldn't), however we just construct a newly updated memory. Now the problem is how to specifiy a new memory with respect to old one. It is given in the definition. Since you can consider the type state as a function, and function can be specified only if you specify what output will be returned for each input, you have to define the new memory by specifying its behavior with respect to the reading operation on the arbitrary position x'. If you want to read the value of new memory on x', first you have to check whether x' is equal to x. If they are same, you will read updated value n. Otherwise, you will read the value already written in the old memory, so you have to read st x' from the old memory st. That's enough for the definition of updated memory.

So that's all. I think your confusion was only due to the fact that you may not be familiar with the notion of functional programming.

[AdamBJ]

So to update "memory" at a position specified by x we take as input the current state of the program, ie st which represents the state of every variable in our program at the time we call update. We return from update a new state that reflects the change we wanted to make (ie location x has a new value n). Then, if our goal is to read the new state at location x' we first check if x' = x. If x'=x then we should return the value we just wrote to position x in the new state, since it's different than the value at location x' in the old state. If on the other hand x'!=x then we should return the value at position x' in the old memory - since we didn't update that position its value now will be the same as its value before the update.

The "memory" and "writing operations" I mentioned in my description of update are just conceptual though, there is no actual writing going on since this is all happening within the realm of functional programming.

[jaewooklee93]

I think you may understand correctly.

In C++, we may simply implement a memory with using a large block of array, and the update operation will simply update the element of that array. However, in Coq, memory should be implemented rather, a long chain of functions, starting from empty_state and every function in the chain completely relies on the previous function except for the value of only one updated cell. If we want to read a value from such memory, we have to begin at the tail of that chain (latest one) and then trace back to its head until we find the update we look for. Of course, Coq already did this process internally.

[AdamBJ]

Ok, that makes a lot more sense. Thank you!