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

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?

• Commented Apr 14, 2016 at 18:38

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.

• Thanks! A question: is there any drawback about the notation of $D(x\mapsto x+ax^2)$?
– Eric
Commented Apr 15, 2016 at 5:09
• No if people are comfortable with it. While people are usually comfortable enough with an example like that, you will quickly have examples like $(x,y) \mapsto D(u \mapsto D(v \mapsto u^2 + v^2)(y))(x)$. Admittedly, with the right concepts, rarely will things get so hairy. Also, this does at least have the benefit of making clear exactly what's going on with regards to binding. Commented Apr 15, 2016 at 5:41
• After hours of thinking, I think $D(x\mapsto x^2)=x\mapsto 2x$ is good, but not the origin meaning(usage) of what the symbol $\frac{d}{dx}$ represent. I think $\frac{d}{dx}$ is far more closed to say that it takes an expression of $x$, and outputs another (reasonable) expression in $x$. For example, taking $x^2$, returning $2x$, both of which are more likely to be an expression, not a function(e.g. $x\mapsto x^2$). Am I correct? So, is there a direct formalization of this usage of $\frac{d}{dx}$
– Eric
Commented Apr 15, 2016 at 17:01
• You can definitely formalize this. You just need to formalize what you mean by "expression" and define $\frac{d}{dx}$ as an operation on expressions. The problems with this approach are that $\frac{d}{dx}$ becomes a meta-operation so you couldn't talk about it's properties within your language, i.e. the chain rule would just be meaningless (instead it would be part of your implementation of $\frac{d}{dx}$); secondly, you would only be able to differentiate things for which you manifestly have an expression, e.g. polynomials or (piece-wise) analytic functions explicitly presented as a ... Commented Apr 15, 2016 at 19:56
• formal sum and polynomials of such. This is probably not what Leibniz was thinking. An alternative approach is to directly formalize $\frac{d}{dx}$ as a binding operator in the same way $\lambda$ is in the lambda calculus. You would still need to formalize expressions, but you could now talk about expressions like $\frac{d}{dx}(f(g(x))$ for arbitrary $f$ and $g$. You could add the rules as rewrites which will run you straight into concerns of alpha-equivalence and capture-avoiding substitution, ... Commented Apr 15, 2016 at 20:07