2.3. Currying and tuples
Formalizing operations and relations
To formalize in set theory every notion of operation
(resp. relation) with any fixed
arity n>1, acting as n-ary structures between n sets, would involve the
following symbols (generalizing the case n = 1 of functions which we took as primitive):
- A list of n domain functors (sometimes not available but not needed since
domains are usually fixed by the context);
- Its evaluator is an (n+1)-ary operator (resp. predicate) written in filled form as
f(x0,…,xn−1),
with arguments one n-ary operation (resp. relation) f, and its
n arguments x0,…,xn−1;
- Its definer binds n variables to their respective ranges on a term (resp. a formula).
Let us give to the operation definers, the following notation which will
be later (2.7) justified as reflecting their definitions: in the binary case (n = 2), operations
defined by a binary operator A with domains E and F will be written
E×F ∋ (x,y) ↦ A(x,y)
After seeing what operations and relations are (which role they play) let us discuss how
they are reducible to something else.
One aspect is that relations are reducible to operations, and vice-versa:
- The notion of n-ary relation can be constructed as a class of n-ary
operations, by taking the Boolean pair as target set, as we did in 1.4 (for predicates) and will
formalize in 2.4.
- Inversely, the notion of n-ary operation can be constructed as a
class of (n+1)-ary relations (2.7).
These constructions can be useful despite their circularity (they are not decreasing
the arity). But for foundational purposes, we need a construction which reduces to lower arity
cases, down to sets and functions. There are actually 2 such constructions.
Currying
The simplest constructions of the notions of n-ary operation from our primitive tools for functions,
are their curried representations, defined as classes of functions by expressing the operation definer
as n successive uses of the function definer (one for each bound variable); and thus the
evaluator as n uses of the function evaluator. For n=2, this means a
binary operation in curried form b with domains E and F, is defined from a binary
operator B, and evaluated back as B, by the formulas
b = (E ∋ x ↦ (F ∋ y ↦ B(x,y)))
Dom b = E ∧ ∀x∈E, Dom b(x) = F
∧ ∀y∈F, B(x,y) = b(x)(y)
whose equivalence, similar to the axiom
1. for functions, is deducible from it.
The first domain functor comes
as Dom b = E, but the second one, given as common value of all
Dom b(x), is only definite for E ≠ ∅.
The intermediate function b(x) = (F ∋ y
↦ B(x,y)) represents the functor defined by
B with parameter x (free) and argument y (bound).
This somehow makes each binary operation work as a function evaluator,
by giving x the role of a function with argument y ; the curried
function evaluator just gives back each function it takes : f ↦
((Dom f) ∋ y ↦ f(y)).
Similarly, the notion of n-ary relation can be defined in curried form as a class,
giving the role of definer to a succession of n−1 uses of the function
definer and 1 use of the set-builder.
The curried form r of a binary relation with domains E and F, is so defined
from a binary predicate R, and evaluated back as R,
by the equivalent formulas
r = (E ∋ x ↦
{y ∈ F | R(x,y)})
Dom r = E ∧ (∀x∈E, r(x) ⊂ F
∧ ∀y∈F, R(x,y) ⇔ y ∈ r(x))
This leaves no way to define second domain functor (F cannot be restored
from r).
These constructions have the defect of breaking the symmetry
of role between arguments. The next construction method, by tuples, will preserve
this symmetry, and will be usually preferred for this reason.
Tuples
For any theory and any natural number n, a notion of n-tuple is a notion
constructed for its variables to serve as abbreviations for a pack of n variables
from previous notions.
A 2-tuple is called an ordered pair, a 3-tuple is a triple, a 4-tuple is a
quadruple and so on. So each tuple x (so constructed object) represents
a meta-function of "interpretation" from this list (meta-set) of n variables, into
the model. The definer and evaluator symbols for tuples take a
special form because, while tuples are meta-functions, the role they play in the
theory differs from those of functors or functions.
An n-tuple definer is not a binder but an n-ary operator, packing its
n variables into one by taking them as its arguments in a
parenthesis and separated by commas: ( ,…, ).
Now, each structure
(resp. operation, relation) can be re-formalized as a unary structure (resp. a function,
a unary relation) with domain a type (resp. a class which is actually a set) of tuples, to be
used with the relevant tuples definer. This can be implicitly done by re-interpreting the notation:
S(x,y) can be read seeing S either as a binary
structure (resp. operation, relation), or as a unary one taking as argument the
ordered pair given by the term (x,y) formed by the ordered pair definer
with arguments x and y.
The role of n-tuple evaluator is played by a list of n functors
called projections which extract each variable from the given pack.
This list plays the role of the function evaluator curried in the reverse way, by fixing its
meta-argument whose range (the domain of tuples as meta-functions) is not seen by
the theory as a set of objects but as a list of n symbols to be taken separately.
The formal details of this construction depend whether we take a generic theory or a
set theory. Tuples axiom
In generic theories, it must be a distinct constructed type for not only each n
but also each choice of the type of each of these n variables (if starting from
a theory with multiple types - this choice of a list of variables with their types amounts
to the choice of a predicate
symbol type), but this directly forms a
legitimate construction (4.11).
For n=2 (other cases are similar), and a type P of ordered pairs
(x,y) where x,y have
types E and F, the projections π0 and π1
are related to the ordered pair definer, by the axiom
∀E x, ∀F y,
∀P z, (x = π0(z) ∧ y =
π1(z)) ⇔ (x,y) = z
which implies
∀P z, (π0(z),
π1(z)) = z
∀E x,
∀F y, π0(x,y) = x
∀E x, ∀F y,
π1(x,y) = y
∀E x,x', ∀F y,y',
(x,y) = (x',y') ⇔ (x = x' ∧ y = y')
Tuples in set theory
Set theory having no types only needs one notion of n-tuple for each n.
But it faces one difficulty : in order to rigorously justify that all tools of set theory remain
applicable to tuples in the same way as to the rest of elements, tuples need to be
integrated among elements. Namely, set theory needs to develop its notions of tuples
by defining them as classes of already existing elements, instead of simply accepting
them by the above constructions, which would leave them as separate types.
For this, since tuples are meta-functions, they are naturally represented by functions.
This involves copying their meta-domain, which is a list of symbols, into a set (of
elements). Namely, let us represent the domain of considered n-tuples by the set
Vn of n numbers from 0 to n−1 all named by constant
symbols we shall simply conceive as digits. To justify this as a development
of set theory, these digits can be defined by any ground terms with distinct
values, such as ∅, {∅}, {∅, {∅}} and endlessly many more sets and
functions expressed from there. The notion of n-tuple is then defined
as the class of all functions with domain Vn.
Then, the projections are defined by the function evaluator applied to the respective
digits, which can be read as disguised in their notations : for all n-tuples x,
∀i∈Vn, πi(x) =
x(i).
This index notation, making a pun of the equivalence between reading
the index i as an argument or a meta-argument that means to take the i-th
symbol from a list (here πi is the i-th projection), is also commonly
used for tuples : xi can be either read as the i-th variable in
the tuple x = (x0,…,xn−1), or as a third
notation for the same evaluator after x(i) and πi(x).
More tools need to be introduced before defining in set theory the
tuple definers (2.4) and the operation definers working with tuples (2.7).
Other languages:
FR : 2.3. Curryfication et uplets