3 ms·
Mathematical notation is terrible. I don't mean this in the usual "we need to invent new symbols to make it clearer" way. I mean it in the way that it has imp
by konjin 6y ago
Mathematical notation is terrible.
I don't mean this in the usual "we need to invent new symbols to make it clearer" way.
I mean it in the way that it has implicit typing that gets coerced constantly. Using Haskell types D :: (R -> R) -> (R -> R). Yet it gets used on things like D 2 = 0 which implies D :: (R -> R).
What you've actually done is an implicit conversion of 2 :: R to 2(x) = 2 :: R -> R and 0 is not 0::R it is 0(x) = 0 :: R -> R.
The Q_0 system described in [0] is a good start for a mathematical system that is both sane and as expressive as the one we have now. With term rewriting you can even keep the ridiculous notation we have today if you love it so much. Though I have grown incredibly fond of typing out extended typed lambda calculus using scheme notation in Emacs with a home grown automated theorem proving mode that was trivial to implement.
[0] https://www.springer.com/gp/book/9781402007637 https://www.springer.com/gp/book/9781402007637
- euiq 6y agoThat's not a very convincing example, given that numeric literals are polymorphic in Haskell.
- bunje 6y agoSo you say we should specify when 2 means number two and when it means the constant function? How does it help?
- konjin 6y agoDerivatives then are a higher order function that follow it's definition in all cases. You can't exactly apply it's definition as a limit in cases where it's applied to non-fictions.
- ccortes 6y agoThat sounds more like a lazy mathematician tbh. Do you have any other resource about the link you provided?
- 6gvONxR4sf7o 6y agoI agree that your example isn’t very convincing, for an additional reason. You can treat 2x as a function, or you can treat it as an expression, where x is its own special kind of thing: a symbol. With how the notation is typically used, it’s at least closer to my mental model. Treating the expression as a function under substitution is one way to look at it, but not the only way.
- konjin 6y agoThe point is that 2 and (λ (x) 2) are vastly different objects, yet in standard math are treated the same. Also you don't need a symbol type to deal with variables, you just need to allow type variables to be used in standard expressions. (define x R) (^ x 2) is just as easy to manipulate as (λ (x) (^ x 2)), the only issue is that your rewrite rules how aren't just looking at syntax, but semantics too.
- ubercow13 6y agoI honestly never found this an issue. Shorthand and type coercion is used a lot but at least when taught, it's usually made very explicit what notation means and when things are being excluded. After that point, the notation is the least challenging part.
- konjin 6y agoIt is not an issue until you start trying to teach any sort of fix point theorem, at which point the wheels fall off because the notion can't deal with higher order functions at all.
- ubercow13 6y agoI guess I just don't get your point. D 2 = 0 doesn't imply anything, it's just shorthand to make working on something less tedious for people who are already familiar with it. It seems perfectly expressive and sane: mathematicians have successfully studied differentiation using standard math notation. 2 and (λ (x) 2) aren't 'treated the same', that's just a strawman.
- konjin 6y agoFunny how its also used in every textbook for people who aren't. This is getting to be apologia on the levels that I'd only seen in history books about why Roman numerals were superior.
- deleted 6y ago[deleted]
- ubercow13 6y agoThe premise of your argument is that this notation is confusing people, or it's impossible to make explicit what it means. I don't buy it, you even explained the type elision using standard mathematical notaion in your original comment. So if there is some superior notation that would benefit all of maths, that sounds very interesting but I don't think you've made that point very well. Maybe a better example is needed, because on its own, eliding repetitive information from notation does not seem like a problem.
- carapace 6y agoAre you talking about this? https://en.wikipedia.org/wiki/Q0_(mathematical_logic) https://en.wikipedia.org/wiki/Q0_(mathematical_logic)