headers
Alessio Guglielmi | 6 Jul 2004 19:06
Picon
Favicon

Re: Light logics vs. CoS

Ugo, I only found very little time to work on that: I think you're 
right, my proposal doesn't work and right now I have no constructive 
suggestion. I hope I'll find some time to work on this. For now, I go 
on holiday!   -Alessio

At 9:47 AM +0200 11.6.04, Ugo Dal_Lago wrote:
>  > At 17:32 +0200 10.6.04, Ugo Dal_Lago wrote:
>>  >  > What about
>>  >>
>>  >>       S{![R,T]}
>>  >>      ----------- ,
>>  >  >     S{![!R,?T]}
>>  >>
>>  >>  together with !1 = 1, of course?
>>  >
>>  >I am not able to understand your intuition. If you can freely use
>>  >this rule, you can build a derivation such as the following:
>>  >
>>  >     ![[a,a,a],b]
>>  >     ----------------
>>  >     ![![[a,a],a],?b]
>>  >     ------------------
>>  >     ![![![a,a],?a],?b]
>>  >     ------------------
>>  >     ![![!a,?a,?a],?b]
>>  >
>>  >If you map structures to "equivalent" sequents in the usual way, you
>>  >can prove much more than what you prove in LAL...
>>
>>  No, with my rule the bottommost inference in your example is
(Continue reading)

Permalink | Reply | 0 comments |
headers
Prakash Panangaden | 6 Jul 2004 19:39
Picon
Favicon

CBV and Quantum Entanglement

Hi, Prakash suggested me to redirect this message (for Rick Blute and 
me) to Frogs, what I do with much pleasure after deleting the 
personal parts: [...]. The paper is available at 
<http://www.ki.inf.tu-dresden.de/~guglielm/res/pap/BVQuantCausEvol.pdf>. 
I think this is very exciting!   -Alessio

Dear Rick and Alessio,
After much dithering I wrote a short note on the use of the logic CBV
for describing quantum causal propagation.  It is not very formal; at
the end I just wrote some stray thoughts rather than a conclusion.  The
note includes a long summary of the quantum situation and a recap of the
problems we had with the sequent calculus version. [Rick can glance at
this].  The last couple of pages shows how CBV deals with the
problematic graph with induced entanglement.  I still think it is great!
[Rick, I contributed more or less zero to this part; these are all
Alessio's ideas].  I think there is much to do and much to rethink.
Quantum mechanics is undergoing change and this can be - at least - a
small part of it.  I leave for [...] and then [...] this weekend.  My
[...] is returning to [...] this weekend; I will [...] at the end of
[...].  Have a nice holiday [...]!  If you think this note is suitable
for frogs please post it there.  Thanks and thanks also for numerous
[...], whisky and the [...].

Best wishes,
Prakash
Permalink | Reply | 1 comment |
headers
Alessio Guglielmi | 6 Jul 2004 19:56
Picon
Favicon

Re:CBV and Quantum Entanglement

At 7:39 PM +0200 6.7.04, Prakash Panangaden wrote:
>After much dithering I wrote a short note on the use of the logic CBV
>for describing quantum causal propagation.

The paper uses CBV, a commutative version of BV. Of course, two 
questions are in order:

1 Does cut elimination hold for CBV?

2 Is deep inference necessary for CBV?

I'll try to see whether my cut elimination proof can be adapted to 
CBV and I'll keep you posted.

I have the impression that Alwen's counterexample does not crucially 
depend on seq being non-commutative, is it right, Alwen? If this is 
the case, then deep inference is necessary.

-Alessio
Permalink | Reply | 0 comments |

Gmane