Comment by adamnemecek | Hacker News Reader

Comment by adamnemecek | Hacker News Reader

Constructive mathematics is the way forward. It's connected to linear logic via Chu spaces [0] (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

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) which has been present in Western philosophy since Aristotle through Kant, Hegel and Marx (it's a funny story).

> Constructive mathematics is the way forward.

This sweeping assumption leads to my sweeping assumption that you are "a programmer".

No offense, but that is really handwavy. In what way does constructive mathematics unlock the door to being closer to all the quantum shit?

Ask 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 Page 14. But do a google search “constructive mathematics” “quantum” or “linear logic” “quantum”, a lot has been written.

I 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) and some truly fascinating models for intuitionistic logics (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...

I 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.

I 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

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.

How 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.

Good 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

“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.

> 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.

I'm sorry, but he is right.

Adjoints are everywhere [1]. Referencing adjoints is indeed pretty vague. You can't make a case for why things are interesting by quoting a bunch of resources of other people making cases why things are interesting. (I guess you can, but then, why make the argument at all if it is not yours?)

You don't even need funny names to get x^2=0. This is true for any of the two elements of the group of order 2.

Linear logic is indeed having a mini revival, but so is general category theory. I don't see the particular advantage for people to evangelise certain parts of mathematics, especially if the case being made is not clear.

[1] Not attributed to me.

> I'm sorry, but he is right.

That’s like your opinion, man.

You conveniently ignored the continousness of both constructive mathematics and Lie groups.

Did you read the paper on chu spaces and constructive mathematics? What did it say about adjoints?

There’s a reason why intuitionistic logic comes into studying Lie Groupoids, but I’m not quite sure you understand why. It’s great to see some enthusiasm, but I’d recommend spending a few months working through Barr and Wells before you start publicly advocating like this.

Lie groups come up very naturally in synthetic differential geometry (SDG) (http://www.fuw.edu.pl/~kostecki/sdg.pdf). In fact, the main advantage of SDG over the classical formulation of differential geometry is that it can be developed in a largely coordinate free fashion and that you can talk natively about differential forms.

That said, there is a design space here and while SDG is close enough to ordinary mathematics that you can explain it to high-school students, it might not be the best fit for developing modern physics. There are several different approaches (e.g., working in the internal language of a "synthetic differential infinity-topos") which seem promising. It's an area of active research and one that is still extraordinarily difficult to get into.

Does this have anything to do with constructive mathematics though? I still don’t see the connection.

These are all models of a constructive type theory/intuitionistic logic. The axiom of excluded middle fails in SDG and in any infinity-topos.

Is there a constructive version of Gleason and Montgomery-Zippin solution of the Hilbert 5th problem? Reference pls if any.

Previous discussion :) https://news.ycombinator.com/item?id=17641789

What about it?

Interesting! Do you have a book on the subject to recommend?

Read 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.

Reply on news.ycombinator.com