Re: Two more FAQ entries

On Tuesday 31 August 2004 21:40, Alessio Guglielmi wrote:
> At 16:20 +0200 31.8.04, Lutz Strassburger wrote:
> >On Tue, 31 Aug 2004, Alessio Guglielmi wrote:
> >  > I don't understand your remark. Take
> >>
> >>      +----+   +----+
> >>
> >>      a   -a   a   -a
> >>       \   |   |   /
> >>        \  +---+  / .
> >>         \       /
> >>          \     /
> >>           \   /
> >>           a P -a
> >>
> >>  How am I supposed to turn around this?
> >
> >like this:
> >
> >          -a P a
> >           /   \
> >          /     \
> >         /       \
> >        /  +---+  \
> >       /   |   |   \
> >     -a    a  -a    a
> >
> >      +----+   +----+
>
> OK, as I suspected, you have a personal, still not very frequent
> notion of proof net; my problem was to address the frequent notion
> known to the people who frequently ask questions.

OK, I agree with you on the that point. But I still think that you should 
reformulate your FAQ entry a little, maybe saying that as most people see 
proof nets, the symmetry is only partial, but that there is work in progress 
to carry the full symmetry of CoS to PN.

> As a side remark, I would say: with super-symmetries come
> super-responsibilities (like for Marvel super-heroes). Flipping a
> proof net and getting a refutation net is trivial; after you do this,
> you should also feel the moral obligation of talking about
> *derivation* nets, meaning top-down symmetric objects with non-unit
> premise and conclusion. They represent the natural closure of the
> symmetry you're talking about.

Of course, this it what I was talking about. The examples above are just 
special cases.

> And then: what is a correct derivation
> net? Do you have a correctness criterion,

The correctness criterion stays literally the same, because from the graph 
theoretic point of view a "derivation net" is exactly the same thing as a 
"proof net". It is just a matter of how you draw it, ie which formulas are at 
the bottom (the conclusions, in a big par relation) and wich are at the top 
(the premises, in a big tensor relation)

> sequentialisation, etc.?

this is a bit more tricky, because sequent calculus is of no use anymore. But 
in the case of (unit-free) MLL it is easy to come up with a 
"sequentialization" in the CoS, i.e., the system {ai_, s, ai^}

The idea is this: you take the "derivation net", read is as ordinary proof 
net, come up with the sequentialization in the sequent calculus, use the 
trivial translation to get a proof in CoS ant then apply splitting repeatedly 
until you have the derivation corresponding to the original net. This, of 
course, requires some additional lemmas, saying that if you apply splitting 
in the right way you do not change the net (this, in fact, more or less also 
follows from the work on the free *-autonomous category that Francois an me 
got accepted at CSL this year 
http://www.loria.fr/~strassbu/papers/multPN-CSLfinal.pdf)

> What I mean is that a `correct point of view' should be productive in
> some technical sense. I guess we agree, but I still don't see the
> practical benefits of your point of view.

I agree, that everything I said above is more or less trivial (I assumed that 
it is obvious). But I intend to do exactly the same thing to my classical 
logic proof nets, where it is not as trivial. I am still working on the right 
"sequentialization" (again, using splitting).

-Lutz