# Expressing semantics of an array as a function

An assignment questions asks the following:

Consider an array 'var a : array[1..10] of real'. Express the semantics of this array as a function, defining the domain and codomain (you might also be able to write the rule). In this programming language, the subrange '1..10' is viewed as a genuine type, so we can comfortably say that 'a[13]' is a type error.

I've come up with a semantic that works as a function, that is: f(a[$x$]) -> $y$ where $x$ is a type defined by the numbers $1$ to $10$ and $y$ is the set of all Real numbers. Does this seems correct?

Would there be any difference if I wrote the function in the opposite way, that is: f($y$) -> a[$x$] ?

-
The question is ill-defined, unless you can provide more context. The standard way of encoding arrays as functions is to use a state monad and two functions, one for accessing and one for setting the values of the array. –  Andrej Bauer Jan 27 '13 at 20:44
@AndrejBauer Encoding an array as a mapping from indices to values is quite common (for example in Hoare logic). –  Gilles Jan 27 '13 at 22:21

First of all, an array is and has always been a function. It is a function from the set of indices (1..10 in your example) to memory locations that hold the array elements. When we write $a[i]$ in the programming language, we are just using stylized notation for saying $a(i)$, i.e., apply the function $a$ to $i$ and give me the location that it represents. When we write $$a[i] := a[i] + 1$$ we are using the memory location $a(i)$ both on the left and the right hand side of the assignment statement. On the left, it means the location itself (also called an L-value) and, on the right, it means the contents of the location (also called an R-value).

So, treating is an array as a function is no big deal. It is like calling a spade a spade.

However, what your professor wants you to do is to think of the array as a function from the set of indices to data values (like real numbers). No memory locations in the picture. That involves a bit more thinking and some rethinking.

In this view, $a$ is a variable whose value is an entire array value (which is now a function) and $a(i)$ is a real number. That represents the R-value of what we normally write as $a[i]$. What do we do about its L-value? Well, it doesn't exist, in this view. So, we think of an assignment to a subscripted variable, like the one I have shown as above, as really meaning an assignment to the array variable $a$, like this: $$a := a[i: a(i)+1]$$ Here, the right hand side means "a function $a'$ that is just like $a$, except that the value of $a'(i)$ is going to be $a(i)+1$". So, we take the old function value of $a$, tweak it little to obtain a new function value, and assign it to $a$. Remarkably, with this little bit of rewriting, everything works!

It is quite remarkable that one of our most basic data structures should allow such radically different views. When we add procedures, things get a bit more complicated in the second view, because, as I said, there are no L-values for subscripted variables in this view. However, there are more abstract forms of L-values (called "acceptors") that can be used to deal with subscripted variables as procedure parameters. So, it all works fine.

For an introductory treatment of the two views, see J. C. Reynolds, Craft of Programming, Chapter 2. In particular, the introduction of the chapter, and the section 2.2.8, cover the two views.

-

It makes little sense to think about how we are to encode an array as a function without explaining how we intend to implement the basic array operations. The characteristic property of an array is that we can

1. access the $i$-th element, and

2. set the $i$-th element.

In addition, certain equations must be satisfied. For example, if we look up the $i$-th element twice in a row, we will see the same value, etc. (These equations can be looked up in any standard source on the state monad.)

Now, it is quite obvious that an array can be encoded as a function. But we also have to implement get and set. Here is how we might do it in Haskell.

-- An array is represented as a function from integers to floats.
type Array = Int -> Float

-- create a new array all of whose elements are initialized to 0.0
new :: () -> Array
new () = \i -> 0.0

-- get a i returns the i-th element of aray a
get :: Array -> Int -> Float
get a i = a i

-- set a i x returns the array a, but with i-th element set to x
set :: Array -> Int -> Float -> Array
set a i x = \j -> if j == i then x else a j


We are not checking and bounds here, which we should. It may seem a bit unusual that set returns a new array, but there really is no way of modifying an existing one in a purely functional setting. Haskell has the so-called "monadic style" of programming which makes it much easier to work with this sort of encoding (although I wouldn't recommend the encoding for a real appliaction).

-

The function is defined as follows, given array $a$, for $1 \leq i \leq 10$, $$f(i) = a[i].$$

The domain is thus $\text{dom}(f) = \{1,2,3,4,5,6,7,8,9,10\}$ and the codomain is simply $\text{codom}(f) = \bigcup_{i=1}^{10}f(i) = \bigcup_{i=1}^{10}a[i] \subset \mathbb{R}$.

-
This is certainly not the answer, and if it is, the question is totally bogus. –  Andrej Bauer Jan 27 '13 at 20:44
This is what I mentioned in my question, but Andrej is saying it's totally bogus. Nonetheless I believe this is the answer my professor is looking for (he's totally bogus too) –  Imray Jan 27 '13 at 21:05
@AndrejBauer I interpreted the question in the sense that it might be an introduction to programming question, not a category theory type theory question. Imray: Can you provide information on the course this question appeared? –  Pål GD Jan 27 '13 at 21:13