25
$\begingroup$

I am self-studying and have a basic or naive question that follows from a simple observation. I have also included tags for type theory, etc because "evaluation" probably has a different meaning in these constructive approaches, which I'm also curious about.

Any set $X$ with elements $x_i$ can be characterized by a set denoted $(X)$ of pairs $(\star, x_i)$, alternatively denoted $(\star \mapsto x_i)$ (for all $x_i \in X$). Each one of these latter pairs encodes a distinct function from common domain $\{ \star \}$ to (each different element of) $X$. If we name such functions after their image, i.e. $(x_i):\star \mapsto x_i$, then the symbol "$f(x_i)$", traditionally interpreted as function evaluation, is reinterpreted as function composition, i.e. $f\circ (x_i)$ and the $\circ$ is often notationally suppressed. And roughly, $f = \cup_xf(x)$, every function decomposes to a unique set of singleton functions (better word?).

Question: Is there anything more to evaluation, or can I exactly equate evaluation with composition and forever de-clutter my mind of the term "evaluation"? Is the above perspective unusual or fruitful beyond reducing terminological clutter?

The notion of evaluation above - perhaps "extensional" is the right term? - means essentially subsetting the function at the chosen argument $x$. Perhaps I will see that a full answer to my question requires considering an intentional (?) or constructive perspective on "evaluation" (as in lambda calculus, etc). Perhaps only there will composition and evaluation legitimately have distinct meanings.

Edit: The notation $(x)$ seemed the most natural way to denote any function with singleton domain because it coheres with the conventional way to write evaluation as $f(x)$. The notation seems unambiguous because there is no context I can think of, other than "evaluation", where a single symbol, say $x$, is enclosed in brackets "()"? It does seem useful to notationally distinguish functions on singleton domain in some way: I would like the notation to be a mnemonic for whether the resulting function composite is a singleton function (i.e. a "value" like $f(x_i) = f \circ (x_i) = (\star, y_j)$) versus a non-singleton function. Perhaps there is a conventional notation for functions from singleton domain, other than $(x)$ and a conventional name for such functions, other than "singleton functions"?

$\endgroup$
1
  • 10
    $\begingroup$ This idea is really at the heart of category theory. It's a great insight! $\endgroup$
    – N. Virgo
    Jan 29 '21 at 12:53
16
$\begingroup$

Thatโ€™s right, evaluation is not in any serious way distinct from composition with a function with singleton domainโ€”or to remove all talk of elements entirely, a function whose domain is a terminal object. This kind of function can entirely replace the role of elements, which is at the heart of the categorical axiomatization of set theory called ETCS.

$\endgroup$
2
  • 1
    $\begingroup$ Thanks for the sanity check! $\endgroup$
    – JRC
    Feb 1 '21 at 9:16
  • $\begingroup$ RE: my edit, I wonder if there is another notation for functions from singleton domain, other than "(๐‘ฅ)" and an official name for such functions, other than "singleton functions". $\endgroup$
    – JRC
    Feb 1 '21 at 9:33
13
$\begingroup$

Basically, yes, what you are saying is that in the category of sets and functions the action of composition of $f\colon A\to B$ with $(a)\colon \star \to A$ is precisely encoding function evaluation $f(a)$. So this can indeed neatly be written as $f(x)=f\circ (x)$. This paves the way to thinking about functions and elements in a dual way: a function $f\colon A\to B$ is a machine that converts elements of type $A$ into elements of type $B$; dually an element of type $A$ is a thing that any machine $f\colon A\to B$ can act on to turn into something of type $B$. This tells us that we can take elementhood as primitive and define functions in terms of elements (as is classically done) or that we can treat functions as primitive and define elementhood in terms of functions (as is categorically done). In some sense, for sets and functions (at least naively) the two approaches agree.

However, in many other situations the two options are very different. Suppose that instead of sets and functions your world consists of the non-negative reals $[0,\infty ]$ (with $\infty $ thrown in) and you keep track of magnitude by means of $x\to y$ iff $x\ge y$. The special element $0$, the additive neutral element, serves here as the 'singleton' $\star$ (the reason is that a singleton set is neutral (up to isomorphism) with respect to the cartesian product of sets; similarly $0$ is neutral with respect to addition of real numbers). Now, in the world of sets the arrows $\star\to A$ encode the elements of $A$. What is encoded in the world of non-negative reals? Well, $\star \to a$ is no simply saying that $a=0$. So, if $a=0$, then it has a unique 'element' while any $a>0$ has no elements at all.

This is probably not surprising since real numbers are quite different from sets. Places that behave more like sets than real numbers are called toposes. But there is really no need to abandon the "composition=evaluation" paradigm in non-toposes. Indeed, evaluation can further be understood in terms of a much simpler operation. Going back to sets, if $[A,B]$ is the set of all functions $f\colon [A\to B]$, then the evaluation mapping is $\mathrm {ev}\colon [A,B]\times A\to B$ given by $\mathrm {ev}(f,a)=f(a)$. This evaluation function has a very special universal property. If $f\colon T\to [A,B]$ is any function from any set $T$ we can form the composition $\mathrm {ev}\circ (f\times \mathrm {Id}_A)$ to get a function $h\colon T\times A\to B$. But also conversely, any such function $h$ arises uniquely in this way from a function $f\colon T\to [A,B]$.

In other words, there is a natural bijection between functions $f\colon T\to [A,B]$ and functions $h\colon T\times A\to B$. The translation is performed universally by the evaluation function. So, we observe that the internal notion of the set of all functions $[A,B]$ together with the notion of evaluation is fully encoded by the much simpler notion of the cartesian product of sets. The encoding is done by stating the natural bijectiveness above. The technical way of saying it is that evaluation is the counit of an adjunction whose right adjoint is cross multiplying with a fixed set $A$.

Now we can replace the world of sets and functions with their cartesian product by other things. For instance, non-negative real numbers, magnitude comparison, and addition. It turns one (nice exercise) that there is here too an internal notion of "the real numbers of all magnitudes from $a$ to $b$", namely $[a,b]$, complete with an evaluation mapping with formally the same properties as for sets. Such places are called closed monoidal categories.

$\endgroup$
4
  • $\begingroup$ Thanks very much. There is so much meat here. Just to connect two ideas, I guess from within the "functional" perspective, your evaluation mapping - given by ev(๐‘“,๐‘Ž)=๐‘“(๐‘Ž) can be expanded to explicitly reference maps from โ‹†, i.e. ev(๐‘“,๐‘Ž)=๐‘“โˆ˜(๐‘Ž) with the "โˆ˜"? Also, to clarify: by the "internal notion of the set of all functions [๐ด,๐ต] together with the notion of evaluation is fully encoded by the much simpler notion of the cartesian product of sets" you mean the product ๐‘‡×๐ด in โ„Ž:๐‘‡×๐ดโ†’๐ต? I'd have to digest this. $\endgroup$
    – JRC
    Feb 1 '21 at 9:14
  • 1
    $\begingroup$ You're very welcome @JRC. The intention of the answer was precisely to attract one's (inclined) mind to the meatyness of the situation. To answer the two followups: yes and yes. The first yes is straightforward. The second yes is too but perhaps in a simpler way than you currently perceive. What I'm saying is that the internal notion of mappings and evaluation is already encoded in the notion of cartesian product. The latter determines the former via the notion of adjunction. This is really the beginning of topos theory. Lawver's "conceptual mathematics" book should be a good further read. $\endgroup$ Feb 1 '21 at 11:11
  • $\begingroup$ Fantastic. Thanks again. $\endgroup$
    – JRC
    Feb 1 '21 at 11:23
  • 2
    $\begingroup$ Although this is not a new concept for me, the fact that $f(a)$ can be interpreted as $f\circ (a)$ by choosing suitable notation is the coolest thing I've seen in the past few months. $\endgroup$ Feb 3 '21 at 12:47
5
$\begingroup$

Is there anything more to evaluation, or can I exactly equate evaluation with composition and forever de-clutter my mind of the term "evaluation"?

Frankly, there is no way to non-circularly 'get rid' of the notion of "evaluation". A rose by any other name is still a rose. Even Lawvere's axiomatization of ETCS explicitly axiomatizes the evaluation mapping in Axiom 2, just phrased in category theory terms.

I think what you must realize is that certain mathematical notions are core notions and whatever implementation you use for them does not make them disappear at all. For example, it makes no sense to try to argue that ZFC set theory has eliminated the notion of function application because instead of "$f(x)$" we can use "$\bigcup \{ y : โŸจx,yโŸฉโˆˆf \}$" given by the Union axiom and the Replacement schema (or a slightly more complicated expression if you use Specification and Powerset instead of Replacement).

The whole point is that we design foundational systems to be able to do the mathematics that we want to do. Since we want to have the usual natural numbers with the usual induction, we also want our foundational system to be able to construct a model of PA (for suitable encoding of "model"). And since we want to be able to reason about functions on $โ„•$, functions on $โ„$ and so on, with the usual notion of "function", including evaluation, composition, function types and equality, we make sure that our foundational system is able to construct representations of the usual functions and prove those usual properties! See also this related post explaining why we care about abstractions rather than how things are concretely implemented in the foundational system.

There is nothing wrong with thinking about weaker systems that cannot do some of these things, but most logicians would not consider these systems viable as foundations for all mathematics, precisely for that reason!

$\endgroup$
10
  • $\begingroup$ Yes thanks. This is very helpful. Point well-taken. $\endgroup$
    – JRC
    Feb 1 '21 at 8:47
  • $\begingroup$ @JRC: You're welcome! =) $\endgroup$
    – user21820
    Feb 1 '21 at 8:54
  • $\begingroup$ While I agree with the spirit presented I would argue that it is not a-priori clear that we want to have the usual natural numbers, the usual reals, or the usual functions on them. In some sense, topos theory is trying to be agnostic as possible and only force you to decide which variant of natural numbers, reals, and functions you really want only at the very last minute. Some times we want infinitely large natural numbers. Some times we want infinitesimal reals. Some times we want all functions to be continuous. There are toposes where these happen. $\endgroup$ Feb 3 '21 at 12:33
  • $\begingroup$ @IttayWeiss: What I meant was that we always want to be able to get at least concrete real analysis (as used in applied mathematics in engineering design), and basic number theory (as used in applied cryptography), otherwise we would not consider such a system foundational. We certainly can be interested in unusual systems as mathematical objects, just as logicians who completely accept ZFC are still interested in weak fragments of PA such as Iฮฃ1, or weak subsystems of Z2 such as WKL0, but none of those are ever considered to be foundational. $\endgroup$
    – user21820
    Feb 3 '21 at 12:46
  • $\begingroup$ @user21820 I don't think it is very clear which real numbers are the concrete ones used in applied mathematics. $\endgroup$ Feb 3 '21 at 12:50

Your Answer

By clicking โ€œPost Your Answerโ€, you agree to our terms of service, privacy policy and cookie policy

Not the answer you're looking for? Browse other questions tagged or ask your own question.