Timeline for If d/dx is an operator, on what does it operate?
Current License: CC BY-SA 4.0
9 events
when toggle format | what | by | license | comment | |
---|---|---|---|---|---|
Jan 21 at 10:26 | comment | added | Michael Bächtold | There is clearly a difference between a mathematical operator like the derivative ', which acts on modern functions and your d/dx, which acts on syntactical expressions. For instance, from $y=x^2$ we cannot conclude $dy/dx=d(x^2)/dx$ inside the formal system. | |
Jan 20 at 2:16 | comment | added | NinjaDarth | It doesn't "stop being a mathematical operation". The syntax, itself, is a mathematical structure that can be, and is normally, formalized as a magma or as its generalization to different signatures, which are called term algebras for that signature. The elements of a free object in a term algebra are, in fact, one and the same as an abstract syntax tree over that signature, and it is here that you formalize such notions as abstract syntax tree. This is where the "syntax" or "meta level" - as you refer to it - actually lives. | |
Jan 15 at 8:44 | comment | added | Michael Bächtold | In your comments you observe correctly that with (2), $d/dx$ acts on syntactic expression (I'd say at the meta level), so it stops being a mathematical operation, which is different from how mathematicians used to use it, I find. | |
Jan 15 at 8:42 | comment | added | Michael Bächtold | Yes, what I meant was your (1) $\frac{d}{dx}: (x\mapsto f(x))\mapsto (x\mapsto f'(x))$ and later (2) $\frac{d}{dx}(y)=D\lambda x(y)$. (1) suggests that $d/dx$ takes a function $f:\mathbb{R}\to\mathbb{R}$ and returns a function $f':\mathbb{R}\to\mathbb{R}$, while in (2) $d/dx$ takes a term $y:\mathbb{R}$ containing a free variable $x$ (which is not a function) and returns a function of type $\mathbb{R}\to\mathbb{R}$ (not the same as (1)). | |
Jan 15 at 0:02 | comment | added | NinjaDarth | This gets more directly to the question: what type of functional or operator is this: $λx(\_)$; i.e. $y ↦ λx(y)$, when we want bound $x$'s in $y$ to be regarded as such? I think you need to fall back to term algebras, and to magmas (or whatever the generalization of magma's is called) to formalize that as a function that respects the handling of bound variables. It's just easier to skip the formalization and describe it as just a syntactic functional, instead; somewhat like Landin's "let (_) = (_) in (_)". | |
Jan 14 at 23:55 | comment | added | NinjaDarth | You need to be more specific. This one: $\frac{d}{dx}(y) = Dλx(y)$? The $(\_)$ place-holder is not an argument in the usual sense, because it can take bound variables. So it has to be read as something at the "alpha level", so to say, rather than "beta level"; and the place holder is more akin to being of what's referred to as a "reference type" in programming languages. It is a syntactic functional, maybe formalized as such in the Magma (or generalization thereof) underlying the Term algebra. | |
Jan 10 at 8:12 | comment | added | Michael Bächtold | Your first typing judgement says that $d/dx$ takes a function as input and returns a function, but your definition a few lines below suggests it takes a number as input and returns a function. | |
Oct 22, 2023 at 22:44 | history | edited | NinjaDarth | CC BY-SA 4.0 |
Redoing the adjustment - to compensate for an apparent bug in the math rendering software being used on this site.
|
Oct 22, 2023 at 22:38 | history | answered | NinjaDarth | CC BY-SA 4.0 |