Mappings

Two sets may be related to each other in a variety of ways. One important type of relation is the mapping of one set to another.

To introduce this idea, consider the set U of all authorised users of a main-frame machine. User $u \in U$ has a user-number which we suppose is a positive integer which we can denote by a(u). For instance if John Smith is an authorised user (and so is a member of the set U) and has user-number 2136, then we can write $a(John \enskip Smith) = 2136$. We observe that, in general, each element $u \in U$ will give rise to a specific and unique element $a(u) \in \Nat$. This relationship is an instance of a mapping of U to $\Nat$, where in this example, a is the user-number mapping. Formally, we use the notation

$a \enskip : \enskip U \rightarrow \Nat$

to mean that a is a mapping (or map) of U to $\Nat$. The above notation also defines a signature for the mapping.

The application of functions and mappings is one of the most commonly used techniques in formal specification methodologies and indeed, the concept of mappings plays a key role in computer science with wide-ranging applications. One way to think of a mapping f is to treat it as a function which takes an input and transforms this input into an output, so that symbolically

f(input) = output

In this context, a Pascal compiler can be thought of as a function which takes a high-level source program as input and transforms it into the corresponding object program (the output). One essential characteristic of this (and any) mapping is the uniqueness of the output (result) !

On a more concrete level, use of finite maps such as finite sets of (index,value) or (key,value) pairs underlies the implementation of such data structures as arrays, hash-tables, keyed files and colour look-up tables. Mappings also play a crucial role in operating systems, for example dynamic address translation mechanisms need to maintain address translation maps illustrating which virtual storage locations are currently in real storage and exactly where they are.