nLab
binary function

Contents

Idea

A binary function, or function of two variables, is like a function but with two domains. That is, while a function ff from the set AA to the set CC maps an element xx of AA to a unique element f(x)f(x) of CC, a binary function from AA and BB to CC maps an element xx of AA and an element yy of BB to a unique element f(x,y)f(x,y) of CC.

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 AA and BB to CC is simply a function ff to CC from the binary cartesian product A×BA \times B. We write f(x,y)f(x,y) for f((x,y))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 CC is simply a function ff to CC such that every element of the domain of ff is an ordered pair. Again, we write f(x,y)f(x,y) for f((x,y))f((x,y)).

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

Definition

A binary function to CC is a ternary relation ff such that

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

Now we write f(x,y)f(x,y) for the unique zz (if any) such that (x,y,z)f(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 AA and BB to CC is a function to CC from a subset of A×BA \times B.

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 xx of the set AA, an element yy of BB, and a binary function from AA and BB to CC, we have an element f(x,y)f(x,y) of CC.

  • If xx and xx' are equal elements of AA and yy and yy' are equal elements of BB, then f(x,y)=f(x,y)f(x,y) = f(x',y').

  • Given two such binary functions ff and ff', if f(x,y)=f(x,y)f(x,y) = f'(x,y) for every xx in AA and every yy in BB, then f=ff = f'.

Internalisation

We could conceivably have the notion of binary function without the notion of cartesian product; then a binary function could not be understood as a special case of a function. I doubt that anybody has proposed such a foundation of mathematics, but there are situations where this is true in some internal logic.

In particular, a binary function internal to a multicategory is simply a binary morphism in that multicategory. This is most like a binary function between sets in the case of a cartesian multicategory. But even so, there may be no tensor product in the multicategory, and then a binary morphism cannot be understood as a special case of a morphism.

Revised on September 2, 2012 06:53:03 by Toby Bartels (98.23.143.147)