I second RobinZ’s request for an elaboration. I know a little (a very little) about the technical topics of that paper, but I find Girard’s philosophising here and elsewhere (for example) impenetrable.
This particular idea seems straightforward, at least in non-technical sense: “infinity” should only appear from “traces” of finite dynamical processes, as a way of talking about their dynamics. Infinite objects are artifacts of objectifying time, and any infinite object can as well be regarded as a statement about a finite dynamical system. I liked this remark as a self-contained way of thinking about infinity (on informal level, apart from the specific axiomatizations).
(For example: think of the process of normalization as the dynamic on a term not in a normal form; whether it’ll terminate is undecidable, and a priori the normal form can’t be considered as another term (finitely encoded), yet we may reason about this output as another term, considering how it’ll reduce in interactions with other terms, etc.)
Is there a way of describing it that doesn’t require a computer science background? What are “traces” in this context? And what is a “finite dynamical process” that introduces infinities, and what is the “objectifying”? I can tell this is grammatical English, but the terminology is opaque.
Trace is something like a list of execution steps of a program, a list of what happens at each step, for all steps. When a program runs indefinitely, it’ll be a potentially infinite list (or actually infinite if we know the program won’t terminate). Finite dynamical system is something like a program (together with its current state) that is itself finite, and allows to compute data of the same kind (e.g. program + state) for the next step: this transition from the current step to the next step is the dynamic. Infinity appears in this process when we consider all the (future) steps, not just one, even though one step is enough to determine them all. Objectification as I used it is a concept from mathematics, when you are trying to capture some phenomenon as a certain kind of single mathematical object (as opposed to a thing with whistles, processes and hand-waving).
-- Jean-Yves Girard
I second RobinZ’s request for an elaboration. I know a little (a very little) about the technical topics of that paper, but I find Girard’s philosophising here and elsewhere (for example) impenetrable.
This particular idea seems straightforward, at least in non-technical sense: “infinity” should only appear from “traces” of finite dynamical processes, as a way of talking about their dynamics. Infinite objects are artifacts of objectifying time, and any infinite object can as well be regarded as a statement about a finite dynamical system. I liked this remark as a self-contained way of thinking about infinity (on informal level, apart from the specific axiomatizations).
(For example: think of the process of normalization as the dynamic on a term not in a normal form; whether it’ll terminate is undecidable, and a priori the normal form can’t be considered as another term (finitely encoded), yet we may reason about this output as another term, considering how it’ll reduce in interactions with other terms, etc.)
Is there a way of describing it that doesn’t require a computer science background? What are “traces” in this context? And what is a “finite dynamical process” that introduces infinities, and what is the “objectifying”? I can tell this is grammatical English, but the terminology is opaque.
Trace is something like a list of execution steps of a program, a list of what happens at each step, for all steps. When a program runs indefinitely, it’ll be a potentially infinite list (or actually infinite if we know the program won’t terminate). Finite dynamical system is something like a program (together with its current state) that is itself finite, and allows to compute data of the same kind (e.g. program + state) for the next step: this transition from the current step to the next step is the dynamic. Infinity appears in this process when we consider all the (future) steps, not just one, even though one step is enough to determine them all. Objectification as I used it is a concept from mathematics, when you are trying to capture some phenomenon as a certain kind of single mathematical object (as opposed to a thing with whistles, processes and hand-waving).
Thanks—that’s much clearer.
Elaboration, please?