Chapter 2: Mathematical Preliminaries

 < 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.

2.1 Sets, Relations, and Functions

2.1.1 Definition

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).

2.1.2 Definition

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.

2.1.3 Definition

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.

2.1.4 Definition

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.

2.1.5 Definition

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.

2.1.6 Definition

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."

2.1.7 Definition

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.

2.1.8 Definition

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.

2.1.9 Definition

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.

2.1.10 Definition

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 > 



Types and Programming Languages
Types and Programming Languages
ISBN: 0262162091
EAN: 2147483647
Year: 2002
Pages: 262

flylib.com © 2008-2017.
If you may any questions please contact us: flylib@qtcs.net