16
$\begingroup$

Jean-Yves Girard writes at the end of his paper "Towards a Geometry of Interaction", page 105, that we have three intuitions about the nature of time:

  1. time is logic modulo the order of rules,
  2. time is the cut elimination process,
  3. time is the contents of noncommutative linear logic.

Can anyone explain what these means? Does anyone know if Girard has developed these thoughts any further?

Improve this question
$\endgroup$
7
  • 5
    $\begingroup$ Sometimes, some people say some things, not because the things are true, deep, or in any sense smart, but to make other people think. Such people, are usually called "controversial" (sometimes even "excentric") by the community. For sure, Y.J. Girard is one of the greatest logicians of our time; yet he is a bit "controversial" :-) $\endgroup$
    – Michal R. Przybylek
    Aug 23, 2014 at 21:39
  • 9
    $\begingroup$ My first thought upon seeing the question title was that it was going to be about mustard watches. $\endgroup$
    – Henry Cohn
    Aug 24, 2014 at 2:02
  • 7
    $\begingroup$ For me, reading Girard often feels like reading Derrida. In both cases I typically feel stupid for not being able to really follow the obscure allusions and suggestions, or else I get a feeling similar to taking a Rorschach test. Also I sense a kind of cultish mystique surrounding these men. I like it much more when Girard does some hard mathematics and produces a proof, as he has been known to do on occasion. $\endgroup$
    – Todd Trimble ♦
    Aug 24, 2014 at 2:22
  • $\begingroup$ Derrida’s work never crystalizes into actual results - so I think his work is for the most part worthless. However, the analytic/pragmatic philosopher Mark Wilson is able to (independently of Derrida) articulate some somewhat Derridean points in in a clear and rational manner, illustrated with concrete examples from fields like applied mathematics, physics, engineering, and linguistics. (There's a good review/summary of his magnum opus here pitt.edu/~rbrandom/BrandomPPPG.pdf and I can go into more detail if anyone is interested. Wilson sees concepts as something like a collection... $\endgroup$
    – Trent
    Aug 24, 2014 at 5:55
  • $\begingroup$ ... of different mapping conventions (mercator, hammer, goode ...) and rules for moving between those mapping conventions. However, the objects that concepts refer to are (according to Wilson, I’m not sure whether I agree with him) not always unitary things like a 3d globe, they are just patchwork things like the maps used to understand them.). Girard is able to turn his cryptic remarks into actual results, but, yes, not all the time. In the case of this question for example: I can’t figure out what Girard ... $\endgroup$
    – Trent
    Aug 24, 2014 at 5:56

1 Answer 1

Reset to default
34
$\begingroup$

I did my PhD thesis in Girard's team in Marseille (my supervisor was Laurent Regnier, himself a student of Girard's) so I have quite a bit of experience with his "excentric" way of communicating and I can attempt an exegesis ( :-) ) of this particular sentence (besides, I am quite familiar with both the philosophical and technical contents of what Girard calls "geometry of interaction", or GoI).

First of all, the concept of time Girard is talking about is computational time, i.e., the step-by-step evolution of a computational process. This is where his words make the most technical sense. Any broader interpretation of the word "time" in this context may (or may not) lead to futile and meaningless musings. Now, the three "intuitions" Girard is talking about correspond to three different views of logic, the first two belonging to the proof-theoretic tradition, the third more model-theoretic:

  1. logic as proof search;
  2. logic as functional programming;
  3. logic as a descriptive tool.

In logic as proof search, one step of computation corresponds to one inference rule (read bottom-up). Certain inference rules commute, which means that they may possibly be applied in parallel, whereas others are related by causal dependencies, yielding a sequential evaluation. These latter are the ones that make the time "tick", so one may see computational time in proof search to be given by the successive application of clusters of mutually independent rules. This idea finds a technical realization in the notion of polarity and focusing proofs in linear logic, which was unknown at the time Girard wrote "Towards a GoI". Polarity in linear logic was introduced in the early 90s by Jean-Marc Andreoli and today is an essential aspect not only of linear proof search but of games semantics and the theory of programming languages in general.

The second view is the simplest to explain: it is the well-known Curry-Howard correspondence, under which a proof may be seen as a program, the execution of which corresponds to cut-elimination. So computational time is just the succession of cut-elimination steps, i.e., rewriting steps leading to a result, which is fairly standard and intuitive I would say. The relationship between evaluation time in this sense ($\beta$-reduction/cut-elimination) and the usual notion of time defined using Turing machines (or other low-level machines) has been the direct or indirect subject of countless papers from the 90s onwards (google "implicit computational complexity", or take a look for example at this paper by Blelloch and Greiner or this very recent paper by Accattoli and Dal Lago).

The third view is also very standard: logic is seen as a language in which we may state facts/propositions about some kind of world. There is a whole class of logical languages (known as temporal logics) which are taylored so as to be able to speak of worlds in which there is a notion of time. Here, Girard is suggesting that non-commutative logic, with its non-symmetric connectives distinguishing "left" from "right" (hence, presumably, "before" from "after") may provide a language with a built-in notion of time. This latter point is the most hand-wavy and, in fact, it is the only one that has had no technical development so far (at least as far as I know).

Improve this answer
$\endgroup$
4
  • 3
    $\begingroup$ Thanks, excellent answer. What does Girard say when people ask him why his style is the way it is? I recall him writing somewhere that one reason why he reads a lot of surrealist literature and incorporates that style into his work is b/c he thinks that to understand what reason is, you need to understand where it's borders lie, and to understand where it's borders lie, you need to understand what reason is not. $\endgroup$
    – Trent
    Aug 24, 2014 at 23:45
  • 1
    $\begingroup$ Also, do you know whether Girard has explored things like trickster folklore/mythology, the concept of metis ("cunning intelligence") in Ancient Greece, scholarship on allusive distance in chinese thought/philosophy etc? I think such things would help him clearly articulate how the "controversial" or "excentric" portions of his thought function. It is essential to articulate how those portions function so people who say are intelligent mathematicians or computer scientists but don't have much experience interacting with literary-artistic types can figure out what is going on. $\endgroup$
    – Trent
    Aug 24, 2014 at 23:52
  • $\begingroup$ I wasn't aware of Girard's fondness for surrealist literature and, apart from the occasional mundane conversation (such as lengthy discussions about postwar Italian filmmakers :-) ), I never talked much about non-mathematical stuff with him, so I'm afraid I cannot help you... $\endgroup$
    – Damiano Mazza
    Aug 25, 2014 at 17:04
  • $\begingroup$ @Trent, I think the style is intentional and goes back to Georg Kreisel and even Ludwig Wittgenstein. $\endgroup$
    – Kaveh
    Aug 25, 2014 at 20:52

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service and acknowledge you have read our privacy policy.

Not the answer you're looking for? Browse other questions tagged or ask your own question.