One of the most basic ways of building new objects in mathematics and programming involves the ordered pairing constructor. For example, in mathematics one builds rational numbers as pairs of integers and complex numbers as pairs of reals. In programming, a data processing record might consist of a name paired with basic information such as age, social security number, account number and value of the account, e.g., . This item might be thought of as a single 5--tuple or as compound pair . In Nuprl we write for the pair consisting of a and b; n--tuples are built from pairs.
The rules for pairs are simpler than those for functions because the canonical notations are built in a simple way from components. We say that is a canonical value for elements of the type of pairs; the name is canonical even if a and b are not canonical. If a is in type A and b is in type B then the type of pairs is written and is called the cartesian product . The Nuprl notation is very similar to the set--theoretic notation, where a cartesian product is written ; we choose as the operator because it is a standard ASCII character while is not. In programming languages one might denote the cartesian product as , as in the Pascal record type, or as , as in Algol 68 structures.
The pair decomposition rule is the only Nuprl rule for products that is not as one might expect from cartesian products in set theory or from record types in programming. One might expect operations, say and , obeying
andInstead of this notation we use a single form that generalizes both forms. One reason for this is that it allows a single form which is the inverse of pairing. Another more technical reason will appear when we discuss dependent products below. The form is
,where p is an expression denoting a pair and where b is any expression in u and v. We think of u and v as names of the elements of the pair; these names are bound in b. Using spread we can define the selectors and as
Figure: Rules for Cartesian Product
Figure lists the rules for cartesian product. These rules allow us to assign types to pairs and to the spread terms. We will see later that Nuprl allows variations on these rules.