nLab binary function

Idea

A binary function, or function of two variables, is like a function but with two domains. That is, while a function $f$ from the set $A$ to the set $C$ maps an element $x$ of $A$ to a unique element $f(x)$ of $C$, a binary function from $A$ and $B$ to $C$ maps an element $x$ of $A$ and an element $y$ of $B$ to a unique element $f(x,y)$ of $C$.

We can generalise further to multiary functions, or functions of several variables.

Definitions

The possible definitions depend on foundations; for us, the simplest is probably this:

Definition

A binary function from $A$ and $B$ to $C$ is simply a function $f$ to $C$ from the binary cartesian product $A \times B$. We write $f(x,y)$ for $f((x,y))$.

This is natural in structural set theory; it makes sense in any set theory and (suitably interpreted) in a foundational type theory.

In material set theory, one often declines to specify the domain of a function (since this can be recovered from it); then we can say this:

Definition

A binary function to $C$ is simply a function $f$ to $C$ such that every element of the domain of $f$ is an ordered pair. Again, we write $f(x,y)$ for $f((x,y))$.

An equivalent (but different) definition in material set theory is this:

Definition

A binary function to $C$ is a ternary relation $f$ such that

• given $(x,y,z) \in f$, we have $z \in C$, and
• given $(x,y,z) \in f$ and $(x,y,z') \in f$, we have $z = z'$.

Now we write $f(x,y)$ for the unique $z$ (if any) such that $(x,y,z) \in f$.

Either way, the material concept is actually more general than the structural one, because the domain of a material binary function might not be a cartesian product. The link is provided by the binary version of a partial function:

Definition

A partial binary function from $A$ and $B$ to $C$ is a function to $C$ from a subset of $A \times B$.

One can also define a notion of binary function without any notion of ordered pair, as long as one has the set of functions from any set to any other set. This is called a curried representation.

Definition

A binary function from $A$ and $B$ to $C$ is a function from $A$ to the set $C^B$ of all functions from $B$ to $C$.

The connection is that if $f$ is a binary function defined as having ordered pairs in its domain, the corresponding function from $A$ to $C^B$ sends $a\in A$ to the function that sends $b\in B$ to $f(a,b)\in C$. One can give a similar comparison of material and structural versions of this definition. In addition, this definition is usually the one used in type theory.

It's also possible to take the concept of binary function as an undefined primitive concept, on the same level as that of function. Then we want axioms such as the following (depending on the style of foundations):

• Given an element $x$ of the set $A$, an element $y$ of $B$, and a binary function from $A$ and $B$ to $C$, we have an element $f(x,y)$ of $C$.

• If $x$ and $x'$ are equal elements of $A$ and $y$ and $y'$ are equal elements of $B$, then $f(x,y) = f(x',y')$.

• Given two such binary functions $f$ and $f'$, if $f(x,y) = f'(x,y)$ for every $x$ in $A$ and every $y$ in $B$, then $f = f'$.

Internalization

The cartesian-product-based definitions make sense internal to any category with binary cartesian products. More generally, we can consider any monoidal category.

Similarly, the curried definition makes sense internal to any closed category. The cartesian analogue of a closed category (not to be confused with a cartesian closed category, which also has finite products) exists but is not well-known.

Finally, the undefined concept of “binary function” can be internalized to the binary morphisms in any multicategory, in particular perhaps a cartesian multicategory. If a multicategory has tensor products, then its binary morphisms are representable in the ordered-pair style, while if it has hom-objects, they are representable in the curried style; but in general a multicategory may have neither.

Special cases

A binary function to the set of truth values is a binary relation.

A binary function from $A$ and $A$ to $C$ may be simply called a binary function from $A$ to $C$.

A binary function $f$ from $A$ to $C$ is symmetric if $f(a,b) = f(b,a)$ always.

Related concepts

• binary function, bilinear map, multilinear map

• binary morphism, multimorphism

• bifunctor, Quillen bifunctor