Is the $x$ in $\frac{\mathrm{d}}{\mathrm{d}x}$ a symbol in the sense of Harper's PFPL?

The role of $x$ in $\frac{\mathrm{d}}{\mathrm{d}x} y$ not only confuses my calculus students, it has also puzzled some well known mathematicians. Questions one might ask are:

-
Does the $x$ in the denominator bind the $x$ in $y$? (Clearly no, since $\frac{dx^2}{dx}=2x$.)

-
Can one substitute for $x$ in the denominator? (Looks like not, what should $\frac{dx^2}{d3}$ mean?)

-
Is the $x$ in the denominator itself bound?

I was wondering if interpreting that $x$ as a symbol, in the sense of Bob Harper's Practical Foundations for Programming Languages (Chapter 1.2 on abstract binding trees) might solve these riddles, and if this had already been worked out by someone?

Here's a quote from PFPL:


It will often be necessary to consider languages whose abstract syntax
cannot be specified by a fixed set of operators, but rather requires
that the available operators be sensitive to the context in which they
occur. For our purposes it will suffice to consider a set of symbolic
parameters, or symbols, that index families of operators so that as
the set of symbols varies, so does the set of operators. [...] The
only difference between symbols and variables is that the only
operation on symbols is renaming; there is no notion of substitution
for a symbol.

Some mathematicians find it natural to substitute for the variable in the denominator of a derivative, writing things like $\frac{d \log V}{d\log p}$. This suggests that the $x$ in the denominator $\frac{dy}{dx}$ is neither bound nor binding nor a symbol.

Rather $\frac{dy}{dx}$ seems to be an operation on "variable quantities" $y,x$ requiring some side conditions, similar to how the usual division $a/b$ requires $b\neq 0$, or how the operation $\frac{v}{v_1^0\ldots v_i^1\ldots v_n^0}$ in my comment requires $v_1,\ldots,v_n$ to be linearly independent and $v$ to lie in their span.

I suspect that the side condition for $\frac{dy}{dx}$ should be analogous: $dx$ needs to be linearly independent and $dy$ has to be a multiple of $dx$.

With these side conditions we are not allowed to substitute a constant for $x$ in $\frac{dy}{dx}$ since then $dx=0$ and so $dx$ is not linearly independent. That would explain why we are not allowed to write $\frac{d x^2}{d3}$ or to take the derivative of equation $x=0$ w.r.t. to $x$ to conclude $1=0$.

I'd be interested in hearing if someone sees an immediate problem with this interpretation.

(I see some subtlety in the fact that $d(x|_{x=3})$ cannot mean the same as $(dx)|_{x=3}$, since otherwise I'd expect $\frac{dy}{dx}|_{x=3}$ to be the same as $\frac{d(y|_{x=3})}{d(x|_{x=3})}$ which would not be allowed by the side condition. On the other hand, that is not so strange from a differential geometric point of view if we read $|_{x=a}$ as restriction: there is a difference between restricting a differential form and pulling it back. But I need to think more about this.)

StackExchange Computer Science Q#82230, answer score: 2