3 ms·
I'm not very familiar with the static analysis of algorithms, abstract interpretation and collapsing stacks of interpreters but I'm curious if you have any intu
by engboris 2y ago
I'm not very familiar with the static analysis of algorithms, abstract interpretation and collapsing stacks of interpreters but I'm curious if you have any intuitions (even vague ones).
I don't think there is any concrete steps in this direction. However, those ideas still live in the transcendental syntax since it is the successor of his geometry of interaction programme.
> or is there anything holding back Girard's theories from practical application
In theory, I don't think so. In practice, it's very difficult to approach his ideas. Not only because he's hard to read but also because you have to read and understand a lot of his previous works but also of other people's work to put everything into context. Once you do it, you then need enough practical knowledge to have an idea of what applications can come out of it.
> I know that Girard's Geometry of Interaction was supposed to have problems with additives, of which exact implications I do not quite comprehend, which may or may not be relevant
It's not very clear. From what I understand, he now considers he was "doing it wrong" and then the problem disappeared because he now distinguishes between "local" (asystemic/particular) and "global" (systemic/generic) mechanisms which are apparently and mistakenly mixed in logic. Full additives are global and live in a "system" (which defines contraints over a "free" computational space -- think of "complex systems") although we can define weaker "local" additives. This difference between local (he calls it first-order but it has nothing to do with FOL/predicate calculus) and global (he calls it "second-order") is mentionned in his "Logique 2.0" paper.
- qazxcvbnm 2y agoThank you for pointing out these distinctions which I had not grasped, and the relevant literature! Time for me to dig back into Girardesque pages. Is "Logique 2.0" this paper https://girard.perso.math.cnrs.fr/logique2.0.pdf https://girard.perso.math.cnrs.fr/logique2.0.pdf? Is there an English translation available?
- Nevermark 2y agoClaude translation of the intro: > Abstract: > In this tract, I lay the foundations for a radical re-reading of logic. I illustrate this with technical developments: in particular, a notion of truth based on the Euler-Poincaré invariant. > Introduction: The Return of Philosophy > At the end of the 19th century, logic experienced a spectacular renaissance. But, like a snake that grew too quickly while forgetting to shed its skin, logic remains prisoner today of a Nessus tunic - the scientistic format concocted by the founding fathers that has become obsolete. This obsolescence is made manifest by the proof networks derived from linear logic [2]. It is high time to change our reading grid and carry out a "Copernican revolution": the transition to logic 2.0. > The first point of resistance is the dominant philosophy - analytical, to simplify - whose main thesis is that... philosophy serves no purpose: a simple translation would allow bypassing it by reducing it to predicate calculus. This thesis, due roughly to Russell, places logic in the position of an irrefutable arbiter. And thus, how can we judge it if it is its own jury? To top it off, modern "analytics" reduce philosophy to logic... from Russell's time, the only one they know. This outdated logic thus dictates its law under the cover of scientistic philosophy. I am not sure the poetic flourishes are helping with clarity and formalization... but I would dearly love to watch a video of him shouting in this style from upon a box in a town square.
- qazxcvbnm 2y agoIt may not help with clarity, but I do love dearly how, so refreshingly, he allows me to feel how he himself feels of the world and its significance with his work, and in that I do feel I understand his point of view better.
- engboris 2y agoYes, it's this paper but there's no English translation. Girard mostly (only?) write in French now. I believe LLM like ChatGPT or Claude do a great job nowadays?