Skip to main content
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