(Untitled)

[roseandsigil]

Adventures!

I forgot to mention in my last post that sometime last week, I finally saw Tank Girl. It was magnificent and wonderful and horrible, and I greatly enjoyed it

Comments

[jcreed]

In a certain sense, it's by taking a UMP away that you get linear logic

[roseandsigil]

Oh. Hrm. Is it really that easy? That feels like cheating in that...um, don't we want anything more out of tensor?

And what does & look like, then? This feels to me like the connective where the weirdness in LL really shows up, in that you "have" both sides of the connective but can only "use" one.

[jcreed]

& is actually then just the ordinary product!

The linear weirdness comes from the fact that you interpret the linear context by turning every comma into basically a ⊗, so you can't use even the additive products twice. i.e., there's no arrow from A × A to A ⊗ A (at least not for every A)

[roseandsigil]

Ahhhhhh. That makes things less murky.

[aleffert]

I think I tried to read that paper once, but didn't get very far. I'd guess that the correspondence between quantum computation and linear logic are pretty sketchy, since in quantum, 1. Everything is reversible. 2. You can actually duplicate terms, but (and I'm just guessing here) since everything is reversible, that essentially costs you a holder for a resource somewhere else.

I guess the linearity property gives you essentially every resource in the conclusion so you know what you did?

Are there any logics that deal with contexts of finite size? It seems like you could define a modality indexed by the size of the context.

Maybe you could hack it up in linear logic by having some sort of term resource that needs to be used with atoms.

[roseandsigil]

So, the paper gets around the reversibility bit in a kind of sketchy way, in that it actually keeps a history of everything it is done. Super roughly, it has an operational judgment of the form

H;e -> H';e'

where H is a history of expressions it has evaluated before, so you can always go back to the previous state with just (hd H).

The linearity is the interesting part because in quantum you can't duplicate terms. More correctly, quantum state is uncopyable without measuring, which collapses it.

In other news, firefox things "judgment" is spelled "judgement".

[wjl]

actually, my thought was about intuitionistic logic and quantum mechanics having something to do with one another. it went by considering the double slit experiment: classical reasoning (in either sense) would suggest that we know any particle that made it through the barrier had to have gone through one slit or the other. but intuitionists would argue that we can't say for sure that it went through one slit or the other unless we have evidence to that effect. and the same is true of quantum, in a way: you don't know which slit the particle went through unless you actually observe it going through one or the other, and in fact it doesn't even make sense to talk about which slit it went through, since it turns out it goes through both.

i've never been properly divested of this notion, though a couple of people have squinted their eyes funny when i explained it :P

[aleffert]

"We might mention that there have been prior attempts to relate linear logic to quantum mechanics, starting with a suggestion by Girard."