Also see Pairs for newer supplementary material.

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

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.

Thu Sep 14 08:45:18 EDT 1995