4 ms·
> Galois connections may be used to describe many forms of abstraction in the theory of abstract interpretation of programming languages. https://en.wikipedia.
by Syzygies 4y ago
> Galois connections may be used to describe many forms of abstraction in the theory of abstract interpretation of programming languages.
https://en.wikipedia.org/wiki/Galois_connection https://en.wikipedia.org/wiki/Galois_connection
- 082349872349872 4y agoSince you've brought out the power tools*, may I ask you to briefly (2-5 min?) consider the last paragraph of https://news.ycombinator.com/item?id=32617344 https://news.ycombinator.com/item?id=32617344 : "if we think geometrically" et seq.? advThanksance * Galois connexions subsume, among other things, Dijkstra's weakest preconditions/strongest postconditions.
- Syzygies 4y agoI believe that these "groupoid" ideas lead into higher category theory, and the supporting mathematics for theorem provers such as Lean.
- peter_d_sherman 4y agoI think you may be right! Also, I think that some of the next breakthroughs for AI might be as follows: 1) Given any Turing-complete computer programming language A, construct a translator to a higher-order intermediate representation, then from that higher-order intermediate representation, construct a translator to programming language B... 2) Do this for all known Turing-complete computer programming languages; 3) Do this for all known Mathematical categories, groups, lemmas, theories, etc., and other Mathematical "objects" (for lack of a better term!) -- in other words, create an intermediate data model "map" (analagous to an intermediate higher-order language used by a transpiler) -- between all of these things in all of Mathematics... Category Theory -- seems like it would be "The next level up"... (Note that I am speculating about most of this(!) -- I claim to be an idiot in [some/many/all] of these areas! <g>)