Want to take part in these discussions? Sign in if you have an account, or apply for one below
Vanilla 1.1.10 is a product of Lussumo. More Information: Documentation, Community Support.
1 to 20 of 20
The following simple thought must have been voiced and discussed before, where?
Namely there is some relation between categorical semantics for (the multiplictive fragment of) linear type theory in which each monomorphism is a split monomorphism and the notorious concept known as “collapse of the wave function” in quantum physics:
Since monomorphisms are the semantics of propositions, if they all split then equivalently projections become semantics for propositions. We may then think of inspecting the truth of a proposition by applying the corresponding projection. But that projection is just the “wave function collapse”.
This thought must have been expressed before. Where?
Sorry to be critical, but could you be more precise? That is, instead of “categorical semantics for (the multiplicative fragment of) linear type theory”, could you say what you mean more exactly, e.g., $\ast$-autonomous categories or symmetric monoidal closed categories. (We’ve had discussions before on just how elastic the nLab usage of “linear type theory” is, so that when you use phrases like this, I’m not sure what you mean.)
For what I am after few of this extra structure matters. Consider any non-cartesian symmetric monoidal category where all monos are split. The archetypical example to think of for the purposes of the question is just the category of finite dimensional vector spaces. The allusion to linear logic is just there to put us in the mindset that monos are propositions. So now propositions are projections. What I am asking is whether anyone considered a paradigm of “propositions as projections” in linear type theory as being the logical mindset in which to naturally understand what elsewhere is referred to as collapse of the wave function.
Ah, now that I wrote this I googled “propositions as projections” and am getting pointer to
which seems to say just what I am after.
You’d have thought Bob Coecke would have something on this. But all I have found is an MSc thesis by his student, Linde Wester, which at least speaks of
Ordinary monoidal dagger compact categories correspond to interpretation of quantum theory, which explains measurements as a collapse of wave functions.
And then considers how this fits with a 2-categorical treatment:
The 2-categorical models correspond to the many worlds and decoherence interpretation. The embedding of monoidal categories in 2-categories demonstrates how these different interpretations are related.
What I am really after is something with genuine internal logic perspective. It seems possible that one could do away with the confusion and debate about “wavefunction collaps” and the like by finding that this is a generic phenomenon of deduction in linear logics with split monos. Common lore says that wavefunction collaps is effected by “observers” and then there is endless debate as to what constitutes an observer, but maybe the right perspective is rather that it is more fundamentally about truth in linear type theoretic contexts with split monos, via a propositions-as-projections paradigm.
I don’t really want to start a discussion of this here. I’d just like to know if anybody has previously tried to discuss this elsewhere. That text by Engesser et al (pdf) seems to go in the right direction, but if you come across anything else, please let me know.
I might know further references, but I’m not completely sure what you’re looking for. How does the propositions-as-projections paradigm differ from Birkhoff-von Neumann quantum logic?
Right, my point is first of all that it makes good sense to think of BvN logic as embedded into linear type theory logic: BvN is about the subobject lattices in (a model for the multiplicative fragment of) linear type theory. Then, second, from that larger perspective, since in the linear type theory the projections exist as actual maps, i.e. as “processes”, it becomes “logically clear” that propositions-as-projections is really propositions-as-processes, and these processes are just the “wavefunction collapses”.
Think of what I am after as another instance of “pure type theorists could have and would have (or did) eventually discover phenomenon X, just from within type theory, without knowing of the traditional treatment of X”. Known examples for “X”s are LCCCs, star-automonous categories, infinity-toposes, etc. I am wondering: might a pure linear type theorist not eventually have concluded (or did conclude) that reasoning in linear logic, at least when monomorphisms split, involves something that elsewhere has been called “collapse of the wave function”?
There are a number of such results on subobjects of dagger kernel categories. E.g. this paper by Heunen and Jacobs.
From propositions as projections
In intuitionistic type theory the perspective of propositions as types identifies mere propositions with (speaking in categorical semantics) monomorphisms into the given context type.
I hadn’t made the obvious connection with the claim of some philosophers that propositions are subsets of worlds. So in the context of a type $World$, (World-dependent) propositions are monomorphisms.
Re #6,
What I am really after is something with genuine internal logic perspective. It seems possible that one could do away with the confusion and debate about “wavefunction collapse” and the like by finding that this is a generic phenomenon of deduction in linear logics with split monos. Common lore says that wavefunction collapse is effected by “observers” and then there is endless debate as to what constitutes an observer, but maybe the right perspective is rather that it is more fundamentally about truth in linear type theoretic contexts with split monos, via a propositions-as-projections paradigm.
Doesn’t the clever money these days follow the decoherence (perhaps with consistent histories) approach? I thought that was how most people avoided the confusion and debate about “wavefunction collapse”. So then does linear type theory have anything to say about decoherence?
Hmm, we didn’t have consistent histories approach to quantum mechanics so I started that, which required James Hartle.
…and Robert Griffiths and einselection.
Decoherence explains why quantum probability dsitributions of measurement results turn into classical probability distributions in suitable limits, i.e. why certain correlations decohere. It does not however address the problem (if one regards it as such) as to why a quantum state would probabilistically (either way) collapse to one measurement outcome or other in the first place.
This issue has prominently been raised in the context of quantum cosmology, where, by nature of the setup, there is no ambient heat bath to appeal to.
As I said, I don’t really want to enter into this debate. I was rather wondering whether there is formal means to avoid debate and replace it by formalism.
So something like:
All of the debate can be factored through writing the formalism in a suitable linear typed language. Certain rules in the formal setting will pick out what people debate as “wave collapse”, but the debates will then just be seen to be about interpretations of the formalism, which can therefore be avoided, just as Hilbert said we don’t really need debates about what points, lines, planes really are.
Regarding this sentence at propositions as projections:
If we regard the propositions as the projection, then it is natural to think of it as being the application of the projection, in that the truth of the proposition is thought of as the image of applying this projection.
What does the ’it’ in “think of it” stand for? Measurement, perhaps.
Also we should match the grammatical number in “regard the propositions as the projection”.
The “it” is meant refer to “the proposition”. But yes, the intended suggestion is that this translates to measurement (e.g. Proposition: “The electron hits this square inch of the detector here”) and that the identification of propositions with the application of their corresponding projection corrsponds to the wave function collapse upon this measurement.
Please feel free to improve on the grammar as you see the need.
The “it” is meant refer to “the proposition”.
So we start out from proposition as a mono into the context which is split, then pass to the corresponding epi from the context, i.e., to a projection.
Now we’re passing from the proposition seen as a projection to it being seen as the application of the projection, from $p: A \to A$ to $p: A \to A , x: A \vdash p(x):A$ (or perhaps $p: A \multimap A$).
I guess the controversy comes in as to whether this corresponds to a change in your knowledge of the system (on learning the value of a measurement) or a change to the system itself. Doesn’t the use of ’wave function collapse’ usually correspond to believing in the latter?
whether this corresponds to a change in your knowledge of the system (on learning the value of a measurement) or a change to the system itself. Doesn’t the use of ’wave function collapse’ usually correspond to believing in the latter?
Yes. If $\psi$ is the wavefunction, then its collapse refers to sending it to $p(\psi)$, hence to the result of applying the projection to it, the one which corresoponds to the monomorphism that corresponds to the proposition being measured.
I’m not sure I know where your sympathies lie in terms of interpretation. I had always though the reasonable position was that recently expressed by a certain Czech physics blogger, i.e., that QM is a calculus which allows you to make judgements as to the values (or likelihood of values) of measurements, given some recent measurements. That there may be a sudden change in your knowledge after a measurement, but not a sudden collapse of an objectively meaningful wave function.
I’m not sure I know where your sympathies lie in terms of interpretation.
I have no sympathy for any interpretation of quantum mechanics. I am just looking at the maths.
The entry we were talking about simply points out what is probably evident, but seems noteworthy. Namely that the projection that gives the collapse of the wave function (irrespective of how you interpet it) is the same projection that comes with the split monomorphism which corresponds, under propositions-as-types, to the proposition whose truth was being measured.
The implication is that whenever you are reasoning in linear type theory and decide to verify the truth of any proposition corresponding to a split monomorphism by applying the corresponding projection, then your computations will show the same effect as one sees on quantum physics with the collapse rule in effect.
I suspect this way of going about linear type theory has some established name. I once tried to ask around, but to no avail.
1 to 20 of 20