| < Free Open Study > |
|
Before getting started, we need to establish some common notation and state a few basic mathematical facts. Most readers should just skim this chapter and refer back to it as necessary.
We use standard notation for sets: curly braces for listing the elements of a set explicitly ({...}) or showing how to construct one set from another by "comprehension" ({x Î S | ...} ), ø for the empty set, and S \ T for the set difference of S and T (the set of elements of S that are not also elements of T). The size of a set S is written |S|. The powerset of S, i.e., the set of all the subsets of S, is written P(S).
The set {0, 1, 2, 3, 4, 5, ...} of natural numbers is denoted by the symbol . A set is said to be countable if its elements can be placed in one-to-one correspondence with the natural numbers.
An n-place relation on a collection of sets S1, S2, ..., Sn is a set R ⊆ S1 × S2 × ... × Sn of tuples of elements from S1 through Sn. We say that the elements s1 Î S1 through sn Î Sn are related by R if (s1,...,sn) is an element of R.
A one-place relation on a set S is called a predicate on S. We say that P is true of an element s Î S if s Î P. To emphasize this intuition, we often write P(s) instead of s Î P, regarding P as a function mapping elements of S to truth values.
A two-place relation R on sets S and T is called a binary relation. We often write s R t instead of (s, t) Î R. When S and T are the same set U, we say that R is a binary relation on U.
For readability, three- or more place relations are often written using a "mixfix" concrete syntax, where the elements in the relation are separated by a sequence of symbols that jointly constitute the name of the relation. For example, for the typing relation for the simply typed lambdacalculus in Chapter 9, we write Г ⊢ s : T to mean "the triple (Г, s, T) is in the typing relation."
The domain of a relation R on sets S and T, written dom(R), is the set of elements s Î S such that (s, t) Î R for some t. The codomain or range of R, written range(R), is the set of elements t Î T such that (s, t) Î R for some s.
A relation R on sets S and T is called a partial function from S to T if, whenever (s, t1) Î R and (s, t2) Î R, we have t1 = t2. If, in addition, dom(R) = S, then R is called a total function (or just function) from S to T.
A partial function R from S to T is said to be defined on an argument s Î S if s Î dom(R), and undefined otherwise. We write f(x) ↑, or f(x) = ↑, to mean "f is undefined on x," and f(x)↓" to mean "f is defined on x.
In some of the implementation chapters, we will also need to define functions that may fail on some inputs (see, e.g., Figure 22-2). It is important to distinguish failure (which is a legitimate, observable result) from divergence; a function that may fail can be either partial (i.e., it may also diverge) or total (it must always return a result or explicitly fail)-indeed, we will often be interested in proving totality. We write f(x) = fail when f returns a failure result on the input x.
Formally, a function from S to T that may also fail is actually a function from S to T ∩ {fail}, where we assume that fail does not belong to T.
Suppose R is a binary relation on a set S and P is a predicate on S. We say that P is preserved by R if whenever we have s R s′ and P(s), we also have P(s′).
| < Free Open Study > |
|