4 ms·
Constructive mathematics is the way forward. It's connected to linear logic via Chu spaces [0] (https://arxiv.org/abs/1805.07518 https://arxiv.org/abs/1805.0751
by adamnemecek 8y ago
Constructive mathematics is the way forward. It's connected to linear logic via Chu spaces [0] (https://arxiv.org/abs/1805.07518 https://arxiv.org/abs/1805.07518). This correspondence is unreal as constructive mathematics / linear logic unlocks the door to several key advantages such as being closer to computation, probability theory, type theory, Lie groups, a generalized topology, optimization, “differentiable Turing machines”, all the quantum shit, game theory etc the list goes on.
[0] https://en.wikipedia.org/wiki/Chu_space https://en.wikipedia.org/wiki/Chu_space
Linear logic is fundamentally about formulating computation as an adversarial relationship between two parties. It's also the foundation of e.g. the Rust ownership system (I know, I know, affine types).
It's also the foundation of the min-max algorithm which in turn is the foundation of Generative adversarial neural networks.
Ironically, this idea isn't exactly new. It's directly related to Dialectics (https://en.wikipedia.org/wiki/Dialectic https://en.wikipedia.org/wiki/Dialectic) which has been present in Western philosophy since Aristotle through Kant, Hegel and Marx (it's a funny story).
- gbhn 8y agoInteresting! Do you have a book on the subject to recommend?
- adamnemecek 8y agoRead the wiki on every term you aren't familiar with and then do pairwise google searches for papers containing any two of the words in the set, so e.g. "probability" "Lie groups". If you have specific question I can maybe answer them or provide a link at least.
- aportnoy 8y agoNo offense, but that is really handwavy. In what way does constructive mathematics unlock the door to being closer to all the quantum shit?
- adamnemecek 8y agoAsk specific questions. Like I have a papers backing up most of my claims. Sometimes you need to take a leap of faith but you don’t need to draw every line in the connect the dot puzzle to see that it’s a fucking elephant. https://arxiv.org/pdf/0805.2859.pdf https://arxiv.org/pdf/0805.2859.pdf Page 14. But do a google search “constructive mathematics” “quantum” or “linear logic” “quantum”, a lot has been written.
- fmap 8y agoI am not sure what the parent meant specifically, but yes, there is quite a lot of work on quantum physics and logic, with regular conferences (https://arxiv.org/html/1701.00242 https://arxiv.org/html/1701.00242) and some truly fascinating models for intuitionistic logics (https://arxiv.org/abs/0909.3468 https://arxiv.org/abs/0909.3468). Not being a physicist I have no idea whether this is "the way forward" for quantum physics or anything, but the results that I do understand are non-trivial so there seems to be something there...
- joppy 8y agoHow is constructive mathematics closer to Lie groups than regular mathematics? From what I read in that presentation, a bunch of basic assumptions in calculus (such as the intermediate value theorem) no longer hold, and the theory of Lie groups is built on manifolds/calculus/real analysis etc.
- adamnemecek 8y agoGood question. I don’t have a direct answer answer but fundamentally the connection has something to do with adjoints. Google for adjoints and constructive mathematics and Lie groups and adjoints. This particular pair I understand only indirectly, I somewhat understand the relationship between linear logic and Lie groups and constructive mathematics and linear logic and this is a transitive relationship. Edit: in the presentation they mention “In constructive mathematics, there can also be numbers† d such that d^2 = 0 but not necessarily d = 0.”. They are talking about alternarivity, one of the three requirements for a Lie algebra https://en.m.wikipedia.org/wiki/Lie_algebra https://en.m.wikipedia.org/wiki/Lie_algebra
- joppy 8y ago“Something to do with adjoints” is hopelessly vague, and what do you mean by transitive? In regular mathematics there can be nonzero numbers whose square is zero (for example, the “dual numbers”). But I don’t see how this has anything to do with constructive vs nonconstructive mathematics.
- adamnemecek 8y ago> hopelessly vague, You didn’t do the reading so hold your horses with hopelessly. From the slides “In constructive mathematics, every function is continuous”. (From the presentation) Sounds like Lie groups to me. I’m aware of dual numbers funny that you bring them up as they correspond to Lie groups. I have been talking about dual quaternions nonstop on hn.
- mikorym 8y ago
- yantrams 8y agoI started teaching myself Racket recently and eventually ended up looking into the innards of lambda calculus formalism. It got me thinking about what the ramifications of embracing constructivism would be towards computability in general. Can you recommend any good introductory literature on constructivism ? I'm familiar with the foundational crisis and the whole formalism vs logicism vs constructivism debate but never really dug deeper. Thanks.
- adamnemecek 8y agoI would recommend starting with linear logic to be honest. Logic is very simple to understand, mathematics is hard. Analogously, linear logic is simpler than constructive mathematics. https://johnwickerson.github.io/talks/linearlogic.pdf https://johnwickerson.github.io/talks/linearlogic.pdf I know this might not be what you were looking for but to be honest Linear logic is the simplest to understand of all of these. I’m still struggling with these ideas, but all the signs are pointing towards this being the case.
- deleted 8y ago[deleted]
- mikorym 8y ago> Constructive mathematics is the way forward. This sweeping assumption leads to my sweeping assumption that you are "a programmer".
- adamnemecek 8y agoDid you read the presentation? Did you read this? http://www.ams.org/journals/bull/2017-54-03/S0273-0979-2016-01556-4/S0273-0979-2016-01556-4.pdf http://www.ams.org/journals/bull/2017-54-03/S0273-0979-2016-... No, you are just closing your eyes and clinging to the sense of security that mathematics claims to provide. Your comment wasn’t very specific and concentrated in the peripheral part of my claim rather than the central.
- cscurmudgeon 8y agoDid you read this? https://www.jstor.org/stable/30226269?seq=1#page_scan_tab_contents https://www.jstor.org/stable/30226269?seq=1#page_scan_tab_co...
- adamnemecek 8y agoI’m just reading it but I disagree as would most mathematicians.
- cscurmudgeon 8y agoAmazing that you are just reading but already know what most mathematicians think about it :) Realistically and honestly, most mathematicians agree with it. Most mathematicians consider constructivism to be useful AND a subset of normal mathematics. Also, it intellectually pains me to see proofs of meta theorems in intuitionistic logic use classical logic (not talking about object level proofs).
- alimw 8y agoPrevious discussion :) https://news.ycombinator.com/item?id=17641789 https://news.ycombinator.com/item?id=17641789
- adamnemecek 8y agoWhat about it?