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
Instead 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 isand
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
and
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.
