Currying syntax clarification - how to work through an example of currying?

Question

I understand currying from a computer science background, so I'm happy explaining currying with a before and after example in specific languages, eg, in Java

public static Function<Integer, Function<Integer, Integer>> add() {
    return x -> y -> x + y;
} 

is the curried form of

public static int add(int a, int b) {
    return a + b;
}

or even

λa.(λb. + a b) as the curried form of λab.+ a b in lambda calculus

but I'm not sure how to represent it with just mathematics syntax, would it be like this?

Give some function f,

$$f(a, b) = a + b$$

The curried version would be this?

$$f(a) \rightarrow f(b) \rightarrow a + b$$

or this?

$$f(a) \Rightarrow f(b) \Rightarrow a + b$$

or even this?

$$f(a) \rightarrow f(b) = a + b$$

As you can see, I'm floundering with the "f(a) returns a function f(b)" part. I'm not sure if "material implication" or "map" are even suitable!

Answer 1

First I would like to say that lambda calculus certainly also is a form of mathematical notation. But onwards to your question.

When we talk about functions, we usually specify two things: the domain and codomain of the function, and what the function actually does. So in this case, your function would have domain $\mathbb{Z} \times \mathbb{Z}$ and codomain $\mathbb{Z}$, so we would write $$f: \mathbb{Z} \times \mathbb{Z} \to \mathbb{Z}.$$ To curry this, we want to make sure that each domain only has one dimension, so that we can write $$curry(f):\mathbb{Z} \to (\mathbb{Z} \to \mathbb{Z}).$$ So this is the correct context to use the $\to$-notation.

However, we of course also want to give a description of what the curried function actually does, which is more along the lines of what you have tried to do in your question. So we start with a function $$f(a,b) = a + b,$$ and we make a new function $$g(a) = (b \mapsto f(a,b))$$ where the notation $b \mapsto f(a,b)$ means that $b$ is mapped to $f(a,b)$. With regards to computer science, you can think of the notation $x \mapsto y$ as an anonymous function instead of writing $f(x) = y$. Note also that, technically, we make a new function for each value of $b$, so if we were pedantic mathematicians, we would write $$g_b(a) = (b \mapsto (f(a,b))$$ to make explicit that the function $g$ depends on our choice of $b$.

As a last comment, the symbol $\implies$ for implication is not applicable in this case.