Metamath Proof Explorer


Table of Contents - 20.43.22.13. N-ary functions

According to Wikipedia ("Arity", https://en.wikipedia.org/wiki/Arity, 19-May-2024): "In logic, mathematics, and computer science, arity is the number of arguments or operands taken by a function, operation or relation."

N-ary functions are often also called multivariate functions, without indicating the actual number of argumens. See also Wikipedia ("Multivariate functions", 19-May-2024, https://en.wikipedia.org/wiki/Function_(mathematics)#Multivariate_functions): "A multivariate function, multivariable function, or function of several variables is a function that depends on several arguments. ... Formally, a function of n variables is a function whose domain is a set of n-tuples. For example, multiplication of integers is a function of two variables, or bivariate function, whose domain is the set of all ordered pairs (2-tuples) of integers, and whose codomain is the set of integers. The same is true for every binary operation. Commonly, an n-tuple is denoted enclosed between parentheses, such as in ( 1 , 2 , ... , n ). When using functional notation, one usually omits the parentheses surrounding tuples, writing f ( x1 , ... , xn ) instead of f ( ( x1 , ... , xn ) ). Given n sets X1 , ... , Xn , the set of all n-tuples ( x1 , ... , xn ) such that x1 is element of X1 , ... , xn is element of Xn is called the Cartesian product of X1 , ... , Xn , and denoted X1 X ... X Xn . Therefore, a multivariate function is a function that has a Cartesian product or a proper subset of a Cartesian product as a domain: where where the domain has the form ."

In the following, n-ary functions are defined as mappings (see df-map) from a finite sequence of arguments, which themselves are defined as mappings from the half-open range of nonnegative integers to the domain of each argument. Furthermore, the definition is restricted to endofunctions, meaning that the domain(s) of the argument(s) is identical with its codomain. This means that the domains of all arguments are identical (in contrast to the definition in Wikipedia, see above: here, we have X1 = X2 = ... = Xn = X).

For small n, n-ary functions correspond to "usual" functions with a different number of arguments:

- n = 0 (nullary functions): These correspond actually to constants, see 0aryfvalelfv and mapsn:

- n = 1 (unary functions): These correspond actually to usual endofunctions, see 1aryenef and efmndbas:

- n = 2 (binary functions): These correspond to usual operations on two elements of the same set, also called "binary operation" (according to Wikipedia ("Binary operation", 19-May-2024, https://en.wikipedia.org/wiki/Binary_operation): "In mathematics, a binary operation or dyadic operation is a rule for combining two elements (called operands) to produce another element. More formally, a binary operation is an operation of arity two. More specifically, a binary operation on a set is a binary operation whose two domains and the codomain are the same set." Sometimes also called "closed internal binary operation"), see 2aryenef and compare with df-clintop: .

Instead of using indexed arguments (represented by a mapping as described above), elements of Cartesian exponentiations (see df-finxp) could have been used to represent multiple arguments. However, this concept is not fully developed yet (it is within a mathbox), and it is currently based on ordinal numbers, e.g., , instead of integers, e.g., , which is not very practical.

The definition df-ixp of infinite Cartesian product could also have been used to represent multiple arguments, but this would have been more cumbersome without any additional advantage. naryfvalixp shows that both definitions are equivalent.

  1. cnaryf
  2. df-naryf
  3. naryfval
  4. naryfvalixp
  5. naryfvalel
  6. naryrcl
  7. naryfvalelfv
  8. naryfvalelwrdf
  9. 0aryfvalel
  10. 0aryfvalelfv
  11. 1aryfvalel
  12. fv1arycl
  13. 1arympt1
  14. 1arympt1fv
  15. 1arymaptfv
  16. 1arymaptf
  17. 1arymaptf1
  18. 1arymaptfo
  19. 1arymaptf1o
  20. 1aryenef
  21. 1aryenefmnd
  22. 2aryfvalel
  23. fv2arycl
  24. 2arympt
  25. 2arymptfv
  26. 2arymaptfv
  27. 2arymaptf
  28. 2arymaptf1
  29. 2arymaptfo
  30. 2arymaptf1o
  31. 2aryenef