How to formalize a variable-binding operator, such like $\frac{d}{dx}$?

Question

How to formalize a variable-binding operator, such like $\frac{d}{dx}f(x)$? For instance, I think we should treat $\frac{d}{dx}$ as a higher-order function of $x$, returning a function that takes it argument(usually an expression of its letter be mentioned, say $x$, e.g. $x^2+1$) to its corresponding expression(e.g. $2x$). Few examples are:

1. $(\frac{d}{dx})(3x^2+4x)=6x+4$

2. $(\frac{d}{dz})(3z^2+4z)=6z+4$

3. $(D_y)\cos y=-\sin y$ ($D_y$ is equivalent to $\frac{d}{dy}$)

Mathematicians, or logicians, often say that $\frac{d}{dx}$ is a so-called variable-binding operator, which means the letter(i.e. variable) specified in the $d(\cdot)$ is just a independent, place-holder variable, being bound by the symbol, and does not be affected by the stand-in variables outside. So one is allowable to write an expression like defining $f(x)=\frac{d}{dx}(x^2)$, and get $f(10)=(2x)|_{x=10}=20$, not $f(10)=\frac{d}{d10}(10^2)$. The latter is non-sense.

In a normal way undergraduate students learn about a function definition, there is no such way to make a variable-binding mechanism in the plain function definition(via n-ary relation). There is no place for us to say(specify) in the definition of a function that the function should hold its arguments being unevaluated and independent!

The another related operator is $\sum$, such like $\displaystyle\sum_{i=1}^{10}i^2$, is also have the function(no pun intended) of binding variable.

So, my question is, how to formalize such things? Is it possible? Is it been discussed by logicians yet? It there a standard way that is accepted by people?

Answer 1

The computer science community has a vast literature on this topic because when you are implementing systems you don't have the option of being lax about what exactly you mean by a binding form. For example, there is a blog dedicated to just this that mentions many different approaches.

The simplest thing to do from a mathematical perspective is to treat these operations as higher order functions, i.e. functions that take functions (often called "functionals" in mathematics.) This doesn't really solve the problem, so much as push it off to a (not so) "well-understood" case. For example, you would treat one-dimensional differentiation as a function $D : \mathbb{R}^\mathbb{R}\to\mathbb{R}^\mathbb{R}$, and so differentiation of $x + ax^2$ would be $D(x \mapsto x + ax^2)$. One nice thing about this perspective is it makes you think about what's happening a bit more. For example, you should consider what a precise type for multi-variable differentiation or single-variable integration would be.

Still, in practice this approach can either become rather opaque or requires "anonymous" functions, like the example I used above, which, as I said, is where the problem is pushed off. You could avoid anonymous functions in this case by defining lifted versions of addition and multiplication and constants and defining $x$ as the identity function. Then you could write $D(x+ax^2)$. You couldn't replace $x$ with $y$, in this case, as $y$ is simply not defined (though you could also define it as the identity function). If you did handle the multi-variable case, you could define $x$ as the first projection of a 2-tuple, and $y$ as the second projection, and finagle a "normal" looking syntax but it would likely cause a lot of confusion if you tried to rigorously stick to such an approach. It would probably be clearer at that point, to just explicitly use the identity and projection as values, i.e. $D(\mathsf{id}+a\mathsf{id}^2)$ or $D(\pi_1 + \pi_2)$ for $\nabla(x+y)$.

If you do want to spell out the details of handling name binding, most introductions to the lambda calculus, which is basically nothing but anonymous functions, will give a basic description of how it is handled. In particular the notions of alpha-equivalence and capture-avoiding substitution. The plethora of approaches I mentioned at the beginning is driven, in computer science, by concerns such as ease of implementation, ease of proving results, efficiency of implementation, and "non-standard" binding constructs as would be present in e.g. the linear lambda calculus.