4 ms·
I don't fully agree with Pfenning here. The pi-calculus is not that good a proof system for linear logic: pi-calculus imposes sequentiality constraints on proof
by mafribe 11y ago
I don't fully agree with Pfenning here. The pi-calculus is not that good a proof system for linear logic: pi-calculus imposes sequentiality constraints on proofs that impede parallelism. Take for example the term
x!<a> | y!<b> | x?(c).y?(d).P
You have to sequentialise the two possible reductions on x and y.
The culprit is the pi-calculus's input prefix, which
combines two operations: blocking input and scoping of
the bound variables (here c and d). This sequentialisation is not true to the spirit of linear logic proofs (think e.g. proof nets).
Conversely, I don't think linear logic is a good typing system for pi-calculus for a variety of reasons: among them that linear logic does not track causality well, and because it doesn't take care of affine (at most once) interactions well.
- tel 11y agoThese are good points and I'll have to consider them. I was planning on going back through Pfenning's notes again in a bit and I'll keep a more critical eye this next time. Thanks! (Also, to be clear and with reference to other threads we've conversed on here, I think of linear logic and pi calculus, even if they aren't well-corresponding, as fantastic, unavoidable examples of non-function-application style programming.)